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

Question

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

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

此操作意味着，只要系统状态满足变量 x 的 PredicateA 为 true，并且变量 PredicateB 为 true， y 或 PredicateC 对于 z 为 true，那么系统可能会更改其状态，以便除了 x 之外一切都保持不变code> 更改为当前值加 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) 行为可能会使你的生活稍微轻松一些。

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