diff --git a/Beispiele/LandingGear_R6.java b/Beispiele/LandingGear_R6.java index 720a831b66eb536eefcc2ec40c16c06fc0f89f38..d9d49144aeed9863121bf91520352e0b79442c7a 100644 --- a/Beispiele/LandingGear_R6.java +++ b/Beispiele/LandingGear_R6.java @@ -819,8 +819,8 @@ public class LandingGear_R6 { return new BBoolean(!gear.equal(GEAR_STATE.gear_moving).booleanValue() || door.equal(DOOR_STATE.open).booleanValue()).booleanValue(); } - public boolean _check_inv_() { - return !(!state._check_inv_1() || !state._check_inv_2() || !state._check_inv_3() || !state._check_inv_4() || !state._check_inv_5() || !state._check_inv_6() || !state._check_inv_7() || !state._check_inv_8() || !state._check_inv_9() || !state._check_inv_10() || !state._check_inv_11() || !state._check_inv_12() || !state._check_inv_13() || !state._check_inv_14() || !state._check_inv_15() || !state._check_inv_16() || !state._check_inv_17() || !state._check_inv_18() || !state._check_inv_19() || !state._check_inv_20() || !state._check_inv_21() || !state._check_inv_22() || !state._check_inv_23() || !state._check_inv_24() || !state._check_inv_25()); + public boolean _check_inv() { + return !(!this._check_inv_1() || !this._check_inv_2() || !this._check_inv_3() || !this._check_inv_4() || !this._check_inv_5() || !this._check_inv_6() || !this._check_inv_7() || !this._check_inv_8() || !this._check_inv_9() || !this._check_inv_10() || !this._check_inv_11() || !this._check_inv_12() || !this._check_inv_13() || !this._check_inv_14() || !this._check_inv_15() || !this._check_inv_16() || !this._check_inv_17() || !this._check_inv_18() || !this._check_inv_19() || !this._check_inv_20() || !this._check_inv_21() || !this._check_inv_22() || !this._check_inv_23() || !this._check_inv_24() || !this._check_inv_25()); } public LandingGear_R6 _copy() { @@ -829,4 +829,3 @@ public class LandingGear_R6 { } - diff --git a/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java index ba4d5bb43aacae90177ab5a064c6de73393e13f8..7e46378186e589cbab977d4287abec3bb8b9f712 100644 --- a/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java +++ b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java @@ -451,8 +451,8 @@ public class Train_1_beebook_deterministic_MC_POR_v2 { return rsrtbl.relationImage(OCC).subset(frm).booleanValue(); } - public boolean _check_inv_() { - return !(!state._check_inv_1() || !state._check_inv_2() || !state._check_inv_3() || !state._check_inv_4() || !state._check_inv_5() || !state._check_inv_6() || !state._check_inv_7() || !state._check_inv_8() || !state._check_inv_9() || !state._check_inv_10() || !state._check_inv_11() || !state._check_inv_12()); + public boolean _check_inv() { + return !(!this._check_inv_1() || !this._check_inv_2() || !this._check_inv_3() || !this._check_inv_4() || !this._check_inv_5() || !this._check_inv_6() || !this._check_inv_7() || !this._check_inv_8() || !this._check_inv_9() || !this._check_inv_10() || !this._check_inv_11() || !this._check_inv_12()); } public Train_1_beebook_deterministic_MC_POR_v2 _copy() { diff --git a/JavaModelChecker/libs/btypes.jar b/JavaModelChecker/libs/btypes.jar index eb7cddc7491f197216ffc5d0d93d0994dd07f920..e1385f4447dd5e015037a39a3dbb339a26df521c 100644 Binary files a/JavaModelChecker/libs/btypes.jar and b/JavaModelChecker/libs/btypes.jar differ diff --git a/notes b/notes index 6b3654a5c7cdbb2f505da85e9711c11b5d00558d..c17fe25197cf8fd0d3df030b3467240edcb2f915 100644 --- a/notes +++ b/notes @@ -4,7 +4,7 @@ Scheduler: 35 states, 144 transitions Sorting Algorithm: 5050 states, 5050 transitions Cruise Controller: 1360 states, 26148 transitions CAN BUS: 132598 states, 340264 transitions -Landing Gear: 131328 states, 884369 transitions -Train: 672174 states, 2244486 transitions +Landing Gear: 131328 states, 884368 transitions +Train: 672173 states, 2244484 transitions No Invariant Violations, No Deadlocks