init keyword -> init-condition keyword

Docs/docs/tutorial/advanced/twophasecommitverification.md

@@ -148,14 +148,14 @@ We want our model to capture many different system configurations (e.g., number
 In our 2PC model, for example, we can state that, at initialization, there is a unique machine of type coordinator, and the `coordinator` function points to that machine; and every machine in the participants set is a machine of type participant.
 
 ```
-init forall (m: machine) :: m == coordinator() == m is Coordinator;
-init forall (m: machine) :: m in participants() == m is Participant;
+init-condition forall (m: machine) :: m == coordinator() == m is Coordinator;
+init-condition forall (m: machine) :: m in participants() == m is Participant;
 ```
 
 We can also state that all `yesVotes` tallies start empty.
 
 ```
-init forall (c: Coordinator) :: c.yesVotes == default(set[machine]);
+init-condition forall (c: Coordinator) :: c.yesVotes == default(set[machine]);
 ```
 
 When we write a proof of correctness later in this tutorial, we will be restricting the systems that we consider to those that satisfy the initialization conditions listed above.
@@ -164,7 +164,7 @@ When we write a proof of correctness later in this tutorial, we will be restrict
 
 Our initialization conditions contain two new P features: the `init` keyword, and quantified expressions (`forall` and `exists`). Even more interesting, one quantifier above is over a machine subtype (`coordinator`). 
 
-In P, the only way to dereference a machine variable inside of a specification (like the init conditions above) is by specifically quantifying over that machine type. In other words, `forall (c: Coordinator) :: c.yesVotes == default(set[machine])` is legal but `forall (c: machine) :: c.yesVotes == default(set[machine])` is not, even though they might appear to be similar. The reason for this is that selecting (using the `.` operator) on an incorrect subtype (e.g., trying to get `yesVotes` from a participant machine) is undefined. Undefined behavior in formal verification can lead to surprising results that can be really hard to debug, so in P we syntactically disallow this kind of undefined behavior altogether.
+In P, the only way to dereference a machine variable inside of a specification (like the `init-condition`s above) is by specifically quantifying over that machine type. In other words, `forall (c: Coordinator) :: c.yesVotes == default(set[machine])` is legal but `forall (c: machine) :: c.yesVotes == default(set[machine])` is not, even though they might appear to be similar. The reason for this is that selecting (using the `.` operator) on an incorrect subtype (e.g., trying to get `yesVotes` from a participant machine) is undefined. Undefined behavior in formal verification can lead to surprising results that can be really hard to debug, so in P we syntactically disallow this kind of undefined behavior altogether.
 
 ## P's Builtin Specifications And Our First Proof Attempt
 
@@ -375,7 +375,7 @@ In this tutorial, we formally verified a simplified 2PC protocol in P. The full,
 Our proof followed the running example of Zhang et al. but also included the verification of builtin P specifications. Along the way, we introduced the following new P keywords and concepts.
 
 1. `pure` functions;
-2. `init`ialization conditions;
+2. `init-condition` predicates;
 3. quantifiers;
 4. proofs by induction;
 5. `invariant`s;

Src/PCompiler/CompilerCore/Parser/PLexer.g4

@@ -64,6 +64,7 @@ WHILE     : 'while' ;
 WITH      : 'with' ;
 CHOOSE    : 'choose' ;
 
+// PVerifier keywords
 INVARIANT  : 'invariant';
 AXIOM      : 'axiom';
 IS         : 'is';
@@ -78,6 +79,9 @@ THEOREM    : 'Theorem';
 EXCEPT     : 'except';
 REQUIRES   : 'requires';
 ENSURES    : 'ensures';
+FORALL     : 'forall' ;
+EXISTS     : 'exists' ;
+INIT       : 'init-condition';
 
 // module-system-specific keywords
 
@@ -156,10 +160,6 @@ COMMA  : ',' ;
 DOT    : '.' ;
 COLON  : ':' ;
 
-FORALL  : 'forall' ;
-EXISTS  : 'exists' ;
-INIT    : 'init';
-
 // Identifiers
 
 Iden : PLetter PLetterOrDigit* ;

Tutorial/Advanced/1_ChainReplicationVerification/PSrc/System.p

@@ -98,15 +98,15 @@ pure tail(): machine;
 pure next_(m: machine): machine;
 
 // set all the fields to their default values
-init forall (p: Head) :: p.kv == default(map[int, int]);
-init forall (p: Body) :: p.kv == default(map[int, int]);
-init forall (p: Tail) :: p.kv == default(map[int, int]);
-init StrongConsistency.kv == default(map[int, int]);
+init-condition forall (p: Head) :: p.kv == default(map[int, int]);
+init-condition forall (p: Body) :: p.kv == default(map[int, int]);
+init-condition forall (p: Tail) :: p.kv == default(map[int, int]);
+init-condition StrongConsistency.kv == default(map[int, int]);
 
 // assume the pure functions match the state at the start
-init forall (m: machine) :: m == head() == m is Head;
-init forall (m: machine) :: m == tail() == m is Tail;
-init forall (m: machine) :: next_(m) is Body || next_(m) is Tail;
+init-condition forall (m: machine) :: m == head() == m is Head;
+init-condition forall (m: machine) :: m == tail() == m is Tail;
+init-condition forall (m: machine) :: next_(m) is Body || next_(m) is Tail;
 // ensure that the pure functions continue to match the state as time goes on
 invariant next_1: forall (m: machine) :: m == head() == m is Head;
 invariant next_2: forall (m: machine) :: m == tail() == m is Tail;

Tutorial/Advanced/2_TwoPhaseCommitVerification/KeyValue/PSrc/System.p

@@ -185,23 +185,23 @@ pure subset(small: set[rvPair], large: set[rvPair]) : bool = forall (rv: rvPair)
 axiom exists (x: machine) :: x in participants();
 
 // assumptions about how the system is setup and the pure functions above
-init coordinator() is Coordinator;
-init forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2;
-init forall (m: machine) :: m in participants() == m is Participant;
+init-condition coordinator() is Coordinator;
+init-condition forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2;
+init-condition forall (m: machine) :: m in participants() == m is Participant;
 
 // making sure that our assumptions about pure functions are not pulled out from underneath us
 invariant c_is_coordinator: coordinator() is Coordinator;
 invariant one_coordinator:  forall (c1: machine, c2: machine) :: (c1 is Coordinator && c2 is Coordinator) ==> c1 == c2;
 invariant participant_set:  forall (m: machine) :: m in participants() == m is Participant;
 
 // set all the fields to their default values
-init forall (c: Coordinator) :: c.yesVotes == default(map[krvTriple, set[machine]]);
-init forall (c: Coordinator) :: c.commited == default(set[krvTriple]);
-init forall (c: Coordinator) :: c.aborted == default(set[krvTriple]);
-init forall (p: Participant) :: p.commited == default(set[krvTriple]);
-init forall (p: Participant) :: p.aborted == default(set[krvTriple]);
-init forall (p: Participant) :: p.kv == default(map[tKey, set[rvPair]]);
-init Consistency.kv == default(map[tKey, set[rvPair]]);
+init-condition forall (c: Coordinator) :: c.yesVotes == default(map[krvTriple, set[machine]]);
+init-condition forall (c: Coordinator) :: c.commited == default(set[krvTriple]);
+init-condition forall (c: Coordinator) :: c.aborted == default(set[krvTriple]);
+init-condition forall (p: Participant) :: p.commited == default(set[krvTriple]);
+init-condition forall (p: Participant) :: p.aborted == default(set[krvTriple]);
+init-condition forall (p: Participant) :: p.kv == default(map[tKey, set[rvPair]]);
+init-condition Consistency.kv == default(map[tKey, set[rvPair]]);
 
 // make sure we never get a message that we're not expecting
 invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e;

Tutorial/Advanced/2_TwoPhaseCommitVerification/Rounds/PSrc/System.p

@@ -97,19 +97,19 @@ pure coordinator(): machine;
 pure preference(m: machine, r: Round) : Vote;
 
 // assumptions about how the system is setup and the pure functions above
-init forall (m: machine) :: m == coordinator() == m is Coordinator;
-init forall (m: machine) :: m in participants() == m is Participant;
+init-condition forall (m: machine) :: m == coordinator() == m is Coordinator;
+init-condition forall (m: machine) :: m in participants() == m is Participant;
 
 // making sure that our assumptions about pure functions are not pulled out from underneath us
 invariant one_coordinator: forall (m: machine) :: m == coordinator() == m is Coordinator;
 invariant participant_set: forall (m: machine) :: m in participants() == m is Participant;
 
 // set all the fields to their default values
-init forall (c: Coordinator) :: c.yesVotes == default(map[Round, set[machine]]);
-init forall (c: Coordinator) :: c.commited == default(set[Round]);
-init forall (c: Coordinator) :: c.aborted == default(set[Round]);
-init forall (p: Participant) :: p.commited == default(set[Round]);
-init forall (p: Participant) :: p.aborted == default(set[Round]);
+init-condition forall (c: Coordinator) :: c.yesVotes == default(map[Round, set[machine]]);
+init-condition forall (c: Coordinator) :: c.commited == default(set[Round]);
+init-condition forall (c: Coordinator) :: c.aborted == default(set[Round]);
+init-condition forall (p: Participant) :: p.commited == default(set[Round]);
+init-condition forall (p: Participant) :: p.aborted == default(set[Round]);
 
 // make sure we never get a message that we're not expecting
 invariant never_commit_to_coordinator: forall (e: event) :: e is eCommit && e targets coordinator() ==> !inflight e;

Tutorial/Advanced/2_TwoPhaseCommitVerification/Single/PSrc/System.p

@@ -82,11 +82,11 @@ pure coordinator(): machine;
 pure preference(m: machine) : bool;
 
 // assumptions about how the system is setup and the pure functions above
-init forall (m: machine) :: m == coordinator() == m is Coordinator;
-init forall (m: machine) :: m in participants() == m is Participant;
+init-condition forall (m: machine) :: m == coordinator() == m is Coordinator;
+init-condition forall (m: machine) :: m in participants() == m is Participant;
 
 // set all the fields to their default values
-init forall (c: Coordinator) :: c.yesVotes == default(set[machine]);
+init-condition forall (c: Coordinator) :: c.yesVotes == default(set[machine]);
 
 // making sure that our assumptions about pure functions are not pulled out from underneath us
 Lemma system_config {