Migration of TLA+ files from the spec repo (#8004)

spec/consensus/proposer-based-timestamp/tla/Apalache.tla

@@ -0,0 +1,109 @@
+--------------------------- MODULE Apalache -----------------------------------
+(*
+ * This is a standard module for use with the Apalache model checker.
+ * The meaning of the operators is explained in the comments.
+ * Many of the operators serve as additional annotations of their arguments.
+ * As we like to preserve compatibility with TLC and TLAPS, we define the
+ * operator bodies by erasure. The actual interpretation of the operators is
+ * encoded inside Apalache. For the moment, these operators are mirrored in
+ * the class at.forsyte.apalache.tla.lir.oper.ApalacheOper.
+ *                                                                          
+ * Igor Konnov, Jure Kukovec, Informal Systems 2020-2021                    
+ *)
+
+(**
+ * An assignment of an expression e to a state variable x. Typically, one
+ * uses the non-primed version of x in the initializing predicate Init and
+ * the primed version of x (that is, x') in the transition predicate Next.
+ * Although TLA+ does not have a concept of a variable assignment, we find
+ * this concept extremely useful for symbolic model checking. In pure TLA+,
+ * one would simply write x = e, or x \in {e}.
+ *
+ * Apalache automatically converts some expressions of the form
+ * x = e or x \in {e} into assignments. However, if you like to annotate
+ * assignments by hand, you can use this operator.
+ *
+ * For a further discussion on that matter, see:
+ * https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md
+ *)
+x := e == x = e
+
+(**
+ * A generator of a data structure. Given a positive integer `bound`, and
+ * assuming that the type of the operator application is known, we
+ * recursively generate a TLA+ data structure as a tree, whose width is
+ * bound by the number `bound`.
+ *
+ * The body of this operator is redefined by Apalache.
+ *)
+Gen(size) == {}
+
+(**
+ * Convert a set of pairs S to a function F. Note that if S contains at least
+ * two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,
+ * then F is not uniquely defined. We use CHOOSE to resolve this ambiguity.
+ * Apalache implements a more efficient encoding of this operator
+ * than the default one.
+ *
+ * @type: Set(<<a, b>>) => (a -> b);
+ *)
+SetAsFun(S) ==
+    LET Dom == { x: <<x, y>> \in S }
+        Rng == { y: <<x, y>> \in S }
+    IN
+    [ x \in Dom |-> CHOOSE y \in Rng: <<x, y>> \in S ]
+
+(**
+ * As TLA+ is untyped, one can use function- and sequence-specific operators
+ * interchangeably. However, to maintain correctness w.r.t. our type-system,
+ * an explicit cast is needed when using functions as sequences.
+ *)
+LOCAL INSTANCE Sequences
+FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)
+
+(**
+ * Annotating an expression \E x \in S: P as Skolemizable. That is, it can
+ * be replaced with an expression c \in S /\ P(c) for a fresh constant c.
+ * Not every exisential can be replaced with a constant, this should be done
+ * with care. Apalache detects Skolemizable expressions by static analysis.
+ *)
+Skolem(e) == e
+
+(**
+ * A hint to the model checker to expand a set S, instead of dealing
+ * with it symbolically. Apalache finds out which sets have to be expanded
+ * by static analysis.
+ *)
+Expand(S) == S
+
+(**
+ * A hint to the model checker to replace its argument Cardinality(S) >= k
+ * with a series of existential quantifiers for a constant k.
+ * Similar to Skolem, this has to be done carefully. Apalache automatically
+ * places this hint by static analysis.
+ *)
+ConstCardinality(cardExpr) == cardExpr
+
+(**
+ * The folding operator, used to implement computation over a set.
+ * Apalache implements a more efficient encoding than the one below.
+ * (from the community modules).
+ *)
+RECURSIVE FoldSet(_,_,_)
+FoldSet( Op(_,_), v, S ) == IF S = {}
+                            THEN v
+                            ELSE LET w == CHOOSE x \in S: TRUE
+                                  IN LET T == S \ {w}
+                                      IN FoldSet( Op, Op(v,w), T )
+
+(**
+ * The folding operator, used to implement computation over a sequence.
+ * Apalache implements a more efficient encoding than the one below.
+ * (from the community modules).
+ *)
+RECURSIVE FoldSeq(_,_,_)
+FoldSeq( Op(_,_), v, seq ) == IF seq = <<>>
+                              THEN v
+                              ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) )
+
+===============================================================================

spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla

