在 erlang 中表达动作的时间逻辑。有什么自然的方法吗？

Question

我想翻译一些指定的动作 TLA 在 埃尔兰. 。你能想到在 Erlang 中直接执行此操作的任何自然方法或任何可用的框架吗？简而言之（非常小的一个），TLA 动作是变量的条件，其中一些是预先准备的，这意味着它们代表下一个状态中变量的值。例如：

Action(x,y,z) ->
    and PredicateA(x),
    and or PredicateB(y)
        or PredicateC(z)
    and x' = x+1

此操作意味着，每当系统状态满足以下条件时 PredicateA 对于变量来说是正确的 x 以及 PredicateB 是真的 y 或者 PredicateC 是真的 z, ，那么系统可能会改变它的状态，以便一切都保持不变，除了 x 更改为当前值加 1。

在 Erlang 中表达这一点需要大量的管道，至少以我发现的方式。例如，通过一个在触发条件之前评估条件的循环，例如：

what_to_do(State,NewInfo) ->
    PA = IsPredicateA(State,NewInfo),
    PB = IsPredicateB(State,NewInfo),
    PC = IsPredicateC(State,NewInfo),
    [{can_do_Action1, PA and (PB or PC}, %this is the action specified above.
     {can_do_Action2, PA and PC},        %this is some other action
     {can_do_Action3, true}]             %this is some action that may be executed at any time.

 loop(State) ->
     NewInfo = get_new_info(),
     CanDo = what_to_do(State,NewInfo),
     RandomAction = rand_action(CanDo),

     case RandDomAction of
          can_do_Action1 -> NewState = Action(x,y,z);
          can_do_Action2 -> NewState = Action2(State);
          can_do_Action3 -> NewState = Action3(State)
     end,
     NewestState = clean_up_old_info(NewState,NewInfo),
     loop(NewestState).

我正在考虑编写一个框架来隐藏这个管道，将消息传递合并到 get_new_info() 功能，并希望仍然使其符合 OTP 标准。如果您知道任何已经做到这一点的框架，或者您能想到一种简单的方法来实现这一点，我将很高兴听到它。

Answer 1

我相信 gen_fsm(3) 行为可能会让你的生活稍微轻松一些。

有限状态机来自 有限状态机, ，而不是飞行面条怪物，尽管后者也可以提供帮助。