Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit 443ecb6

Browse files
sohahmmuesly
sohah
authored and
mmuesly
committed
adding updated version of the benchmarks that creates symbolic inputs at the constructor of each object
1 parent b514f13 commit 443ecb6

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+1723
-6740
lines changed

‎java/java-ranger-regression/alarm/impl/Alarm_Outputs.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11

22
public class Alarm_Outputs {
3-
int Is_Audio_Disabled;
4-
int Notification_Message;
5-
int Audio_Notification_Command;
6-
int Highest_Level_Alarm;
7-
int Log_Message_ID;
3+
int Is_Audio_Disabled = Verifier.nondetInt();
4+
int Notification_Message = Verifier.nondetInt();
5+
int Audio_Notification_Command = Verifier.nondetInt();
6+
int Highest_Level_Alarm = Verifier.nondetInt();
7+
int Log_Message_ID = Verifier.nondetInt();
88
}

‎java/java-ranger-regression/alarm/impl/Config_Outputs.java‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,28 @@
11

22
public class Config_Outputs {
3-
int Patient_ID;
4-
int Drug_Name;
5-
int Drug_Concentration;
6-
int Infusion_Total_Duration;
7-
int VTBI_Total;
8-
int Flow_Rate_Basal;
9-
int Flow_Rate_Intermittent_Bolus;
10-
int Duration_Intermittent_Bolus;
11-
int Interval_Intermittent_Bolus;
12-
int Flow_Rate_Patient_Bolus;
13-
int Duration_Patient_Bolus;
14-
int Lockout_Period_Patient_Bolus;
15-
int Max_Number_of_Patient_Bolus;
16-
int Flow_Rate_KVO;
17-
int Entered_Reservoir_Volume;
18-
int Reservoir_Volume;
19-
int Configured;
20-
int Error_Message_ID;
21-
boolean Request_Config_Type;
22-
boolean Request_Confirm_Infusion_Initiate;
23-
boolean Request_Patient_Drug_Info;
24-
boolean Request_Infusion_Info;
25-
int Log_Message_ID;
26-
int Config_Timer;
27-
int Config_Mode;
3+
int Patient_ID = Verifier.nondetInt();
4+
int Drug_Name = Verifier.nondetInt();
5+
int Drug_Concentration = Verifier.nondetInt();
6+
int Infusion_Total_Duration = Verifier.nondetInt();
7+
int VTBI_Total = Verifier.nondetInt();
8+
int Flow_Rate_Basal = Verifier.nondetInt();
9+
int Flow_Rate_Intermittent_Bolus = Verifier.nondetInt();
10+
int Duration_Intermittent_Bolus = Verifier.nondetInt();
11+
int Interval_Intermittent_Bolus = Verifier.nondetInt();
12+
int Flow_Rate_Patient_Bolus = Verifier.nondetInt();
13+
int Duration_Patient_Bolus = Verifier.nondetInt();
14+
int Lockout_Period_Patient_Bolus = Verifier.nondetInt();
15+
int Max_Number_of_Patient_Bolus = Verifier.nondetInt();
16+
int Flow_Rate_KVO = Verifier.nondetInt();
17+
int Entered_Reservoir_Volume = Verifier.nondetInt();
18+
int Reservoir_Volume = Verifier.nondetInt();
19+
int Configured = Verifier.nondetInt();
20+
int Error_Message_ID = Verifier.nondetInt();
21+
boolean Request_Config_Type = Verifier.nondetBoolean();
22+
boolean Request_Confirm_Infusion_Initiate = Verifier.nondetBoolean();
23+
boolean Request_Patient_Drug_Info = Verifier.nondetBoolean();
24+
boolean Request_Infusion_Info = Verifier.nondetBoolean();
25+
int Log_Message_ID = Verifier.nondetInt();
26+
int Config_Timer = Verifier.nondetInt();
27+
int Config_Mode = Verifier.nondetInt();
2828
}

‎java/java-ranger-regression/alarm/impl/Device_Configuration_Inputs.java‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
11

