擴展簽名和原子實例化

我正在使用Alloy 4.2，並且我有使用繼承的複雜性問題。很明顯，簽名之間的繼承不像我以前在面向對象編程中面對的那樣（或者至少如我所期待的那樣）。擴展簽名和原子實例化

顯然，當運行命令中沒有設置完全關鍵字時，即使根抽象類是抽象的，原子也會實例化爲根抽象簽名的原子。當精確關鍵字用於指定一個命令時，原子被指定爲實例化：葉具體類。

我希望能夠搜索具有從另一個抽象繼承的可變性的解決方案。它允許我指定葉簽名中存在的抽象簽名中的關係。

例如（冗長需要設置到高）：

abstract sig A {} 

sig B extends A {} 

sig C extends A {} 

pred show {} 

run show for 6 B, 6 C 
run show for exactly 6 B, exactly 6 C

當我運行2謂詞這裏有以下追蹤：

Executing "Run show1 for 6 B, 6 C" 
    Sig this/B scope <= 6 
    Sig this/C scope <= 6 
    Sig this/A scope <= 12 
    Sig this/A in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] 
    Sig this/B in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] with size<=6 
    Sig this/C in [[A$0], [A$1], [A$2], [A$3], [A$4], [A$5], [A$6], [A$7], [A$8], [A$9], [A$10], [A$11]] with size<=6 
    Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=4 Symmetry=20 
    15152 vars. 24 primary vars. 55808 clauses. 55164ms. 
    Instance found. Predicate is consistent. 225ms.

在此執行跟蹤，我們可以看到，所有儘管A是抽象的，但B和C被實例化爲A原子。我們可以看到B和C在A元素集中選擇了6個不相交的元素。

Executing "Run show2 for exactly 6 B, exactly 6 C" 
    Sig this/B scope <= 6 
    Sig this/C scope <= 6 
    Sig this/A scope <= 12 
    Sig this/A in [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5], [C$0], [C$1], [C$2], [C$3], [C$4], [C$5]] 
    Sig this/B == [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5]] 
    Sig this/C == [[C$0], [C$1], [C$2], [C$3], [C$4], [C$5]] 
    Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=4 Symmetry=20 
    0 vars. 0 primary vars. 0 clauses. 2ms. 
    Instance found. Predicate is consistent. 14ms.

在這種跟蹤中，我們可以看出，一組僅由B和C的元素，而不是A的元素組成。即使第二個命令解決的問題比第一個命令更簡單，我們也可以看到由於組合爆炸，解決時間非常不同。

爲了儘量減少解決時間，是否有可能通過使用簽名上的事實或設置約束來使蹤跡看起來像這樣？

Executing "Run show2 for 6 B, 6 C" 
    Sig this/B scope <= 6 
    Sig this/C scope <= 6 
    Sig this/A scope <= 12 
    Sig this/A in [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5], [C$0], [C$1], [C$2], [C$3], [C$4], [C$5]] 
    Sig this/B == [[B$0], [B$1], [B$2], [B$3], [B$4], [B$5]] 
    Sig this/C == [[C$0], [C$1], [C$2], [C$3], [C$4], [C$5]]

來源

2014-03-19 user2858691

當我執行'run'指令時，分析儀顯示出我的B和C原子。我認爲這也是它向你展示的原子。爲什麼對你而言，如果在處理原子的某個階段給出的標識符反映了它們是簽名A的實例以及B或C的實例的事實？換句話說：究竟是什麼問題？ –

問題是，如果我在B-> C之間有一個關係，例如在所有B和C都被實例化爲A元素的情況下，Alloy會嘗試A-> A的所有不同組合，其中第一個A屬於B，第二個C的複雜性是關於A * A的。在B和C被實例化爲B和C元素的情況下，合金操縱B和C元素不是A元素，所以複雜度大約是B * C，其中B + C = A（因爲A是抽象的）。 – user2858691

事實是，A應該是抽象的，這意味着沒有具體的A實例存在，並且Alloy在第一種情況下實例化B和C作爲A元素。在第二種情況下，如果我們指定B和C使得B + C = A且B＆C = none，那麼我們就不能在繼承指定它時在B和C中自動存在A中指定關係。 – user2858691

當不使用的「精確」關鍵字，那麼就不可能解決模型之前知道實際類型的每個原子的。換句話說，範圍

run show for 6 B, 6 C

僅指定上限，這意味着一個有效的實例允許包含，例如，B 2個原子和C 1個原子（取決於該模型中的實際約束）。這就是爲什麼Alloy只能分配足夠的原子開始（給它們一些通用的名稱，在這種情況下是從基本類型名稱派生的名稱），並且在找到實例後，每個原子將被重命名爲（在可視化器中）爲反映其實際類型。

只有當您指定確切的範圍合金可以最小化邊界（如您注意到的），以便可能減少解決時間。

來源

2014-03-29 15:21:21

好吧，我明白了，但是在搜索解決方案的範圍中指定超級簽名並讓解算器與邊界一起玩時，此策略是有意義的。但是，如果在範圍中指定了子簽名，則應將它們實例化爲類似於沒有擴展名的簽名。 – user2858691

擴展簽名和原子實例化

回答

相關問題