fixing some benchmraks for java ranger

Author: sohah

java/java-ranger-regression/alarm/Alarm_prop7.yml

@@ -5,4 +5,4 @@ input_files:
   - prop8_True/
 properties:
   - property_file: ../../properties/assert.prp
-    expected_verdict: false
+    expected_verdict: true

java/java-ranger-regression/alarm/Alarm_prop8.yml

@@ -222,7 +222,7 @@ public static void main(String[] args) {
         rtu_const_in.Max_Paused_Duration = Max_Paused_Duration;
         rtu_const_in.Max_Idle_Duration = Max_Idle_Duration;
         rtu_const_in.Tolerance_Max = Tolerance_Max;
-        
+
         rtu_const_in.Tolerance_Min = Tolerance_Min;
         rtu_const_in.Log_Interval = Log_Interval;
         rtu_const_in.System_Test_Interval = System_Test_Interval;
@@ -416,8 +416,8 @@ public static void main(String[] args) {
             // this assertion should pass
 
             //Prop2: air_in_line_implies_grt_L3_alarm
-        checkCondition = (rtu_TLM_MODE_IN.System_On && rtu_SENSOR_IN.Air_In_Line);
-        checkOutput = (rty_ALARM_OUT.Highest_Level_Alarm >= 3);
+        checkCondition = (rtu_tlm_mode_in.System_On && rtu_sensor_in.Air_In_Line);
+        checkOutput = (rty_alarm_out.Highest_Level_Alarm >= 3);
         assert (!checkCondition || checkOutput);
 
         }

java/java-ranger-regression/alarm/prop2_True/Main.java

@@ -1,6 +1,6 @@
 import org.sosy_lab.sv_benchmarks.Verifier;
 
-public class Main_T3 {
+public class Main {
 
     public static void main(String[] args) {
         ALARM_Functional alarm = new ALARM_Functional();

java/java-ranger-regression/alarm/prop3_True/Main.java

@@ -55,7 +55,7 @@ public static void main(String[] args) {
         int Flow_Rate_Low = Verifier.nondetInt();
 
         //Symbolic input of Device_Senso            // this assertion should pass
-        r_Inputs
+        
         int Flow_Rate = Verifier.nondetInt();
         boolean Flow_Rate_Not_Stable = Verifier.nondetBoolean();
         boolean Air_In_Line = Verifier.nondetBoolean();
@@ -223,7 +223,7 @@ public static void main(String[] args) {
         rtu_const_in.Max_Paused_Duration = Max_Paused_Duration;
         rtu_const_in.Max_Idle_Duration = Max_Idle_Duration;
         rtu_const_in.Tolerance_Max = Tolerance_Max;
-        
+
         rtu_const_in.Tolerance_Min = Tolerance_Min;
         rtu_const_in.Log_Interval = Log_Interval;
         rtu_const_in.System_Test_Interval = System_Test_Interval;

java/java-ranger-regression/alarm/prop5_True/Main.java

@@ -271,7 +271,7 @@ public static void main(String[] args) {
         rty_alarm_out.Log_Message_ID = Log_Message_ID5;
 
         B_ALARM_Functional_c_T localB = new B_ALARM_Functional_c_T();
-        DW_ALARM_Funcrtu_op_cmd_intional_f_T localDW = new DW_ALARM_Functional_f_T();
+        DW_ALARM_Functional_f_T localDW = new DW_ALARM_Functional_f_T();
 
         alarm.ALARM_Functional_Init(localB, localDW);
 

java/java-ranger-regression/alarm/prop6_True/Main.java

@@ -236,7 +236,7 @@ public static void main(String[] args) {
             checkCondition = (rtu_TLM_MODE_IN.System_On && (rtu_ALARM_IN.Highest_Level_Alarm == 2));
             checkOutput =
                     ((rty_IM_OUT.Current_System_Mode == 1) || (rty_IM_OUT.Current_System_Mode == 2) || (rty_IM_OUT.Current_System_Mode == 6) || (rty_IM_OUT.Current_System_Mode == 7) || (rty_IM_OUT.Current_System_Mode == 8));
-            assert (!checkCondition || checkOutput);*/
+            assert (!checkCondition || checkOutput);
 
         }