[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 在那个范围内是不可满足的

如果您运行您的原始模型，其详细程度至少设置为 "medium"，您应该会在控制台 window 的 right-hand 端看到类似这样的内容

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

[Alloy]没有找到没有事实的实例

[Alloy]No instance found with no fact

instance

alloy