improve comments

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

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/specifications/Paxos/MCVotingApalache.tla b/specifications/Paxos/MCVotingApalache.tla
@@ -1,5 +1,11 @@
 --------------------------- MODULE MCVotingApalache -------------------------------
 
+(*********************************************************************************)
+(* In this module we instantiate VotingApalache with small constants in order to *)
+(* run the `^Apalache^' model-checker. We also give type annotations for the     *)
+(* variables, which are required by `^Apalache^'.                                *)
+(*********************************************************************************)
+
 EXTENDS Integers
 
 Value == {"V1_OF_VALUE","V2_OF_VALUE"}
@@ -11,7 +17,7 @@ Quorum == {
     {"A2_OF_ACCEPTOR","A3_OF_ACCEPTOR"}}
 
 MaxBal == 2
-Ballot == 0..MaxBal \* NOTE: has to be finite for `^Apalache^' because it is used as the domain of a function
+Ballot == 0..MaxBal \* NOTE: we have to make this a finite set for `^Apalache^'
 
 VARIABLES
     \* @type: ACCEPTOR -> Set(<<Int,VALUE>>);

diff --git a/specifications/Paxos/VotingApalache.tla b/specifications/Paxos/VotingApalache.tla
@@ -4,7 +4,8 @@
 (* This is a version of `^Voting.tla^' that can be analyzed by the `^Apalache^'    *)
 (* model-checker. Here are the differences compared to `^Voting.tla^':             *)
 (*                                                                                 *)
-(*     * We make Ballot a constant in order to be able to substitute a finite set. *)
+(*     * We make Ballot a constant in order to be able to substitute a finite set  *)
+(*       for model-checking with Apalache.                                         *)
 (*                                                                                 *)
 (*     * We rewrite SafeAt and ShowsSafeAt to avoid ranges of integers with        *)
 (*       non-constant bounds (which `^Apalache^' does not support).                *)