@@ -0,0 +1,77 @@
+----------------------------- MODULE MC_PBT -------------------------------
+CONSTANT 
+  \* @type: ROUND -> PROCESS;
+  Proposer
+
+VARIABLES
+  \* @type: PROCESS -> ROUND;
+  round,    \* a process round number
+  \* @type: PROCESS -> STEP;
+  step,     \* a process step
+  \* @type: PROCESS -> DECISION;
+  decision, \* process decision
+  \* @type: PROCESS -> VALUE;
+  lockedValue,  \* a locked value
+  \* @type: PROCESS -> ROUND;
+  lockedRound,  \* a locked round
+  \* @type: PROCESS -> PROPOSAL;
+  validValue,   \* a valid value
+  \* @type: PROCESS -> ROUND;
+  validRound    \* a valid round
+
+\* time-related variables
+VARIABLES  
+  \* @type: PROCESS -> TIME;
+  localClock, \* a process local clock: Corr -> Ticks
+  \* @type: TIME;
+  realTime   \* a reference Newtonian real time
+
+\* book-keeping variables
+VARIABLES
+  \* @type: ROUND -> Set(PROPMESSAGE);
+  msgsPropose,   \* PROPOSE messages broadcast in the system, Rounds -> Messages
+  \* @type: ROUND -> Set(PREMESSAGE);
+  msgsPrevote,   \* PREVOTE messages broadcast in the system, Rounds -> Messages
+  \* @type: ROUND -> Set(PREMESSAGE);
+  msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
+  \* @type: Set(MESSAGE);
+  evidence, \* the messages that were used by the correct processes to make transitions
+  \* @type: ACTION;
+  action,       \* we use this variable to see which action was taken
+  \* @type: PROCESS -> Set(PROPMESSAGE);
+  receivedTimelyProposal, \* used to keep track when a process receives a timely VALUE message
+  \* @type: <<ROUND,PROCESS>> -> TIME;
+  inspectedProposal \* used to keep track when a process tries to receive a message
+  
+\* Invariant support
+VARIABLES
+  \* @type: ROUND -> TIME;
+  beginRound, \* the minimum of the local clocks at the time any process entered a new round
+  \* @type: PROCESS -> TIME;
+  endConsensus, \* the local time when a decision is made
+  \* @type: ROUND -> TIME;
+  lastBeginRound, \* the maximum of the local clocks in each round
+  \* @type: ROUND -> TIME;
+  proposalTime, \* the real time when a proposer proposes in a round
+  \* @type: ROUND -> TIME;
+  proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
+
+
+INSTANCE TendermintPBT_002_draft WITH
+  Corr <- {"c1", "c2"},
+  Faulty <- {"f3", "f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 5,
+  MaxTimestamp <- 10,
+  MinTimestamp <- 2,
+  Delay <- 2,        
+  Precision <- 2
+
+\* run Apalache with --cinit=CInit
+CInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

@@ -5,10 +5,11 @@
  the Tendermint TLA+ specification for fork accountability: 
     https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/TendermintAcc_004_draft.tla
  
- * Version 1. A preliminary specification.
+ * Version 2. A preliminary specification.
 
  Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
  Ilina Stoilkovska, Josef Widder, Informal Systems, 2021.
+ Jure Kukovec, Informal Systems, 2022.
  *)
 
 EXTENDS Integers, FiniteSets, Apalache, typedefs
@@ -38,13 +39,11 @@ CONSTANTS
   \* @type: TIME;
   MaxTimestamp,  \* the maximal value of the clock tick
   \* @type: TIME;
-  Delay,         \* message delay
+  MinTimestamp,  \* the minimal value of the clock tick
   \* @type: TIME;
-  Precision,     \* clock precision: the maximal difference between two local clocks  
+  Delay,         \* message delay
   \* @type: TIME;
-  Accuracy,      \* clock accuracy: the maximal difference between a local clock and the real time
-  \* @type: Bool;
-  ClockDrift     \* is there clock drift between the local clocks and the global clock
+  Precision     \* clock precision: the maximal difference between two local clocks  
 
 ASSUME(N = Cardinality(Corr \union Faulty))
 
@@ -66,24 +65,39 @@ Values == ValidValues \union InvalidValues \* the set of all values
 \* @type: VALUE;
 NilValue == "None"  \* a special value for a nil round, outside of Values
 \* @type: Set(PROPOSAL);
-Proposals == Values \X Timestamps
+Proposals == Values \X Timestamps \X Rounds
 \* @type: PROPOSAL;
-NilProposal == <<NilValue, NilTimestamp>>
+NilProposal == <<NilValue, NilTimestamp, NilRound>>
 \* @type: Set(VALUE);
 ValuesOrNil == Values \union {NilValue}
 \* @type: Set(DECISION);
-Decisions == Values \X Timestamps \X Rounds
+Decisions == Proposals \X Rounds
 \* @type: DECISION;
-NilDecision == <<NilValue, NilTimestamp, NilRound>>
-
+NilDecision == <<NilProposal, NilRound>>
 
+ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
 \* a value hash is modeled as identity
 \* @type: (t) => t;
 Id(v) == v
 
 \* The validity predicate
-\* @type: (VALUE) => Bool;
-IsValid(v) == v \in ValidValues
+\* @type: (PROPOSAL) => Bool;
+IsValid(p) == p \in ValidProposals
+
+\* Time validity check. If we want MaxTimestamp = \infty, set ValidTime(t) == TRUE
+ValidTime(t) == t < MaxTimestamp
+
+\* @type: (PROPMESSAGE) => VALUE;
+MessageValue(msg) == msg.proposal[1]
+\* @type: (PROPMESSAGE) => TIME;
+MessageTime(msg) == msg.proposal[2]
+\* @type: (PROPMESSAGE) => ROUND;
+MessageRound(msg) == msg.proposal[3]
+
+\* @type: (TIME, TIME) => Bool;
+IsTimely(processTime, messageTime) ==
+  /\ processTime >= messageTime - Precision
+  /\ processTime <= messageTime + Precision + Delay
 
 \* the two thresholds that are used in the algorithm
 \* @type: Int;
@@ -91,23 +105,24 @@ THRESHOLD1 == T + 1     \* at least one process is not faulty
 \* @type: Int;
 THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
 
+\* @type: (TIME, TIME) => TIME;
+Min2(a,b) == IF a <= b THEN a ELSE b
 \* @type: (Set(TIME)) => TIME;
-Min(S) == CHOOSE x \in S : \A y \in S : x <= y
+Min(S) == FoldSet( Min2, MaxTimestamp, S )
+\* Min(S) == CHOOSE x \in S : \A y \in S : x <= y
 
