我想建模一個HTTP交互，即一系列HTTPRequest/HTTPResponse，並且我試圖將其作爲一個轉換系統進行建模。 我通過使用定義的一類狀態下的排序： open util/ordering[State]
一國就是一組消息的： sig State {
msgSet: set Message
}
每對（HTTPRequest->類HTTPResponse）和（HTTPRe
是否有直接的方式來表示Alloy中的餘數類型，而不是必須顯式減去union all的所有子類型？例如，在： sig Test {}
one sig A, B extends Test {}
我希望能夠通過速記並不需要改變每次Test獲得由新SIG延伸到指表達Test-(A+B)。雖然這隻會是語法糖，但它可以幫助我在重構模型時避免錯誤。
我已經定義了以下合金模型 使用單個狀態對象來指向兩棵樹的根State.a和State.b。 sig N {
children: set N
}
fact {
let p = ~children |
~p.p in iden
and no iden & ^p
}
one sig State {
a: one N,
b: one
當我運行我的例子，我有以下類型的錯誤： Translation capacity exceeded.
In this scope, universe contains 21 atoms
and relations of arity 8 cannot be represented.
Visit http://alloy.mit.edu/ for advice on refactoring.