diff --git a/CryptoAnalysis/src/main/resources/CostumClasses/Requires.crysl b/CryptoAnalysis/src/main/resources/CostumClasses/Requires.crysl
deleted file mode 100644
index 705583ab1..000000000
--- a/CryptoAnalysis/src/main/resources/CostumClasses/Requires.crysl
+++ /dev/null
@@ -1,213 +0,0 @@
-SPEC main.prefined.Requires
-
-OBJECTS	
-	// SIMPLE
-	main.prefined.A p1inS1;
-	main.prefined.A p1inS2;
-	// AND
-	main.prefined.A p1inA1;
-	main.prefined.A p2inA1;
-	main.prefined.A p1inA2;
-	main.prefined.A p2inA2;
-	main.prefined.A p1inA3;
-	main.prefined.A p2inA3;
-	main.prefined.A p1inA4;
-	main.prefined.A p2inA4;
-	main.prefined.A p1inA5;
-	main.prefined.A p2inA5;
-	main.prefined.A p1inA6;
-	main.prefined.A p2inA6;
-	main.prefined.A p1inA7;
-	main.prefined.A p2inA7;
-	main.prefined.A p1inA8;
-	main.prefined.A p2inA8;
-	// OR
-	main.prefined.A p1inO1;
-	main.prefined.A p2inO1;
-	main.prefined.A p1inO2;
-	main.prefined.A p2inO2;
-	main.prefined.A p1inO3;
-	main.prefined.A p2inO3;
-	main.prefined.A p1inO4;
-	main.prefined.A p2inO4;
-	main.prefined.A p1inO5;
-	main.prefined.A p2inO5;
-	main.prefined.A p1inO6;
-	main.prefined.A p2inO6;
-	main.prefined.A p1inO7;
-	main.prefined.A p2inO7;
-	main.prefined.A p1inO8;
-	main.prefined.A p2inO8;
-		// 3 cases same predicate
-	main.prefined.A p1inO9;
-	main.prefined.A p2inO9;
-	main.prefined.A p3inO9;
-	main.prefined.A p1inO10;
-	main.prefined.A p2inO10;
-	main.prefined.A p3inO10;
-	main.prefined.A p1inO11;
-	main.prefined.A p2inO11;
-	main.prefined.A p3inO11;
-	main.prefined.A p1inO12;
-	main.prefined.A p2inO12;
-	main.prefined.A p3inO12;
-	main.prefined.A p1inO13;
-	main.prefined.A p2inO13;
-	main.prefined.A p3inO13;
-	main.prefined.A p1inO14;
-	main.prefined.A p2inO14;
-	main.prefined.A p3inO14;
-	main.prefined.A p1inO15;
-	main.prefined.A p2inO15;
-	main.prefined.A p3inO15;
-	main.prefined.A p1inO16;
-	main.prefined.A p2inO16;
-	main.prefined.A p3inO16;
-	// IMPLICATE
-	main.prefined.A p1inI1;
-	main.prefined.A p2inI1;
-	main.prefined.A p1inI2;
-	main.prefined.A p2inI2;
-	main.prefined.A p1inI3;
-	main.prefined.A p2inI3;
-	main.prefined.A p1inI4;
-	main.prefined.A p2inI4;
-	main.prefined.A p1inI5;
-	main.prefined.A p2inI5;
-	main.prefined.A p1inI6;
-	main.prefined.A p2inI6;
-	main.prefined.A p1inI7;
-	main.prefined.A p2inI7;
-	main.prefined.A p1inI8;
-	main.prefined.A p2inI8;
-	
-
-	
-EVENTS
-	cons : Requires();
-	Cons := cons;
-	
-	// SIMPLE
-	
-	s1: pred1onP1(p1inS1);
-	s2: notPred1onP1(p1inS2);
-	S := s1 | s2;
-	
-	// AND
-	
-	// same predicate
-	a1: pred1onP1_AND_pred1onP2(p1inA1, p2inA1);
-	a2: pred1onP1_AND_notPred1onP2(p1inA2, p2inA2);
-	a3: notPred1onP1_AND_pred1onP2(p1inA3, p2inA3);
-	a4: notPred1onP1_AND_notPred1onP2(p1inA4, p2inA4);
-
-	// multi predicates
-	a5: pred1onP1_AND_pred2onP2(p1inA5, p2inA5);
-	a6: pred1onP1_AND_notPred2onP2(p1inA6, p2inA6);
-	a7: notPred1onP1_AND_pred2onP2(p1inA7, p2inA7);
-	a8: notPred1onP1_AND_notPred2onP2(p1inA8, p2inA8);
-	
-	A:= a1 | a2 | a3 | a4 | a5 | a6 | a7 | a8;
-	
-	// OR
-	
-	// same predicate
-	o1: pred1onP1_OR_pred1onP2(p1inO1, p2inO1);
-	o2: pred1onP1_OR_notPred1onP2(p1inO2, p2inO2);
-	o3: notPred1onP1_OR_pred1onP2(p1inO3, p2inO3);
-	o4: notPred1onP1_OR_notPred1onP2(p1inO4, p2inO4);
-	
-	// multi predicates
-	o5: pred1onP1_OR_pred2onP2(p1inO5, p2inO5);
-	o6: pred1onP1_OR_notPred2onP2(p1inO6, p2inO6);
-	o7: notPred1onP1_OR_pred2onP2(p1inO7, p2inO7);
-	o8: notPred1onP1_OR_notPred2onP2(p1inO8, p2inO8);
-	
-	// 3 cases same predicate
-	o9: pred1onP1_OR_pred1onP2_OR_pred1onP3(p1inO9, p2inO9, p3inO9);
-	o10: pred1onP1_OR_notPred1onP2_OR_pred1onP3(p1inO10, p2inO10, p3inO10);
-	o11: notPred1onP1_OR_pred1onP2_OR_pred1onP3(p1inO11, p2inO11, p3inO11);
-	o12: notPred1onP1_OR_notPred1onP2_OR_pred1onP3(p1inO12, p2inO12, p3inO12);
-	o13: pred1onP1_OR_pred1onP2_OR_notPred1onP3(p1inO13, p2inO13, p3inO13);
-	o14: pred1onP1_OR_notPred1onP2_OR_notPred1onP3(p1inO14, p2inO14, p3inO14);
-	o15: notPred1onP1_OR_pred1onP2_OR_notPred1onP3(p1inO15, p2inO15, p3inO15);
-	o16: notPred1onP1_OR_notPred1onP2_OR_notPred1onP3(p1inO16, p2inO16, p3inO16);
-	
-	O:= o1 | o2 | o3 | o4 | o5 | o6 | o7 | o8 | o9 | o10 | o11 | o12 | o13 | o14 | o15 | o16;
-	
-	// IMPLICATE
-	
-	// same predicate
-	i1: pred1onP1_IMPL_pred1onP2(p1inI1, p2inI1);
-	i2: pred1onP1_IMPL_notPred1onP2(p1inI2, p2inI2);
-	i3: notPred1onP1_IMPL_pred1onP2(p1inI3, p2inI3);
-	i4: notPred1onP1_IMPL_notPred1onP2(p1inI4, p2inI4);
-	
-	// multi predicates
-	i5: pred1onP1_IMPL_pred2onP2(p1inI5, p2inI5);
-	i6: pred1onP1_IMPL_notPred2onP2(p1inI6, p2inI6);
-	i7: notPred1onP1_IMPL_pred2onP2(p1inI7, p2inI7);
-	i8: notPred1onP1_IMPL_notPred2onP2(p1inI8, p2inI8);
-	
-	I:= i1 | i2 | i3 | i4 | i5 | i6 | i7 | i8;
-	
-	All:= S | A | O | I;
-	
-ORDER
-	Cons, All
-	
-REQUIRES
-	// SIMPLE
-	pred1[p1inS1];
-	!pred1[p1inS2];
-	
-	// AND
-	pred1[p1inA1];
-	pred1[p2inA1];
-	pred1[p1inA2];
-	!pred1[p2inA2];
-	!pred1[p1inA3];
-	pred1[p2inA3];
-	!pred1[p1inA4];
-	!pred1[p2inA4];
-	pred1[p1inA5];
-	pred2[p2inA5];
-	pred1[p1inA6];
-	!pred2[p2inA6];
-	!pred1[p1inA7];
-	pred2[p2inA7];
-	!pred1[p1inA8];
-	!pred2[p2inA8];
-	
-	//OR
-	pred1[p1inO1] || pred1[p2inO1];
-	pred1[p1inO2] || !pred1[p2inO2];
-	!pred1[p1inO3] || pred1[p2inO3];
-	!pred1[p1inO4] || !pred1[p2inO4];
-	pred1[p1inO5] || pred2[p2inO5];
-	pred1[p1inO6] || !pred2[p2inO6];
-	!pred1[p1inO7] || pred2[p2inO7];
-	!pred1[p1inO8] || !pred2[p2inO8];
-	
-	// 3 cases same predicate
-	pred1[p1inO9] || pred1[p2inO9] || pred1[p3inO9];
-	pred1[p1inO10] || !pred1[p2inO10] || pred1[p3inO10];
-	!pred1[p1inO11] || pred1[p2inO11] || pred1[p3inO11];
-	!pred1[p1inO12] || !pred1[p2inO12] || pred1[p3inO12];
-	pred1[p1inO13] || pred1[p2inO13] || !pred1[p3inO13];
-	pred1[p1inO14] || !pred1[p2inO14] || !pred1[p3inO14];
-	!pred1[p1inO15] || pred1[p2inO15] || !pred1[p3inO15];
-	!pred1[p1inO16] || !pred1[p2inO16] || !pred1[p3inO16];
-	
-	// IMPLICATE
-	// same predicate
-	pred1[p1inI1] => pred1[p2inI1];
-	pred1[p1inI2] => !pred1[p2inI2];
-	// multi predicates
-	pred1[p1inI5] => pred2[p2inI5];
-	pred1[p1inI6] => !pred2[p2inI6];
-	
-ENSURES
-	requiredPredicateWasEnsured[this];
-
-	
\ No newline at end of file
diff --git a/CryptoAnalysis/src/main/resources/CostumClasses/A.crysl b/CryptoAnalysis/src/main/resources/CustomRules/A.crysl
similarity index 85%
rename from CryptoAnalysis/src/main/resources/CostumClasses/A.crysl
rename to CryptoAnalysis/src/main/resources/CustomRules/A.crysl
index 55e83fb0b..6ad59572c 100644
--- a/CryptoAnalysis/src/main/resources/CostumClasses/A.crysl
+++ b/CryptoAnalysis/src/main/resources/CustomRules/A.crysl
@@ -1,11 +1,11 @@
-SPEC main.prefined.A
+SPEC tests.customrules.customclass.A
 
 OBJECTS
 	byte[] attr1;
 	byte[] attr2;
 	byte[] attr3;