+\* @type: (TIME, TIME) => TIME;
+Max2(a,b) == IF a >= b THEN a ELSE b
 \* @type: (Set(TIME)) => TIME;
-Max(S) == CHOOSE x \in S : \A y \in S : y <= x
-
-(********************* TYPE ANNOTATIONS FOR APALACHE **************************)
-
-\* a type annotation for an empty set of messages
-\* @type: Set(MESSAGE);
-EmptyMsgSet == {}
-
-\* @type: Set(RCVPROP);
-EmptyRcvProp == {}
+Max(S) == FoldSet( Max2, NilTimestamp, S )
+\* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
 
-\* @type: Set(PROCESS);
-EmptyProcSet == {}
+\* @type: (Set(MESSAGE)) => Int;
+Card(S) == 
+  LET 
+    \* @type: (Int, MESSAGE) => Int;
+    PlusOne(i, m) == i + 1
+  IN FoldSet( PlusOne, 0, S )
 
 (********************* PROTOCOL STATE VARIABLES ******************************)
 VARIABLES
@@ -121,11 +136,15 @@ VARIABLES
   lockedValue,  \* a locked value
   \* @type: PROCESS -> ROUND;
   lockedRound,  \* a locked round
-  \* @type: PROCESS -> VALUE;
+  \* @type: PROCESS -> PROPOSAL;
   validValue,   \* a valid value
   \* @type: PROCESS -> ROUND;
   validRound    \* a valid round
 
+coreVars == 
+  <<round, step, decision, lockedValue, 
+  lockedRound, validValue, validRound>>
+
 \* time-related variables
 VARIABLES  
   \* @type: PROCESS -> TIME;
@@ -133,6 +152,8 @@ VARIABLES
   \* @type: TIME;
   realTime   \* a reference Newtonian real time
 
+temporalVars == <<localClock, realTime>>
+
 \* book-keeping variables
 VARIABLES
   \* @type: ROUND -> Set(PROPMESSAGE);
@@ -145,28 +166,35 @@ VARIABLES
   evidence, \* the messages that were used by the correct processes to make transitions
   \* @type: ACTION;
   action,       \* we use this variable to see which action was taken
-  \* @type: Set(RCVPROP);
+  \* @type: PROCESS -> Set(PROPMESSAGE);
   receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message
-  \* @type: ROUND -> Set(PROCESS);
-  inspectedProposal, \* used to keep track when a process tries to receive a message
-  \* @type: TIME;
-  beginConsensus, \* the minimum of the local clocks in the initial state
+  \* @type: <<ROUND,PROCESS>> -> TIME;
+  inspectedProposal \* used to keep track when a process tries to receive a message
+  
+\* Action is excluded from the tuple, because it always changes
+bookkeepingVars == 
+  <<msgsPropose, msgsPrevote, msgsPrecommit, 
+  evidence, (*action,*) receivedTimelyProposal, 
+  inspectedProposal>>
+
+\* Invariant support
+VARIABLES
+  \* @type: ROUND -> TIME;
+  beginRound, \* the minimum of the local clocks at the time any process entered a new round
   \* @type: PROCESS -> TIME;
   endConsensus, \* the local time when a decision is made
-  \* @type: TIME;
-  lastBeginConsensus, \* the maximum of the local clocks in the initial state
+  \* @type: ROUND -> TIME;
+  lastBeginRound, \* the maximum of the local clocks in each round
   \* @type: ROUND -> TIME;
   proposalTime, \* the real time when a proposer proposes in a round
   \* @type: ROUND -> TIME;
   proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
 
+invariantVars == 
+  <<beginRound, endConsensus, lastBeginRound,
+  proposalTime, proposalReceivedTime>>
+
 (* to see a type invariant, check TendermintAccInv3 *)  
- 
-\* a handy definition used in UNCHANGED
-vars == <<round, step, decision, lockedValue, lockedRound,
-          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-          localClock, realTime, receivedTimelyProposal, inspectedProposal, action,
-          beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
 
 (********************* PROTOCOL INITIALIZATION ******************************)
 \* @type: (ROUND) => Set(PROPMESSAGE);
@@ -255,30 +283,37 @@ BenignRoundsInMessages(msgfun) ==
 \* The initial states of the protocol. Some faults can be in the system already.
 Init ==
     /\ round = [p \in Corr |-> 0]
-    /\ \/ /\ ~ClockDrift
-          /\ localClock \in [Corr -> 0..Accuracy]
-       \/ /\ ClockDrift
-          /\ localClock = [p \in Corr |-> 0]
+    /\ localClock \in [Corr -> MinTimestamp..(MinTimestamp + Precision)]
     /\ realTime = 0
     /\ step = [p \in Corr |-> "PROPOSE"]
     /\ decision = [p \in Corr |-> NilDecision]
     /\ lockedValue = [p \in Corr |-> NilValue]
     /\ lockedRound = [p \in Corr |-> NilRound]
-    /\ validValue = [p \in Corr |-> NilValue]
+    /\ validValue = [p \in Corr |-> NilProposal]
     /\ validRound = [p \in Corr |-> NilRound]
     /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
     /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
     /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
-    /\ receivedTimelyProposal = EmptyRcvProp
-    /\ inspectedProposal = [r \in Rounds |-> EmptyProcSet]
+    /\ receivedTimelyProposal = [p \in Corr |-> {}]
+    /\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp]
     /\ BenignRoundsInMessages(msgsPropose)
     /\ BenignRoundsInMessages(msgsPrevote)
     /\ BenignRoundsInMessages(msgsPrecommit)
