PetriNetReachability.cs

using System;
using System.Collections.Generic;
using System.Collections.Immutable;
using System.Linq;
using System.Text;

class Program
{
    static void Main(string[] args)
    {
        var net1 = new PetriNet(6, 4);
        net1.AddPlaceToTransitionArc(1, 2);
        net1.AddPlaceToTransitionArc(2, 1);
        net1.AddPlaceToTransitionArc(3, 4);
        net1.AddPlaceToTransitionArc(4, 3);
        net1.AddPlaceToTransitionArc(5, 4);
        net1.AddPlaceToTransitionArc(6, 3);
        net1.AddTransitionToPlaceArc(1, 1);
        net1.AddTransitionToPlaceArc(1, 5);
        net1.AddTransitionToPlaceArc(2, 2);
        net1.AddTransitionToPlaceArc(2, 6);
        net1.AddTransitionToPlaceArc(3, 3);
        net1.AddTransitionToPlaceArc(4, 4);
        var net1InitialMarking = ImmutableArray.Create(1, 0, 0, 1, 0, 0);
        var net1TreeRoot = net1.CreateReachabilityTree(net1InitialMarking);
        Console.WriteLine("Net 1");
        Console.WriteLine(net1TreeRoot.ToDot());

        var net2 = new PetriNet(4, 4);
        net2.AddPlaceToTransitionArc(1, 2);
        net2.AddPlaceToTransitionArc(1, 4);
        net2.AddPlaceToTransitionArc(2, 1);
        net2.AddPlaceToTransitionArc(2, 3);
        net2.AddPlaceToTransitionArc(3, 4);
        net2.AddPlaceToTransitionArc(4, 3);
        net2.AddTransitionToPlaceArc(1, 1);
        net2.AddTransitionToPlaceArc(2, 2);
        net2.AddTransitionToPlaceArc(3, 2);
        net2.AddTransitionToPlaceArc(3, 3);
        net2.AddTransitionToPlaceArc(4, 1);
        net2.AddTransitionToPlaceArc(4, 4);
        var net2InitialMarking = ImmutableArray.Create(1, 0, 0, 1);
        var net2TreeRoot = net2.CreateReachabilityTree(net2InitialMarking);
        Console.WriteLine("Net 2");
        Console.WriteLine(net2TreeRoot.ToDot());
    }
}

class PetriNet
{
    public const int Omega = -1;
    public int NumPlace { get; }
    public int NumTransition { get; }
    private readonly bool[,] _arcs;

    public PetriNet(int numPlace, int numTransition)
    {
        this.NumPlace = numPlace;
        this.NumTransition = numTransition;
        this._arcs = new bool[numPlace + numTransition, numPlace + numTransition];
    }

    public void AddPlaceToTransitionArc(int sourcePlace, int destinationTransition)
    {
        if (sourcePlace < 1 || sourcePlace > this.NumPlace)
            throw new ArgumentOutOfRangeException(nameof(sourcePlace));
        if (destinationTransition < 1 || destinationTransition > this.NumTransition)
            throw new ArgumentOutOfRangeException(nameof(destinationTransition));

        this._arcs[sourcePlace - 1, this.NumPlace + destinationTransition - 1] = true;
    }

    public void AddTransitionToPlaceArc(int sourceTransition, int destinationPlace)
    {
        if (sourceTransition < 1 || sourceTransition > this.NumTransition)
            throw new ArgumentOutOfRangeException(nameof(sourceTransition));
        if (destinationPlace < 1 || destinationPlace > this.NumPlace)
            throw new ArgumentOutOfRangeException(nameof(destinationPlace));

        this._arcs[this.NumPlace + sourceTransition - 1, destinationPlace - 1] = true;
    }

    public bool IsEnabled(int transition, IReadOnlyList<int> marking)
    {
        if (transition < 1 || transition > this.NumTransition)
            throw new ArgumentOutOfRangeException(nameof(transition));
        if (marking.Count != this.NumPlace) throw new ArgumentException();

        var transitionIndex = this.NumPlace + transition - 1; // _arcs におけるこのトランジションのインデックス

        for (var i = 0; i < this.NumPlace; i++)
        {
            if (this._arcs[i, transitionIndex])
            {
                if (marking[i] <= 0 && marking[i] != Omega)
                    return false;
            }
        }

        return true;
    }

