anchor.diff:  -export([all_tps_informed/1]).
   -export([all_pax_decided/1]).
   -export([all_tps_registered/1]).
  -%% tx_state: {TId,
  -%%            tx_state,
  -%%            Client,
  -%%            ClientsId,
  -%%            RTMs,
  -%%            _tlogtxitemids = [{TLogEntry, TxItemId}],
  -%%            Learner,
  -%%            NumIds,
  -%%            NumPrepared,
  -%%            NumAbort,
  -%%            NumTPsInformed
   
  +-type tx_id() :: {tx_id, util:global_uid()}.
  +-type tx_state() ::
  +        {tx_id(),                  %% Tid
  +         tx_state,                 %% type-marker (unnecessary in principle)
  +         comm:mypid() | unknown,   %% Client
  +         any(),                    %% ClientsId,
  +         [{?RT:key(), comm:mypid(), non_neg_integer()}], %% [{Key, RTM, Nth}]
  +         any(),                    %% _tlogtxitemids = [{TLogEntry, TxItemId}],
  +         [comm:mypid()],           %% Learners,
  +         undecided | false | abort | commit, %% Status decided?
  +         non_neg_integer(),        %% NumIds,
  +         non_neg_integer(),        %% NumPrepared,
  +         non_neg_integer(),        %% NumAbort,
  +         non_neg_integer(),        %% NumTPsInformed
  +         non_neg_integer(),        %% NumPaxDecided
  +         non_neg_integer(),        %% NumTpsRegistered
  +         new | uninitialized | ok, %% status: new / uninitialized / ok
  +         [any()]                   %% HoldBack
  +         }.
   %% @TODO also necessary?
   %%               Majority of RTMs,
   %%               timeout before RTM takes over
   %%               }
   
  +-spec new(tx_id(), _, _, _, _, _) -> tx_state().
   new(Tid, Client, ClientsID, RTMs, TLogTxItemIds, Learners) ->
       {Tid, tx_state, Client, ClientsID, RTMs, TLogTxItemIds, Learners,
        undecided, length(TLogTxItemIds),
  -     _Prepared = 0, _Aborts = 0, _Informed =0, _PaxDecided = 0,
  +     _Prepared = 0, _Aborts = 0, _Informed = 0, _PaxDecided = 0,
        _TpsRegistered = 0, _Status = uninitialized, _HoldBackQueue = []}.
  +-spec new(tx_id()) -> tx_state().
   new(Tid) ->
       new(Tid, unknown, unknown, _RTMs = [], _TLogTxItemIds = [], []).
   
  +-spec get_tid(tx_state()) -> tx_id().
   get_tid(State) ->                 element(1, State).
  +-spec set_tid(tx_state(), tx_id()) -> tx_state().
   set_tid(State, Val) ->            setelement(1, State, Val).
  +-spec get_client(tx_state()) -> comm:mypid() | unknown.
   get_client(State) ->              element(3, State).
  +-spec set_client(tx_state(), comm:mypid() | unknown) -> tx_state().
   set_client(State, Val) ->         setelement(3, State, Val).
  +-spec get_clientsid(tx_state()) -> any().
   get_clientsid(State) ->           element(4, State).
  +-spec set_clientsid(tx_state(), any()) -> tx_state().
   set_clientsid(State, Val) ->      setelement(4, State, Val).
  +-spec get_rtms(tx_state()) -> [{?RT:key(), comm:mypid(), non_neg_integer()}].
   get_rtms(State) ->                element(5, State).
  +-spec set_rtms(tx_state(), [{?RT:key(), comm:mypid(), non_neg_integer()}])
  +              -> tx_state().
   set_rtms(State, Val) ->           setelement(5, State, Val).
   get_tlog_txitemids(State) ->      element(6, State).
   set_tlog_txitemids(State, Val) -> setelement(6, State, Val).
  +-spec get_learners(tx_state()) -> [comm:mypid()].
   get_learners(State) ->            element(7, State).
  +-spec is_decided(tx_state()) -> undecided | false | abort | commit.
   is_decided(State) ->              element(8, State).
  +-spec set_decided(tx_state(), undecided | false | abort | commit) -> tx_state().
   set_decided(State, Val) ->        setelement(8, State, Val).
  +-spec get_numids(tx_state()) -> non_neg_integer().
   get_numids(State) ->              element(9, State).
  +-spec get_numprepared(tx_state()) -> non_neg_integer().
   get_numprepared(State) ->         element(10, State).
  +-spec inc_numprepared(tx_state()) -> tx_state().
   inc_numprepared(State) ->         setelement(10, State, 1 + element(10, State)).
  +-spec get_numabort(tx_state()) -> non_neg_integer().
   get_numabort(State) ->            element(11, State).
  +-spec inc_numabort(tx_state()) -> tx_state().
   inc_numabort(State) ->            setelement(11, State, 1 + element(11, State)).
  +-spec get_numinformed(tx_state()) -> non_neg_integer().
   get_numinformed(State) ->         element(12, State).
  +-spec inc_numinformed(tx_state()) -> tx_state().
   inc_numinformed(State) ->         setelement(12, State, 1 + element(12, State)).
  +-spec set_numinformed(tx_state(), non_neg_integer()) -> tx_state().
   set_numinformed(State, Val) ->    setelement(12, State, Val).
  +-spec get_numpaxdecided(tx_state()) -> non_neg_integer().
   get_numpaxdecided(State) ->       element(13, State).
  +-spec inc_numpaxdecided(tx_state()) -> tx_state().
  +inc_numpaxdecided(State) ->       setelement(13, State, 1 + element(13, State)).
  +-spec set_numpaxdecided(tx_state(), non_neg_integer()) -> tx_state().
   set_numpaxdecided(State, Val) ->  setelement(13, State, Val).
  -inc_numpaxdecided(State) ->       setelement(13, State, 1 + element(13, State)).
  +-spec get_numtpsregistered(tx_state()) -> non_neg_integer().
   get_numtpsregistered(State) ->    element(14, State).
  +-spec inc_numtpsregistered(tx_state()) -> tx_state().
   inc_numtpsregistered(State) ->    setelement(14, State, 1 + element(14, State)).
   
  -%% new / uninitialized / ok.
  +-spec get_status(tx_state()) -> new | uninitialized | ok.
   get_status(State) -> element(15, State).
  +-spec set_status(tx_state(), new | uninitialized | ok) -> tx_state().
   set_status(State, Status) -> setelement(15, State, Status).
  +-spec hold_back(comm:message(), tx_state()) -> tx_state().
   hold_back(Msg, State) -> setelement(16, State, [Msg | element(16, State)]).
  +-spec get_hold_back(tx_state()) -> [comm:message()].
   get_hold_back(State) -> element(16, State).
  +-spec set_hold_back(tx_state(), [comm:message()]) -> tx_state().
   set_hold_back(State, Queue) -> setelement(16, State, Queue).
   
  +-spec newly_decided(tx_state()) -> undecided | false | abort | commit.
   newly_decided(State) ->
       case (undecided =:= is_decided(State)) of
           false -> false; %% was already decided
  
positive.code: -module(tx_state).
  -author('schintke@onscale.de').
  -vsn('$Id$').
  
  %-define(TRACE(X,Y), io:format(X,Y)).
  -define(TRACE(X,Y), ok).
  
negative.code:             end
      end.
  
  -spec all_tps_informed(tx_state()) -> boolean().
  all_tps_informed(State) ->
      %% @TODO use repl. degree
      get_numinformed(State) =:= get_numids(State) * 4.
  
  -spec all_pax_decided(tx_state()) -> boolean().
  all_pax_decided(State) ->
      %% @TODO use repl. degree
      get_numpaxdecided(State) =:= get_numids(State) * 4.
  
  -spec all_tps_registered(tx_state()) -> boolean().
  all_tps_registered(State) ->
      %% @TODO use repl. degree
      get_numtpsregistered(State) =:= get_numids(State) * 4.
  