erlang - アクションの時相論理をアーランで表現。自然な方法は？

Question

TLAで指定されたいくつかのアクションをErlangに翻訳したいと考えています。これを Erlang で直接行う自然な方法や、そのようなことができるフレームワークを思いつきますか? 一言で言えば (非常に小さなものです)、TLA アクションは変数の条件であり、その一部はプライミングされています。つまり、次の状態の変数の値を表します。例えば：

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

このアクションは、システムの状態がPredicateAvariable に対してtrue であり、に対して trueまたはtrue のxいずれかである場合は常に、システムはその状態を変更して、現在の値に 1 を加えた値に変更されることを除いてすべてが同じままになることを意味します。 .PredicateByPredicateCzx

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 準拠にすることを考えています。すでにそれを行っているフレームワークを知っている場合、またはこれを実装する簡単な方法を考えられる場合は、それについて聞いていただければ幸いです。