1つのイベントをステップごとに転記できますが、複数削除された状態変更の定義方法は苦労しています。私は、このモデルを持っている： open util/ordering[State]
sig Event {}
sig State {
queue : set Event
}
pred State.post(next' : State, event : Event) {
ne
私は、次のモデルがあります： sig A1 {
// ...
}
sig A2 {
// ...
}
sig S {
s_a1: one A1,
s_a2: one A2
}
私はサブセットS1を「作る」したいと思い ：S0の要素に基づいてS：次へS対象制約： S1は、これらの原子は、条件C1 [s_valid.s_a1]を満たすS0にs_valid S0と
付録E ソフトウェアアブストラクションには、Hotel Operationsのモデルがあります。モデルはアサートNoIntruderと命名されています。 check NoIntruder for 6 but 12 Time, 3 Room, 3 Guest
は合金アナライザはチェックコマンドのその評価に考えていることを例数を確認する方法はあります：アサートが、このコマンドを使用して評価されます
以下合金述語pは、パラメータtはタイプS.起動run pのシングルトンとして宣言し、正しい結果が得られるので、Tは、2つの異なる要素sとs'を含んでいてもよい述語体状態。しかし、第2のrunコマンドでは、タイプSの2つの分離した要素のセットが述語pに渡され、このコマンドはインスタンスを与えます。それはなぜですか？ sig S {}
pred p(t: one S) {
some s,