Undo trigger removals

utwente-fmt · Jul 4, 2023 · 3384680 · 3384680
1 parent a9678a5
commit 3384680
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/examples/publications/2020/permutations/evenPhase.pvl b/examples/publications/2020/permutations/evenPhase.pvl
@@ -297,17 +297,17 @@ class EvenPhase {
 		invariant inv(Perm(isSorted[0], write) ** Perm(inp_seq_cur, 1) ** input.length == |inp_seq_cur|
         		    ** contrib.length == input.length ** Perm(loopCounter[0], write) ** Perm(inp_seq_all, 1)
         		    ** (loopCounter[0] >= 0 && |inp_seq_all| == loopCounter[0] + 1)
-        		    ** (\forall int i; 0 <= i && i < loopCounter[0]+1; input.length == |inp_seq_all[i]|)
+        		    ** (\forall int i; 0 <= i && i < loopCounter[0]+1; input.length == |{: inp_seq_all[i] :}|)
         		    ** (\forall* int i; 0 <= i && i < contrib.length; Perm({: contrib[i] :}, 1\2))
         		    ** (\forall* int i; 0 <= i && i < input.length; Perm( {:input[i] :}, write))
         		    ** (\forall int i; 0 <= i && i < input.length; input[i] == inp_seq_cur[i])
         		    ** isApermutation(inp_seq_all[0], inp_seq_cur)
         		    ** ((\forall int i; 0 <= i && i < contrib.length/2 && 2*i < contrib.length; contrib[2*i] == 0)
-        		    ==> (\forall int j; j >= 0 && j < |inp_seq_cur|; inp_seq_all[loopCounter[0]][j] == inp_seq_cur[j]))
+        		    ==> (\forall int j; j >= 0 && j < |inp_seq_cur|; {: inp_seq_all[loopCounter[0]][j] :} == {: inp_seq_cur[j] :} ))
 
         		    ** ((\forall int i; 0 <= i && i < |inp_seq_all[loopCounter[0]]|/2 && 2*i < |inp_seq_all[loopCounter[0]]| - 1;
          	 	    inp_seq_all[loopCounter[0]][2*i] <= inp_seq_all[loopCounter[0]][2*i+1])
-         	 	 	==> (\forall int i; 0 <= i && i < |inp_seq_all[loopCounter[0]]|; inp_seq_cur[i] == inp_seq_all[loopCounter[0]][i]))
+         	 	 	==> (\forall int i; 0 <= i && i < |inp_seq_all[loopCounter[0]]|; {: inp_seq_cur[i] :} == inp_seq_all[loopCounter[0]][i]))
 
          	 	 	** (\forall int i; 0 <= i && i < input.length/2 && 2*i+1 < input.length && (contrib[2*i] == 1); input[2*i] <= input[2*i+1])
          	 	 	** (\forall int i; 0 <= i && i < |inp_seq_all[loopCounter[0]]|/2 && 2*i+1 < |inp_seq_all[loopCounter[0]]|;
@@ -324,7 +324,7 @@ class EvenPhase {
         	 		** ((\exists int i; 0 <= i && i < |inp_seq_all[loopCounter[0]]|/2 && 2*i+1 < |inp_seq_all[loopCounter[0]]|;
         			inp_seq_all[loopCounter[0]][2*i] > inp_seq_all[loopCounter[0]][2*i+1] && contrib[2*i] == 1) ==> !isSorted[0])
         			** ((isSorted[0] && (\forall int i; 0 <= i && i < contrib.length/2 && 2*i < contrib.length; contrib[2*i] == 1))
-        			==> (\forall int j; j >= 0 && j < |inp_seq_cur|; inp_seq_all[loopCounter[0]][j] == inp_seq_cur[j])))
+        			==> (\forall int j; j >= 0 && j < |inp_seq_cur|; {: inp_seq_all[loopCounter[0]][j] :} == {: inp_seq_cur[j] :})))
         		{
 			par even(int tid=0..((input.length)/2))
 			requires tid*2 < contrib.length ==> Perm(contrib[tid*2], 1\2);