22
public class Device_Configuration_Inputs {
3-
int Audio_Enable_Duration;
4-
int Audio_Level;
5-
int Config_Warning_Duration;
6-
int Empty_Reservoir;
7-
int Low_Reservoir;
8-
int Max_Config_Duration;
9-
int Max_Duration_Over_Infusion;
10-
int Max_Duration_Under_Infusion;
11-
int Max_Paused_Duration;
12-
int Max_Idle_Duration;
13-
int Tolerance_Max;
14-
int Tolerance_Min;
15-
int Log_Interval;
16-
int System_Test_Interval;
17-
int Max_Display_Duration;
18-
int Max_Confirm_Stop_Duration;
3+
int Audio_Enable_Duration = Verifier.nondetInt();
4+
int Audio_Level = Verifier.nondetInt();
5+
int Config_Warning_Duration = Verifier.nondetInt();
6+
int Empty_Reservoir = Verifier.nondetInt();
7+
int Low_Reservoir = Verifier.nondetInt();
8+
int Max_Config_Duration = Verifier.nondetInt();
9+
int Max_Duration_Over_Infusion = Verifier.nondetInt();
10+
int Max_Duration_Under_Infusion = Verifier.nondetInt();
11+
int Max_Paused_Duration = Verifier.nondetInt();
12+
int Max_Idle_Duration = Verifier.nondetInt();
13+
int Tolerance_Max = Verifier.nondetInt();
14+
int Tolerance_Min = Verifier.nondetInt();
15+
int Log_Interval = Verifier.nondetInt();
16+
int System_Test_Interval = Verifier.nondetInt();
17+
int Max_Display_Duration = Verifier.nondetInt();
18+
int Max_Confirm_Stop_Duration = Verifier.nondetInt();
1919
}

‎java/java-ranger-regression/alarm/impl/Device_Sensor_Inputs.java‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,24 @@
11

22
public class Device_Sensor_Inputs {
33

4-
int Flow_Rate;
5-
boolean Flow_Rate_Not_Stable;
6-
boolean Air_In_Line;
7-
boolean Occlusion;
8-
boolean Door_Open;
9-
boolean Temp;
10-
boolean Air_Pressure;
11-
boolean Humidity;
12-
boolean Battery_Depleted;
13-
boolean Battery_Low;
14-
boolean Battery_Unable_To_Charge;
15-
boolean Supply_Voltage;
16-
boolean CPU_In_Error;
17-
boolean RTC_In_Error;
18-
boolean Watchdog_Interrupted;
19-
boolean Memory_Corrupted;
20-
boolean Pump_Too_Hot;
21-
boolean Pump_Overheated;
22-
boolean Pump_Primed;
23-
boolean Post_Successful;
4+
int Flow_Rate = Verifier.nondetInt();
5+
boolean Flow_Rate_Not_Stable = Verifier.nondetBoolean();
6+
boolean Air_In_Line = Verifier.nondetBoolean();
7+
boolean Occlusion = Verifier.nondetBoolean();
8+
boolean Door_Open = Verifier.nondetBoolean();
9+
boolean Temp = Verifier.nondetBoolean();
10+
boolean Air_Pressure = Verifier.nondetBoolean();
11+
boolean Humidity = Verifier.nondetBoolean();
12+
boolean Battery_Depleted = Verifier.nondetBoolean();
13+
boolean Battery_Low = Verifier.nondetBoolean();
14+
boolean Battery_Unable_To_Charge = Verifier.nondetBoolean();
15+
boolean Supply_Voltage = Verifier.nondetBoolean();
16+
boolean CPU_In_Error = Verifier.nondetBoolean();
17+
boolean RTC_In_Error = Verifier.nondetBoolean();
18+
boolean Watchdog_Interrupted = Verifier.nondetBoolean();
19+
boolean Memory_Corrupted = Verifier.nondetBoolean();
20+
boolean Pump_Too_Hot = Verifier.nondetBoolean();
21+
boolean Pump_Overheated = Verifier.nondetBoolean();
22+
boolean Pump_Primed = Verifier.nondetBoolean();
23+
boolean Post_Successful = Verifier.nondetBoolean();
2424
}

