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

Commit

Permalink
Cleaning up WBS_vt/Main.java
Browse files Browse the repository at this point in the history 
I've deleted commented lines and used a loop to run WBS 10 times instead
of 10 calls to WBS' step function.
  • Loading branch information
@vaibhavbsharma
vaibhavbsharma committed Oct 28, 2019
1 parent 9073cf3 commit ea11856
Showing 1 changed file with 3 additions and 46 deletions.
49 changes: 3 additions & 46 deletions java/java-ranger-regression/WBS_prop1/Main.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,6 @@ public void update(int PedalPos, boolean AutoBrake,
}
}
}
//Debug.printPC("PC @fter(PadalPos == 0) [Region 1] = ");


if ((AutoBrake &&
Expand All @@ -74,15 +73,13 @@ public void update(int PedalPos, boolean AutoBrake,
} else {
WBS_Node_WBS_BSCU_Command_Switch = 0;
}
//Debug.printPC("PC @fter(AutoBrake && WBS_Node_WBS_BSCU_Command_Is_Normal_Relational_Operator) [Region 2] = ");


WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6 = ((((!(WBS_Node_WBS_BSCU_Unit_Delay1 == 0)) &&
(WBS_Node_WBS_Unit_Delay2 <= 0)) &&
WBS_Node_WBS_BSCU_Command_Is_Normal_Relational_Operator) ||
(!WBS_Node_WBS_BSCU_Command_Is_Normal_Relational_Operator));

// Debug.printPC("PC @fter(WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6 = ((((!(WBS_Node_WBS_BSCU_Unit_Delay1 == 0)) &&) = ");

if (WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) {
if (Skid)
Expand All @@ -94,7 +91,6 @@ public void update(int PedalPos, boolean AutoBrake,
WBS_Node_WBS_BSCU_Switch3 = 4;
}

// Debug.printPC("PC @fter((WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6)) = ");


if (WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) {
Expand All @@ -103,7 +99,6 @@ public void update(int PedalPos, boolean AutoBrake,
WBS_Node_WBS_Green_Pump_IsolationValve_Switch = 5;
}

// Debug.printPC("PC @fter(WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) = ");

if ((WBS_Node_WBS_Green_Pump_IsolationValve_Switch >= 1)) {
WBS_Node_WBS_SelectorValve_Switch1 = 0;
Expand All @@ -112,7 +107,6 @@ public void update(int PedalPos, boolean AutoBrake,
WBS_Node_WBS_SelectorValve_Switch1 = 5;
}

// Debug.printPC("PC @fter(WBS_Node_WBS_Green_Pump_IsolationValve_Switch >= 1) = ");

if ((!WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6)) {
WBS_Node_WBS_AccumulatorValve_Switch = 0;
Expand All @@ -125,7 +119,6 @@ public void update(int PedalPos, boolean AutoBrake,
}
}

// Debug.printPC("PC @fter(!WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) = ");


if ((WBS_Node_WBS_BSCU_Switch3 == 0)) {
Expand All @@ -149,7 +142,6 @@ public void update(int PedalPos, boolean AutoBrake,
}
}
}
// Debug.printPC("PC @fter(WBS_Node_WBS_BSCU_Switch3 == 0) = ");



Expand All @@ -158,15 +150,13 @@ public void update(int PedalPos, boolean AutoBrake,
} else {
WBS_Node_WBS_BSCU_Command_AntiSkidCommand_Normal_Switch = (WBS_Node_WBS_BSCU_Command_Switch+WBS_Node_WBS_BSCU_Command_PedalCommand_Switch1);
}
//Debug.printPC("PC @fter(Skid) [Region 3] = ");


if (WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) {
Sys_Mode = 1;
} else {
Sys_Mode = 0;
}
// Debug.printPC("PC @fter(WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) = ");


if (WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) {
Expand Down Expand Up @@ -194,7 +184,6 @@ public void update(int PedalPos, boolean AutoBrake,
}
}
}
//Debug.printPC("PC @fter(WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6) = ");



Expand All @@ -203,7 +192,6 @@ public void update(int PedalPos, boolean AutoBrake,
} else {
WBS_Node_WBS_SelectorValve_Switch = 0;
}
// Debug.printPC("PC @fter(WBS_Node_WBS_Green_Pump_IsolationValve_Switch >= 1) = ");



Expand All @@ -229,7 +217,6 @@ public void update(int PedalPos, boolean AutoBrake,
}
}

// Debug.printPC("PC before(WBS_Node_WBS_BSCU_Command_PedalCommand_Switch1 == 0) [region 4] = ");

if ((WBS_Node_WBS_BSCU_Command_PedalCommand_Switch1 == 0)) {
Alt_Pressure = 0;
Expand All @@ -252,54 +239,24 @@ public void update(int PedalPos, boolean AutoBrake,
}
}
}
// Debug.printPC("PC @fter(WBS_Node_WBS_BSCU_Command_PedalCommand_Switch1 == 0) [Region 4] = ");


WBS_Node_WBS_rlt_PRE2 = Nor_Pressure;

WBS_Node_WBS_BSCU_rlt_PRE1 = WBS_Node_WBS_BSCU_Switch2;

WBS_Node_WBS_BSCU_SystemModeSelCmd_rlt_PRE = Sys_Mode;
// WBS_Node_WBS_BSCU_SystemModeSelCmd_rlt_PRE += WBS_Node_WBS_BSCU_SystemModeSelCmd_Logical_Operator6 ? 1 : 0;

// Assertions added by MWW: these are the truth values for "my" version of the model - may not be true for this code, but should be
// consistent between SPF and Veritest-SPF.

// I prefer ite to !a || b for implications.

// This assertion should prove:
//boolean myassert = (PedalPos > 0 && PedalPos <= 4 && !Skid) ? (Alt_Pressure > 0 || Nor_Pressure > 0) : true;
//assert(myassert);
//assert((PedalPos > 0 && PedalPos <= 4 && !Skid) ? (Alt_Pressure > 0 || Nor_Pressure > 0) : true);

// This assertion should fail:
assert((PedalPos > 0 && PedalPos <= 4 && !Skid) ? (Alt_Pressure > 0) : true);

// This assertion may fail (depending on encoding):
//Debug.printPC("PC before assertion ((PedalPos > 0 && PedalPos <= 4 && !Skid) ? (Nor_Pressure > 0) : true) = ");

// assert((PedalPos > 0 && PedalPos <= 4 && !Skid) ? (Nor_Pressure > 0) : true);

// This assertion should fail:
//assert((PedalPos > 0 && PedalPos <= 4) ? (Alt_Pressure > 0 || Nor_Pressure > 0) : true);

// This assertion should also fail:
//assert((PedalPos > 0 && !Skid) ? (Alt_Pressure > 0 || Nor_Pressure > 0) : true);
}


public static void main(String[] args) {
Main Main = new Main();
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
for (int i = 0; i < 10; i++) {
Main.update(Verifier.nondetInt(), Verifier.nondetBoolean(), Verifier.nondetBoolean());
}
}

}

0 comments on commit ea11856

Please sign in to comment.