我想了解如何在Alloy中訂購。我有一個我用來實例化排序模塊的時間簽名。我希望謂詞addPage在時間t'添加一個頁面到書中，其中t'= t.next。 （基本上在下一次添加頁面到圖書）然而，它不按預期工作，而是Time2的頁面數量少於Time1。有人可以向我解釋爲什麼會發生這種情況嗎？謝謝。 open util/ordering[Page] as P0
open util/ordering[T
該簽名包含兩個字段，每個保持的整數： sig Test {
a: Int,
b: Int
}
該斷言包含一系列約束： pred Show (t: Test) {
t.a = 0
t.b = 1
}
這些約束被隱式AND關係結合在一起。所以，這謂詞相當於這個謂詞： pred Show (t: Test) {
t.a = 0 and
是否約束爲了在這個pred件事： pred Example {
A
B
C
}
A，B，C表示約束。 那是pred與此相同pred： pred Example {
B
A
C
}
處於IF-THEN-ELSE下令限制？例如，是ReadMemory和WriteMemory在此IF-THEN-ELSE下令： pred Exampl
頁Software Abstractions 293說，這兩者是等價的： all x: X, y: Y | F
all x: X | all y: Y | F
但是這兩個是不相等的： one x: X, y: Y | F
one x: X | one y: Y | F
爲什麼是後兩者並不等同？ 我用最具體的例子來學習，所以我們舉一個具體的例子。 上週我乘坐郵輪去了阿拉斯加。晚餐時，
我經常聽到類似這樣的論點：傳統測試的一個缺點是它是不完整的，而Alloy分析是詳盡而完整的（在一個界限內）。但是，第一個是談論軟件，第二個是談論模型。這不是一個蘋果與橘子的比較嗎？ 更新：我錯了。比較不是這樣的：testing code versus analyzing models。這是一個蘋果與橙子的比較。相反，比較是這些： Testing models versus analysis of
簽名Test的蘊涵算有兩個字段，a和b： sig Test {
a: lone Value,
b: lone Value
}
sig Value {}
注意a和b可能會或可能不會有一個值。 一個Test是唯一有效的，如果它滿足這個相互依賴：如果a有一個值，那麼b還必須有一個值： pred valid (t: Test) {
one t.a => one t.
中一套的所有子集我正在努力如何定義一個事件可以發佈每個步驟，但多個刪除的狀態更改。我有這樣的模式： open util/ordering[State]
sig Event {}
sig State {
queue : set Event
}
pred State.post(next' : State, event : Event) {
next'.queue = th