TLA

OT.tla

-------------------------------- MODULE OT --------------------------------
EXTENDS Integers, TLC, FiniteSets, Sequences

CONSTANTS i_set, i_inc, i_nop \* Instruction model values
CONSTANT NULL

CONSTANT ImprovedAlgo

ASSUME ImprovedAlgo \in BOOLEAN

SetRange == -3..3 \union {NULL}
IncRange == -2..2 \ {0}

Sets == [i: {i_set}, v: SetRange, default: {FALSE}, ts: {0}]
Incs == [i: {i_inc}, v: IncRange, ts: {0}]
Instructions == Sets \union Incs

SimpleInstructionLists(n) == [1..n -> Instructions]
InstructionSets(n) == 
    {[ix \in DOMAIN list |-> [list[ix] EXCEPT !.ts = ix]] : list \in SimpleInstructionLists(n)}

Nop == [i |-> i_nop]
      
NewValue(op, old) == 
    CASE op.i = i_set -> op.v
      [] op.i = i_inc -> IF ImprovedAlgo /\ old = NULL THEN NULL ELSE op.v + old
      [] op.i = i_nop -> old

Transform_SetSet(op1, op2) == 
    IF op1.default = op2.default
    THEN IF op1.ts < op2.ts
         THEN <<Nop, op2>>
         ELSE <<op1, Nop>>
    ELSE IF op1.default
         THEN <<Nop, op2>>
         ELSE <<op1, Nop>>
         
Transform_IncSet(inc, set) ==
    IF ~ImprovedAlgo /\ set.v = NULL THEN <<Nop, set>>
    ELSE IF 
        \/ /\ ImprovedAlgo
           /\ set.default
        \/ set.ts < inc.ts
        THEN <<inc, [set EXCEPT !.v = NewValue(inc, set.v)]>>
    ELSE <<Nop, set>>
    

Reverse(pair) == <<pair[2], pair[1]>>

TransformFull(op1, op2) ==
    CASE op1.i = i_nop \/ op2.i = i_nop -> <<op1, op2>>
      [] op1.i = i_inc /\ op2.i = i_inc -> <<op1, op2>>      
      [] op1.i = i_set /\ op2.i = i_set -> Transform_SetSet(op1, op2)
      [] op1.i = i_inc /\ op2.i = i_set -> Transform_IncSet(op1, op2)
      [] op1.i = i_set /\ op2.i = i_inc -> Reverse(Transform_IncSet(op2, op1))
      
Transform(op1, op2) == TransformFull(op1, op2)[1]

Sequence(op1, op2) == <<op1, Transform(op2, op1)>>

RECURSIVE TransformMulti(_,_)
TransformMulti(op, ops) ==
    IF ops = <<>> 
    THEN op
    ELSE TransformMulti(Transform(op, Head(ops)), Tail(ops))
                            
RECURSIVE ApplyMulti(_,_)
ApplyMulti(val, ops) ==
    IF ops = <<>>
    THEN val
    ELSE ApplyMulti(NewValue(Head(ops), val), Tail(ops))

RECURSIVE SequenceMultiHelper(_,_)
SequenceMultiHelper(ops, hist) == IF ops = <<>> THEN hist ELSE
    LET
      op == Head(ops)
      rest == Tail(ops)
      transformed == TransformMulti(op, hist)
    IN SequenceMultiHelper(rest, Append(hist, transformed))

SequenceMulti(ops) == SequenceMultiHelper(ops, <<>>)

=============================================================================

test.tla

-------------------------------- MODULE test --------------------------------
EXTENDS Integers, TLC, FiniteSets, Sequences, OT

CONSTANTS MaxLen

Permutes(list) == { [i \in 1..Len(list) |-> list[p[i]]] : p \in Permutations(1..Len(list)) }

Range(f) == {f[k] : k \in DOMAIN f}


(* --algorithm merge
variables len \in 1..MaxLen
        , instructions \in InstructionSets(len)
        , value \in {0, NULL};
begin
  assert LET 
             histories == [p \in Permutes(instructions) |-> SequenceMulti(p)]
             endStates == [p \in Permutes(instructions) |-> ApplyMulti(value, histories[p])]
         IN Cardinality(Range(endStates)) = 1;
end algorithm; *)


\* BEGIN TRANSLATION
VARIABLES len, instructions, value, pc

vars == << len, instructions, value, pc >>

Init == (* Global variables *)
        /\ len \in 1..MaxLen
        /\ instructions \in InstructionSets(len)
        /\ value \in {0, NULL}
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ Assert(LET
                       histories == [p \in Permutes(instructions) |-> SequenceMulti(p)]
                       endStates == [p \in Permutes(instructions) |-> ApplyMulti(value, histories[p])]
                   IN Cardinality(Range(endStates)) = 1, 
                   "Failure of assertion at line 16, column 3.")
         /\ pc' = "Done"
         /\ UNCHANGED << len, instructions, value >>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION
=============================================================================