2

背景: CPN-Toolsは、色付きのペトリネットを使用するモデル チェッカーであり、クエリ言語として CPN ML を使用します。CPN MLは、型推論関数型言語である Standard ML の拡張です。

問題: CPN ツールは、状態空間分析を必要とするドメインをモデル化するために広く使用されています。これを使用して、ある場所から出入りするアークの数を知る必要があるドメインをモデル化しています。違いは、状態空間ではなく、ペトリ ネット モデル表現を見ていることです。したがって、ある場所から弧を数えるというときは、状態空間ノードではなく、場所を意味します。これまでの私の研究では、場所と遷移のプロパティを含むCPN'PlaceTableと構造に出くわし、私の探求に有望に見えます。CPN'TransitionTableただし、これらの構造を使用して着信/発信アークをカウントする方法を理解するのに役立つ CPN ML の例は見つかりませんでした。

質問:私の質問、または実際の質問は次のとおりです。

  1. 特定の場所への着信アークをカウントするには、どのように使用するCPN'PlaceTableか、または他の方法を使用しますか?
  2. 特定のトランジションからの出力アークをカウントするには、どのように使用するCPN'TransitionTableか、または適切な方法を使用しますか?

ケース例: この単純なペトリネットを使用して、私が期待していることについてのアイデアを提供しています。イラストはこちらのリンクをご覧ください。

画像では、3 つの場所と 2 つのトランジションが見られます。私が理想的に望んでいるのは、CPN ML関数を持つことができることでincoming(place_name)あり、outgoing(transition_name)それはこのように機能します

incoming(Place1) = 0
incoming(Place2) = 2
incoming(Place3) = 1
outgoing(Transition1) = 2
outgoing(Transition2) = 1

その他の情報: 状態空間ノードについて言及していないことを再度強調したいと思います。CPN-Tools には、状態空間のアーク プロパティに関するドキュメントが多数ありますが、CPN-Tools サポート フォーラムでの質問に関する情報はあまり見つかりませんでした。さらに悪いことにCPN'、一般的な構造は CPN ツールではほとんど文書化されていません。

4

0 に答える 0