[PVerifier] exception handling for PVerifier-specific tokens (#906)

* [tweak] exception handling for PVerifier-specific tokens

* save

* fix Raft pproj config

---------

Co-authored-by: Ankush Desai <[email protected]>

Author: AD1024

Src/PCompiler/CompilerCore/Compiler.cs

@@ -34,6 +34,12 @@ public int Compile(ICompilerConfiguration job)
                 Environment.ExitCode = 1;
                 return Environment.ExitCode;
             }
+            catch (NotSupportedException e)
+            {
+                job.Output.WriteError("[NotSupportedError:]\n" + e.Message);
+                Environment.ExitCode = 1;
+                return Environment.ExitCode;
+            }
 
             job.Output.WriteInfo("Type checking ...");
             // Run type checker and produce AST
@@ -163,7 +169,7 @@ private static PParser.ProgramContext Parse(ICompilerConfiguration job, FileInfo
                         case PParser.INIT:
                         case PParser.PURE:
                             throw new NotSupportedException(
-                                $"line {token.Line}:{token.Column} \"{token.Text}\" only supported by PVerifier backend.");
+                                $"{inputFile.FullName} (line {token.Line}:{token.Column}): \"{token.Text}\" keyword is only supported by PVerifier backend.");
                     }
                 }
 

Tutorial/5_Paxos/PSpec/common.p

@@ -1,52 +1,52 @@
 // Unreliably send event `e` with payload `p` to every `target`
-fun UnreliableBroadcast(targets: set[machine], e: event, payload: any) {
+fun UnreliableBroadcast(target_machines: set[machine], e: event, payload: any) {
 	var i: int;
-	while (i < sizeof(targets)) {
+	while (i < sizeof(target_machines)) {
 		if (choose()) {
-			send targets[i], e, payload;
+			send target_machines[i], e, payload;
 		}
 		i = i + 1;
 	}
 }
 
 // Unreliably send event `e` with payload `p` to every `target`, potentially multiple times
-fun UnreliableBroadcastMulti(targets: set[machine], e: event, payload: any) {
+fun UnreliableBroadcastMulti(target_machines: set[machine], e: event, payload: any) {
 	var i: int;
 	var n: int;
 	var k: int;
 
-	while (i < sizeof(targets)) {
+	while (i < sizeof(target_machines)) {
 		// Each message is sent `k` is that number of times 
 		k = choose(3);
 		// Times we've sent the packet so far
 		n = 0;
 		while (n < k) {		
-			send targets[i], e, payload;
+			send target_machines[i], e, payload;
 			n = n + 1;
 		}
 		i = i + 1;
 	}
 }
 
 // Reliably send event `e` with payload `p` to every `target`
-fun ReliableBroadcast(targets: set[machine], e: event, payload: any) {
+fun ReliableBroadcast(target_machines: set[machine], e: event, payload: any) {
 	var i: int;
-	while (i < sizeof(targets)) {
-		send targets[i], e, payload;
+	while (i < sizeof(target_machines)) {
+		send target_machines[i], e, payload;
 		i = i + 1;
 	}
 }
 
 // Reliably send event `e` with payload `p` to a majority of `target`. Unreliable send to remaining, potentially multiple times.
-fun ReliableBroadcastMajority(targets: set[machine], e: event, payload: any) {
+fun ReliableBroadcastMajority(target_machines: set[machine], e: event, payload: any) {
 	var i: int;
 	var n: int;
 	var k: int;
 	var majority: int;
 
-	majority = sizeof(targets) / 2 + 1;
+	majority = sizeof(target_machines) / 2 + 1;
 
-	while (i < sizeof(targets)) {
+	while (i < sizeof(target_machines)) {
 		// Each message is sent `k` is that number of times 
 		k = 1;
 		if (i >= majority) {
@@ -55,7 +55,7 @@ fun ReliableBroadcastMajority(targets: set[machine], e: event, payload: any) {
 		// Times we've sent the packet so far
 		n = 0;
 		while (n < k) {		
-			send targets[i], e, payload;
+			send target_machines[i], e, payload;
 			n = n + 1;
 		}
 		i = i + 1;

Tutorial/6_Raft/Raft.pproj

@@ -6,5 +6,5 @@
 	<PFile>./PTst/</PFile>
 </InputFiles>
 <OutputDir>./PGenerated/</OutputDir>
-<Target>CSharp</Target>
+<Target>PChecker</Target>
 </Project>