Skip to content

Instantly share code, notes, and snippets.

@RedBeard0531
Created Dec 13, 2019
Embed
What would you like to do?
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, <<>>)
=============================================================================
-------------------------------- 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
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment