[合金]没有发现没有事实的实例-Java 学习之路

我在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

1 回答

1
- 您未在 run 命令中指定范围
- 范围默认为3（意思是，宇宙包含每个信号的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
```
回复于 2024-05-02T21:37:03+08:00

[合金]没有发现没有事实的实例

1 回答

相关问题