From 36343322bbccb4239785cfb7f811676e6b02daa8 Mon Sep 17 00:00:00 2001
From: "Vu, Fabian (favu100)" <fabian.vu@uni-duesseldorf.de>
Date: Sun, 24 Jul 2022 14:20:33 +0200
Subject: [PATCH] Update LandingGear, Train and notes
---
Beispiele/LandingGear_R6.java | 5 ++---
Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java | 4 ++--
notes | 4 ++--
3 files changed, 6 insertions(+), 7 deletions(-)
diff --git a/Beispiele/LandingGear_R6.java b/Beispiele/LandingGear_R6.java
index 720a831..d9d4914 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 ba4d5bb..7e46378 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/notes b/notes
index 6b3654a..c17fe25 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
--
GitLab