rename files

Signed-off-by: Giuliano Losa <[email protected]>
tlaplus · Jan 22, 2024 · fb0b1d8 · fb0b1d8
1 parent 05ebed1
commit fb0b1d8
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 11 deletions.
diff --git a/manifest.json b/manifest.json
@@ -1263,14 +1263,14 @@
           ]
         },
         {
-          "path": "specifications/Paxos/VotingApalache.tla",
+          "path": "specifications/Paxos/Voting2.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],
           "models": []
         },
         {
-          "path": "specifications/Paxos/MCVotingApalache.tla",
+          "path": "specifications/Paxos/ApaVoting2.tla",
           "communityDependencies": [],
           "tlaLanguageVersion": 2,
           "features": [],

diff --git a/specifications/Paxos/MCVotingApalache.tla → specifications/Paxos/ApaVoting2.tla b/specifications/Paxos/MCVotingApalache.tla → specifications/Paxos/ApaVoting2.tla
@@ -1,4 +1,4 @@
---------------------------- MODULE MCVotingApalache -------------------------------
+--------------------------- MODULE ApaVoting2 -------------------------------
 
 (*********************************************************************************)
 (* In this module we instantiate VotingApalache with small constants in order to *)
@@ -25,7 +25,7 @@ VARIABLES
     \* @type: ACCEPTOR -> Int;
     maxBal
 
-INSTANCE VotingApalache
+INSTANCE Voting2
 
 \* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^'.
 \* Note that this is not necessary if you are using the devcontainer, as `^Apalache,^' is already installed.

diff --git a/specifications/Paxos/README b/specifications/Paxos/README
@@ -30,10 +30,10 @@ MCPaxos
   for the user to write such specs, essentially producing them
   itself from the models defined by the user.
 
-VotingApalache
+Voting2
   A version of the Voting specification that can be analyzed
   by the Apalache model-checker. Also contains an inductive
   invariant that Apalache can verify for small system sizes.
-MCVotingApalache
-  Specification used to model-check VotingApalache with the
-  Apalache model-checker.
+ApaVoting2
+  Specification used to model-check Voting2 with the Apalache
+  model-checker.
diff --git a/specifications/Paxos/VotingApalache.tla → specifications/Paxos/Voting2.tla b/specifications/Paxos/VotingApalache.tla → specifications/Paxos/Voting2.tla
@@ -1,4 +1,4 @@
-------------------------------- MODULE VotingApalache -------------------------------
+------------------------------- MODULE Voting2 -------------------------------
 
 (***********************************************************************************)
 (* This is a version of `^Voting.tla^' that can be analyzed by the `^Apalache^'    *)
@@ -13,7 +13,7 @@
 (* We also give an inductive invariant that proves the consistency property. On a  *)
 (* desktop computer from 2022, `^Apalache^' takes 1 minute and 45 seconds to check *)
 (* that the invariant is inductive when there are 3 values, 3 processes, and 4     *)
-(* ballots. For model-checking with `^Apalache,^'see `^MCVotingApalache.tla^'.     *)
+(* ballots. For model-checking with `^Apalache,^'see `^ApaVoting2.tla^'.           *)
 (***********************************************************************************)
 
 EXTENDS Integers
@@ -106,6 +106,5 @@ Invariant ==
   /\ OneValuePerBallot
   /\ NoVoteAfterMaxBal
   /\ Consistency
-Invariant_ == Invariant
 
 =====================================================================================