‎java/java-ranger-regression/alarm/impl/Div_s32.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
public class Div_s32 {
33

44
static final int MAX_int = 2147483647;
5-
static final int MIN_int = -2147483647 - 1;
5+
static final int MIN_int = -2147483648;
66

77
public static int div_s32(int numerator, int denominator) {
88
int quotient;

‎java/java-ranger-regression/alarm/impl/Drug_Database_Inputs.java‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11

22
public class Drug_Database_Inputs {
33

4-
boolean Known_Prescription;
5-
int Drug_Name;
6-
int Drug_Concentration_High;
7-
int Drug_Concentration_Low;
8-
int VTBI_High;
9-
int VTBI_Low;
10-
int Interval_Patient_Bolus;
11-
int Number_Max_Patient_Bolus;
12-
int Flow_Rate_KVO;
13-
int Flow_Rate_High;
14-
int Flow_Rate_Low;
4+
boolean Known_Prescription = Verifier.nondetBoolean();
5+
int Drug_Name = Verifier.nondetInt();
6+
int Drug_Concentration_High = Verifier.nondetInt();
7+
int Drug_Concentration_Low = Verifier.nondetInt();
8+
int VTBI_High = Verifier.nondetInt();
9+
int VTBI_Low = Verifier.nondetInt();
10+
int Interval_Patient_Bolus = Verifier.nondetInt();
11+
int Number_Max_Patient_Bolus = Verifier.nondetInt();
12+
int Flow_Rate_KVO = Verifier.nondetInt();
13+
int Flow_Rate_High = Verifier.nondetInt();
14+
int Flow_Rate_Low = Verifier.nondetInt();
1515
}

‎java/java-ranger-regression/alarm/impl/Infusion_Manager_Outputs.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11

22
public class Infusion_Manager_Outputs {
3-
public int Commanded_Flow_Rate;
4-
public int Current_System_Mode;
5-
public boolean New_Infusion;
6-
public int Log_Message_ID;
7-
public int Actual_Infusion_Duration;
3+
public int Commanded_Flow_Rate = Verifier.nondetInt();
4+
public int Current_System_Mode = Verifier.nondetInt();
5+
public boolean New_Infusion = Verifier.nondetBoolean();
6+
public int Log_Message_ID = Verifier.nondetInt();
7+
public int Actual_Infusion_Duration = Verifier.nondetInt();
88
}

‎java/java-ranger-regression/alarm/impl/Log_Output.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11

22
public class Log_Output {
3-
public int Log;
4-
public boolean Logging_Failed;
3+
public int Log = Verifier.nondetInt();
4+
public boolean Logging_Failed = Verifier.nondetBoolean();
55
}

‎java/java-ranger-regression/alarm/impl/Operator_Commands.java‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,18 @@
11

22
public class Operator_Commands {
33

4-
boolean System_Start;
5-
boolean System_Stop;
6-
boolean Infusion_Initiate;
7-
boolean Infusion_Inhibit;
8-
boolean Infusion_Cancel;
9-
boolean Data_Config;
10-
boolean Next;
11-
boolean Back;
12-
boolean Cancel;
13-
boolean Keyboard;
14-
int Disable_Audio;
15-
boolean Notification_Cancel;
16-
int Configuration_Type;
17-
boolean Confirm_Stop;
4+
boolean System_Start = Verifier.nondetBoolean();
5+
boolean System_Stop = Verifier.nondetBoolean();
6+
boolean Infusion_Initiate = Verifier.nondetBoolean();
7+
boolean Infusion_Inhibit = Verifier.nondetBoolean();
8+
boolean Infusion_Cancel = Verifier.nondetBoolean();
9+
boolean Data_Config = Verifier.nondetBoolean();
10+
boolean Next = Verifier.nondetBoolean();
11+
boolean Back = Verifier.nondetBoolean();
12+
boolean Cancel = Verifier.nondetBoolean();
13+
boolean Keyboard = Verifier.nondetBoolean();
14+
int Disable_Audio = Verifier.nondetInt();
15+
boolean Notification_Cancel = Verifier.nondetBoolean();
16+
int Configuration_Type = Verifier.nondetInt();
17+
boolean Confirm_Stop = Verifier.nondetBoolean();
1818
}

‎java/java-ranger-regression/alarm/impl/System_Monitor_Output.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11

22
public class System_Monitor_Output {
3-
boolean System_Monitor_Failed;
3+
boolean System_Monitor_Failed = Verifier.nondetBoolean();
44
}

0 commit comments

Comments
 (0)