-    /\ evidence = EmptyMsgSet
+    /\ evidence = {}
     /\ action' = "Init"
-    /\ beginConsensus = Min({localClock[p] : p \in Corr})
+    /\ beginRound = 
+      [r \in Rounds |-> 
+        IF r = 0
+        THEN Min({localClock[p] : p \in Corr})
+        ELSE MaxTimestamp
+      ]
     /\ endConsensus = [p \in Corr |-> NilTimestamp]
-    /\ lastBeginConsensus = Max({localClock[p] : p \in Corr})
+    /\ lastBeginRound = 
+      [r \in Rounds |-> 
+        IF r = 0
+        THEN Max({localClock[p] : p \in Corr})
+        ELSE NilTimestamp
+      ]
     /\ proposalTime = [r \in Rounds |-> NilTimestamp]
     /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
 
@@ -296,7 +331,7 @@ BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
       validRound |-> pValidRound
     ]
   IN
-  msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
+  /\ msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
 
 \* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
 BroadcastPrevote(pSrc, pRound, pId) ==
@@ -310,7 +345,7 @@ BroadcastPrevote(pSrc, pRound, pId) ==
       id    |-> pId
     ]
   IN
-  msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
+  /\ msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
 
 \* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
 BroadcastPrecommit(pSrc, pRound, pId) ==
@@ -324,7 +359,7 @@ BroadcastPrecommit(pSrc, pRound, pId) ==
       id    |-> pId
     ]
   IN
-  msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
+  /\ msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
 
 (***************************** TIME **************************************)
 
@@ -339,14 +374,14 @@ SynchronizedLocalClocks ==
                /\ localClock[q] - localClock[p] < Precision
     
 \* [PBTS-PROPOSE.0]
-\* @type: (VALUE, TIME) => PROPOSAL;
-Proposal(v, t) ==
-    <<v, t>>
+\* @type: (VALUE, TIME, ROUND) => PROPOSAL;
+Proposal(v, t, r) ==
+    <<v, t, r>>
 
 \* [PBTS-DECISION-ROUND.0]
-\* @type: (VALUE, TIME, ROUND) => DECISION;
-Decision(v, t, r) ==
-    <<v, t, r>>
+\* @type: (PROPOSAL, ROUND) => DECISION;
+Decision(p, r) ==
+    <<p, r>>
 
 (**************** MESSAGE PROCESSING TRANSITIONS *************************)
 \* lines 12-13
@@ -354,7 +389,10 @@ Decision(v, t, r) ==
 StartRound(p, r) ==
    /\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
    /\ round' = [round EXCEPT ![p] = r]
-   /\ step' = [step EXCEPT ![p] = "PROPOSE"] 
+   /\ step' = [step EXCEPT ![p] = "PROPOSE"]
+   \* We only need to update (last)beginRound[r] once a process enters round `r`
+   /\ beginRound' = [beginRound EXCEPT ![r] = Min2(@, localClock[p])]
+   /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
 
 \* lines 14-19, a proposal may be sent later
 \* @type: (PROCESS) => Bool;
@@ -365,20 +403,22 @@ InsertProposal(p) ==
     \* if the proposer is sending a proposal, then there are no other proposals
     \* by the correct processes for the same round
   /\ \A m \in msgsPropose[r]: m.src /= p
+  \* /\ localClock[p] > 
   /\ \E v \in ValidValues: 
-      LET value == 
-        IF validValue[p] /= NilValue 
+      LET proposal == 
+        IF validValue[p] /= NilProposal 
         THEN validValue[p]
-        ELSE v
-      IN LET 
-        proposal == Proposal(value, localClock[p]) 
+        ELSE Proposal(v, localClock[p], r)
       IN               
-      /\ BroadcastProposal(p, round[p], proposal, validRound[p])
+      /\ BroadcastProposal(p, r, proposal, validRound[p])
       /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
-  /\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
-                validValue, step, validRound, msgsPrevote, msgsPrecommit,
-                localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                beginConsensus, endConsensus, lastBeginConsensus, proposalReceivedTime>>
+  /\ UNCHANGED <<temporalVars, coreVars>>
+  /\ UNCHANGED 
+    <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, 
+    evidence, receivedTimelyProposal, inspectedProposal>>
+  /\ UNCHANGED
+    <<beginRound, endConsensus, lastBeginRound,
+    (*proposalTime,*) proposalReceivedTime>>
   /\ action' = "InsertProposal"
   
 \* a new action used to filter messages that are not on time
@@ -394,92 +434,120 @@ ReceiveProposal(p) ==
             type       |-> "PROPOSAL", 
             src        |-> Proposer[round[p]],
             round      |-> round[p], 
-            proposal   |-> Proposal(v, t), 
+            proposal   |-> Proposal(v, t, r), 
             validRound |-> NilRound
           ] 
        IN
       /\ msg \in msgsPropose[round[p]] 