-	main.prefined.B b;
-	main.prefined.C c;
+	tests.customrules.customclass.B b;
+	tests.customrules.customclass.C c;
 	
 EVENTS
 	cons : A();
@@ -15,8 +15,8 @@ EVENTS
 	ens2 : b = ensurePred2OnReturnB();
 	ens3 : c = ensurePred1OnReturnC();
 	ens4 : c = ensurePred2OnReturnC();
-	ens5 : ensurePred1OnThis();
-	ens6 : ensurePred2OnThis();
+	ens5 : ensurePred1onThis();
+	ens6 : ensurePred2onThis();
 	ens7 : ensurePred1OnAttr1();
 	ens8 : ensurePred2OnAttr1();
 	ens9 : ensurePred1OnAttr2();
diff --git a/CryptoAnalysis/src/main/resources/CostumClasses/B.crysl b/CryptoAnalysis/src/main/resources/CustomRules/B.crysl
similarity index 89%
rename from CryptoAnalysis/src/main/resources/CostumClasses/B.crysl
rename to CryptoAnalysis/src/main/resources/CustomRules/B.crysl
index a6a451e30..664d2ca9a 100644
--- a/CryptoAnalysis/src/main/resources/CostumClasses/B.crysl
+++ b/CryptoAnalysis/src/main/resources/CustomRules/B.crysl
@@ -1,11 +1,11 @@
-SPEC main.prefined.B
+SPEC tests.customrules.customclass.B
 
 OBJECTS
 	byte[] attr1;
 	byte[] attr2;
 	byte[] attr3;
-	main.prefined.A a;
-	main.prefined.C c;
+	tests.customrules.customclass.A a;
+	tests.customrules.customclass.C c;
 	
 EVENTS
 	cons : B();
diff --git a/CryptoAnalysis/src/main/resources/CostumClasses/C.crysl b/CryptoAnalysis/src/main/resources/CustomRules/C.crysl
similarity index 89%
rename from CryptoAnalysis/src/main/resources/CostumClasses/C.crysl
rename to CryptoAnalysis/src/main/resources/CustomRules/C.crysl
index abb0a468b..a58be3e39 100644
--- a/CryptoAnalysis/src/main/resources/CostumClasses/C.crysl
+++ b/CryptoAnalysis/src/main/resources/CustomRules/C.crysl
@@ -1,11 +1,11 @@
-SPEC main.prefined.A
+SPEC tests.customrules.customclass.C
 
 OBJECTS
 	byte[] attr1;
 	byte[] attr2;
 	byte[] attr3;
