#414 account for Igor's naming suggestions

informalsystems · Sep 24, 2020 · 6ab98d3 · 6ab98d3
1 parent 1f02ef0
commit 6ab98d3
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/docs/spec/lightclient/verification/Lightclient_A_1.tla b/docs/spec/lightclient/verification/Lightclient_A_1.tla
@@ -32,20 +32,20 @@ VARIABLES
 (* the variables of the lite client *)
 lcvars == <<state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified>>
 
-(* the variables used by the light client in the previous state *)
+(* the light client previous state components, used for monitoring *)
 VARIABLES
   prevVerified,
   prevCurrent,
   prevNow,
   prevVerdict
 
-InitHistory(verified, current, now, verdict) ==
+InitMonitor(verified, current, now, verdict) ==
   /\ prevVerified = verified
   /\ prevCurrent = current
   /\ prevNow = now
   /\ prevVerdict = verdict
 
-NextHistory(verified, current, now, verdict) ==
+NextMonitor(verified, current, now, verdict) ==
   /\ prevVerified' = verified
   /\ prevCurrent' = current
   /\ prevNow' = now