Specification of ForceMove to exhibit safety.

.gitignore

@@ -1,4 +1,11 @@
 # The tla+ toolbox creates a .toolbox folder for each specification you create
 # While this folder does contain model details, which we potentially want to check
 # in, it also contains a lot of other files, so we ignore it for the moment
-*.toolbox/
+*.toolbox/
+
+# The tlatex utility produces auxilliary files when compiling the spec
+*.aux
+*.dvi
+*.log
+*.old
+*.tex

ForceMove/EveCannotFrontRun.cfg

@@ -0,0 +1,15 @@
+CONSTANT
+NULL = NULL
+StartingTurnNumber <- const_StartingTurnNumber
+NumParticipants <- const_NumParticipants
+AlicesIDX <- const_AlicesIDX
+Nat <- def_ov_Nat
+
+SPECIFICATION
+Spec
+
+INVARIANT
+TypeOK
+
+PROPERTY
+EveCannotFrontRun

ForceMove/FiveParticipants.tla

@@ -0,0 +1,8 @@
+---- MODULE FiveParticipants ----
+EXTENDS ForceMove, TLC
+
+const_StartingTurnNumber == 6
+const_NumParticipants == 5
+const_AlicesIDX == 3
+def_ov_Nat == 0..15
+=============================================================================

ForceMove/Success.cfg

@@ -0,0 +1,18 @@
+CONSTANT
+NULL = NULL
+StartingTurnNumber <- const_StartingTurnNumber
+NumParticipants <- const_NumParticipants
+AlicesIDX <- const_AlicesIDX
+Nat <- def_ov_Nat
+
+SPECIFICATION
+Spec
+
+INVARIANT
+TypeOK
+
+PROPERTY
+Termination
+AliceCanProgressChannel
+AliceMustSubmitTransactions
+TurnNumberIncrements

ForceMove/ThreeParticipants.tla

@@ -0,0 +1,8 @@
+---- MODULE ThreeParticipants ----
+EXTENDS ForceMove, TLC
+
+const_StartingTurnNumber == 5
+const_NumParticipants == 3
+const_AlicesIDX == 3
+def_ov_Nat == 0..20
+=============================================================================

ForceMove/TwoParticipants.tla

@@ -0,0 +1,8 @@
+---- MODULE TwoParticipants ----
+EXTENDS ForceMove, TLC
+
+const_StartingTurnNumber == 5
+const_NumParticipants == 2
+const_AlicesIDX == 2
+def_ov_Nat == 0..20
+=============================================================================

ForceMove/TwoParticipantsLongHistory.tla

@@ -0,0 +1,8 @@
+---- MODULE TwoParticipantsLongHistory ----
+EXTENDS ForceMove, TLC
+
+const_StartingTurnNumber == 31
+const_NumParticipants == 2
+const_AlicesIDX == 2
+def_ov_Nat == 0..64
+=============================================================================

ForceMove/Utils.tla

@@ -0,0 +1,20 @@
+------------------------------- MODULE Utils -------------------------------
+EXTENDS Integers
+ChannelMode == [
+  OPEN      |-> "OPEN",
+  CHALLENGE |-> "CHALLENGE"
+]
+
+TX_Type == [
+  FORCE_MOVE |-> "FORCE_MOVE",
+  REFUTE     |-> "REFUTE",
+  RESPOND    |-> "RESPOND"
+]
+
+Range(f) == { f[x] : x \in DOMAIN f }
+Maximum(a,b) == IF a > b THEN a ELSE b
+
+=============================================================================
+\* Modification History
+\* Last modified Tue Sep 10 18:36:13 MDT 2019 by andrewstewart
+\* Created Tue Sep 10 18:35:45 MDT 2019 by andrewstewart