Adding a property that should fail in the Wheel Brake System as a benchmark

java/ReachSafety-Java.set

@@ -2,5 +2,6 @@ jayhorn-recursive/*.yml
 jbmc-regression/*.yml
 jpf-regression/*.yml
 java-ranger-regression/*.yml
+java-ranger-regression/WBS/*.yml
 MinePump/*.yml
 algorithms/*.yml

java/java-ranger-regression/WBS/WBS_prop1.yml

@@ -0,0 +1,9 @@
+format_version: "1.0"
+input_files:
+  - ../../common/
+  - impl/
+  - prop1/
+properties:
+  - property_file: ../../properties/assert.prp
+    expected_verdict: false
+

java/java-ranger-regression/WBS/WBS_prop2.yml

@@ -0,0 +1,9 @@
+format_version: "1.0"
+input_files:
+  - ../../common/
+  - impl/
+  - prop2/
+properties:
+  - property_file: ../../properties/assert.prp
+    expected_verdict: true
+

java/java-ranger-regression/WBS/WBS_prop3.yml

@@ -0,0 +1,9 @@
+format_version: "1.0"
+input_files:
+  - ../../common/
+  - impl/
+  - prop3/
+properties:
+  - property_file: ../../properties/assert.prp
+    expected_verdict: false
+

java/java-ranger-regression/WBS/WBS_prop4.yml

@@ -0,0 +1,9 @@
+format_version: "1.0"
+input_files:
+  - ../../common/
+  - impl/
+  - prop4/
+properties:
+  - property_file: ../../properties/assert.prp
+    expected_verdict: false
+

java/java-ranger-regression/WBS_prop4/Main.java → java/java-ranger-regression/WBS/impl/WBS.java

@@ -1,17 +1,17 @@
 import org.sosy_lab.sv_benchmarks.Verifier;
-public class Main {
+public class WBS {
 
 	//Internal state
 	private int WBS_Node_WBS_BSCU_SystemModeSelCmd_rlt_PRE; 
 	private int WBS_Node_WBS_BSCU_rlt_PRE1; 
 	private int WBS_Node_WBS_rlt_PRE2;
 
 	//Outputs
-	private int Nor_Pressure;
-	private int Alt_Pressure;
-	private int Sys_Mode;
+	public int Nor_Pressure;
+	public int Alt_Pressure;
+	public int Sys_Mode;
 
-	public Main() {
+	public WBS() {
 		WBS_Node_WBS_BSCU_SystemModeSelCmd_rlt_PRE = 0;
 		WBS_Node_WBS_BSCU_rlt_PRE1 = 0;
 		WBS_Node_WBS_rlt_PRE2 = 100;
@@ -247,16 +247,5 @@ public void update(int PedalPos, boolean AutoBrake,
 
 	   WBS_Node_WBS_BSCU_SystemModeSelCmd_rlt_PRE = Sys_Mode;
 
-          // This assertion should fail:
-          assert((PedalPos > 0 && !Skid) ? (Alt_Pressure > 0 || Nor_Pressure > 0) : true);
 	}
-
-
-	public static void main(String[] args) {
-		Main Main = new Main();
-		for (int i = 0; i < 4; i++) {
-		  Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
-		}
-	}
-
 }

java/java-ranger-regression/WBS/prop1/Main.java

@@ -0,0 +1,18 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+public class Main {
+
+	public static void main(String[] args) {
+		WBS wbs= new WBS();
+		int PedalPos;
+		boolean AutoBrake, Skid;
+		for (int i = 0; i < 2; i++) {
+		  PedalPos = Verifier.nondetInt();
+		  AutoBrake = Verifier.nondetBoolean();
+		  Skid = Verifier.nondetBoolean();
+		  wbs.update(PedalPos, AutoBrake, Skid);
+		  // This assertion should fail:
+		  assert((PedalPos > 0 && PedalPos <= 4 && !Skid) ? (wbs.Alt_Pressure > 0) : true);
+		}
+	}
+
+}

java/java-ranger-regression/WBS/prop2/Main.java

@@ -0,0 +1,18 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+public class Main {
+
+	public static void main(String[] args) {
+		WBS wbs= new WBS();
+		int PedalPos;
+		boolean AutoBrake, Skid;
+		for (int i = 0; i < 2; i++) {
+		  PedalPos = Verifier.nondetInt();
+		  AutoBrake = Verifier.nondetBoolean();
+		  Skid = Verifier.nondetBoolean();
+		  wbs.update(PedalPos, AutoBrake, Skid);
+                  // This assertion should prove:
+                  assert((PedalPos > 0 && PedalPos <= 4 && !Skid) ? (wbs.Alt_Pressure > 0 || wbs.Nor_Pressure > 0) : true);
+		}
+	}
+
+}

java/java-ranger-regression/WBS/prop3/Main.java

@@ -0,0 +1,18 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+public class Main {
+
+	public static void main(String[] args) {
+		WBS wbs= new WBS();
+		int PedalPos;
+		boolean AutoBrake, Skid;
+		for (int i = 0; i < 2; i++) {
+		  PedalPos = Verifier.nondetInt();
+		  AutoBrake = Verifier.nondetBoolean();
+		  Skid = Verifier.nondetBoolean();
+		  wbs.update(PedalPos, AutoBrake, Skid);
+                  // This assertion should fail:
+	          assert((PedalPos > 0 && PedalPos <= 4) ? (wbs.Alt_Pressure > 0 || wbs.Nor_Pressure > 0) : true);
+		}
+	}
+
+}

java/java-ranger-regression/WBS/prop4/Main.java

@@ -0,0 +1,18 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+public class Main {
+
+	public static void main(String[] args) {
+		WBS wbs= new WBS();
+		int PedalPos;
+		boolean AutoBrake, Skid;
+		for (int i = 0; i < 4; i++) {
+		  PedalPos = Verifier.nondetInt();
+		  AutoBrake = Verifier.nondetBoolean();
+		  Skid = Verifier.nondetBoolean();
+		  wbs.update(PedalPos, AutoBrake, Skid);
+                  // This assertion should fail:
+                  assert((PedalPos > 0 && !Skid) ? (wbs.Alt_Pressure > 0 || wbs.Nor_Pressure > 0) : true);
+		}
+	}
+
+}