1

私はAlloyで少し作業をしたので、それについてかなり理解しています. ただし、省略形の多くは実際にはどこにも記載されていません。私が疑問に思っていたのは、以下の例です。

open util/relation

abstract sig Proc { prv : lone (Proc - Remove) 
}{
}

fact {acyclic[prv,Proc] // no cycles 
}
sig Remove extends Proc{}
sig Begin extends Proc{}{no prv}
sig Action extends Proc{}

pred show() {} 
run show for 3

最終的な Proc が常に Begin になるようにしたいと思います (現時点では、Action にもなる可能性があります)。

手書きで書く方法はたくさんあります。以下に 1 つ含めました。これを含めると、最終的な Proc (つまり、ドメインにないもの) が常に Begin になります。

fact {
all p : Proc  |   p not in dom[prv] implies p in Begin
}

ただし、(Proc - Remove) の行に沿って省略形を使用するのが好きです。たとえば、読みやすくするためです。つまり、Remove を別の Proc からリンクすることはできません。うまく説明できたと思います。本当に明白な答えがあると思いますが、それが何であるかはわかりません。アイデアはありますか？

4

2 に答える 2

0

これはどう

fact { ^prv.Begin = Proc - Begin }

極端に短いわけではありませんが、少なくとも数量詞は使用していません。あなたがそれ以上のことをできるかどうかはわかりません。

prvグラフの用語では、基本的に次のように言います。グラフ内のすべてのエッジをできるだけ多くたどってグラフを完全に展開する場合(つまり、 prv, の推移閉包を取る^prv)、Begin を指すエッジのソース ノードを選択します。ノード ( ^prv.Begin)、そのセットには、Begin ノードを除くすべてのノードが含まれている必要があります。開始ノードには prv がないという事実がすでにあるということは、非開始ノードから開始してprvリンクのみをたどると、開始ノードに到達し、チェーンがそこで終了することを意味します。この事実により、Action ノードとそのようなチェーンは許可されません。

アサートすることで、Alloy でこのクレームを確認できます。

check {
  // there is no non-Begin node that does not lead to a Begin node
  no p: Proc-Begin | no (Begin & p.^prv)
} for 6

反例が見つからないことを確認します。

于 2013-09-14T18:15:05.947 に答える