如何设置事件式模型的可视化

Question

我正在阅读这本书并尝试合金 6 中的示例。对于第 6.2.4 节“基于事件的变化”，我无法真正理解结果。特别删除NoIntervening事实会产生反例，但即使缩小范围也很难遵循。虽然跟踪样式通过简单的时间投影可视化非常容易理解。以下是我移植到 Alloy 6 的示例版本：https://gist.github.com/CheatEx/dc7ee7e8bd0750f350c5a270095c792e

可视化看起来与书本完全不同。时间和事件预测都没有意义，因为图表中充斥着不相关时间的不相关事件。

有没有好的方法来调整可视化工具以显示事件式模型？专门为了仅显示时间投影中的相关事件？

Answer 1

首先，您需要投影时间，以获得瞬间的表示。那么，问题是您仍然可以看到所有事件。要仅保留给定时刻发生的事件，您可以更改主题以表示事件不应该可见，但集合

pre

应该可见（意味着触发时刻是当前时刻的事件）。

我应该补充一点，使用合金 6 的新功能可以使这一点变得更加清晰（目前还没有完成的印刷书籍描述它，但有讲义这里）。