在erlang中表达动作的时间逻辑.任何自然的方式？

Question

我想在Erlang中翻译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)行为可能会让你的生活变得更轻松.

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