合金中的简单状态机答案

【问题标题】：Simple State Machine in Alloy合金中的简单状态机
【发布时间】：2014-10-25 16:45:51
【问题描述】：

我对合金及其功能也很陌生。最近，我有一个关于简单状态机的任务：begin_state->normal_state->end_state。只有一个 begin_state，但有一些 normal_state 和一些 end_state。然后我不能用下面的合金代码使实例视图正确：

abstract sig state
{
    prev : some state,
    next : some state
}

one sig begin extends state{}
some sig end extends state{}
sig mid extends state{}

//There is no state after end state, and there is no state before begin state

pred dosomething
{
    no s : state | s in begin.prev and s in end.next
}

run{dosomething}

所以基本上我只想要在开始状态之前没有状态，在结束状态之后没有状态，实例示例可以是这样的：

开始->正常->结束

或

开始->正常->结束
|
正常->正常->结束
|
正常---正常
| |
结束

...类似的东西。谢谢

【问题讨论】：

标签： state alloy

【解决方案1】：

考虑以下命题：

每个状态都指向前一个状态。
开始状态是一种状态。
开始状态不指向前一个状态。

如果（如我所愿）您认为这三个命题相互矛盾，那么问问自己 (a) 这些命题是否与您的合金模型中给出的规则相似？ (b) 你如何将它们改写为有意义且不相互矛盾？ (c) 你对它们的改写如何翻译成合金？

我希望这会有所帮助。

【讨论】：

【解决方案2】：

注意你的量词！公式

no s : state | s in begin.prev and s in end.next

说没有状态 s 既是 begin 的前身又是 end 的后继。

【讨论】：