-	main.prefined.B b;
-	main.prefined.A a;
+	tests.customrules.customclass.B b;
+	tests.customrules.customclass.A a;
 	
 EVENTS
 	cons : C();
diff --git a/CryptoAnalysis/src/main/resources/CustomRules/Requires.crysl b/CryptoAnalysis/src/main/resources/CustomRules/Requires.crysl
new file mode 100644
index 000000000..a937d051c
--- /dev/null
+++ b/CryptoAnalysis/src/main/resources/CustomRules/Requires.crysl
@@ -0,0 +1,224 @@
+SPEC tests.customrules.customclass.Requires
+
+OBJECTS	
+	// SIMPLE
+	tests.customrules.customclass.A p1inS1;
+	tests.customrules.customclass.A p1inS2;
+	// AND
+	tests.customrules.customclass.A p1inA1;
+	tests.customrules.customclass.A p2inA1;
+	tests.customrules.customclass.A p1inA2;
+	tests.customrules.customclass.A p2inA2;
+	tests.customrules.customclass.A p1inA3;
+	tests.customrules.customclass.A p2inA3;
+	tests.customrules.customclass.A p1inA4;
+	tests.customrules.customclass.A p2inA4;
+	tests.customrules.customclass.A p1inA5;
+	tests.customrules.customclass.A p2inA5;
+	tests.customrules.customclass.A p1inA6;
+	tests.customrules.customclass.A p2inA6;
+	tests.customrules.customclass.A p1inA7;
+	tests.customrules.customclass.A p2inA7;
+	tests.customrules.customclass.A p1inA8;
+	tests.customrules.customclass.A p2inA8;
+	// OR
+	tests.customrules.customclass.A p1inO1;
+	tests.customrules.customclass.A p2inO1;
+	tests.customrules.customclass.A p1inO2;
+	tests.customrules.customclass.A p2inO2;
+	tests.customrules.customclass.A p1inO3;
+	tests.customrules.customclass.A p2inO3;
+	tests.customrules.customclass.A p1inO4;
+	tests.customrules.customclass.A p2inO4;
+	tests.customrules.customclass.A p1inO5;
+	tests.customrules.customclass.A p2inO5;
+	tests.customrules.customclass.A p1inO6;
+	tests.customrules.customclass.A p2inO6;
+	tests.customrules.customclass.A p1inO7;
+	tests.customrules.customclass.A p2inO7;
+	tests.customrules.customclass.A p1inO8;
+	tests.customrules.customclass.A p2inO8;
+		// 3 cases same predicate
+	tests.customrules.customclass.A p1inO9;
+	tests.customrules.customclass.A p2inO9;
+	tests.customrules.customclass.A p3inO9;
+	tests.customrules.customclass.A p1inO10;
+	tests.customrules.customclass.A p2inO10;
+	tests.customrules.customclass.A p3inO10;
+	tests.customrules.customclass.A p1inO11;
+	tests.customrules.customclass.A p2inO11;
+	tests.customrules.customclass.A p3inO11;
+	tests.customrules.customclass.A p1inO12;
+	tests.customrules.customclass.A p2inO12;
+	tests.customrules.customclass.A p3inO12;
+	tests.customrules.customclass.A p1inO13;
+	tests.customrules.customclass.A p2inO13;
+	tests.customrules.customclass.A p3inO13;
+	tests.customrules.customclass.A p1inO14;
+	tests.customrules.customclass.A p2inO14;
+	tests.customrules.customclass.A p3inO14;
+	tests.customrules.customclass.A p1inO15;
+	tests.customrules.customclass.A p2inO15;
+	tests.customrules.customclass.A p3inO15;
+	tests.customrules.customclass.A p1inO16;
+	tests.customrules.customclass.A p2inO16;
+	tests.customrules.customclass.A p3inO16;
+	// IMPLICATE
+	tests.customrules.customclass.A p1inI1;
+	tests.customrules.customclass.A p2inI1;
+	tests.customrules.customclass.A p1inI2;
+	tests.customrules.customclass.A p2inI2;
+	tests.customrules.customclass.A p1inI3;
+	tests.customrules.customclass.A p2inI3;
+	tests.customrules.customclass.A p1inI4;
+	tests.customrules.customclass.A p2inI4;
+	tests.customrules.customclass.A p1inI5;
+	tests.customrules.customclass.A p2inI5;
+	tests.customrules.customclass.A p1inI6;
+	tests.customrules.customclass.A p2inI6;
+	tests.customrules.customclass.A p1inI7;
+	tests.customrules.customclass.A p2inI7;
+	tests.customrules.customclass.A p1inI8;
+	tests.customrules.customclass.A p2inI8;
+	tests.customrules.customclass.A p1inI9;
+	tests.customrules.customclass.A p2inI9;
+	tests.customrules.customclass.A p1inI10;
+	tests.customrules.customclass.A p2inI10;
+
+	
+EVENTS
+	cons : Requires();
+	Cons := cons;
+	
+	// SIMPLE
+	
+	s1: pred1onPos1(p1inS1);
+	s2: notPred1onPos1(p1inS2);
+	S := s1 | s2;
+	
+	// AND
+	
+	// same predicate
+	a1: pred1onPos1_AND_pred1onPos2(p1inA1, p2inA1);
+	a2: pred1onPos1_AND_notPred1onPos2(p1inA2, p2inA2);
+	a3: notPred1onPos1_AND_pred1onPos2(p1inA3, p2inA3);
+	a4: notPred1onPos1_AND_notPred1onPos2(p1inA4, p2inA4);
+
+	// multi predicates
+	a5: pred1onPos1_AND_pred2onPos2(p1inA5, p2inA5);
+	a6: pred1onPos1_AND_notPred2onPos2(p1inA6, p2inA6);
+	a7: notPred1onPos1_AND_pred2onPos2(p1inA7, p2inA7);
+	a8: notPred1onPos1_AND_notPred2onPos2(p1inA8, p2inA8);
+	
+	A:= a1 | a2 | a3 | a4 | a5 | a6 | a7 | a8;
+	
+	// OR
+	
+	// same predicate
+	o1: pred1onPos1_OR_pred1onPos2(p1inO1, p2inO1);
+	o2: pred1onPos1_OR_notPred1onPos2(p1inO2, p2inO2);
+	o3: notPred1onPos1_OR_pred1onPos2(p1inO3, p2inO3);
+	o4: notPred1onPos1_OR_notPred1onPos2(p1inO4, p2inO4);
+	
+	// multi predicates
+	o5: pred1onPos1_OR_pred2onPos2(p1inO5, p2inO5);
+	o6: pred1onPos1_OR_notPred2onPos2(p1inO6, p2inO6);
+	o7: notPred1onPos1_OR_pred2onPos2(p1inO7, p2inO7);
+	o8: notPred1onPos1_OR_notPred2onPos2(p1inO8, p2inO8);
+	
+	// 3 cases same predicate
+	o9: pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(p1inO9, p2inO9, p3inO9);
+	o10: pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(p1inO10, p2inO10, p3inO10);
+	o11: notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(p1inO11, p2inO11, p3inO11);
+	o12: notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(p1inO12, p2inO12, p3inO12);
+	o13: pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(p1inO13, p2inO13, p3inO13);
+	o14: pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(p1inO14, p2inO14, p3inO14);
+	o15: notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(p1inO15, p2inO15, p3inO15);
+	o16: notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(p1inO16, p2inO16, p3inO16);
+	
+	O:= o1 | o2 | o3 | o4 | o5 | o6 | o7 | o8 | o9 | o10 | o11 | o12 | o13 | o14 | o15 | o16;
+	
+	// IMPLICATE
+	
+	// same predicate
+	i1: pred1onPos1_IMPL_pred1onPos2(p1inI1, p2inI1);
+	i2: pred1onPos1_IMPL_notPred1onPos2(p1inI2, p2inI2);
+	i3: notPred1onPos1_IMPL_pred1onPos2(p1inI3, p2inI3);
+	i4: notPred1onPos1_IMPL_notPred1onPos2(p1inI4, p2inI4);
+	
+	// multi predicates
+	i5: pred1onPos1_IMPL_pred2onPos2(p1inI5, p2inI5);
+	i6: pred1onPos1_IMPL_notPred2onPos2(p1inI6, p2inI6);
+	i7: notPred1onPos1_IMPL_pred2onPos2(p1inI7, p2inI7);
+	i8: notPred1onPos1_IMPL_notPred2onPos2(p1inI8, p2inI8);
+
+	// OR with IMPLICATE
+	i9: pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2(p1inI9, p2inI9);
+	i10: pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2(p1inI10, p2inI10);
+	
+	I:= i1 | i2 | i3 | i4 | i5 | i6 | i7 | i8 | i9 | i10;
+	
+	All:= S | A | O | I;
+	
+ORDER
+	Cons, All
+	
+REQUIRES
+	// SIMPLE
+	pred1[p1inS1];
+	!pred1[p1inS2];
+	
+	// AND
+	pred1[p1inA1];
+	pred1[p2inA1];
+	pred1[p1inA2];
+	!pred1[p2inA2];
+	!pred1[p1inA3];
+	pred1[p2inA3];
+	!pred1[p1inA4];
+	!pred1[p2inA4];
+	pred1[p1inA5];
+	pred2[p2inA5];
+	pred1[p1inA6];
+	!pred2[p2inA6];
+	!pred1[p1inA7];
+	pred2[p2inA7];
+	!pred1[p1inA8];
+	!pred2[p2inA8];
+	
+	//OR
+	pred1[p1inO1] || pred1[p2inO1];
+	pred1[p1inO2] || !pred1[p2inO2];
+	!pred1[p1inO3] || pred1[p2inO3];
+	!pred1[p1inO4] || !pred1[p2inO4];
+	pred1[p1inO5] || pred2[p2inO5];
+	pred1[p1inO6] || !pred2[p2inO6];
+	!pred1[p1inO7] || pred2[p2inO7];
+	!pred1[p1inO8] || !pred2[p2inO8];
+	
+	// 3 cases same predicate
+	pred1[p1inO9] || pred1[p2inO9] || pred1[p3inO9];
+	pred1[p1inO10] || !pred1[p2inO10] || pred1[p3inO10];
+	!pred1[p1inO11] || pred1[p2inO11] || pred1[p3inO11];
+	!pred1[p1inO12] || !pred1[p2inO12] || pred1[p3inO12];
+	pred1[p1inO13] || pred1[p2inO13] || !pred1[p3inO13];
+	pred1[p1inO14] || !pred1[p2inO14] || !pred1[p3inO14];
+	!pred1[p1inO15] || pred1[p2inO15] || !pred1[p3inO15];
+	!pred1[p1inO16] || !pred1[p2inO16] || !pred1[p3inO16];
+	
+	// IMPLICATE
+	// same predicate
+	pred1[p1inI1] => pred1[p2inI1];
+	pred1[p1inI2] => !pred1[p2inI2];
+	// multi predicates
+	pred1[p1inI5] => pred2[p2inI5];
+	pred1[p1inI6] => !pred2[p2inI6];
+
+	// OR and IMPLICATE
+	pred1[p1inI9] || pred2[p2inI9] => pred1[p1inI9];
+	pred2[p2inI9] => pred1[p1inI10] || pred2[p2inI10];
+	
+ENSURES
+	requiredPredicateWasEnsured[this];
+
+	
\ No newline at end of file
diff --git a/CryptoAnalysis/src/test/java/test/assertions/PredicateErrorCountAssertion.java b/CryptoAnalysis/src/test/java/test/assertions/PredicateErrorCountAssertion.java
index 9589b0dd1..d25b642bb 100644
--- a/CryptoAnalysis/src/test/java/test/assertions/PredicateErrorCountAssertion.java
+++ b/CryptoAnalysis/src/test/java/test/assertions/PredicateErrorCountAssertion.java
@@ -25,4 +25,9 @@ public boolean isImprecise() {
 		return expectedErrorCounts != actualErrorCounts;
 	}
 
