Merge pull request #672 from utwente-fmt/veymont-check-test-cases

Veymont fix bugs and test cases
utwente-fmt · Jul 23, 2021 · 6627bd1 · 6627bd1
2 parents 23678b2 + f37a126
commit 6627bd1
Show file tree

Hide file tree

Showing 63 changed files with 160 additions and 154 deletions.
diff --git a/examples/veymont-check/checkLTS/ltstest.pvl b/examples/veymont-check/checkLTS/ltstest.pvl
@@ -1,6 +1,6 @@
-// -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases LTSMethodCallTest
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 
 class Role {

diff --git a/examples/veymont-check/checkLTS/simpleifelse.pvl b/examples/veymont-check/checkLTS/simpleifelse.pvl
@@ -1,7 +1,6 @@
-// -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases SimpleIfElse
-//:: suite session-generate
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 
 class Role {
@@ -39,10 +38,11 @@ class Main {
 	requires a.x == 0 && b.x == 8 && c.x == 4;
 	ensures a.x == b.x && b.x == c.x; 
 	void run() {
-
+		assert (a.left != a.x) == (b.left != b.x) && (b.left != b.x) == (c.left != c.x);
 		if(a.left != a.x && b.left != b.x && c.left != c.x) {
 			a.x = a.x + 1;
 		}
+		assert (a.left != 2) == (b.left != 3) && (b.left != 3) == (c.left != 4);
 		if(a.left != 2 && b.left != 3 && c.left != 4) {
 			b.x = 5;
 		} else {

diff --git a/examples/veymont-check/checkLTS/simplemethodcall.pvl b/examples/veymont-check/checkLTS/simplemethodcall.pvl
@@ -1,7 +1,6 @@
-// -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases SimpleMethodCall
-//:: suite session-generate
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 
 class Role {

diff --git a/examples/veymont-check/checkLTS/simplewhile.pvl b/examples/veymont-check/checkLTS/simplewhile.pvl
@@ -1,7 +1,6 @@
-// -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases SimpleWhile
-//:: suite session-generate
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 
 class Role {
@@ -45,6 +44,7 @@ class Main {
 		loop_invariant Perm(a.left, 1) ** Perm(b.left, 1) ** Perm(c.left, 1);
 		loop_invariant b.x - c.x == c.x - a.x;
 		loop_invariant b.left == a.x && c.left == b.x && a.left == c.x;
+		loop_invariant (a.left != a.x) == (b.left != b.x) && (b.left != b.x) == (c.left != c.x);
 		while(a.left != a.x && b.left != b.x && c.left != c.x) {
 				a.x = a.x + 1;
 		}

diff --git a/examples/veymont-check/checkMainClass/MainConstructorArg.pvl b/examples/veymont-check/checkMainClass/MainConstructorArg.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorArg
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/NoMain.pvl b/examples/veymont-check/checkMainClass/NoMain.pvl
@@ -1,6 +1,6 @@
 //:: cases NoMain
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class SomeClass {
 

diff --git a/examples/veymont-check/checkMainClass/NoMainConstructor.pvl b/examples/veymont-check/checkMainClass/NoMainConstructor.pvl
@@ -1,11 +1,11 @@
 //:: cases NoMainConstructor
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 
 
 	void run() {
-	
+
 	}
 }
diff --git a/examples/veymont-check/checkMainClass/NoMainMethod.pvl b/examples/veymont-check/checkMainClass/NoMainMethod.pvl
@@ -1,6 +1,6 @@
 //:: cases MainMethod
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/NoMainMethod2.pvl b/examples/veymont-check/checkMainClass/NoMainMethod2.pvl
@@ -1,6 +1,6 @@
 //:: cases MainMethod2
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/NoRunArg.pvl b/examples/veymont-check/checkMainClass/NoRunArg.pvl
@@ -1,6 +1,6 @@
 //:: cases NoRunArg
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/NoRunMethod.pvl b/examples/veymont-check/checkMainClass/NoRunMethod.pvl
@@ -1,6 +1,6 @@
 //:: cases NoRunMethod
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl b/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl
@@ -1,6 +1,6 @@
 //:: cases OtherMainConstructor
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl b/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl
@@ -1,6 +1,6 @@
 //:: cases TwoMainConstructors
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainClass/WrongRunType.pvl b/examples/veymont-check/checkMainClass/WrongRunType.pvl
@@ -1,6 +1,6 @@
 //:: cases WrongRunType
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorAssignmenWrongType
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorAssignNoRole
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorBlock
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorNonRoleAssignment
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorNonRoleAssignment2
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorNonRoleAssignment3
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorNonRoleAssignment4
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl
@@ -1,6 +1,6 @@
 //:: cases MainConstructorWrongRoleNr
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl
@@ -1,6 +1,6 @@
 //:: cases ConstructorCall
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl
@@ -1,6 +1,6 @@
 //:: cases ConstructorCall2
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl
@@ -1,6 +1,6 @@
 //:: cases ForLoop
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl
@@ -1,6 +1,6 @@
 //:: cases GuardedRecursion
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl
@@ -1,6 +1,6 @@
 //:: cases GuardedRecursion2
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl
@@ -1,6 +1,6 @@
 //:: cases IfCondition
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl
@@ -1,6 +1,6 @@
 //:: cases MainMethodCall
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl
@@ -1,6 +1,6 @@
 //:: cases NewNonRoleObject
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl
@@ -1,7 +1,7 @@
 //:: cases NewRoleObject
-//:: suite session-check
-//:: tools session
-//:: verdict Pass
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
+//:: verdict Error
 class Main {
 
 	Role a,b;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl
@@ -1,6 +1,6 @@
 //:: cases NonRoleMethodCall
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl
@@ -1,6 +1,6 @@
 //:: cases PureMethodCall
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl
@@ -1,6 +1,6 @@
 //:: cases RoleFieldAssignment
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 	Role a;

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl
@@ -1,6 +1,6 @@
 //:: cases WaitStatement
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl
@@ -1,6 +1,6 @@
 //:: cases WhileCondition
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl
@@ -1,6 +1,6 @@
 //:: cases WrongAssignment
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl
@@ -1,6 +1,6 @@
 //:: cases WrongAssignment2
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl
@@ -1,6 +1,6 @@
 //:: cases WrongSyntax
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Error
 class Main {
 

diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl
@@ -1,6 +1,6 @@
 //:: cases AbsenceRecursion
-//:: suite session-check
-//:: tools session
+//:: suite veymont veymont-check
+//:: option --veymont tmp.pvl
 //:: verdict Pass
 class Main {