合金 - 無制限の普遍的な数量で

Question

こんにちは、無限の普遍的な数量を扱うとき、私は合金で問題が発生してきた

ディーリング。ダニエル・ジャクソンの本「ソフトウェア抽象化」（第5.3節「無限大の量的限定子」）で説明されているように、Alloyは普遍的な量限定子とアサーションの検査に関して微妙な制限があります。合金は、セットが（前述の本の中で示されている）組合下で閉じていることを確認するためにそのような次のようないくつかの場合には偽反例を生成する：

ような反例製造

sig Set { 
    elements: set Element 
} 
sig Element {} 

assert Closed { 
    all s0, s1: Set | some s2: Set | 
    s2.elements = s0.elements + s1.elements 
} 
check Closed for 3 

：

Set = {(S0),(S1)} 
Element = {(E0),(E1)} 
s0 = {(S0)} 
s1 = {(S1)} 
elements = {(S0,E0), (S1,E1)} 

アナライザは十分な値（S0とS1の和集合を含むSet atom S2がない）をSetに設定しませんでした。この一般的な問題へ

2つの溶液を本の中で、次に提案されています

1）すべての可能なインスタンスを生成する合金を強制的に発電機の公理を宣言します。例えば ：

fact SetGenerator{ 
    some s: Set | no s.elements 
    all s: Set, e: Element | 
    some s': Set | s'.elements = s.elements + e 
} 

この解決策は、しかし、スコープ爆発を生成し、また不整合をもたらし得ます。

2）ジェネレータの公理を省略し、束縛されたユニバーサル形式を制約のために使用する。つまり、定量化された変数の境界式には生成されたシグネチャの名前は含まれていません。しかし、すべてのアサーションがこのような形式で表現されるわけではありません。

私の質問です：これらのソリューションを選択する際の具体的なルールはありますか？この本から私には分かりません。

ありがとうございました。

Answer 1

いいえ、具体的なルールはありません（少なくとも、私が思い付いたものはありません）。実際には、これは非常に頻繁に起こるわけではないので、私はそれぞれのケースが現れたときにそれを扱います。特定の例がありますか？

また、より高次の量量子（つまり、集合または関係の量子）で問題を定式化することができます。その場合、高次解析をサポートする合金の拡張である合金*を使用できます。