[Alloy]沒有發現實例

Question

我在Alloy中編寫了下面的代碼。我想知道爲什麼它沒有找到一個實例，因爲在代碼中根本沒有任何事實。

abstract sig TaskStatus {} 
one sig Completed extends TaskStatus {} 
one sig Waiting extends TaskStatus {} 
one sig OnGoing extends TaskStatus {} 

sig Capability {} 

sig Task { 
    status: one TaskStatus, 
    precondition: set Task, 
    capability: one Capability 
} 

sig Agent { 
    tasks: set Task, 
    capabilities: set Capability 
} 

sig ToDoList { 
    tasks: set Task 
} 


pred show { 
    some Capability 
    some Agent 
    some ToDoList 
    #Task > 3 
} 
run show 

Answer 1

• 你沒有在你的run命令
• 範圍默認爲3指定範圍（意思是，宇宙包含每SIG公司3個原子）
• #Task > 3在範圍無法滿足

如果您運行原始模型，並將詳細度至少設置爲「中等」，則應在右側的控制檯窗口中看到類似這樣的內容

Executing "Run show" 
Sig this/Completed scope <= 1 
Sig this/Waiting scope <= 1 
Sig this/OnGoing scope <= 1 
Sig this/TaskStatus scope <= 3 
Sig this/Capability scope <= 3 
Sig this/Task scope <= 3 
Sig this/Agent scope <= 3 
Sig this/ToDoList scope <= 3 

確認爲Task範圍確實是默認被設置爲3。

要解決該問題，指定一個更大的範圍，例如，

run show for 5