目录
2. 有限状态机（Finite State Machines）
3. 在Alloy中建模有限状态机（Modelling FSMs in Alloy）
4. 在Alloy中检查规格（CHECKING SPECIFICATIONS IN ALLOY）
1. Alloy Modelling Overview
- 签名（Signatures）：在Alloy中声明集合和关系。
- 事实（Facts）：作用在签名上的全局约束，排除模型中的无意义部分。
- 谓词（Predicates）：在模型中定义变量之间的关系，用于指定操作、状态转换。
- 函数（Functions）：表达式的简写。
2. 有限状态机（Finite State Machines）
- 从初始状态s0开始
- 状态是不同类型变量的集合。有一系列操作，每个操作都改变状态。每个操作实现不同的状态转换。
3. 在Alloy中建模有限状态机（Modelling FSMs in Alloy）
- 状态是（类型化的）变量的集合：
sig State {…} - 可能使用约束：
fact blah { always all s : State | … } - 初始状态：
pred Init[s : State] { … } - 操作：
pred Op1[s : State] { … } pred Opn[s : State] { … } - 谓词可能使用函数作为简写
- 示例：
4. 在Alloy中检查规格（CHECKING SPECIFICATIONS IN ALLOY）
-
校验一个规格
- 我们如何知道我们的规格正确地捕获了我们的意图？
- Animation 动画（运行规格以查看它捕获的行为）
- Check Assertions 检查断言（看看哪些属性可能从规格中推导出来）
4.1 Alloy的run命令
- 查找满足在指定边界内的谓词的实例
- 从最小的合理边界开始，如果无法满足，则增加它
4.2 Alloy的assert语句
- 声明应从规格中推导出的属性。
4.3 Alloy的check命令
- 在固定的边界内搜索违反属性的反例。
- 使用“expect”来注解哪些检查应通过，哪些应失败
- 从最小的合理边界开始，如果找不到反例，则增加它
5. deletelsUndo示例
无效的反例（Invalid Counterexamples）
断言作为测试
- Alloy进行有界的断言检查 Alloy does bounded assertion checking
- 像在边界内测试一个断言 Like testing an assertion for all systems up to the bound
- 不能证明断言在任意大小的系统中总是成立 Doesn’t prove the assertion will hold for systems of arbitrary size in general
- 尽管在特定的系统和断言中可能是这样。Although it might for specific systems and assertions.
- 总的来说，如果不是证据，它给出了非常高的信心。In general, it gives very high confidence if not a proof.
断言的信心（Assertion Confidence）
- 如果Alloy说所有的断言都成立，我的规格是对的吗？
- 否
- 只在有限的边界内检查。Checks only within finite bounds.
- 规格可能不完整。Spec could be incomplete.
- 规格可能说了错误的事。Spec could say the wrong thing.