1

次の合金モデルを検討してください。

open util/ordering[C]

abstract sig A {}
sig B extends A {}
sig C extends A {}

pred show {}
run show for 7

このモデルのすべてのインスタンスがシグニチャー C の 7 つのアトムを持っている理由を理解run show for 7しています (まあ、それは正確ではありません。util/ordering が伝えるため、順序付けられたシグニチャーは常にスコープが許す限り多くのアトムを持つことを理解しています)。私はそうです。しかし、それは理由とまったく同じではありません。)

しかし、このモデルのインスタンスに署名 B のアトムがないのはなぜでしょうか? これは、util/ordering で実行される特別な処理の副作用ですか? (意図的? 意図的でない?) util/ordering は、最上位の署名にのみ適用されることを意図していますか?

それとも、私が行方不明になっていることが他にあるのでしょうか?

this からのモデルでは、これは抽象化されています。B と C の和集合に A のような名前を付けたいと思っています。空でない。現時点では、これらの目標のいずれか 2 つを達成できるようです。3つすべてを同時に管理する方法はありますか？

run show for 3 but 3 B, 3 C[補遺: 指定することで、私の 3 つの目標が達成されることに気付きました。対照的に、run show for 2 but 3 Bインスタンスはまったく生成されません。おそらく、スコープ指定のセマンティクスをよりよく理解する必要があります。]

4

2 に答える 2

1

util/ordering が教えてくれるので、順序付けられた署名には常にスコープが許す限り多くのアトムがあることを理解しています。しかし、それは理由とまったく同じではありません。

その理由は、順序付けされた sig にスコープが許す限り多くのアトムを含めるように強制すると、トランスレータが効率的な対称性を破る述語を生成できるためです。これにより、順序付けされた sig を使用するほとんどの例で、解決時間が大幅に短縮されます。したがって、これは単なるトレードオフであり、設計上の決定は、パフォーマンスを向上させるためにこの追加の制約を強制することでした。

于 2013-06-26T16:51:50.507 に答える