+	@Override
+	public String toString() {
+		return "Expected " + expectedErrorCounts + " predicate errors, but got " + actualErrorCounts;
+	}
+
 }
diff --git a/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java b/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java
new file mode 100644
index 000000000..b0e7e166a
--- /dev/null
+++ b/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTest.java
@@ -0,0 +1,1301 @@
+package tests.customrules;
+
+import crypto.analysis.CrySLRulesetSelector.Ruleset;
+import org.junit.Ignore;
+import org.junit.Test;
+
+import test.UsagePatternTestingFramework;
+import test.assertions.Assertions;
+import tests.customrules.customclass.A;
+import tests.customrules.customclass.Requires;
+
+public class RequiredPredicatesTest extends UsagePatternTestingFramework {
+
+	@Override
+	protected Ruleset getRuleSet() {
+		return Ruleset.CustomRules;
+	}
+	
+	//
+	// OBJECTS OF SAME CLASS AS PARAMS
+	//
+	
+	// SIMPLE
+	
+	@Test
+	public void pred1OnPos1() {
+		A pred1OnA = new A();
+		pred1OnA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1OnA);
+
+		A noPred1OnA = new A();
+		Assertions.notHasEnsuredPredicate(noPred1OnA);
+
+		Requires r1 = new Requires();
+		r1.pred1onPos1(pred1OnA);
+		Assertions.hasEnsuredPredicate(r1);
+		
+		Requires r2 = new Requires();
+		r2.pred1onPos1(noPred1OnA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Assertions.predicateErrors(1);
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1() {
+		A pred1OnA = new A();
+		pred1OnA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1OnA);
+
+		A noPred1OnA = new A();
+		Assertions.notHasEnsuredPredicate(noPred1OnA);
+
+		Requires r1 = new Requires();
+		r1.notPred1onPos1(noPred1OnA);
+		Assertions.hasEnsuredPredicate(r1);
+		
+		Requires r2 = new Requires();
+		r2.notPred1onPos1(pred1OnA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Assertions.predicateErrors(1);
+	}
+	
+	// AND
+	
+	// same predicate
+	@Ignore
+	@Test
+	public void pred1onPos1_AND_pred1onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPred1onA = new A();
+		Assertions.notHasEnsuredPredicate(noPred1onA);
+
+		Requires r1 = new Requires();
+		r1.pred1onPos1_AND_pred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+		
+		Requires r2 = new Requires();
+		r2.pred1onPos1_AND_pred1onPos2(pred1onA, noPred1onA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_AND_pred1onPos2(noPred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_AND_pred1onPos2(noPred1onA, noPred1onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+
+	@Ignore
+	@Test
+	public void pred1onPos1_AND_notPred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		Requires r1 = new Requires();
+		r1.pred1onPos1_AND_notPred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+		
+		Requires r2 = new Requires();
+		r2.pred1onPos1_AND_notPred1onPos2(noPredOnA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r2);
+		
+		Requires r3 = new Requires();
+		r3.pred1onPos1_AND_notPred1onPos2(pred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r3);
+		
+		Requires r4 = new Requires();
+		r4.pred1onPos1_AND_notPred1onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_AND_pred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_AND_pred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+		
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_AND_pred1onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r2);
+		
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_AND_pred1onPos2(pred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r3);
+		
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_AND_pred1onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_AND_notPred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_AND_notPred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+		
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_AND_notPred1onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r2);
+		
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_AND_notPred1onPos2(pred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r3);
+		
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_AND_notPred1onPos2(noPredOnA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(3);
+	}
+
+	// multi predicates
+	@Test
+	public void pred1onPos1_AND_pred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		Requires r1 = new Requires();
+		r1.pred1onPos1_AND_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_AND_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_AND_pred2onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_AND_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+
+	@Ignore
+	@Test
+	public void pred1onPos1_AND_notPred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		Requires r1 = new Requires();
+		r1.pred1onPos1_AND_notPred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_AND_notPred2onPos2(noPredOnA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_AND_notPred2onPos2(pred1onA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_AND_notPred2onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_AND_pred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_AND_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_AND_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_AND_pred2onPos2(pred1onA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_AND_pred2onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_AND_notPred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_AND_notPred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_AND_notPred2onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_AND_notPred2onPos2(pred1onA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_AND_notPred2onPos2(noPredOnA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(4);
+	}
+	
+	// OR
+	
+	// same predicate
+	@Test
+	public void pred1onPos1_OR_pred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		//assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_pred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_pred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_pred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_pred1onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	@Ignore	// Nullpointer
+	@Test
+	public void pred1onPos1_OR_notPred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_notPred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_notPred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_notPred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_notPred1onPos2(noPredOnA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	@Ignore		// Nullpointer
+	@Test
+	public void notPred1onPos1_OR_pred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_pred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_pred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_pred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_pred1onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_OR_notPred1onPos2(){
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred1onA2 = new A();
+		pred1onA2.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA2);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_notPred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_notPred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_notPred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_notPred1onPos2(pred1onA, pred1onA2);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	// multi predicates
+	@Test
+	public void pred1onPos1_OR_pred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_pred2onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	@Ignore
+	@Test
+	public void pred1onP1_OR_notPred2onP2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_notPred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_notPred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_notPred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_notPred2onPos2(noPredOnA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onP1_OR_pred2onP2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_pred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onP1_OR_notPred2onP2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_notPred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_notPred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_notPred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_notPred2onPos2(pred1onA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(2); // two, because each parameter will be reported
+	}
+	
+	// 3 cases same predicate
+	
+	@Test
+	public void pred1onPos1_OR_pred1onPos2_OR_pred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+		Requires r5 = new Requires();
+		r5.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+
+		Requires r7 = new Requires();
+		r7.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore		// NullPointerException
+	@Test
+	public void pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Requires r5 = new Requires();
+		r5.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+
+		Requires r7 = new Requires();
+		r7.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore		// Nullpointer
+	@Test
+	public void notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Requires r5 = new Requires();
+		r5.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+
+		Requires r7 = new Requires();
+		r7.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore		// Nullpointer
+	@Test
+	public void notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Requires r5 = new Requires();
+		r5.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+
+		Requires r7 = new Requires();
+		r7.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore		// Nullpointer
+	@Test
+	public void pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Requires r5 = new Requires();
+		r5.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+		Requires r7 = new Requires();
+		r7.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r8);
+		
+		Assertions.hasEnsuredPredicate(pred1onA);
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore		// Nullpointer
+	@Test
+	public void pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Requires r5 = new Requires();
+		r5.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+
+		Requires r7 = new Requires();
+		r7.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore 	// Nullpointer
+	@Test
+	public void notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+		Requires r5 = new Requires();
+		r5.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+		Requires r7 = new Requires();
+		r7.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Requires r5 = new Requires();
+		r5.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r5);
+
+		Requires r6 = new Requires();
+		r6.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r6);
+
+		Requires r7 = new Requires();
+		r7.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(noPredOnA, noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r7);
+		
+		// assert false
+		Requires r8 = new Requires();
+		r8.notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(pred1onA, pred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r8);
+
+		Assertions.predicateErrors(3); // three, because each parameter will be reported
+	}
+	
+	// IMPLICATE
+	
+	// same predicate
+	@Ignore
+	@Test
+	public void pred1onPos1_IMPL_pred1onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_IMPL_pred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_IMPL_pred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_IMPL_pred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+		
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_IMPL_pred1onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void pred1onPos1_IMPL_notPred1onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_IMPL_notPred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_IMPL_notPred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_IMPL_notPred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+		
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_IMPL_notPred1onPos2(pred1onA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_IMPL_pred1onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_IMPL_pred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_IMPL_pred1onPos2(noPredOnA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_IMPL_pred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_IMPL_pred1onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onPos1_IMPL_notPred1onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_IMPL_notPred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_IMPL_notPred1onPos2(pred1onA, pred1onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_IMPL_notPred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_IMPL_notPred1onPos2(noPredOnA, pred1onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+	
+	// multi predicates
+	@Ignore
+	@Test
+	public void pred1onPos1_IMPL_pred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_IMPL_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_IMPL_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_IMPL_pred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+		
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_IMPL_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void pred1onP1_IMPL_notPred2onP2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_IMPL_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_IMPL_notPred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_IMPL_notPred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_IMPL_notPred2onPos2(pred1onA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onP1_IMPL_pred2onP2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_IMPL_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_IMPL_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_IMPL_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_IMPL_pred2onPos2(noPredOnA, noPredOnA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void notPred1onP1_IMPL_notPred2onP2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+
+		// assert true
+		Requires r1 = new Requires();
+		r1.notPred1onPos1_IMPL_notPred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.notPred1onPos1_IMPL_notPred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.notPred1onPos1_IMPL_notPred2onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.notPred1onPos1_IMPL_notPred2onPos2(noPredOnA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+	
+	// OR WITH IMPLICATION
+	// same predicate
+	@Ignore
+	@Test
+	public void pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2(noPredOnA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+		
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2(noPredOnA, pred2onA);
+		Assertions.notHasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+
+	@Ignore
+	@Test
+	public void pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2() {
+		A pred1onA = new A();
+		pred1onA.ensurePred1onThis();
+		Assertions.hasEnsuredPredicate(pred1onA);
+
+		A pred2onA = new A();
+		pred2onA.ensurePred2onThis();
+		Assertions.hasEnsuredPredicate(pred2onA);
+
+		A noPredOnA = new A();
+		Assertions.notHasEnsuredPredicate(noPredOnA);
+		
+		// assert true
+		Requires r1 = new Requires();
+		r1.pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2(pred1onA, pred2onA);
+		Assertions.hasEnsuredPredicate(r1);
+
+		Requires r2 = new Requires();
+		r2.pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r2);
+
+		Requires r3 = new Requires();
+		r3.pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2(pred1onA, noPredOnA);
+		Assertions.hasEnsuredPredicate(r3);
+
+		// assert false
+		Requires r4 = new Requires();
+		r4.pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2(noPredOnA, pred2onA);
+		Assertions.hasEnsuredPredicate(r4);
+
+		Assertions.predicateErrors(1); // only the missing will be reported
+	}
+}
diff --git a/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTests.java b/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTests.java
deleted file mode 100644
index 1a716c48d..000000000
--- a/CryptoAnalysis/src/test/java/tests/customrules/RequiredPredicatesTests.java
+++ /dev/null
@@ -1,1009 +0,0 @@
-package tests.customerules;
-
-import java.io.File;
-import java.net.URI;
-import java.util.ArrayList;
-import java.util.List;
-
-import org.junit.Assert;
-import org.junit.Before;
-import org.junit.Test;
-
-import com.google.inject.internal.util.Lists;
-
-import crypto.HeadlessCryptoScanner;
-import crypto.analysis.CrySLRulesetSelector.Ruleset;
-import crypto.analysis.errors.IncompleteOperationError;
-import crypto.cryslhandler.CrySLModelReaderClassPath;
-import main.prefined.A;
-import main.prefined.B;
-import main.prefined.Requires;
-import test.UsagePatternTestingFramework;
-import test.assertions.Assertions;
-import test.core.selfrunning.ImprecisionException;
-import tests.headless.AbstractHeadlessTest;
-import tests.headless.MavenProject;
-
-public class RequiredPredicatesTests extends UsagePatternTestingFramworkForCustomRules {
-	
-	
-	//
-	// OBJECTS OF SAME CLASS AS PARAMS
-	//
-	
-	// SIMPLE
-	
-	@Test
-	public void pred1onP1() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r; 
-		r = new Requires();
-		r.pred1onP1(pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1(noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1);
-	}
-	
-	@Test
-	public void notPred1onP1(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r; 
-		r = new Requires();
-		r.pred1onP1(noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1(pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1);
-	}
-	
-	// AND
-	
-	// same predicate
-	@Test
-	public void pred1onP1_AND_pred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(noPredOnA, pred1onA);
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(pred1onA, noPredOnA);
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	@Test
-	public void pred1onP1_AND_notPred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_AND_notPred1onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1_AND_notPred1onP2(noPredOnA, pred1onA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_notPred1onP2(pred1onA, pred1onA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_notPred1onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	@Test
-	public void notPred1onP1_AND_pred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(pred1onA, noPredOnA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(pred1onA, pred1onA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	@Test
-	public void notPred1onP1_AND_notPred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(pred1onA, noPredOnA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(pred1onA, pred1onA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred1onP2(noPredOnA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-
-	// multi predicates
-	@Test
-	public void pred1onP1_AND_pred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_AND_pred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred2onP2(pred1onA, noPredOnA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred2onP2(noPredOnA, noPredOnA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_pred2onP2(noPredOnA, pred2onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	@Test
-	public void pred1onP1_AND_notPred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_AND_notPred2onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.pred1onP1_AND_notPred2onP2(noPredOnA, pred2onA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_notPred2onP2(pred1onA, pred2onA);
-		
-		r = new Requires();
-		r.pred1onP1_AND_notPred2onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	@Test
-	public void notPred1onP1_AND_pred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_AND_pred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.notPred1onP1_AND_pred2onP2(pred1onA, noPredOnA);
-		
-		r = new Requires();
-		r.notPred1onP1_AND_pred2onP2(pred1onA, pred2onA);
-		
-		r = new Requires();
-		r.notPred1onP1_AND_pred2onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	@Test
-	public void notPred1onP1_AND_notPred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_AND_notPred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		r = new Requires();
-		r.notPred1onP1_AND_notPred2onP2(pred1onA, noPredOnA);
-		r = new Requires();
-		r.notPred1onP1_AND_notPred2onP2(pred1onA, pred2onA);
-		r = new Requires();
-		r.notPred1onP1_AND_notPred2onP2(noPredOnA, pred2onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(4);
-	}
-	
-	// OR
-	
-	// same predicate
-	@Test
-	public void pred1onP1_OR_pred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		//assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-		
-	@Test
-	public void pred1onP1_OR_notPred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2(noPredOnA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-		
-	@Test
-	public void notPred1onP1_OR_pred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		Requires r;
-		// assert true
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2(pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-		
-	@Test
-	public void notPred1onP1_OR_notPred1onP2(){
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred1onA2 = new A();
-		pred1onA2.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2(pred1onA, pred1onA2);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-
-	// multi predicates
-	@Test
-	public void pred1onP1_OR_pred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_pred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred2onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_pred2onP2(noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-		
-	@Test
-	public void pred1onP1_OR_notPred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_notPred2onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_notPred2onP2(noPredOnA, pred2onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-		
-	@Test
-	public void notPred1onP1_OR_pred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_pred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_pred2onP2(pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-		
-	@Test
-	public void notPred1onP1_OR_notPred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_notPred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred2onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_notPred2onP2(pred1onA, pred2onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(2); // two, because each parameter will be reported
-	}
-	
-	// 3 cases same predicate
-	
-	@Test
-	public void pred1onP1_OR_pred1onP2_OR_pred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void pred1onP1_OR_notPred1onP2_OR_pred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void notPred1onP1_OR_pred1onP2_OR_pred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_pred1onP3(pred1onA, noPredOnA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void notPred1onP1_OR_notPred1onP2_OR_pred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_notPred1onP2_OR_pred1onP3(pred1onA, pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void pred1onP1_OR_pred1onP2_OR_notPred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void pred1onP1_OR_notPred1onP2_OR_notPred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_OR_notPred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void notPred1onP1_OR_pred1onP2_OR_notPred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	@Test
-	public void notPred1onP1_OR_notPred1onP2_OR_notPred1onP3() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(noPredOnA, noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.notPred1onP1_OR_pred1onP2_OR_notPred1onP3(pred1onA, pred1onA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(3); // two, because each parameter will be reported
-	}
-	
-	// IMPLICATE
-	
-	// same predicate
-	@Test
-	public void pred1onP1_IMPL_pred1onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2(pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1); // only the missing will be reported
-	}
-	
-	@Test
-	public void pred1onP1_IMPL_notPred1onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred1onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred1onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred1onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred1onP2(pred1onA, pred1onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1); // only the missing will be reported
-	}
-	
-	// multi predicates
-	@Test
-	public void pred1onP1_IMPL_pred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_IMPL_pred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_IMPL_pred2onP2(pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1); // only the missing will be reported
-	}
-	
-	@Test
-	public void pred1onP1_IMPL_notPred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_IMPL_pred2onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert false
-		r = new Requires();
-		r.pred1onP1_IMPL_notPred2onP2(pred1onA, pred2onA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1); // only the missing will be reported
-	}
-	
-	// OR WITH IMPLICATION
-	// same predicate
-	@Test
-	public void pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_pred2onP2() {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_pred2onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_pred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_pred2onP2(noPredOnA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		
-		// assert false
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_pred2onP2(pred1onA, noPredOnA);
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(1); // only the missing will be reported
-	}
-	public void pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(A p1, A p2) {
-		A pred1onA = new A();
-		pred1onA.ensurePred1OnThis();
-		A pred2onA = new A();
-		pred2onA.ensurePred2OnThis();
-		A noPredOnA = new A();
-		
-		// assert true
-		Requires r;
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(pred1onA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(noPredOnA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(pred1onA, pred2onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(pred1onA, noPredOnA);
-		Assertions.hasEnsuredPredicate(r);
-		r = new Requires();
-		r.pred1onP1_IMPL_pred1onP2_OR_notPred1onP1_IMPL_pred2onP2(noPredOnA, pred1onA);
-		Assertions.hasEnsuredPredicate(r);
-		// assert nothing false, because one condition is always not satisfied
-		
-		Assertions.hasEnsuredPredicate(pred1onA);
-		Assertions.hasEnsuredPredicate(pred2onA);
-		Assertions.notHasEnsuredPredicate(noPredOnA);
-		Assertions.predicateErrors(0); // only the missing will be reported
-	}
-		
-}
diff --git a/CryptoAnalysis/src/test/java/tests/customrules/customclass/A.java b/CryptoAnalysis/src/test/java/tests/customrules/customclass/A.java
index d1585757f..6dfb3454e 100644
--- a/CryptoAnalysis/src/test/java/tests/customrules/customclass/A.java
+++ b/CryptoAnalysis/src/test/java/tests/customrules/customclass/A.java
@@ -1,7 +1,4 @@
-package main.prefined;
-
-import main.prefined.B;
-import main.prefined.C;
+package tests.customrules.customclass;
 
 public class A {
 	
@@ -25,11 +22,11 @@ public C ensurePred2OnReturnC() {
 		return new C();
 	}
 	
-	public void ensurePred1OnThis() {
+	public void ensurePred1onThis() {
 		return;
 	}
 	
-	public void ensurePred2OnThis() {
+	public void ensurePred2onThis() {
 		return;
 	}
 
diff --git a/CryptoAnalysis/src/test/java/tests/customrules/customclass/B.java b/CryptoAnalysis/src/test/java/tests/customrules/customclass/B.java
index f3c3e04f9..e79192045 100644
--- a/CryptoAnalysis/src/test/java/tests/customrules/customclass/B.java
+++ b/CryptoAnalysis/src/test/java/tests/customrules/customclass/B.java
@@ -1,7 +1,4 @@
-package main.prefined;
-
-import main.prefined.A;
-import main.prefined.C;
+package tests.customrules.customclass;
 
 public class B {
 	
diff --git a/CryptoAnalysis/src/test/java/tests/customrules/customclass/C.java b/CryptoAnalysis/src/test/java/tests/customrules/customclass/C.java
index b1a344336..3c4fa83bc 100644
--- a/CryptoAnalysis/src/test/java/tests/customrules/customclass/C.java
+++ b/CryptoAnalysis/src/test/java/tests/customrules/customclass/C.java
@@ -1,7 +1,4 @@
-package main.prefined;
-
-import main.prefined.A;
-import main.prefined.B;
+package tests.customrules.customclass;
 
 public class C {
 	
diff --git a/CryptoAnalysis/src/test/java/tests/customrules/customclass/Requires.java b/CryptoAnalysis/src/test/java/tests/customrules/customclass/Requires.java
index 0d8f9484d..ff366ede1 100644
--- a/CryptoAnalysis/src/test/java/tests/customrules/customclass/Requires.java
+++ b/CryptoAnalysis/src/test/java/tests/customrules/customclass/Requires.java
@@ -1,67 +1,66 @@
-package main.prefined;
+package tests.customrules.customclass;
 
-import main.prefined.A;
-import main.prefined.B;
-import main.prefined.C;
 
 public class Requires {
 	
 	// SIMPLE
 	
-	public void pred1onP1(A p1) {}
-	public void notPred1onP1(A p1) {}
+	public void pred1onPos1(A p1) {}
+	public void notPred1onPos1(A p1) {}
 	
 	// AND
 	
 	// same predicate
-	public void pred1onP1_AND_pred1onP2(A p1, A p2) {}
-	public void pred1onP1_AND_notPred1onP2(A p1, A p2) {}
-	public void notPred1onP1_AND_pred1onP2(A p1, A p2) {}
-	public void notPred1onP1_AND_notPred1onP2(A p1, A p2) {}
+	public void pred1onPos1_AND_pred1onPos2(A p1, A p2) {}
+	public void pred1onPos1_AND_notPred1onPos2(A p1, A p2) {}
+	public void notPred1onPos1_AND_pred1onPos2(A p1, A p2) {}
+	public void notPred1onPos1_AND_notPred1onPos2(A p1, A p2) {}
 	
 	// multi predicates
-	public void pred1onP1_AND_pred2onP2(A p1, A p2) {}
-	public void pred1onP1_AND_notPred2onP2(A p1, A p2) {}
-	public void notPred1onP1_AND_pred2onP2(A p1, A p2) {}
-	public void notPred1onP1_AND_notPred2onP2(A p1, A p2) {}
+	public void pred1onPos1_AND_pred2onPos2(A p1, A p2) {}
+	public void pred1onPos1_AND_notPred2onPos2(A p1, A p2) {}
+	public void notPred1onPos1_AND_pred2onPos2(A p1, A p2) {}
+	public void notPred1onPos1_AND_notPred2onPos2(A p1, A p2) {}
 	
 	// OR
 	
 	// same predicate
-	public void pred1onP1_OR_pred1onP2(A p1, A p2) {}
-	public void pred1onP1_OR_notPred1onP2(A p1, A p2) {}
-	public void notPred1onP1_OR_pred1onP2(A p1, A p2) {}
-	public void notPred1onP1_OR_notPred1onP2(A p1, A p2) {}
+	public void pred1onPos1_OR_pred1onPos2(A p1, A p2) {}
+	public void pred1onPos1_OR_notPred1onPos2(A p1, A p2) {}
+	public void notPred1onPos1_OR_pred1onPos2(A p1, A p2) {}
+	public void notPred1onPos1_OR_notPred1onPos2(A p1, A p2) {}
 	
 	// multi predicates
-	public void pred1onP1_OR_pred2onP2(A p1, A p2) {}
-	public void pred1onP1_OR_notPred2onP2(A p1, A p2) {}
-	public void notPred1onP1_OR_pred2onP2(A p1, A p2) {}
-	public void notPred1onP1_OR_notPred2onP2(A p1, A p2) {}
+	public void pred1onPos1_OR_pred2onPos2(A p1, A p2) {}
+	public void pred1onPos1_OR_notPred2onPos2(A p1, A p2) {}
+	public void notPred1onPos1_OR_pred2onPos2(A p1, A p2) {}
+	public void notPred1onPos1_OR_notPred2onPos2(A p1, A p2) {}
 	
 	// 3 cases same predicate
-	public void pred1onP1_OR_pred1onP2_OR_pred1onP3(A p1, A p2, A p3) {}
-	public void pred1onP1_OR_notPred1onP2_OR_pred1onP3(A p1, A p2, A p3) {}
-	public void notPred1onP1_OR_pred1onP2_OR_pred1onP3(A p1, A p2, A p3) {}
-	public void notPred1onP1_OR_notPred1onP2_OR_pred1onP3(A p1, A p2, A p3) {}
-	public void pred1onP1_OR_pred1onP2_OR_notPred1onP3(A p1, A p2, A p3) {}
-	public void pred1onP1_OR_notPred1onP2_OR_notPred1onP3(A p1, A p2, A p3) {}
-	public void notPred1onP1_OR_pred1onP2_OR_notPred1onP3(A p1, A p2, A p3) {}
-	public void notPred1onP1_OR_notPred1onP2_OR_notPred1onP3(A p1, A p2, A p3) {}
+	public void pred1onPos1_OR_pred1onPos2_OR_pred1onPos3(A p1, A p2, A p3) {}
+	public void pred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(A p1, A p2, A p3) {}
+	public void notPred1onPos1_OR_pred1onPos2_OR_pred1onPos3(A p1, A p2, A p3) {}
+	public void notPred1onPos1_OR_notPred1onPos2_OR_pred1onPos3(A p1, A p2, A p3) {}
+	public void pred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(A p1, A p2, A p3) {}
+	public void pred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(A p1, A p2, A p3) {}
+	public void notPred1onPos1_OR_pred1onPos2_OR_notPred1onPos3(A p1, A p2, A p3) {}
+	public void notPred1onPos1_OR_notPred1onPos2_OR_notPred1onPos3(A p1, A p2, A p3) {}
 	
 	// IMPLICATE
 	
 	// same predicate
-	public void pred1onP1_IMPL_pred1onP2(A p1, A p2) {}
-	public void pred1onP1_IMPL_notPred1onP2(A p1, A p2) {}
+	public void pred1onPos1_IMPL_pred1onPos2(A p1, A p2) {}
+	public void pred1onPos1_IMPL_notPred1onPos2(A p1, A p2) {}
+	public void notPred1onPos1_IMPL_pred1onPos2(A p1, A p2) {}
+	public void notPred1onPos1_IMPL_notPred1onPos2(A p1, A p2) {}
 	
 	// multi predicates
-	public void pred1onP1_IMPL_pred2onP2(A p1, A p2) {}
-	public void pred1onP1_IMPL_notPred2onP2(A p1, A p2) {}
+	public void pred1onPos1_IMPL_pred2onPos2(A p1, A p2) {}
+	public void pred1onPos1_IMPL_notPred2onPos2(A p1, A p2) {}
+	public void notPred1onPos1_IMPL_pred2onPos2(A p1, A p2) {}
+	public void notPred1onPos1_IMPL_notPred2onPos2(A p1, A p2) {}
 	
 	// OR WITH IMPLICATION
-	// same predicate
-	public void pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_pred2onP2(A p1, A p2) {}
-	public void pred1onP1_IMPL_pred1onP2_OR_pred1onP1_IMPL_!pred2onP2(A p1, A p2) {}
-	
+	public void pred1onPos1_OR_pred2onPos1_IMPL_pred1onPos2(A p1, A p2) {}
+	public void pred2onPos1_IMPL_pred1onPos2_OR_pred2onPos2(A p1, A p2) {}
 }
diff --git a/CustomClassesForSpecification/CustomClasses/pom.xml b/CustomClassesForSpecification/CustomClasses/pom.xml
deleted file mode 100644
index 48b029780..000000000
--- a/CustomClassesForSpecification/CustomClasses/pom.xml
+++ /dev/null
@@ -1,31 +0,0 @@
-<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
-  <modelVersion>4.0.0</modelVersion>
-  <groupId>de.tests</groupId>
-  <artifactId>CustomClasses</artifactId>
-  <version>0.0.1-SNAPSHOT</version>
-  <name>CustomClasses</name>
-	<build>
-		<plugins>
-			<plugin>
-				<artifactId>maven-compiler-plugin</artifactId>
-				<version>3.8.0</version>
-				<configuration>
-					<source>1.8</source>
-					<target>1.8</target>
-				</configuration>
-			</plugin>
-			<plugin>
-				<groupId>org.apache.maven.plugins</groupId>
-				<artifactId>maven-source-plugin</artifactId>
-				<executions>
-					<execution>
-						<id>attach-sources</id>
-						<goals>
-							<goal>jar</goal>
-						</goals>
-					</execution>
-				</executions>
-			</plugin>
-		</plugins>
-	</build>
-</project>
\ No newline at end of file