    public int[] Fire(int transition, IReadOnlyList<int> marking)
    {
        if (transition < 1 || transition > this.NumTransition)
            throw new ArgumentOutOfRangeException(nameof(transition));
        if (marking.Count != this.NumPlace) throw new ArgumentException();

        var transitionIndex = this.NumPlace + transition - 1; // _arcs におけるこのトランジションのインデックス
        var newMarking = marking.ToArray();

        // トークンを減らす
        for (var i = 0; i < this.NumPlace; i++)
        {
            if (this._arcs[i, transitionIndex])
            {
                if (newMarking[i] <= 0)
                {
                    if (newMarking[i] != Omega)
                        throw new ArgumentException("発火可能ではありません。");
                    // ωのとき、変化なし
                }
                else
                {
                    newMarking[i]--;
                }
            }
        }

        // トークンを増やす
        for (var i = 0; i < this.NumPlace; i++)
        {
            if (this._arcs[transitionIndex, i] && newMarking[i] != Omega)
                newMarking[i]++;
        }

        return newMarking;
    }

    public ReachabilityTreeNode CreateReachabilityTree(ImmutableArray<int> initialMarking)
    {
        if (initialMarking.Length != this.NumPlace) throw new ArgumentException();

        var id = 0;
        var root = new ReachabilityTreeNode(CreateId(), initialMarking, null);
        AddBranches(root);
        return root;

        string CreateId() => $"Node{++id}";

        void AddBranches(ReachabilityTreeNode sourceNode)
        {
            // 親に同じマーキングがあれば、何もしない
            if (SameMarkingInAncestors(sourceNode)) return;

            for (var transition = 1; transition <= this.NumTransition; transition++)
            {
                if (!this.IsEnabled(transition, sourceNode.Marking)) continue;

                var newMarking = this.Fire(transition, sourceNode.Marking);

                // ωにできるかチェック
                for (var parent = sourceNode.Parent; parent != null; parent = parent.Parent)
                {
                    if (IsMarkingLessOrEqual(parent.Marking, newMarking))
                    {
                        for (var i = 0; i < this.NumPlace; i++)
                        {
                            if (parent.Marking[i] < newMarking[i])
                                newMarking[i] = Omega;
                        }
                        break;
                    }
                }

                var newNode = new ReachabilityTreeNode(CreateId(), ImmutableArray.CreateRange(newMarking), sourceNode);
                sourceNode.Edges.Add(new ReachabilityTreeEdge(transition, newNode));
                AddBranches(newNode); // 深さ優先探索
            }
        }

        bool SameMarkingInAncestors(ReachabilityTreeNode node)
        {
            for (var parent = node.Parent; parent != null; parent = parent.Parent)
            {
                if (node.Marking.SequenceEqual(parent.Marking))
                    return true;
            }
            return false;
        }

        //lhs <= rhs
        bool IsMarkingLessOrEqual(IReadOnlyList<int> lhs, IReadOnlyList<int> rhs)
        {
            if (lhs.Count != rhs.Count) throw new ArgumentException();

            var count = lhs.Count;
            for (var i = 0; i < count; i++)
            {
                if (rhs[i] == Omega) continue; // 右辺がωなら必ず lhs[i] <= rhs[i] になる
                if (lhs[i] == Omega || lhs[i] > rhs[i]) return false;
            }

            return true;
        }
    }
}

class ReachabilityTreeNode
{
    public string Id { get; }
    public ImmutableArray<int> Marking { get; }
    public ReachabilityTreeNode? Parent { get; }
    public IList<ReachabilityTreeEdge> Edges { get; } = new List<ReachabilityTreeEdge>();

    public ReachabilityTreeNode(string id, ImmutableArray<int> marking, ReachabilityTreeNode? parent)
    {
        this.Id = id;
        this.Marking = marking;
        this.Parent = parent;
    }

    public string ToDot()
    {
        var sb = new StringBuilder().AppendLine("digraph {");
        WriteNode(this);
        WriteEdges(this);
        return sb.AppendLine("}").ToString();

        void WriteNode(ReachabilityTreeNode node)
        {
            sb.Append("  ").Append(node.Id)
                .Append(" [label=\"(")
                .AppendJoin(',', node.Marking.Select(x => x == PetriNet.Omega ? "ω" : x.ToString()))
                .AppendLine(")\"];");

            foreach (var edge in node.Edges)
                WriteNode(edge.Destination);
        }

        void WriteEdges(ReachabilityTreeNode node)
        {
            foreach (var edge in node.Edges)
            {
                sb.AppendFormat("  {0} -> {1} [label=\"t{2}\"];\n",
                    node.Id, edge.Destination.Id, edge.Transition);
            }

            foreach (var edge in node.Edges)
                WriteEdges(edge.Destination);
        }
    }
}

readonly struct ReachabilityTreeEdge
{
    public int Transition { get; }
    public ReachabilityTreeNode Destination { get; }

    public ReachabilityTreeEdge(int transition, ReachabilityTreeNode destination)
    {
        this.Transition = transition;
        this.Destination = destination;
    }
}