spec tweaks

apalache-mc · Oct 10, 2022 · 6aa3c16 · 6aa3c16
1 parent a10f6f6
commit 6aa3c16
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 28 deletions.
diff --git a/examples/bcastByz/bcastByz.tla b/examples/bcastByz/bcastByz.tla
@@ -79,8 +79,7 @@ UponAcceptNotSentBefore(self) ==
   /\ pc[self] \in { "V0", "V1" }
   /\ \E newRcvd \in Int:
     /\ rcvd' = [rcvd EXCEPT ![self] = newRcvd]
-    /\ newRcvd >= N - 2*T
-    /\ newRcvd <= N 
+    /\ newRcvd >= N - T
   /\ pc' = [ pc EXCEPT ![self] = "AC" ]
   /\ sent' = sent + 1
 
@@ -89,7 +88,6 @@ UponAcceptSentBefore(self) ==
   /\ \E newRcvd \in Int:
     /\ rcvd' = [rcvd EXCEPT ![self] = newRcvd]
     /\ newRcvd >= N - T
-    /\ newRcvd <= N 
   /\ pc' = [pc EXCEPT ![self] = "AC"]
   /\ UNCHANGED sent
 

diff --git a/examples/bosco/bosco.tla b/examples/bosco/bosco.tla
@@ -25,11 +25,6 @@ CONSTANTS
     \* @type: Int;
     F
 
-CInit ==
-  /\ N = 4
-  /\ T = 1
-  /\ F = 1
-
 \* The set of correct processes
 Corr == 1..(N - F)
 
@@ -159,15 +154,7 @@ Init ==
   /\ sent1 = 0
   /\ rcvd0 = [ i \in Corr |-> 0 ]
   /\ rcvd1 = [ i \in Corr |-> 0 ]
-
- (* Initial step *)
-Init0 ==
-   /\ pc \in [ Corr -> {"V0"} ]
-   /\ sent0 = 0
-   /\ sent1 = 0
-   /\ rcvd0 = [ i \in Corr |-> 0 ]
-   /\ rcvd1 = [ i \in Corr |-> 0 ]
-
+
 Next == 
   \E self \in Corr: Step(self)
 
@@ -200,9 +187,4 @@ OneStep1 ==
             /\ pc[i] /= "U0"
             /\ pc[i] /= "U1")
 
-OneStep0Mod == \A i \in Corr:
-                    /\ pc[i] /= "D1"
-                    /\ pc[i] /= "U0"
-                    /\ pc[i] /= "U1"
-
 =============================================================================
diff --git a/examples/cf1s_folklore/cf1s_folklore.tla b/examples/cf1s_folklore/cf1s_folklore.tla
@@ -6,8 +6,6 @@
    
    [1] Dobre, Dan, and Neeraj Suri. "One-step consensus with zero-degradation." Dependable Systems and 
    Networks, 2006. DSN 2006. International Conference on. IEEE, 2006.
-                                                               
-   Jure Kukovec, 2022
   
    This file is a subject to the license that is bundled together with this package and can be found 
    in the file LICENSE.
@@ -156,7 +154,8 @@ TypeOK ==
 
  (* If all processes propose 0, then every process crashes or decides 0. *) 
 OneStep0_Ltl ==
-  (\A i \in Proc : pc[i] = "V0") => [](\A i \in Proc : pc[i] # "U0" /\ pc[i] # "U1" /\ pc[i] # "D1")
+  (\A i \in Proc : pc[i] = "V0") => 
+  [](\A i \in Proc : pc[i] # "U0" /\ pc[i] # "U1" /\ pc[i] # "D1")
 
 (* If all processes propose 1, then every process crashes or decides 1. *)
 OneStep1_Ltl ==  

diff --git a/examples/nbacg_guer01/nbacg_guer01.tla b/examples/nbacg_guer01/nbacg_guer01.tla
@@ -5,9 +5,7 @@
  
    [1] Guerraoui, Rachid. "On the hardness of failure-sensitive agreement problems." Information 
    Processing Letters 79.2 (2001): 99-104.
- 
-   Jure Kukovec, 2022
- 
+  
    This file is a subject to the license that is bundled together with this package and can 
    be found in the file LICENSE.
  *)