-      /\ p \notin inspectedProposal[r]
-      /\ <<p, msg>> \notin receivedTimelyProposal
-      /\ inspectedProposal' = [inspectedProposal EXCEPT ![r] = @ \union {p}]
-      /\ \/ /\ localClock[p] - Precision < t 
-            /\ t < localClock[p] + Precision + Delay
-            /\ receivedTimelyProposal' = receivedTimelyProposal \union {<<p, msg>>}
-            /\ \/ /\ proposalReceivedTime[r] = NilTimestamp
-                  /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
-               \/ /\ proposalReceivedTime[r] /= NilTimestamp
-                  /\ UNCHANGED proposalReceivedTime
-         \/ /\ \/ localClock[p] - Precision >= t
-               \/ t >= localClock[p] + Precision + Delay
-            /\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
-      /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
-          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-          localClock, realTime, beginConsensus, endConsensus, lastBeginConsensus, proposalTime>>
+      /\ inspectedProposal[r,p] = NilTimestamp
+      /\ msg \notin receivedTimelyProposal[p]
+      /\ inspectedProposal' = [inspectedProposal EXCEPT ![r,p] = localClock[p]]
+      /\ LET 
+          isTimely == IsTimely(localClock[p], t)
+         IN
+          \/ /\ isTimely
+             /\ receivedTimelyProposal' = [receivedTimelyProposal EXCEPT ![p] = @ \union {msg}]
+             /\ LET
+                  isNilTimestamp == proposalReceivedTime[r] = NilTimestamp
+                IN
+                  \/ /\ isNilTimestamp
+                     /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
+                  \/ /\ ~isNilTimestamp
+                     /\ UNCHANGED proposalReceivedTime
+          \/ /\ ~isTimely
+             /\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
+      /\ UNCHANGED <<temporalVars, coreVars>>
+      /\ UNCHANGED
+        <<msgsPropose, msgsPrevote, msgsPrecommit, 
+        evidence(*, receivedTimelyProposal, inspectedProposal*)>>
+      /\ UNCHANGED 
+        <<beginRound, endConsensus, lastBeginRound,
+        proposalTime(*, proposalReceivedTime*)>>
       /\ action' = "ReceiveProposal"
       
 \* lines 22-27
 \* @type: (PROCESS) => Bool;
 UponProposalInPropose(p) ==
   \E v \in Values, t \in Timestamps:
+    LET 
+      r == round[p]
+    IN LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,r)
+    IN
     /\ step[p] = "PROPOSE" (* line 22 *)
     /\ LET 
         \* @type: PROPMESSAGE; 
         msg ==
         [
           type       |-> "PROPOSAL", 
-          src        |-> Proposer[round[p]],
-          round      |-> round[p], 
-          proposal   |-> Proposal(v, t), 
+          src        |-> Proposer[r],
+          round      |-> r, 
+          proposal   |-> prop, 
           validRound |-> NilRound
         ] 
        IN
-      /\ <<p, msg>> \in receivedTimelyProposal \* updated line 22
+      /\ msg \in receivedTimelyProposal[p] \* updated line 22
       /\ evidence' = {msg} \union evidence
     /\ LET mid == (* line 23 *)
-         IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
-         THEN Id(Proposal(v, t))
+         IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
+         THEN Id(prop)
          ELSE NilProposal
        IN
-       BroadcastPrevote(p, round[p], mid) \* lines 24-26
+       BroadcastPrevote(p, r, mid) \* lines 24-26
     /\ step' = [step EXCEPT ![p] = "PREVOTE"]
-    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
-                   validValue, validRound, msgsPropose, msgsPrecommit,
-                   localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                   beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision, lockedValue, 
+      lockedRound, validValue, validRound>>
+    /\ UNCHANGED 
+      <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInPropose"
 
 \* lines 28-33        
 \* [PBTS-ALG-OLD-PREVOTE.0]
 \* @type: (PROCESS) => Bool;
 UponProposalInProposeAndPrevote(p) ==
-  \E v \in Values, t1 \in Timestamps, t2 \in Timestamps, vr \in Rounds:
-    /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
-    /\ LET 
+  \E v \in Values, t \in Timestamps, vr \in Rounds, pr \in Rounds:
+    LET 
+      r == round[p]
+    IN LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,pr)
+    IN
+    /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < r \* line 28, the while part
+    /\ pr <= vr
+    /\ LET
         \* @type: PROPMESSAGE; 
         msg ==
         [
           type       |-> "PROPOSAL", 
-          src        |-> Proposer[round[p]],
-          round      |-> round[p], 
-          proposal   |-> Proposal(v, t1), 
+          src        |-> Proposer[r],
+          round      |-> r, 
+          proposal   |-> prop, 
           validRound |-> vr
         ]
        IN
-       /\ <<p, msg>> \in receivedTimelyProposal \* updated line 28
-       /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(Proposal(v, t2)) } IN
+       \* Changed from 001: no need to re-check timeliness
+       /\ msg \in msgsPropose[r] \* line 28
+       /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(prop) } IN
           /\ Cardinality(PV) >= THRESHOLD2 \* line 28
           /\ evidence' = PV \union {msg} \union evidence
     /\ LET mid == (* line 29 *)
-         IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
-         THEN Id(Proposal(v, t1)) 
+         IF IsValid(prop) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
+         THEN Id(prop) 
          ELSE NilProposal 
        IN
-       BroadcastPrevote(p, round[p], mid) \* lines 24-26
+       BroadcastPrevote(p, r, mid) \* lines 24-26
     /\ step' = [step EXCEPT ![p] = "PREVOTE"]
-    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
-                   validValue, validRound, msgsPropose, msgsPrecommit,
-                   localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                   beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision, lockedValue, 
+      lockedRound, validValue, validRound>>
+    /\ UNCHANGED 
+      <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInProposeAndPrevote"
                      
 \* lines 34-35 + lines 61-64 (onTimeoutPrevote)
