爲什麼可能合金負基數

Question

我正在用合金語言描述一些模型。 爲了描述一個有限狀態機我公司提供的代碼，這幾行：

sig FSA_state { 
    transitions: some FSA_state, 
    initial: lone InitialState 
} 

sig InitialState {} 

fact i { 
    all f: FSA_state | #(f.transitions) <= 0 
} 

pred show { 
} 

run show for 5 but 1 InitialState 

現在我試圖找出爲什麼它使得在單一狀態大於零個過渡。 使用「評估者」工具我發現某些世界在設置轉換時具有負基數，它怎麼可能（一個集合不能少於零個元素）？ 我在Evaluator中使用的指令是#(FSA_state.transitions)

Answer 1

在你的事實上，我強制要求每個FSA_state的轉換次數都是負數。 在您的簽名FSA_state中，使用關鍵字「some」會強制轉換次數至少爲1次。

在您設法生成的實例中，Alloy利用Integer簽名的有限範圍來滿足兩個矛盾的約束條件。實際上，如果整數範圍從-2到3，例如，如果每個狀態的轉換數是4，＃（f.transition）將是-2。

TL; DR： 刪除我其實

Answer 2

如果你想排除有溢出的所有車型中，可以設置（有些已經實施，有每FSA_state至少一種過渡關鍵字）的「禁止溢出「在4.2版本中可用。