[Alloy]没有发现实例

我在Alloy中编写了下面的代码。我想知道为什么它没有找到一个实例，因为在代码中根本没有任何事实。[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

来源

2017-02-10 user1315621

你没有在你的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

来源

2017-02-10 16:45:57

[Alloy]没有发现实例

回答

相关问题