@@ -494,10 +562,13 @@ UponQuorumOfPrevotesAny(p) ==
       /\ evidence' = MyEvidence \union evidence
       /\ BroadcastPrecommit(p, round[p], NilProposal)
       /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
-      /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
-                    validValue, validRound, msgsPropose, msgsPrevote,
-                    localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                    beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+      /\ UNCHANGED <<temporalVars, invariantVars>>
+      /\ UNCHANGED
+        <<round, (*step,*) decision, lockedValue, 
+        lockedRound, validValue, validRound>>
+      /\ UNCHANGED 
+        <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
+        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
       /\ action' = "UponQuorumOfPrevotesAny"
                      
 \* lines 36-46
@@ -505,36 +576,47 @@ UponQuorumOfPrevotesAny(p) ==
 \* @type: (PROCESS) => Bool;
 UponProposalInPrevoteOrCommitAndPrevote(p) ==
   \E v \in ValidValues, t \in Timestamps, vr \in RoundsOrNil:
+    LET 
+      r == round[p]
+    IN LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,r)
+    IN
     /\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
     /\ LET
         \* @type: PROPMESSAGE; 
         msg ==
         [
           type       |-> "PROPOSAL", 
-          src        |-> Proposer[round[p]],
-          round      |-> round[p], 
-          proposal   |-> Proposal(v, t), 
+          src        |-> Proposer[r],
+          round      |-> r, 
+          proposal   |-> prop, 
           validRound |-> vr
         ] 
        IN 
-        /\ <<p, msg>> \in receivedTimelyProposal \* updated line 36
-        /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(Proposal(v, t)) } IN
+        \* Changed from 001: no need to re-check timeliness
+        /\ msg \in msgsPropose[r] \* line 36
+        /\ LET PV == { m \in msgsPrevote[r]: m.id = Id(prop) } IN
           /\ Cardinality(PV) >= THRESHOLD2 \* line 36
           /\ evidence' = PV \union {msg} \union evidence
     /\  IF step[p] = "PREVOTE"
         THEN \* lines 38-41:
           /\ lockedValue' = [lockedValue EXCEPT ![p] = v]
-          /\ lockedRound' = [lockedRound EXCEPT ![p] = round[p]]
-          /\ BroadcastPrecommit(p, round[p], Id(Proposal(v, t)))
+          /\ lockedRound' = [lockedRound EXCEPT ![p] = r]
+          /\ BroadcastPrecommit(p, r, Id(prop))
           /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
         ELSE
           UNCHANGED <<lockedValue, lockedRound, msgsPrecommit, step>>
       \* lines 42-43
-    /\ validValue' = [validValue EXCEPT ![p] = v]
-    /\ validRound' = [validRound EXCEPT ![p] = round[p]]
-    /\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote,
-                  localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ validValue' = [validValue EXCEPT ![p] = prop]
+    /\ validRound' = [validRound EXCEPT ![p] = r]
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision(*, lockedValue, 
+      lockedRound, validValue, validRound*)>>
+    /\ UNCHANGED 
+      <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
 
 \* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -547,11 +629,17 @@ UponQuorumOfPrecommitsAny(p) ==
       /\ Cardinality(Committers) >= THRESHOLD2 \* line 47
       /\ evidence' = MyEvidence \union evidence
       /\ round[p] + 1 \in Rounds
-      /\ StartRound(p, round[p] + 1)   
-      /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
-                    validRound, msgsPropose, msgsPrevote, msgsPrecommit,
-                    localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                    beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+      /\ StartRound(p, round[p] + 1)
+      /\ UNCHANGED temporalVars
+      /\ UNCHANGED
+        <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
+        proposalTime, proposalReceivedTime>>
+      /\ UNCHANGED
+        <<(*round, step,*) decision, lockedValue, 
+        lockedRound, validValue, validRound>>
+      /\ UNCHANGED 
+        <<msgsPropose, msgsPrevote, msgsPrecommit,
+        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
       /\ action' = "UponQuorumOfPrecommitsAny"
                      
 \* lines 49-54        
@@ -559,7 +647,11 @@ UponQuorumOfPrecommitsAny(p) ==
 \* @type: (PROCESS) => Bool;
 UponProposalInPrecommitNoDecision(p) ==
   /\ decision[p] = NilDecision \* line 49
-  /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
+  /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, pr \in Rounds, vr \in RoundsOrNil:
+    LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,pr)
+    IN
     /\ LET
         \* @type: PROPMESSAGE; 
         msg == 
@@ -567,24 +659,30 @@ UponProposalInPrecommitNoDecision(p) ==
           type       |-> "PROPOSAL", 
           src        |-> Proposer[r],
           round      |-> r, 
-          proposal   |-> Proposal(v, t), 
+          proposal   |-> prop, 
           validRound |-> vr
         ] 
        IN 
      /\ msg \in msgsPropose[r] \* line 49
-     /\ p \in inspectedProposal[r]
-     /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(Proposal(v, t)) } IN
+     /\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
+     /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN
        /\ Cardinality(PV) >= THRESHOLD2 \* line 49
        /\ evidence' = PV \union {msg} \union evidence
-       /\ decision' = [decision EXCEPT ![p] = Decision(v, t, round[p])] \* update the decision, line 51
+       /\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* update the decision, line 51
     \* The original algorithm does not have 'DECIDED', but it increments the height.
     \* We introduced 'DECIDED' here to prevent the process from changing its decision.
        /\ endConsensus' = [endConsensus EXCEPT ![p] = localClock[p]]
        /\ step' = [step EXCEPT ![p] = "DECIDED"]
