8

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

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

这个动作意味着，只要系统的状态PredicateA对于 variable为 truex并且对于PredicateB为 truey或PredicateC对于 为 true 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。如果您知道任何已经这样做的框架，或者您可以想到一种简单的实现方式，我将很高兴听到它。

4

1 回答 1

6

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

来自有限状态机的FSM ，而不是 Flying Spaghetti Monster，尽管后者也可以提供帮助。

于 2011-02-17T01:30:56.910 回答