Erlangにおけるアクションの時間的論理を表現する。どんな自然な方法ですか？

Question

tla erlang 。これをErlangまたはそのようなフレームワークで直接行う自然な方法を考えることができますか？ Nutshell（非常に小さい1）では、TLAアクションは変数上の条件であり、その一部はプライミングされています。つまり、それらは次の状態の変数の値を表します。例えば：

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

.

この操作は、一般的なPredicateAにxがtrueであり、PredicateBまたはyがPredicateCまたはzがtrueであるようになるたびに、xにも当てはまります。一般的な値と1をプラス1に変化させること以外は

エルランでの表現を、少なくとも私が見つけた方法で多くの配管を必要としています。例えば、それらをトリガする前の条件を評価するループを有することによって、

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

I believe gen_fsm(3) behaviour could probably make your life slightly easier.

FSM from Finite State Machine, not Flying Spaghetti Monster, though the latter could help, too.