-       /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
-                     validRound, msgsPropose, msgsPrevote, msgsPrecommit,
-                     localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                     beginConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+       /\ UNCHANGED temporalVars
+       /\ UNCHANGED
+         <<round, (*step, decision,*) lockedValue, 
+         lockedRound, validValue, validRound>>
+       /\ UNCHANGED 
+         <<msgsPropose, msgsPrevote, msgsPrecommit,
+         (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+       /\ UNCHANGED
+         <<beginRound, (*endConsensus,*) lastBeginRound,
+         proposalTime, proposalReceivedTime>>
        /\ action' = "UponProposalInPrecommitNoDecision"
                                                           
 \* the actions below are not essential for safety, but added for completeness
@@ -596,10 +694,13 @@ OnTimeoutPropose(p) ==
   /\ p /= Proposer[round[p]]
   /\ BroadcastPrevote(p, round[p], NilProposal)
   /\ step' = [step EXCEPT ![p] = "PREVOTE"]
-  /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
-                validRound, decision, evidence, msgsPropose, msgsPrecommit,
-                localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+  /\ UNCHANGED <<temporalVars, invariantVars>>
+  /\ UNCHANGED
+    <<round, (*step,*) decision, lockedValue, 
+    lockedRound, validValue, validRound>>
+  /\ UNCHANGED 
+    <<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
+    evidence, receivedTimelyProposal, inspectedProposal>>
   /\ action' = "OnTimeoutPropose"
 
 \* lines 44-46
@@ -611,10 +712,13 @@ OnQuorumOfNilPrevotes(p) ==
     /\ evidence' = PV \union evidence
     /\ BroadcastPrecommit(p, round[p], Id(NilProposal))
     /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
-    /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
-                  validRound, decision, msgsPropose, msgsPrevote,
-                  localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision, lockedValue, 
+      lockedRound, validValue, validRound>>
+    /\ UNCHANGED 
+      <<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "OnQuorumOfNilPrevotes"
 
 \* lines 55-56
@@ -627,10 +731,16 @@ OnRoundCatchup(p) ==
         /\ Cardinality(Faster) >= THRESHOLD1
         /\ evidence' = MyEvidence \union evidence
         /\ StartRound(p, r)
-        /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
-                      validRound, msgsPropose, msgsPrevote, msgsPrecommit,
-                      localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                      beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+        /\ UNCHANGED temporalVars
+        /\ UNCHANGED
+          <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
+          proposalTime, proposalReceivedTime>>
+        /\ UNCHANGED
+          <<(*round, step,*) decision, lockedValue, 
+          lockedRound, validValue, validRound>>
+        /\ UNCHANGED 
+          <<msgsPropose, msgsPrevote, msgsPrecommit,
+          (*evidence,*) receivedTimelyProposal, inspectedProposal>>
         /\ action' = "OnRoundCatchup"
 
 
@@ -638,28 +748,24 @@ OnRoundCatchup(p) ==
 \* advance the global clock
 \* @type: Bool;
 AdvanceRealTime == 
-    /\ realTime < MaxTimestamp
-    /\ realTime' = realTime + 1
-    /\ \/ /\ ~ClockDrift
-          /\ localClock' = [p \in Corr |-> localClock[p] + 1]  
-       \/ /\ ClockDrift
-          /\ UNCHANGED localClock
-    /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
-                  validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-                  localClock, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>> 
+    /\ ValidTime(realTime)
+    /\ \E t \in Timestamps:
+      /\ t > realTime
+      /\ realTime' = t
+      /\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)]  
+    /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
     /\ action' = "AdvanceRealTime"
     
-\* advance the local clock of node p
-\* @type: (PROCESS) => Bool;
-AdvanceLocalClock(p) ==
-    /\ localClock[p] < MaxTimestamp
-    /\ localClock' = [localClock EXCEPT ![p] = @ + 1]
-    /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
-                  validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-                  realTime, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
-    /\ action' = "AdvanceLocalClock"
+\* advance the local clock of node p to some larger time t, not necessarily by 1
+\* #type: (PROCESS) => Bool;
+\* AdvanceLocalClock(p) ==
+\*     /\ ValidTime(localClock[p])
+\*     /\ \E t \in Timestamps:
+\*       /\ t > localClock[p] 
+\*       /\ localClock' = [localClock EXCEPT ![p] = t]
+\*     /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
+\*     /\ UNCHANGED realTime
+\*     /\ action' = "AdvanceLocalClock"
 
 \* process timely messages
 \* @type: (PROCESS) => Bool;
@@ -684,10 +790,8 @@ MessageProcessing(p) ==
  * A system transition. In this specificatiom, the system may eventually deadlock,
  * e.g., when all processes decide. This is expected behavior, as we focus on safety.
  *)
-Next ==
+Next == 
   \/ AdvanceRealTime
-  \/ /\ ClockDrift
-     /\ \E p \in Corr: AdvanceLocalClock(p)
   \/ /\ SynchronizedLocalClocks
      /\ \E p \in Corr: MessageProcessing(p)
 
@@ -700,59 +804,62 @@ AgreementOnValue ==
     \A p, q \in Corr:
         /\ decision[p] /= NilDecision
         /\ decision[q] /= NilDecision
-        => \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds : 
-            /\ decision[p] = Decision(v, t1, r1)
-            /\ decision[q] = Decision(v, t2, r2)
-
-\* [PBTS-INV-TIME-AGR.0]
-AgreementOnTime ==
-    \A p, q \in Corr: 
-        \A v1 \in ValidValues, v2 \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r \in Rounds :
-            /\ decision[p] = Decision(v1, t1, r)
-            /\ decision[q] = Decision(v2, t2, r)
-            => t1 = t2
+        => \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds : 
+            LET prop == Proposal(v,t,pr)
+            IN
+            /\ decision[p] = Decision(prop, r1)
+            /\ decision[q] = Decision(prop, r2)
 
 \* [PBTS-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
-    \A p \in Corr, t \in Timestamps : 
+    \A p \in Corr: 
     \* if a process decides on v and t
-    (\E v \in ValidValues, r \in Rounds : decision[p] = Decision(v, t, r))
+      \E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
+        decision[p] = Decision(Proposal(v,t,pr), dr)
         \* then 
-        => /\ beginConsensus - Precision <= t 
-           /\ t < endConsensus[p] + Precision + Delay
+        \* TODO: consider tighter bound where beginRound[pr] is replaced
+        \* w/ MedianOfRound[pr]
+        => (/\ beginRound[pr] - Precision - Delay <= t 
+            /\ t <= endConsensus[p] + Precision)
 
 \* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
 ConsensusSafeValidCorrProp ==
-    \A v \in ValidValues, t \in Timestamps :
-        \* if the proposer in the first round is correct
-       (/\ Proposer[0] \in Corr
-        \* and there exists a process that decided on v, t 
-        /\ \E p \in Corr, r \in Rounds : decision[p] = Decision(v, t, r))
-            \* then t is between the minimal and maximal initial local time
-            => /\ beginConsensus <= t 
-               /\ t <= lastBeginConsensus
+    \A v \in ValidValues:
+      \* and there exists a process that decided on v, t 
+      /\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
+        \* if the proposer in the round is correct
+        (/\ Proposer[pr] \in Corr
+        /\ decision[p] = Decision(Proposal(v,t,pr), dr))
+          \* then t is between the minimal and maximal initial local time
+          => /\ beginRound[pr] <= t 
+             /\ t <= lastBeginRound[pr]
 
 \* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
 ConsensusRealTimeValidCorr ==
-    \A t \in Timestamps, r \in Rounds :
-       (/\ \E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r) 
-        /\ proposalTime[r] /= NilTimestamp)
-        => /\ proposalTime[r] - Accuracy < t
-           /\ t < proposalTime[r] + Accuracy
+  \A r \in Rounds :
+    \E p \in Corr, v \in ValidValues, t \in Timestamps, pr \in Rounds: 
+     (/\ decision[p] = Decision(Proposal(v,t,pr), r) 
+      /\ proposalTime[r] /= NilTimestamp)
+        => (/\ proposalTime[r] - Precision <= t
+            /\ t <= proposalTime[r] + Precision)
 
 \* [PBTS-CONSENSUS-REALTIME-VALID.0]
 ConsensusRealTimeValid ==
     \A t \in Timestamps, r \in Rounds :
-       (\E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r)) 
-        => /\ proposalReceivedTime[r] - Accuracy - Precision < t
-           /\ t < proposalReceivedTime[r] + Accuracy + Precision + Delay
+       (\E p \in Corr, v \in ValidValues, pr \in Rounds : 
+        decision[p] = Decision(Proposal(v,t,pr), r)) 
+        => /\ proposalReceivedTime[r] - Precision < t
+           /\ t < proposalReceivedTime[r] + Precision + Delay
+
+DecideAfterMin == TRUE
+  \* if decide => time > min
 
 \* [PBTS-MSG-FAIR.0]
 BoundedDelay ==
     \A r \in Rounds : 
         (/\ proposalTime[r] /= NilTimestamp
          /\ proposalTime[r] + Delay < realTime)
-            => inspectedProposal[r] = Corr
+            => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
 
 \* [PBTS-CONSENSUS-TIME-LIVE.0]
 ConsensusTimeLive ==
@@ -761,19 +868,18 @@ ConsensusTimeLive ==
         /\ proposalTime[r] + Delay < realTime 
         /\ Proposer[r] \in Corr
         /\ round[p] <= r)
-            => \E msg \in RoundProposals(r) : <<p, msg>> \in receivedTimelyProposal
+            => \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p]
 
 \* a conjunction of all invariants
 Inv ==
     /\ AgreementOnValue 
-    /\ AgreementOnTime
     /\ ConsensusTimeValid
     /\ ConsensusSafeValidCorrProp
-    /\ ConsensusRealTimeValid
-    /\ ConsensusRealTimeValidCorr
-    /\ BoundedDelay
+    \* /\ ConsensusRealTimeValid
+    \* /\ ConsensusRealTimeValidCorr
+    \* /\ BoundedDelay
 
-Liveness ==
-    ConsensusTimeLive    
+\* Liveness ==
+\*     ConsensusTimeLive    
 
 =============================================================================    

spec/consensus/proposer-based-timestamp/tla/typedefs.tla

@@ -7,9 +7,8 @@
   @typeAlias: ACTION = Str;
   @typeAlias: TRACE = Seq(Str);
   @typeAlias: TIME = Int;
-  @typeAlias: PROPOSAL = <<VALUE, TIME>>;
-  @typeAlias: DECISION = <<VALUE, TIME, ROUND>>;
-  @typeAlias: RCVPROP = <<PROCESS, PROPMESSAGE>>;
+  @typeAlias: PROPOSAL = <<VALUE, TIME, ROUND>>;
+  @typeAlias: DECISION = <<PROPOSAL, ROUND>>;
   @typeAlias: PROPMESSAGE = 
   [
     type: STEP,