diff --git a/Beispiele/CAN_BUS_MC.json b/Beispiele/CAN_BUS_tlc.json
similarity index 100%
rename from Beispiele/CAN_BUS_MC.json
rename to Beispiele/CAN_BUS_tlc.json
diff --git a/Beispiele/CAN_BUS_tlc.mch b/Beispiele/CAN_BUS_tlc.mch
new file mode 100644
index 0000000000000000000000000000000000000000..515fba702b65f99665dd020b4e93057b90c86fe2
--- /dev/null
+++ b/Beispiele/CAN_BUS_tlc.mch
@@ -0,0 +1,314 @@
+MACHINE CAN_BUS_tlc
+
+SETS
+ T1state={T1_EN,T1_CALC,T1_SEND,T1_WAIT};
+ T2mode={T2MODE_SENSE,T2MODE_TRANSMIT,T2MODE_RELEASE};
+ T2state={T2_EN,T2_RCV,T2_PROC,T2_CALC,T2_SEND,T2_WAIT,T2_RELEASE};
+ T3state={T3_READY,T3_WRITE,T3_RELEASE,T3_READ,T3_PROC,T3_WAIT}
+CONSTANTS
+ NATSET
+PROPERTIES
+ NATSET = 0..5
+VARIABLES
+ BUSpriority,
+ BUSvalue,
+ BUSwrite,
+ T1_state,
+ T1_timer,
+ T1_writevalue,
+ T2_mode,
+ T2_readpriority,
+ T2_readvalue,
+ T2_state,
+ T2_timer,
+ T2_writevalue,
+ T2v,
+ T3_enabled,
+ T3_evaluated,
+ T3_readpriority,
+ T3_readvalue,
+ T3_state
+INVARIANT
+ T2v : INTEGER &
+ T3_evaluated : BOOL &
+ T3_enabled : BOOL &
+ T1_state : T1state &
+ T2_state : T2state &
+ T3_state : T3state &
+ T1_writevalue : INTEGER &
+ T2_writevalue : INTEGER &
+ T2_readvalue : INTEGER &
+ T1_timer : NATURAL &
+ T2_timer : NATURAL &
+ T2_mode : T2mode &
+ BUSvalue : INTEGER &
+ BUSpriority : NATSET &
+ T3_readvalue : INTEGER &
+ T3_readpriority : NATSET &
+ T2_readpriority : NATSET &
+ BUSwrite : NATSET +-> INTEGER &
+ /*BUSwrite : FIN(NATSET*INTEGER) &*/
+ BUSwrite /= {} &
+ 0 : dom(BUSwrite)
+INITIALISATION
+ T2v := 0
+ ||
+ T3_evaluated := TRUE
+ ||
+ T3_enabled := TRUE
+ ||
+ T1_state := T1_EN
+ ||
+ T2_state := T2_EN
+ ||
+ T3_state := T3_READY
+ ||
+ T1_writevalue := 0
+ ||
+ T2_writevalue := 0
+ ||
+ T2_readvalue := 0
+ ||
+ T2_readpriority := 0
+ ||
+ T3_readvalue := 0
+ ||
+ T3_readpriority := 0
+ ||
+ T1_timer := 2
+ ||
+ T2_timer := 3
+ ||
+ BUSwrite := {0 |-> 0}
+ ||
+ BUSvalue := 0
+ ||
+ BUSpriority := 0
+ ||
+ T2_mode := T2MODE_SENSE
+OPERATIONS
+ T1Evaluate =
+ PRE
+ /* @grd1 */ T1_timer = 0
+ & /* @grd3 */ T1_state = T1_EN
+ THEN
+ T1_timer := 0
+ ||
+ T1_state := T1_CALC
+ END;
+ T1Calculate(p) =
+ PRE
+ p : -1..3 &
+ /* @grd2 */ T1_state = T1_CALC
+ THEN
+ T1_writevalue := p
+ ||
+ T1_state := T1_SEND
+ END;
+ T1SendResult(ppriority,pv) =
+ PRE
+ /* @grd2 */ ppriority = 3
+ & /* @grd1 */ pv = T1_writevalue
+ & /* @grd3 */ T1_state = T1_SEND
+ THEN
+ BUSwrite := BUSwrite <+ {ppriority |-> pv}
+ ||
+ T1_state := T1_WAIT
+ END;
+ T1Wait(pt) =
+ PRE
+ /* @grd1 */ pt = 2
+ & /* @grd2 */ T1_state = T1_WAIT
+ THEN
+ T1_timer := pt
+ ||
+ T1_state := T1_EN
+ END;
+ T2Evaluate =
+ PRE
+ /* @grd1 */ T2_timer = 0
+ & /* @grd3 */ T2_state = T2_EN
+ THEN
+ T2_timer := 0
+ ||
+ T2_state := T2_RCV
+ END;
+ T2ReadBus(ppriority,pv) =
+ PRE
+ /* @grd2 */ ppriority = BUSpriority
+ & /* @grd1 */ pv = BUSvalue
+ & /* @grd3 */ T2_state = T2_RCV
+ THEN
+ T2_readvalue := pv
+ ||
+ T2_readpriority := ppriority
+ ||
+ T2_state := T2_PROC
+ END;
+ T2Reset =
+ PRE
+ /* @grd1 */ T2_readpriority = 4
+ & /* @grd2 */ T2_state = T2_PROC
+ THEN
+ T2_writevalue := T2v
+ ||
+ T2v := 0
+ ||
+ T2_state := T2_SEND
+ ||
+ T2_mode := T2MODE_TRANSMIT
+ END;
+ T2Complete =
+ PRE
+ /* @grd2 */ T2_state = T2_PROC
+ & /* @grd1 */ T2_readpriority = 5
+ & /* @grd3 */ T2_mode = T2MODE_TRANSMIT
+ THEN
+ T2_state := T2_RELEASE
+ ||
+ T2_mode := T2MODE_SENSE
+ END;
+ T2ReleaseBus(ppriority) =
+ PRE
+ /* @grd1 */ ppriority = T2_readpriority
+ & /* @grd3 */ ppriority : dom(BUSwrite)
+ & /* @grd4 */ T2_state = T2_RELEASE
+ THEN
+ BUSwrite := {ppriority} <<| BUSwrite
+ ||
+ T2_state := T2_WAIT
+ END;
+
+ T2Calculate =
+ PRE
+ /* @grd1 */ T2_readpriority = 3
+ & /* @grd2 */ T2_state = T2_PROC
+ THEN
+ T2v := T2_readvalue
+ ||
+ T2_state := T2_WAIT
+ END;
+
+ T2WriteBus(ppriority,pv) =
+ PRE
+ /* @grd2 */ ppriority = 5
+ & /* @grd1 */ pv = T2_writevalue
+ & /* @grd3 */ T2_state = T2_SEND
+ THEN
+ BUSwrite := BUSwrite <+ {ppriority |-> pv}
+ ||
+ T2_state := T2_WAIT
+ END;
+
+ T2Wait(pt) =
+ PRE
+ /* @grd1 */ pt = 3
+ & /* @grd2 */ T2_state = T2_WAIT
+ THEN
+ T2_timer := pt
+ ||
+ T2_state := T2_EN
+ END;
+
+ T3Initiate =
+ PRE
+ /* @grd1 */ T3_state = T3_READY
+ & /* @grd2 */ T3_evaluated = FALSE
+ & /* @grd3 */ T3_enabled = TRUE
+ THEN
+ T3_state := T3_WRITE
+ ||
+ T3_enabled := FALSE
+ END;
+
+ T3Evaluate =
+ PRE
+ /* @grd1 */ T3_state = T3_READY
+ & /* @grd2 */ T3_evaluated = FALSE
+ & /* @grd3 */ T3_enabled = FALSE
+ THEN
+ T3_state := T3_READ
+ END;
+
+ T3writebus(ppriority,pv) =
+ PRE
+ /* @grd2 */ ppriority = 4
+ & /* @grd1 */ pv = 0
+ & /* @grd3 */ T3_state = T3_WRITE
+ THEN
+ BUSwrite := BUSwrite <+ {ppriority |-> pv}
+ ||
+ T3_state := T3_WAIT
+ END;
+
+ T3Read(ppriority,pv) =
+ PRE
+ /* @grd2 */ ppriority = BUSpriority
+ & /* @grd1 */ pv = BUSvalue
+ & /* @grd4 */ T3_state = T3_READ
+ THEN
+ T3_readvalue := pv
+ ||
+ T3_readpriority := ppriority
+ ||
+ T3_state := T3_PROC
+ END;
+
+ T3Poll =
+ PRE
+ /* @grd1 */ T3_readpriority < 5
+ & /* @grd2 */ T3_state = T3_PROC
+ THEN
+ T3_state := T3_WAIT
+ END;
+
+ T3ReleaseBus(ppriority) =
+ PRE
+ /* @grd1 */ ppriority = 4
+ & /* @grd2 */ T3_readpriority = 5
+ & /* @grd3 */ T3_state = T3_PROC
+ THEN
+ BUSwrite := {ppriority} <<| BUSwrite
+ ||
+ T3_state := T3_RELEASE
+ END;
+
+ T3Wait =
+ PRE
+ /* @grd1 */ T3_state = T3_WAIT
+ THEN
+ T3_state := T3_READY
+ ||
+ T3_evaluated := TRUE
+ END;
+
+ T3ReEnableWait =
+ PRE
+ /* @grd1 */ T3_state = T3_RELEASE
+ THEN
+ T3_state := T3_READY
+ ||
+ T3_evaluated := TRUE
+ ||
+ T3_enabled := TRUE
+ END;
+
+ Update(pmax) =
+ PRE
+ /* @grd1 */ pmax = max(dom(BUSwrite))
+ & /* @grd2 */ T1_timer > 0
+ & /* @grd3 */ T2_timer > 0
+ & (/* @grd4 */ T3_enabled = TRUE or T3_evaluated = TRUE)
+ THEN
+ BUSvalue := BUSwrite(pmax)
+ ||
+ BUSpriority := pmax
+ ||
+ T1_timer := T1_timer - 1
+ ||
+ T2_timer := T2_timer - 1
+ ||
+ T3_evaluated := FALSE
+ END
+
+END
\ No newline at end of file
diff --git a/Beispiele/Cruise_finite1_deterministic_MC.mch b/Beispiele/Cruise_finite1_deterministic_MC.mch
new file mode 100644
index 0000000000000000000000000000000000000000..a68b981919f7ad927be02538878f38750870c4c9
--- /dev/null
+++ b/Beispiele/Cruise_finite1_deterministic_MC.mch
@@ -0,0 +1,593 @@
+/******************************************************************************
+VOLVO CRUISE CONTROLLER ABSTRACT MODEL
+*
+******************************************************************************/
+
+ MACHINE
+ Cruise_finite1_deterministic_MC
+
+SETS
+ RSset = {RSnone, RSpos, RSneg, RSequal};
+ ODset = {ODnone, ODclose, ODveryclose}
+
+DEFINITIONS
+ /*(ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE) == (ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE);*/
+ ASSERT_LTL == "G (e(SetCruiseSpeed) => e(CruiseBecomesNotAllowed))";
+ ASSERT_LTL1 == "G (e(CruiseBecomesNotAllowed) => e(SetCruiseSpeed))";
+ ASSERT_LTL2 == "G (e(CruiseBecomesNotAllowed) => e(ObstacleDisappears))"
+/* LTL Formulas
+ G (e(SetCruiseSpeed) -> e(CruiseBecomesNotAllowed)) TRUE (2.62 seconds)
+ G (e(CruiseBecomesNotAllowed) -> e(SetCruiseSpeed)) TRUE
+ G (e(CruiseBecomesNotAllowed) -> e(ObstacleDisappears)) FALSE
+ G (e(CruiseBecomesAllowed) -> X e(SetCruiseSpeed)) FALSE (12.78 seconds)
+ G ([CruiseBecomesAllowed] -> X e(SetCruiseSpeed)) TRUE (14.11 seconds)
+
+ G( e(CruiseOff) => Y O [SetCruiseSpeed]) TRUE 12.05 secs (10850 atoms)
+
+G( e(CruiseOff) => O [CruiseBecomesNotAllowed]) -> FALSE
+*/
+ VARIABLES
+ /* User level variables */
+ CruiseAllowed,
+ CruiseActive,
+ VehicleAtCruiseSpeed,
+ VehicleCanKeepSpeed,
+ VehicleTryKeepSpeed,
+ SpeedAboveMax,
+ VehicleTryKeepTimeGap,
+ CruiseSpeedAtMax,
+ ObstaclePresent,
+ ObstacleDistance,
+ ObstacleRelativeSpeed,
+ ObstacleStatusJustChanged,
+ CCInitialisationInProgress,
+ CruiseSpeedChangeInProgress,
+
+ /* Verification support variables */
+ NumberOfSetCruise
+
+
+ INVARIANT
+ /* Typing */
+ CruiseAllowed:BOOL &
+ CruiseActive:BOOL &
+ VehicleAtCruiseSpeed:BOOL &
+ VehicleCanKeepSpeed:BOOL &
+ VehicleTryKeepSpeed:BOOL &
+ SpeedAboveMax:BOOL &
+ VehicleTryKeepTimeGap:BOOL &
+ CruiseSpeedAtMax:BOOL &
+ NumberOfSetCruise:NATURAL &
+ NumberOfSetCruise:0..1 & /* added by mal */
+ ObstaclePresent:BOOL &
+ ObstacleDistance:ODset &
+ ObstacleRelativeSpeed:RSset &
+ ObstacleStatusJustChanged:BOOL &
+ CCInitialisationInProgress:BOOL &
+ CruiseSpeedChangeInProgress:BOOL &
+
+ /* Consistency */
+ (CruiseActive = FALSE => VehicleAtCruiseSpeed = FALSE) &
+ (CruiseActive = FALSE => VehicleCanKeepSpeed = FALSE) &
+ (CruiseActive = FALSE => VehicleTryKeepSpeed = FALSE) &
+ ((NumberOfSetCruise = 0) <=> (CruiseActive = FALSE)) &
+ (CruiseActive = FALSE => VehicleTryKeepTimeGap = FALSE) &
+ (CruiseActive = FALSE => CruiseSpeedAtMax = FALSE) &
+ (CruiseActive = FALSE => ObstacleDistance = ODnone ) &
+ (CruiseActive = FALSE => ObstacleStatusJustChanged = FALSE) &
+ (CruiseActive = FALSE => CCInitialisationInProgress = FALSE) &
+ (CruiseActive = FALSE => CruiseSpeedChangeInProgress = FALSE) &
+ (ObstaclePresent = FALSE => VehicleTryKeepTimeGap = FALSE) &
+ (ObstaclePresent = FALSE => ObstacleDistance = ODnone) &
+ (ObstaclePresent = FALSE <=> (ObstacleRelativeSpeed = RSnone)) &
+ ((ObstacleRelativeSpeed = RSequal & ObstacleDistance = ODnone)
+ => VehicleTryKeepTimeGap = FALSE) &
+ ((ObstacleRelativeSpeed = RSneg & ObstacleDistance = ODnone)
+ => VehicleTryKeepTimeGap = FALSE) &
+ ((ObstacleRelativeSpeed = RSpos & ObstacleDistance /= ODveryclose)
+ => VehicleTryKeepTimeGap = FALSE) &
+
+ /* Laws */
+ (CruiseAllowed = FALSE => CruiseActive = FALSE) &
+ (SpeedAboveMax = TRUE => VehicleAtCruiseSpeed = FALSE) &
+ (CruiseActive = TRUE
+ => (VehicleTryKeepSpeed = TRUE
+ or VehicleTryKeepTimeGap = TRUE
+ or not((ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE)))) &
+ (ObstacleDistance = ODnone & CruiseActive = TRUE & (ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepSpeed = TRUE) &
+ (ObstacleDistance = ODclose & ObstacleRelativeSpeed /= RSpos & (ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepTimeGap = TRUE) &
+ (ObstacleDistance = ODveryclose & (ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepTimeGap = TRUE) &
+ (ObstacleRelativeSpeed = RSpos & ObstacleDistance /= ODveryclose & CruiseActive = TRUE & (ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepSpeed = TRUE)
+
+
+ INITIALISATION
+ CruiseAllowed := TRUE ||
+ CruiseActive := FALSE ||
+ VehicleAtCruiseSpeed := FALSE ||
+ VehicleCanKeepSpeed := FALSE ||
+ VehicleTryKeepSpeed := FALSE ||
+ SpeedAboveMax := FALSE ||
+ VehicleTryKeepTimeGap := FALSE ||
+ NumberOfSetCruise := 0 ||
+ CruiseSpeedAtMax:= FALSE ||
+ ObstacleDistance := ODnone ||
+ ObstacleStatusJustChanged := FALSE ||
+ CCInitialisationInProgress := FALSE ||
+ CruiseSpeedChangeInProgress := FALSE ||
+ ObstaclePresent := FALSE ||
+ ObstacleRelativeSpeed := RSnone
+
+
+ OPERATIONS
+
+ CruiseBecomesNotAllowed =
+ SELECT
+ CruiseAllowed = TRUE
+ THEN
+ CruiseAllowed := FALSE ||
+ CruiseActive := FALSE ||
+ VehicleCanKeepSpeed := FALSE ||
+ VehicleTryKeepSpeed := FALSE ||
+ VehicleAtCruiseSpeed := FALSE ||
+ VehicleTryKeepTimeGap := FALSE ||
+ CruiseSpeedAtMax := FALSE ||
+ ObstacleDistance := ODnone ||
+ NumberOfSetCruise := 0 ||
+ ObstacleStatusJustChanged := FALSE ||
+ CCInitialisationInProgress := FALSE ||
+ CruiseSpeedChangeInProgress := FALSE
+ END;
+
+
+ CruiseBecomesAllowed = SELECT
+ CruiseAllowed = FALSE
+ THEN
+ CruiseAllowed := TRUE
+ END;
+
+
+ SetCruiseSpeed(vcks, csam) =
+ PRE vcks : BOOL & csam : BOOL & CruiseAllowed = TRUE THEN
+
+ CruiseActive := TRUE ||
+ VehicleCanKeepSpeed := vcks ||
+
+ IF SpeedAboveMax = FALSE THEN
+ VehicleAtCruiseSpeed := TRUE ||
+ CruiseSpeedAtMax := csam
+ ELSE
+ CruiseSpeedAtMax:=TRUE
+ END ||
+ ObstacleStatusJustChanged := TRUE ||
+ IF CruiseActive = TRUE THEN
+ CruiseSpeedChangeInProgress := TRUE
+ ELSE
+ CCInitialisationInProgress := TRUE
+ END ||
+ IF NumberOfSetCruise<1 THEN /* added my mal */
+ NumberOfSetCruise := NumberOfSetCruise + 1
+ END
+
+ END;
+
+
+ CCInitialisationFinished(vtks, vtktg) =
+ PRE
+ (vtks : BOOL) &
+ (vtktg : BOOL) &
+ (vtks = TRUE
+ or vtktg = TRUE
+ or ObstacleStatusJustChanged = TRUE
+ or CruiseSpeedChangeInProgress = TRUE) &
+ (ObstaclePresent = FALSE => vtktg = FALSE) &
+ (ObstacleDistance = ODnone => vtks = TRUE) &
+ ((ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed /= RSpos &
+ ObstacleStatusJustChanged = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => vtktg = TRUE) &
+ ((ObstacleDistance = ODveryclose &
+ ObstacleStatusJustChanged = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => vtktg = TRUE) &
+ ((ObstacleRelativeSpeed = RSpos &
+ ObstacleDistance /= ODveryclose&
+ ObstacleStatusJustChanged = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => vtks = TRUE) &
+ ((ObstacleRelativeSpeed = RSequal & ObstacleDistance = ODnone)
+ => vtktg = FALSE) &
+ ((ObstacleRelativeSpeed = RSneg & ObstacleDistance = ODnone)
+ => vtktg = FALSE) &
+ ((ObstacleRelativeSpeed = RSpos & ObstacleDistance /= ODveryclose)
+ => vtktg = FALSE) &
+ CCInitialisationInProgress = TRUE
+ THEN
+
+ VehicleTryKeepTimeGap := vtktg ||
+ VehicleTryKeepSpeed := vtks
+
+ END;
+
+
+ CCInitialisationDelayFinished =
+ SELECT
+ CCInitialisationInProgress = TRUE &
+ (VehicleTryKeepSpeed = TRUE
+ or VehicleTryKeepTimeGap = TRUE
+ or ObstacleStatusJustChanged = TRUE
+ or CruiseSpeedChangeInProgress = TRUE) &
+ (ObstacleDistance = ODnone => VehicleTryKeepSpeed = TRUE) &
+ ((ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed /= RSpos &
+ ObstacleStatusJustChanged = FALSE &
+ CruiseSpeedChangeInProgress = FALSE )
+ => (VehicleTryKeepTimeGap = TRUE)) &
+ ((ObstacleDistance = ODveryclose &
+ ObstacleStatusJustChanged = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepTimeGap = TRUE) &
+ ((ObstacleRelativeSpeed = RSpos &
+ ObstacleDistance /= ODveryclose &
+ ObstacleStatusJustChanged = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepSpeed = TRUE)
+ THEN
+ CCInitialisationInProgress := TRUE
+ END;
+
+
+ CruiseSpeedChangeFinished(vtks, vtktg) =
+ SELECT
+ (vtks : BOOL) &
+ (vtktg : BOOL) &
+ (vtks = TRUE
+ or vtktg = TRUE
+ or ObstacleStatusJustChanged = TRUE
+ or CCInitialisationInProgress = TRUE) &
+ (ObstaclePresent = FALSE => vtktg = FALSE) &
+ (ObstacleDistance = ODnone => vtks = TRUE) &
+ ((ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed /= RSpos &
+ ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE)
+ => vtktg = TRUE) &
+ ((ObstacleDistance = ODveryclose &
+ ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE)
+ => vtktg = TRUE) &
+ ((ObstacleRelativeSpeed = RSpos &
+ ObstacleDistance /= ODveryclose&
+ ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE)
+ => vtks = TRUE) &
+ ((ObstacleRelativeSpeed = RSequal & ObstacleDistance = ODnone)
+ => vtktg = FALSE) &
+ ((ObstacleRelativeSpeed = RSneg & ObstacleDistance = ODnone)
+ => vtktg = FALSE) &
+ ((ObstacleRelativeSpeed = RSpos & ObstacleDistance /= ODveryclose)
+ => vtktg = FALSE) &
+ CruiseSpeedChangeInProgress = TRUE
+ THEN
+
+ VehicleTryKeepTimeGap := vtktg ||
+ VehicleTryKeepSpeed := vtks
+ END;
+
+
+ CruiseSpeedChangeDelayFinished =
+ SELECT
+ CruiseSpeedChangeInProgress = TRUE &
+ (VehicleTryKeepSpeed = TRUE
+ or VehicleTryKeepTimeGap = TRUE
+ or ObstacleStatusJustChanged = TRUE
+ or CCInitialisationInProgress = TRUE) &
+ (ObstacleDistance = ODnone => VehicleTryKeepSpeed = TRUE) &
+ ((ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed /= RSpos &
+ ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE )
+ => (VehicleTryKeepTimeGap = TRUE)) &
+ ((ObstacleDistance = ODveryclose &
+ ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE)
+ => VehicleTryKeepTimeGap = TRUE) &
+ ((ObstacleRelativeSpeed = RSpos &
+ ObstacleDistance /= ODveryclose &
+ ObstacleStatusJustChanged = FALSE &
+ CCInitialisationInProgress = FALSE)
+ => VehicleTryKeepSpeed = TRUE)
+ THEN
+ CruiseSpeedChangeInProgress := TRUE
+ END;
+
+
+ CruiseOff =
+ SELECT
+ CruiseActive = TRUE
+ THEN
+ CruiseActive := FALSE ||
+ VehicleCanKeepSpeed := FALSE ||
+ VehicleTryKeepSpeed := FALSE ||
+ VehicleAtCruiseSpeed := FALSE ||
+ VehicleTryKeepTimeGap := FALSE ||
+ CruiseSpeedAtMax := FALSE ||
+ ObstacleDistance := ODnone ||
+ NumberOfSetCruise := 0 ||
+ ObstacleStatusJustChanged := FALSE ||
+ CCInitialisationInProgress := FALSE ||
+ CruiseSpeedChangeInProgress := FALSE
+ END;
+
+
+ ExternalForcesBecomesExtreme = SELECT
+ VehicleCanKeepSpeed = TRUE
+ THEN
+ VehicleCanKeepSpeed := FALSE
+ END;
+
+
+ ExternalForcesBecomesNormal = SELECT
+ CruiseActive = TRUE &
+ VehicleCanKeepSpeed = FALSE
+ THEN
+ VehicleCanKeepSpeed := TRUE
+ END;
+
+
+ VehicleLeavesCruiseSpeed =
+ SELECT
+ VehicleAtCruiseSpeed = TRUE &
+ (VehicleCanKeepSpeed = FALSE & VehicleTryKeepSpeed = TRUE) or
+ (VehicleTryKeepSpeed = FALSE)
+ THEN
+ VehicleAtCruiseSpeed := FALSE
+ END;
+
+
+ VehicleReachesCruiseSpeed = SELECT
+ CruiseActive = TRUE &
+ VehicleAtCruiseSpeed = FALSE &
+ SpeedAboveMax = FALSE
+ THEN
+ VehicleAtCruiseSpeed := TRUE
+ END;
+
+
+ VehicleExceedsMaxCruiseSpeed = SELECT
+ SpeedAboveMax = FALSE &
+ (CruiseActive = FALSE
+ or VehicleCanKeepSpeed = FALSE
+ or ((ObstacleStatusJustChanged = FALSE & CCInitialisationInProgress = FALSE & CruiseSpeedChangeInProgress = FALSE)))
+ THEN
+ SpeedAboveMax := TRUE ||
+ VehicleAtCruiseSpeed := FALSE
+ END;
+
+
+ VehicleFallsBelowMaxCruiseSpeed = SELECT
+ SpeedAboveMax = TRUE
+ THEN
+ SpeedAboveMax := FALSE ||
+ IF (CruiseActive=TRUE) & (CruiseSpeedAtMax = TRUE) THEN
+ VehicleAtCruiseSpeed := TRUE
+ END
+ END;
+
+ ObstacleDistanceBecomesVeryClose = SELECT
+ ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed = RSneg
+ THEN
+ ObstacleDistance := ODveryclose ||
+ ObstacleStatusJustChanged := TRUE
+ END;
+
+ ObstacleDistanceBecomesClose = SELECT
+ ObstaclePresent = TRUE &
+ CruiseActive = TRUE &
+ ((ObstacleDistance = ODveryclose & ObstacleRelativeSpeed = RSpos)
+ or (ObstacleDistance = ODnone & ObstacleRelativeSpeed = RSneg))
+ THEN
+ ObstacleDistance := ODclose ||
+ ObstacleStatusJustChanged := TRUE ||
+ IF (ObstacleRelativeSpeed = RSpos) THEN
+ VehicleTryKeepTimeGap := FALSE
+ END
+ END;
+
+ ObstacleDistanceBecomesBig = SELECT
+ ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed = RSpos
+ THEN
+ ObstacleStatusJustChanged := TRUE ||
+ ObstacleDistance := ODnone ||
+ VehicleTryKeepTimeGap:= FALSE
+ END;
+
+
+ ObstacleStartsTravelFaster = SELECT
+ ObstaclePresent = TRUE &
+ ObstacleRelativeSpeed = RSequal
+ THEN
+ ObstacleRelativeSpeed := RSpos ||
+ IF CruiseActive = TRUE THEN
+ ObstacleStatusJustChanged := TRUE
+ END ||
+ IF (ObstacleDistance/=ODveryclose) THEN
+ VehicleTryKeepTimeGap:=FALSE
+ END
+ END;
+
+ ObstacleStopsTravelFaster = SELECT
+ ObstacleRelativeSpeed = RSpos
+ THEN
+ ObstacleRelativeSpeed := RSequal ||
+ IF CruiseActive = TRUE THEN
+ ObstacleStatusJustChanged := TRUE
+ END
+ END;
+
+
+ ObstacleStartsTravelSlower = SELECT
+ ObstacleRelativeSpeed = RSequal
+ THEN
+ ObstacleRelativeSpeed := RSneg ||
+ IF CruiseActive = TRUE THEN
+ ObstacleStatusJustChanged := TRUE
+ END
+ END;
+
+
+ ObstacleStopsTravelSlower = SELECT
+ ObstacleRelativeSpeed = RSneg
+ THEN
+ ObstacleRelativeSpeed := RSequal ||
+ IF CruiseActive = TRUE THEN
+ ObstacleStatusJustChanged := TRUE
+ END
+ END;
+
+
+ ObstacleAppearsWhenCruiseActive(ors, od) =
+ PRE ors : RSset - {RSnone} & od : ODset - {ODnone} & ObstaclePresent = FALSE & CruiseActive = TRUE THEN
+ ObstaclePresent := TRUE ||
+ ObstacleStatusJustChanged := TRUE ||
+ ObstacleRelativeSpeed := ors ||
+ ObstacleDistance := od
+ END;
+
+
+ ObstacleAppearsWhenCruiseInactive(ors) =
+ PRE ors : RSset - {RSnone} & ObstaclePresent = FALSE & CruiseActive = FALSE THEN
+ ObstaclePresent := TRUE ||
+ ObstacleRelativeSpeed := ors ||
+ ObstacleDistance := ODnone
+ END;
+
+ ObstacleDisappears = SELECT
+ ObstaclePresent = TRUE
+ THEN
+ ObstaclePresent := FALSE ||
+ ObstacleRelativeSpeed := RSnone ||
+ IF CruiseActive = TRUE THEN
+ ObstacleStatusJustChanged := TRUE
+ END ||
+ ObstacleDistance := ODnone ||
+ VehicleTryKeepTimeGap := FALSE
+ END;
+
+
+ VehicleManageObstacle(vtks, vtktg) =
+ SELECT
+ (vtks : BOOL) &
+ (vtktg : BOOL) &
+ (vtks = TRUE
+ or vtktg = TRUE
+ or CCInitialisationInProgress = TRUE
+ or CruiseSpeedChangeInProgress = TRUE) &
+ (ObstaclePresent = FALSE => vtktg = FALSE) &
+ (ObstacleDistance = ODnone => vtks = TRUE) &
+ ((ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed /= RSpos &
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => vtktg = TRUE) &
+ ((ObstacleDistance = ODveryclose &
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => vtktg = TRUE) &
+ ((ObstacleRelativeSpeed = RSpos &
+ ObstacleDistance /= ODveryclose&
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => vtks = TRUE) &
+ ((ObstacleRelativeSpeed = RSequal & ObstacleDistance = ODnone)
+ => vtktg = FALSE) &
+ ((ObstacleRelativeSpeed = RSneg & ObstacleDistance = ODnone)
+ => vtktg = FALSE) &
+ ((ObstacleRelativeSpeed = RSpos & ObstacleDistance /= ODveryclose)
+ => vtktg = FALSE) &
+ ObstacleStatusJustChanged = TRUE
+
+ THEN
+ VehicleTryKeepTimeGap := vtktg ||
+ VehicleTryKeepSpeed := vtks
+
+ END;
+
+
+ ObstacleBecomesOld =
+ SELECT
+ ObstacleStatusJustChanged = TRUE &
+ (VehicleTryKeepSpeed = TRUE
+ or VehicleTryKeepTimeGap = TRUE
+ or CCInitialisationInProgress = TRUE
+ or CruiseSpeedChangeInProgress = TRUE) &
+ (ObstacleDistance = ODnone => VehicleTryKeepSpeed = TRUE) &
+ ((ObstacleDistance = ODclose &
+ ObstacleRelativeSpeed /= RSpos &
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE )
+ => (VehicleTryKeepTimeGap = TRUE)) &
+ ((ObstacleDistance = ODveryclose &
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepTimeGap = TRUE) &
+ ((ObstacleRelativeSpeed = RSpos &
+ ObstacleDistance /= ODveryclose &
+ CCInitialisationInProgress = FALSE &
+ CruiseSpeedChangeInProgress = FALSE)
+ => VehicleTryKeepSpeed = TRUE)
+ THEN
+ ObstacleStatusJustChanged:= FALSE
+ END
+
+END
+/*
+CTL:
+ e(b(\'SetCruiseSpeed\'/0))
+ ef(and(e(b(\'SetCruiseSpeed\'/0)),not(e(b(\'CruiseBecomesNotAllowed\'/0)))))
+
+ProB: has explored all states (1360 states)
+No invariant violation or deadlock found
+
+Coverage:
+COVERED_OPERATIONS
+initialise_machine:4
+ObstacleAppearsWhenCruiseInactive:12
+CruiseBecomesAllowed:8
+ObstacleAppearsWhenCruiseActive:432
+ObstacleDistanceBecomesBig:96
+VehicleManageObstacle:2208
+ObstacleBecomesOld:624
+ObstacleDistanceBecomesClose:264
+CruiseSpeedChangeFinished:2160
+CruiseSpeedChangeDelayFinished:624
+VehicleLeavesCruiseSpeed:760
+ObstacleStartsTravelFaster:460
+ObstacleStartsTravelSlower:460
+ExternalForcesBecomesNormal:672
+VehicleFallsBelowMaxCruiseSpeed:456
+ObstacleDistanceBecomesVeryClose:192
+ObstacleStopsTravelSlower:460
+CruiseBecomesNotAllowed:1352
+SetCruiseSpeed:4504
+CCInitialisationFinished:3816
+CCInitialisationDelayFinished:1116
+CruiseOff:1344
+ExternalForcesBecomesExtreme:672
+VehicleReachesCruiseSpeed:448
+VehicleExceedsMaxCruiseSpeed:904
+ObstacleStopsTravelFaster:364
+ObstacleDisappears:1284
+UNCOVERED_OPERATIONS
+-none-
+
+
+*/
\ No newline at end of file
diff --git a/Beispiele/LandingGear_R6.java b/Beispiele/LandingGear_R6.java
new file mode 100644
index 0000000000000000000000000000000000000000..720a831b66eb536eefcc2ec40c16c06fc0f89f38
--- /dev/null
+++ b/Beispiele/LandingGear_R6.java
@@ -0,0 +1,832 @@
+import de.hhu.stups.btypes.BRelation;
+import de.hhu.stups.btypes.BTuple;
+import de.hhu.stups.btypes.BSet;
+import de.hhu.stups.btypes.BObject;
+import de.hhu.stups.btypes.BBoolean;
+import java.util.Objects;
+import java.util.Arrays;
+import de.hhu.stups.btypes.BUtils;
+
+
+public class LandingGear_R6 {
+
+ public enum DOOR_STATE implements BObject {
+ open,
+ closed,
+ door_moving;
+
+ public BBoolean equal(DOOR_STATE o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(DOOR_STATE o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum GEAR_STATE implements BObject {
+ retracted,
+ extended,
+ gear_moving;
+
+ public BBoolean equal(GEAR_STATE o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(GEAR_STATE o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum HANDLE_STATE implements BObject {
+ up,
+ down;
+
+ public BBoolean equal(HANDLE_STATE o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(HANDLE_STATE o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum POSITION implements BObject {
+ fr,
+ lt,
+ rt;
+
+ public BBoolean equal(POSITION o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(POSITION o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum SWITCH_STATE implements BObject {
+ switch_open,
+ switch_closed;
+
+ public BBoolean equal(SWITCH_STATE o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(SWITCH_STATE o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum PLANE_STATE implements BObject {
+ ground,
+ flight;
+
+ public BBoolean equal(PLANE_STATE o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(PLANE_STATE o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum VALVE_STATE implements BObject {
+ valve_open,
+ valve_closed;
+
+ public BBoolean equal(VALVE_STATE o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(VALVE_STATE o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ private static BSet<DOOR_STATE> _DOOR_STATE = new BSet<DOOR_STATE>(DOOR_STATE.open, DOOR_STATE.closed, DOOR_STATE.door_moving);
+ private static BSet<GEAR_STATE> _GEAR_STATE = new BSet<GEAR_STATE>(GEAR_STATE.retracted, GEAR_STATE.extended, GEAR_STATE.gear_moving);
+ private static BSet<HANDLE_STATE> _HANDLE_STATE = new BSet<HANDLE_STATE>(HANDLE_STATE.up, HANDLE_STATE.down);
+ private static BSet<POSITION> _POSITION = new BSet<POSITION>(POSITION.fr, POSITION.lt, POSITION.rt);
+ private static BSet<SWITCH_STATE> _SWITCH_STATE = new BSet<SWITCH_STATE>(SWITCH_STATE.switch_open, SWITCH_STATE.switch_closed);
+ private static BSet<PLANE_STATE> _PLANE_STATE = new BSet<PLANE_STATE>(PLANE_STATE.ground, PLANE_STATE.flight);
+ private static BSet<VALVE_STATE> _VALVE_STATE = new BSet<VALVE_STATE>(VALVE_STATE.valve_open, VALVE_STATE.valve_closed);
+
+ private SWITCH_STATE analogical_switch;
+ private BBoolean general_EV;
+ private VALVE_STATE general_valve;
+ private BBoolean handle_move;
+ private BBoolean close_EV;
+ private BBoolean extend_EV;
+ private BBoolean open_EV;
+ private BBoolean retract_EV;
+ private PLANE_STATE shock_absorber;
+ private VALVE_STATE valve_close_door;
+ private VALVE_STATE valve_extend_gear;
+ private VALVE_STATE valve_open_door;
+ private VALVE_STATE valve_retract_gear;
+ private BRelation<POSITION, DOOR_STATE> doors;
+ private BRelation<POSITION, GEAR_STATE> gears;
+ private HANDLE_STATE handle;
+ private DOOR_STATE door;
+ private GEAR_STATE gear;
+
+ public LandingGear_R6() {
+ gears = BRelation.cartesianProduct(_POSITION, new BSet<GEAR_STATE>(GEAR_STATE.extended));
+ doors = BRelation.cartesianProduct(_POSITION, new BSet<DOOR_STATE>(DOOR_STATE.closed));
+ handle = HANDLE_STATE.down;
+ valve_extend_gear = VALVE_STATE.valve_closed;
+ valve_retract_gear = VALVE_STATE.valve_closed;
+ valve_open_door = VALVE_STATE.valve_closed;
+ valve_close_door = VALVE_STATE.valve_closed;
+ open_EV = new BBoolean(false);
+ close_EV = new BBoolean(false);
+ retract_EV = new BBoolean(false);
+ extend_EV = new BBoolean(false);
+ shock_absorber = PLANE_STATE.ground;
+ general_EV = new BBoolean(false);
+ general_valve = VALVE_STATE.valve_closed;
+ analogical_switch = SWITCH_STATE.switch_open;
+ handle_move = new BBoolean(false);
+ gear = GEAR_STATE.extended;
+ door = DOOR_STATE.closed;
+ }
+
+ public LandingGear_R6(SWITCH_STATE analogical_switch, BBoolean general_EV, VALVE_STATE general_valve, BBoolean handle_move, BBoolean close_EV, BBoolean extend_EV, BBoolean open_EV, BBoolean retract_EV, PLANE_STATE shock_absorber, VALVE_STATE valve_close_door, VALVE_STATE valve_extend_gear, VALVE_STATE valve_open_door, VALVE_STATE valve_retract_gear, BRelation<POSITION, DOOR_STATE> doors, BRelation<POSITION, GEAR_STATE> gears, HANDLE_STATE handle, DOOR_STATE door, GEAR_STATE gear) {
+ this.analogical_switch = analogical_switch;
+ this.general_EV = general_EV;
+ this.general_valve = general_valve;
+ this.handle_move = handle_move;
+ this.close_EV = close_EV;
+ this.extend_EV = extend_EV;
+ this.open_EV = open_EV;
+ this.retract_EV = retract_EV;
+ this.shock_absorber = shock_absorber;
+ this.valve_close_door = valve_close_door;
+ this.valve_extend_gear = valve_extend_gear;
+ this.valve_open_door = valve_open_door;
+ this.valve_retract_gear = valve_retract_gear;
+ this.doors = doors;
+ this.gears = gears;
+ this.handle = handle;
+ this.door = door;
+ this.gear = gear;
+ }
+
+ public void begin_flying() {
+ shock_absorber = PLANE_STATE.flight;
+
+ }
+
+ public void land_plane() {
+ shock_absorber = PLANE_STATE.ground;
+
+ }
+
+ public void open_valve_door_open() {
+ valve_open_door = VALVE_STATE.valve_open;
+
+ }
+
+ public void close_valve_door_open() {
+ valve_open_door = VALVE_STATE.valve_closed;
+
+ }
+
+ public void open_valve_door_close() {
+ valve_close_door = VALVE_STATE.valve_open;
+
+ }
+
+ public void close_valve_door_close() {
+ valve_close_door = VALVE_STATE.valve_closed;
+
+ }
+
+ public void open_valve_retract_gear() {
+ valve_retract_gear = VALVE_STATE.valve_open;
+
+ }
+
+ public void close_valve_retract_gear() {
+ valve_retract_gear = VALVE_STATE.valve_closed;
+
+ }
+
+ public void open_valve_extend_gear() {
+ valve_extend_gear = VALVE_STATE.valve_open;
+
+ }
+
+ public void close_valve_extend_gear() {
+ valve_extend_gear = VALVE_STATE.valve_closed;
+
+ }
+
+ public void con_stimulate_open_door_valve() {
+ open_EV = new BBoolean(true);
+
+ }
+
+ public void con_stop_stimulate_open_door_valve() {
+ open_EV = new BBoolean(false);
+
+ }
+
+ public void con_stimulate_close_door_valve() {
+ close_EV = new BBoolean(true);
+
+ }
+
+ public void con_stop_stimulate_close_door_valve() {
+ close_EV = new BBoolean(false);
+
+ }
+
+ public void con_stimulate_retract_gear_valve() {
+ retract_EV = new BBoolean(true);
+
+ }
+
+ public void con_stop_stimulate_retract_gear_valve() {
+ retract_EV = new BBoolean(false);
+
+ }
+
+ public void con_stimulate_extend_gear_valve() {
+ extend_EV = new BBoolean(true);
+
+ }
+
+ public void con_stop_stimulate_extend_gear_valve() {
+ extend_EV = new BBoolean(false);
+
+ }
+
+ public void env_start_retracting_first(POSITION gr) {
+ BRelation<POSITION, GEAR_STATE> _ld_gears = gears;
+ gears = _ld_gears.override(new BRelation<POSITION, GEAR_STATE>(new BTuple<>(gr, GEAR_STATE.gear_moving)));
+ gear = GEAR_STATE.gear_moving;
+
+ }
+
+ public void env_retract_gear_skip(POSITION gr) {
+ gears = gears.override(new BRelation<POSITION, GEAR_STATE>(new BTuple<>(gr, GEAR_STATE.retracted)));
+
+ }
+
+ public void env_retract_gear_last(POSITION gr) {
+ BRelation<POSITION, GEAR_STATE> _ld_gears = gears;
+ gears = _ld_gears.override(new BRelation<POSITION, GEAR_STATE>(new BTuple<>(gr, GEAR_STATE.retracted)));
+ gear = GEAR_STATE.retracted;
+
+ }
+
+ public void env_start_extending(POSITION gr) {
+ BRelation<POSITION, GEAR_STATE> _ld_gears = gears;
+ gears = _ld_gears.override(new BRelation<POSITION, GEAR_STATE>(new BTuple<>(gr, GEAR_STATE.gear_moving)));
+ gear = GEAR_STATE.gear_moving;
+
+ }
+
+ public void env_extend_gear_last(POSITION gr) {
+ BRelation<POSITION, GEAR_STATE> _ld_gears = gears;
+ gears = _ld_gears.override(new BRelation<POSITION, GEAR_STATE>(new BTuple<>(gr, GEAR_STATE.extended)));
+ gear = GEAR_STATE.extended;
+
+ }
+
+ public void env_extend_gear_skip(POSITION gr) {
+ gears = gears.override(new BRelation<POSITION, GEAR_STATE>(new BTuple<>(gr, GEAR_STATE.extended)));
+
+ }
+
+ public void env_start_open_door(POSITION gr) {
+ BRelation<POSITION, DOOR_STATE> _ld_doors = doors;
+ doors = _ld_doors.override(new BRelation<POSITION, DOOR_STATE>(new BTuple<>(gr, DOOR_STATE.door_moving)));
+ door = DOOR_STATE.door_moving;
+
+ }
+
+ public void env_open_door_last(POSITION gr) {
+ BRelation<POSITION, DOOR_STATE> _ld_doors = doors;
+ doors = _ld_doors.override(new BRelation<POSITION, DOOR_STATE>(new BTuple<>(gr, DOOR_STATE.open)));
+ door = DOOR_STATE.open;
+
+ }
+
+ public void env_open_door_skip(POSITION gr) {
+ doors = doors.override(new BRelation<POSITION, DOOR_STATE>(new BTuple<>(gr, DOOR_STATE.open)));
+
+ }
+
+ public void env_start_close_door(POSITION gr) {
+ BRelation<POSITION, DOOR_STATE> _ld_doors = doors;
+ doors = _ld_doors.override(new BRelation<POSITION, DOOR_STATE>(new BTuple<>(gr, DOOR_STATE.door_moving)));
+ door = DOOR_STATE.door_moving;
+
+ }
+
+ public void env_close_door(POSITION gr) {
+ BRelation<POSITION, DOOR_STATE> _ld_doors = doors;
+ doors = _ld_doors.override(new BRelation<POSITION, DOOR_STATE>(new BTuple<>(gr, DOOR_STATE.closed)));
+ door = DOOR_STATE.closed;
+
+ }
+
+ public void env_close_door_skip(POSITION gr) {
+ doors = doors.override(new BRelation<POSITION, DOOR_STATE>(new BTuple<>(gr, DOOR_STATE.closed)));
+
+ }
+
+ public void toggle_handle_up() {
+ handle = HANDLE_STATE.up;
+ handle_move = new BBoolean(true);
+
+ }
+
+ public void toggle_handle_down() {
+ handle = HANDLE_STATE.down;
+ handle_move = new BBoolean(true);
+
+ }
+
+ public void con_stimulate_general_valve() {
+ general_EV = new BBoolean(true);
+
+ }
+
+ public void con_stop_stimulate_general_valve() {
+ general_EV = new BBoolean(false);
+ handle_move = new BBoolean(false);
+
+ }
+
+ public void evn_open_general_valve() {
+ general_valve = VALVE_STATE.valve_open;
+
+ }
+
+ public void evn_close_general_valve() {
+ general_valve = VALVE_STATE.valve_closed;
+
+ }
+
+ public void env_close_analogical_switch() {
+ analogical_switch = SWITCH_STATE.switch_closed;
+
+ }
+
+ public void env_open_analogical_switch() {
+ analogical_switch = SWITCH_STATE.switch_open;
+
+ }
+
+ public SWITCH_STATE _get_analogical_switch() {
+ return analogical_switch;
+ }
+
+ public BBoolean _get_general_EV() {
+ return general_EV;
+ }
+
+ public VALVE_STATE _get_general_valve() {
+ return general_valve;
+ }
+
+ public BBoolean _get_handle_move() {
+ return handle_move;
+ }
+
+ public BBoolean _get_close_EV() {
+ return close_EV;
+ }
+
+ public BBoolean _get_extend_EV() {
+ return extend_EV;
+ }
+
+ public BBoolean _get_open_EV() {
+ return open_EV;
+ }
+
+ public BBoolean _get_retract_EV() {
+ return retract_EV;
+ }
+
+ public PLANE_STATE _get_shock_absorber() {
+ return shock_absorber;
+ }
+
+ public VALVE_STATE _get_valve_close_door() {
+ return valve_close_door;
+ }
+
+ public VALVE_STATE _get_valve_extend_gear() {
+ return valve_extend_gear;
+ }
+
+ public VALVE_STATE _get_valve_open_door() {
+ return valve_open_door;
+ }
+
+ public VALVE_STATE _get_valve_retract_gear() {
+ return valve_retract_gear;
+ }
+
+ public BRelation<POSITION, DOOR_STATE> _get_doors() {
+ return doors;
+ }
+
+ public BRelation<POSITION, GEAR_STATE> _get_gears() {
+ return gears;
+ }
+
+ public HANDLE_STATE _get_handle() {
+ return handle;
+ }
+
+ public DOOR_STATE _get_door() {
+ return door;
+ }
+
+ public GEAR_STATE _get_gear() {
+ return gear;
+ }
+
+ public BSet<DOOR_STATE> _get__DOOR_STATE() {
+ return _DOOR_STATE;
+ }
+
+ public BSet<GEAR_STATE> _get__GEAR_STATE() {
+ return _GEAR_STATE;
+ }
+
+ public BSet<HANDLE_STATE> _get__HANDLE_STATE() {
+ return _HANDLE_STATE;
+ }
+
+ public BSet<POSITION> _get__POSITION() {
+ return _POSITION;
+ }
+
+ public BSet<SWITCH_STATE> _get__SWITCH_STATE() {
+ return _SWITCH_STATE;
+ }
+
+ public BSet<PLANE_STATE> _get__PLANE_STATE() {
+ return _PLANE_STATE;
+ }
+
+ public BSet<VALVE_STATE> _get__VALVE_STATE() {
+ return _VALVE_STATE;
+ }
+
+
+ public boolean _tr_begin_flying() {
+ return shock_absorber.equal(PLANE_STATE.ground).booleanValue();
+ }
+
+ public boolean _tr_land_plane() {
+ return shock_absorber.equal(PLANE_STATE.flight).booleanValue();
+ }
+
+ public boolean _tr_open_valve_door_open() {
+ return new BBoolean(valve_open_door.equal(VALVE_STATE.valve_closed).booleanValue() && open_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_close_valve_door_open() {
+ return new BBoolean(valve_open_door.equal(VALVE_STATE.valve_open).booleanValue() && open_EV.equal(new BBoolean(false)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_open_valve_door_close() {
+ return new BBoolean(valve_close_door.equal(VALVE_STATE.valve_closed).booleanValue() && close_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_close_valve_door_close() {
+ return new BBoolean(valve_close_door.equal(VALVE_STATE.valve_open).booleanValue() && close_EV.equal(new BBoolean(false)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_open_valve_retract_gear() {
+ return new BBoolean(valve_retract_gear.equal(VALVE_STATE.valve_closed).booleanValue() && retract_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_close_valve_retract_gear() {
+ return new BBoolean(valve_retract_gear.equal(VALVE_STATE.valve_open).booleanValue() && retract_EV.equal(new BBoolean(false)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_open_valve_extend_gear() {
+ return new BBoolean(valve_extend_gear.equal(VALVE_STATE.valve_closed).booleanValue() && extend_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_close_valve_extend_gear() {
+ return new BBoolean(valve_extend_gear.equal(VALVE_STATE.valve_open).booleanValue() && extend_EV.equal(new BBoolean(false)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stimulate_open_door_valve() {
+ return new BBoolean(new BBoolean(new BBoolean(open_EV.equal(new BBoolean(false)).booleanValue() && close_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).not().booleanValue()).booleanValue() || new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).not().booleanValue()).booleanValue() && new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && shock_absorber.equal(PLANE_STATE.ground).booleanValue()).not().booleanValue()).booleanValue()).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stop_stimulate_open_door_valve() {
+ return new BBoolean(new BBoolean(new BBoolean(new BBoolean(open_EV.equal(new BBoolean(true)).booleanValue() && extend_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && retract_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() || new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BBoolean(gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || shock_absorber.equal(PLANE_STATE.ground).booleanValue()).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stimulate_close_door_valve() {
+ return new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(close_EV.equal(new BBoolean(false)).booleanValue() && open_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && extend_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && retract_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BBoolean(gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || shock_absorber.equal(PLANE_STATE.ground).booleanValue()).booleanValue()).booleanValue()).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).not().booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stop_stimulate_close_door_valve() {
+ return new BBoolean(new BBoolean(close_EV.equal(new BBoolean(true)).booleanValue() && new BBoolean(new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue() || new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BBoolean(gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || shock_absorber.equal(PLANE_STATE.ground).booleanValue()).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stimulate_retract_gear_valve() {
+ return new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(retract_EV.equal(new BBoolean(false)).booleanValue() && extend_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && open_EV.equal(new BBoolean(true)).booleanValue()).booleanValue() && handle.equal(HANDLE_STATE.up).booleanValue()).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).not().booleanValue()).booleanValue() && shock_absorber.equal(PLANE_STATE.flight).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stop_stimulate_retract_gear_valve() {
+ return new BBoolean(new BBoolean(retract_EV.equal(new BBoolean(true)).booleanValue() && new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stimulate_extend_gear_valve() {
+ return new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(extend_EV.equal(new BBoolean(false)).booleanValue() && retract_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && open_EV.equal(new BBoolean(true)).booleanValue()).booleanValue() && handle.equal(HANDLE_STATE.down).booleanValue()).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).not().booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stop_stimulate_extend_gear_valve() {
+ return new BBoolean(new BBoolean(extend_EV.equal(new BBoolean(true)).booleanValue() && new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue() && general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public BSet<POSITION> _tr_env_start_retracting_first() {
+ BSet<POSITION> _ic_set_18 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && handle.equal(HANDLE_STATE.up).booleanValue()).booleanValue() && gears.functionCall(_ic_gr_1).equal(GEAR_STATE.extended).booleanValue()).booleanValue() && valve_retract_gear.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && new BSet<GEAR_STATE>(GEAR_STATE.extended, GEAR_STATE.gear_moving).elementOf(gear).booleanValue()).booleanValue() && door.equal(DOOR_STATE.open).booleanValue())).booleanValue()) {
+ _ic_set_18 = _ic_set_18.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_18;
+ }
+
+ public BSet<POSITION> _tr_env_retract_gear_skip() {
+ BSet<POSITION> _ic_set_19 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && gears.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).unequal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue() && handle.equal(HANDLE_STATE.up).booleanValue()).booleanValue() && gears.functionCall(_ic_gr_1).equal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue())).booleanValue()) {
+ _ic_set_19 = _ic_set_19.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_19;
+ }
+
+ public BSet<POSITION> _tr_env_retract_gear_last() {
+ BSet<POSITION> _ic_set_20 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && gears.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue() && handle.equal(HANDLE_STATE.up).booleanValue()).booleanValue() && gears.functionCall(_ic_gr_1).equal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && gear.equal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && door.equal(DOOR_STATE.open).booleanValue())).booleanValue()) {
+ _ic_set_20 = _ic_set_20.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_20;
+ }
+
+ public BSet<POSITION> _tr_env_start_extending() {
+ BSet<POSITION> _ic_set_21 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && handle.equal(HANDLE_STATE.down).booleanValue()).booleanValue() && gears.functionCall(_ic_gr_1).equal(GEAR_STATE.retracted).booleanValue()).booleanValue() && valve_extend_gear.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && new BSet<GEAR_STATE>(GEAR_STATE.gear_moving, GEAR_STATE.retracted).elementOf(gear).booleanValue()).booleanValue() && door.equal(DOOR_STATE.open).booleanValue())).booleanValue()) {
+ _ic_set_21 = _ic_set_21.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_21;
+ }
+
+ public BSet<POSITION> _tr_env_extend_gear_last() {
+ BSet<POSITION> _ic_set_22 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && handle.equal(HANDLE_STATE.down).booleanValue()).booleanValue() && gears.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() && gears.functionCall(_ic_gr_1).equal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && gear.equal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && door.equal(DOOR_STATE.open).booleanValue())).booleanValue()) {
+ _ic_set_22 = _ic_set_22.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_22;
+ }
+
+ public BSet<POSITION> _tr_env_extend_gear_skip() {
+ BSet<POSITION> _ic_set_23 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() && handle.equal(HANDLE_STATE.down).booleanValue()).booleanValue() && gears.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).unequal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() && gears.functionCall(_ic_gr_1).equal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue())).booleanValue()) {
+ _ic_set_23 = _ic_set_23.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_23;
+ }
+
+ public BSet<POSITION> _tr_env_start_open_door() {
+ BSet<POSITION> _ic_set_24 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.functionCall(_ic_gr_1).equal(DOOR_STATE.closed).booleanValue() && gears.functionCall(_ic_gr_1).unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && gears.range().notElementOf(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && valve_open_door.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && new BSet<DOOR_STATE>(DOOR_STATE.closed, DOOR_STATE.door_moving).elementOf(door).booleanValue()).booleanValue() && gear.unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gear.equal(GEAR_STATE.retracted).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gear.equal(GEAR_STATE.extended).booleanValue()).booleanValue()).booleanValue())).booleanValue()) {
+ _ic_set_24 = _ic_set_24.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_24;
+ }
+
+ public BSet<POSITION> _tr_env_open_door_last() {
+ BSet<POSITION> _ic_set_25 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.functionCall(_ic_gr_1).equal(DOOR_STATE.door_moving).booleanValue() && gears.functionCall(_ic_gr_1).unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && gears.range().notElementOf(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && doors.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && valve_open_door.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && door.equal(DOOR_STATE.door_moving).booleanValue()).booleanValue() && gear.unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gear.equal(GEAR_STATE.retracted).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gear.equal(GEAR_STATE.extended).booleanValue()).booleanValue()).booleanValue())).booleanValue()) {
+ _ic_set_25 = _ic_set_25.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_25;
+ }
+
+ public BSet<POSITION> _tr_env_open_door_skip() {
+ BSet<POSITION> _ic_set_26 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.functionCall(_ic_gr_1).equal(DOOR_STATE.door_moving).booleanValue() && gears.functionCall(_ic_gr_1).unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && gears.range().notElementOf(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && doors.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).unequal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && valve_open_door.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue())).booleanValue()) {
+ _ic_set_26 = _ic_set_26.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_26;
+ }
+
+ public BSet<POSITION> _tr_env_start_close_door() {
+ BSet<POSITION> _ic_set_27 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.functionCall(_ic_gr_1).equal(DOOR_STATE.open).booleanValue() && gears.functionCall(_ic_gr_1).unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BBoolean(gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && valve_close_door.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && new BSet<DOOR_STATE>(DOOR_STATE.door_moving, DOOR_STATE.open).elementOf(door).booleanValue()).booleanValue() && gear.unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gear.equal(GEAR_STATE.extended).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BSet<GEAR_STATE>(GEAR_STATE.extended, GEAR_STATE.retracted).elementOf(gear).booleanValue()).booleanValue()).booleanValue())).booleanValue()) {
+ _ic_set_27 = _ic_set_27.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_27;
+ }
+
+ public BSet<POSITION> _tr_env_close_door() {
+ BSet<POSITION> _ic_set_28 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.functionCall(_ic_gr_1).equal(DOOR_STATE.door_moving).booleanValue() && gears.functionCall(_ic_gr_1).unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && gears.range().notElementOf(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && doors.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BBoolean(gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && valve_close_door.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && new BBoolean(!new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() || shock_absorber.equal(PLANE_STATE.ground).booleanValue()).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && door.equal(DOOR_STATE.door_moving).booleanValue()).booleanValue() && gear.unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gear.equal(GEAR_STATE.extended).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BSet<GEAR_STATE>(GEAR_STATE.extended, GEAR_STATE.retracted).elementOf(gear).booleanValue()).booleanValue()).booleanValue())).booleanValue()) {
+ _ic_set_28 = _ic_set_28.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_28;
+ }
+
+ public BSet<POSITION> _tr_env_close_door_skip() {
+ BSet<POSITION> _ic_set_29 = new BSet<POSITION>();
+ for(POSITION _ic_gr_1 : gears.domain()) {
+ if((new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(doors.functionCall(_ic_gr_1).equal(DOOR_STATE.door_moving).booleanValue() && gears.functionCall(_ic_gr_1).unequal(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && gears.range().notElementOf(GEAR_STATE.gear_moving).booleanValue()).booleanValue() && doors.relationImage(_POSITION.difference(new BSet<POSITION>(_ic_gr_1))).unequal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && new BBoolean(gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue() || new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue()).booleanValue()).booleanValue() && valve_close_door.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue() && new BBoolean(!new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() || shock_absorber.equal(PLANE_STATE.ground).booleanValue()).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue())).booleanValue()) {
+ _ic_set_29 = _ic_set_29.union(new BSet<POSITION>(_ic_gr_1));
+ }
+
+ }
+ return _ic_set_29;
+ }
+
+ public boolean _tr_toggle_handle_up() {
+ return handle.equal(HANDLE_STATE.down).booleanValue();
+ }
+
+ public boolean _tr_toggle_handle_down() {
+ return handle.equal(HANDLE_STATE.up).booleanValue();
+ }
+
+ public boolean _tr_con_stimulate_general_valve() {
+ return new BBoolean(general_EV.equal(new BBoolean(false)).booleanValue() && handle_move.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_con_stop_stimulate_general_valve() {
+ return new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(general_EV.equal(new BBoolean(true)).booleanValue() && open_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && close_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && retract_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && extend_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && close_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() && new BBoolean(new BBoolean(new BBoolean(new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue() && open_EV.equal(new BBoolean(false)).booleanValue()).booleanValue() || new BBoolean(new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.down).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue() && open_EV.equal(new BBoolean(false)).booleanValue()).booleanValue()).booleanValue() || new BBoolean(new BBoolean(new BBoolean(handle.equal(HANDLE_STATE.up).booleanValue() && gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()).booleanValue() && doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()).booleanValue() && open_EV.equal(new BBoolean(false)).booleanValue()).booleanValue()).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_evn_open_general_valve() {
+ return new BBoolean(new BBoolean(general_EV.equal(new BBoolean(true)).booleanValue() && general_valve.equal(VALVE_STATE.valve_closed).booleanValue()).booleanValue() && analogical_switch.equal(SWITCH_STATE.switch_closed).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_evn_close_general_valve() {
+ return new BBoolean(new BBoolean(general_EV.equal(new BBoolean(false)).booleanValue() || analogical_switch.equal(SWITCH_STATE.switch_open).booleanValue()).booleanValue() && general_valve.equal(VALVE_STATE.valve_open).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_env_close_analogical_switch() {
+ return new BBoolean(analogical_switch.equal(SWITCH_STATE.switch_open).booleanValue() && handle_move.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _tr_env_open_analogical_switch() {
+ return analogical_switch.equal(SWITCH_STATE.switch_closed).booleanValue();
+ }
+
+ public boolean _check_inv_1() {
+ return _SWITCH_STATE.elementOf(analogical_switch).booleanValue();
+ }
+
+ public boolean _check_inv_2() {
+ return BUtils.BOOL.elementOf(general_EV).booleanValue();
+ }
+
+ public boolean _check_inv_3() {
+ return _VALVE_STATE.elementOf(general_valve).booleanValue();
+ }
+
+ public boolean _check_inv_4() {
+ return BUtils.BOOL.elementOf(handle_move).booleanValue();
+ }
+
+ public boolean _check_inv_5() {
+ return BUtils.BOOL.elementOf(close_EV).booleanValue();
+ }
+
+ public boolean _check_inv_6() {
+ return BUtils.BOOL.elementOf(extend_EV).booleanValue();
+ }
+
+ public boolean _check_inv_7() {
+ return BUtils.BOOL.elementOf(open_EV).booleanValue();
+ }
+
+ public boolean _check_inv_8() {
+ return BUtils.BOOL.elementOf(retract_EV).booleanValue();
+ }
+
+ public boolean _check_inv_9() {
+ return _PLANE_STATE.elementOf(shock_absorber).booleanValue();
+ }
+
+ public boolean _check_inv_10() {
+ return _VALVE_STATE.elementOf(valve_close_door).booleanValue();
+ }
+
+ public boolean _check_inv_11() {
+ return _VALVE_STATE.elementOf(valve_extend_gear).booleanValue();
+ }
+
+ public boolean _check_inv_12() {
+ return _VALVE_STATE.elementOf(valve_open_door).booleanValue();
+ }
+
+ public boolean _check_inv_13() {
+ return _VALVE_STATE.elementOf(valve_retract_gear).booleanValue();
+ }
+
+ public boolean _check_inv_14() {
+ return _HANDLE_STATE.elementOf(handle).booleanValue();
+ }
+
+ public boolean _check_inv_15() {
+ return _DOOR_STATE.elementOf(door).booleanValue();
+ }
+
+ public boolean _check_inv_16() {
+ return _GEAR_STATE.elementOf(gear).booleanValue();
+ }
+
+ public boolean _check_inv_17() {
+ return new BBoolean(!new BBoolean(new BBoolean(new BBoolean(open_EV.equal(new BBoolean(true)).booleanValue() || close_EV.equal(new BBoolean(true)).booleanValue()).booleanValue() || retract_EV.equal(new BBoolean(true)).booleanValue()).booleanValue() || extend_EV.equal(new BBoolean(true)).booleanValue()).booleanValue() || general_EV.equal(new BBoolean(true)).booleanValue()).booleanValue();
+ }
+
+ public boolean _check_inv_18() {
+ return new BBoolean(open_EV.equal(new BBoolean(true)).booleanValue() && close_EV.equal(new BBoolean(true)).booleanValue()).not().booleanValue();
+ }
+
+ public boolean _check_inv_19() {
+ return gears.checkDomain(_POSITION).and(gears.checkRange(_GEAR_STATE)).and(gears.isFunction()).and(gears.isTotal(_POSITION)).booleanValue();
+ }
+
+ public boolean _check_inv_20() {
+ return doors.checkDomain(_POSITION).and(doors.checkRange(_DOOR_STATE)).and(doors.isFunction()).and(doors.isTotal(_POSITION)).booleanValue();
+ }
+
+ public boolean _check_inv_21() {
+ return new BBoolean((!door.equal(DOOR_STATE.closed).booleanValue() || doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue()) && (!doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.closed)).booleanValue() || door.equal(DOOR_STATE.closed).booleanValue())).booleanValue();
+ }
+
+ public boolean _check_inv_22() {
+ return new BBoolean((!door.equal(DOOR_STATE.open).booleanValue() || doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue()) && (!doors.range().equal(new BSet<DOOR_STATE>(DOOR_STATE.open)).booleanValue() || door.equal(DOOR_STATE.open).booleanValue())).booleanValue();
+ }
+
+ public boolean _check_inv_23() {
+ return new BBoolean((!gear.equal(GEAR_STATE.extended).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue()) && (!gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.extended)).booleanValue() || gear.equal(GEAR_STATE.extended).booleanValue())).booleanValue();
+ }
+
+ public boolean _check_inv_24() {
+ return new BBoolean((!gear.equal(GEAR_STATE.retracted).booleanValue() || gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue()) && (!gears.range().equal(new BSet<GEAR_STATE>(GEAR_STATE.retracted)).booleanValue() || gear.equal(GEAR_STATE.retracted).booleanValue())).booleanValue();
+ }
+
+ public boolean _check_inv_25() {
+ 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 LandingGear_R6 _copy() {
+ return new LandingGear_R6(analogical_switch, general_EV, general_valve, handle_move, close_EV, extend_EV, open_EV, retract_EV, shock_absorber, valve_close_door, valve_extend_gear, valve_open_door, valve_retract_gear, doors, gears, handle, door, gear);
+ }
+
+
+}
+
diff --git a/Beispiele/LandingGear_R6.json b/Beispiele/LandingGear_R6.json
new file mode 100644
index 0000000000000000000000000000000000000000..0f08a2819b821948825602f024e2308fbb6df292
--- /dev/null
+++ b/Beispiele/LandingGear_R6.json
@@ -0,0 +1,241 @@
+{
+ "machineName": "LandingGear_R6",
+ "variables": [
+ "_get_analogical_switch",
+ "_get_general_EV",
+ "_get_general_valve",
+ "_get_handle_move",
+ "_get_close_EV",
+ "_get_extend_EV",
+ "_get_open_EV",
+ "_get_retract_EV",
+ "_get_shock_absorber",
+ "_get_valve_close_door",
+ "_get_valve_extend_gear",
+ "_get_valve_open_door",
+ "_get_valve_retract_gear",
+ "_get_doors",
+ "_get_gears",
+ "_get_handle",
+ "_get_door",
+ "_get_gear"
+ ],
+ "operationFunctions": [
+ {
+ "opName": "begin_flying",
+ "parameterTypes": []
+ },
+ {
+ "opName": "land_plane",
+ "parameterTypes": []
+ },
+ {
+ "opName": "open_valve_door_open",
+ "parameterTypes": []
+ },
+ {
+ "opName": "close_valve_door_open",
+ "parameterTypes": []
+ },
+ {
+ "opName": "open_valve_door_close",
+ "parameterTypes": []
+ },
+ {
+ "opName": "close_valve_door_close",
+ "parameterTypes": []
+ },
+ {
+ "opName": "open_valve_retract_gear",
+ "parameterTypes": []
+ },
+ {
+ "opName": "close_valve_retract_gear",
+ "parameterTypes": []
+ },
+ {
+ "opName": "open_valve_extend_gear",
+ "parameterTypes": []
+ },
+ {
+ "opName": "close_valve_extend_gear",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stimulate_open_door_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stop_stimulate_open_door_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stimulate_close_door_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stop_stimulate_close_door_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stimulate_retract_gear_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stop_stimulate_retract_gear_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stimulate_extend_gear_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stop_stimulate_extend_gear_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "env_start_retracting_first",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_retract_gear_skip",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_retract_gear_last",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_start_extending",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_extend_gear_last",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_extend_gear_skip",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_start_open_door",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_open_door_last",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_open_door_skip",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_start_close_door",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_close_door",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "env_close_door_skip",
+ "parameterTypes": [
+ "POSITION"
+ ]
+ },
+ {
+ "opName": "toggle_handle_up",
+ "parameterTypes": []
+ },
+ {
+ "opName": "toggle_handle_down",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stimulate_general_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "con_stop_stimulate_general_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "evn_open_general_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "evn_close_general_valve",
+ "parameterTypes": []
+ },
+ {
+ "opName": "env_close_analogical_switch",
+ "parameterTypes": []
+ },
+ {
+ "opName": "env_open_analogical_switch",
+ "parameterTypes": []
+ }
+ ],
+ "transitionEvaluationFunctions": {
+ "close_valve_door_close": "_tr_close_valve_door_close",
+ "close_valve_retract_gear": "_tr_close_valve_retract_gear",
+ "con_stimulate_open_door_valve": "_tr_con_stimulate_open_door_valve",
+ "env_close_door": "_tr_env_close_door",
+ "env_start_close_door": "_tr_env_start_close_door",
+ "toggle_handle_up": "_tr_toggle_handle_up",
+ "toggle_handle_down": "_tr_toggle_handle_down",
+ "open_valve_door_open": "_tr_open_valve_door_open",
+ "env_retract_gear_last": "_tr_env_retract_gear_last",
+ "env_open_door_last": "_tr_env_open_door_last",
+ "con_stop_stimulate_retract_gear_valve": "_tr_con_stop_stimulate_retract_gear_valve",
+ "env_close_door_skip": "_tr_env_close_door_skip",
+ "con_stop_stimulate_close_door_valve": "_tr_con_stop_stimulate_close_door_valve",
+ "env_open_analogical_switch": "_tr_env_open_analogical_switch",
+ "con_stop_stimulate_general_valve": "_tr_con_stop_stimulate_general_valve",
+ "env_extend_gear_last": "_tr_env_extend_gear_last",
+ "evn_open_general_valve": "_tr_evn_open_general_valve",
+ "land_plane": "_tr_land_plane",
+ "con_stimulate_retract_gear_valve": "_tr_con_stimulate_retract_gear_valve",
+ "con_stimulate_general_valve": "_tr_con_stimulate_general_valve",
+ "env_start_retracting_first": "_tr_env_start_retracting_first",
+ "env_retract_gear_skip": "_tr_env_retract_gear_skip",
+ "open_valve_extend_gear": "_tr_open_valve_extend_gear",
+ "begin_flying": "_tr_begin_flying",
+ "open_valve_retract_gear": "_tr_open_valve_retract_gear",
+ "env_close_analogical_switch": "_tr_env_close_analogical_switch",
+ "env_start_extending": "_tr_env_start_extending",
+ "open_valve_door_close": "_tr_open_valve_door_close",
+ "con_stop_stimulate_open_door_valve": "_tr_con_stop_stimulate_open_door_valve",
+ "con_stop_stimulate_extend_gear_valve": "_tr_con_stop_stimulate_extend_gear_valve",
+ "evn_close_general_valve": "_tr_evn_close_general_valve",
+ "close_valve_extend_gear": "_tr_close_valve_extend_gear",
+ "con_stimulate_extend_gear_valve": "_tr_con_stimulate_extend_gear_valve",
+ "close_valve_door_open": "_tr_close_valve_door_open",
+ "con_stimulate_close_door_valve": "_tr_con_stimulate_close_door_valve",
+ "env_extend_gear_skip": "_tr_env_extend_gear_skip",
+ "env_open_door_skip": "_tr_env_open_door_skip",
+ "env_start_open_door": "_tr_env_start_open_door"
+ }
+}
diff --git a/Beispiele/LandingGear_R6.mch b/Beispiele/LandingGear_R6.mch
new file mode 100644
index 0000000000000000000000000000000000000000..72bd1819e166f1370614ab88f8b30a4c1927338b
--- /dev/null
+++ b/Beispiele/LandingGear_R6.mch
@@ -0,0 +1,532 @@
+MACHINE LandingGear_R6
+SETS /* enumerated */
+ DOOR_STATE={open,closed,door_moving};
+ GEAR_STATE={retracted,extended,gear_moving};
+ HANDLE_STATE={up,down};
+ POSITION={fr,lt,rt};
+ SWITCH_STATE={switch_open,switch_closed};
+ PLANE_STATE={ground,flight};
+ VALVE_STATE={valve_open,valve_closed}
+
+VARIABLES
+ analogical_switch,
+ general_EV,
+ general_valve,
+ handle_move,
+ close_EV,
+ extend_EV,
+ open_EV,
+ retract_EV,
+ shock_absorber,
+ valve_close_door,
+ valve_extend_gear,
+ valve_open_door,
+ valve_retract_gear,
+ doors,
+ gears,
+ handle,
+ door,
+ gear
+
+/* PROMOTED OPERATIONS
+ begin_flying,
+ land_plane,
+ open_valve_door_open,
+ close_valve_door_open,
+ open_valve_door_close,
+ close_valve_door_close,
+ open_valve_retract_gear,
+ close_valve_retract_gear,
+ open_valve_extend_gear,
+ close_valve_extend_gear,
+ con_stimulate_open_door_valve,
+ con_stop_stimulate_open_door_valve,
+ con_stimulate_close_door_valve,
+ con_stop_stimulate_close_door_valve,
+ con_stimulate_retract_gear_valve,
+ con_stop_stimulate_retract_gear_valve,
+ con_stimulate_extend_gear_valve,
+ con_stop_stimulate_extend_gear_valve,
+ env_start_retracting_first,
+ env_retract_gear_skip,
+ env_retract_gear_last,
+ env_start_extending,
+ env_extend_gear_last,
+ env_extend_gear_skip,
+ env_start_open_door,
+ env_open_door_last,
+ env_open_door_skip,
+ env_start_close_door,
+ env_close_door,
+ env_close_door_skip,
+ toggle_handle_up,
+ toggle_handle_down,
+ con_stimulate_general_valve,
+ con_stop_stimulate_general_valve,
+ evn_open_general_valve,
+ evn_close_general_valve,
+ env_close_analogical_switch,
+ env_open_analogical_switch */
+INVARIANT
+analogical_switch : SWITCH_STATE
+& general_EV : BOOL
+& general_valve : VALVE_STATE
+& handle_move : BOOL
+& close_EV : BOOL
+& extend_EV : BOOL
+& open_EV : BOOL
+& retract_EV : BOOL
+& shock_absorber : PLANE_STATE
+& valve_close_door : VALVE_STATE
+& valve_extend_gear : VALVE_STATE
+& valve_open_door : VALVE_STATE
+& valve_retract_gear : VALVE_STATE
+& handle : HANDLE_STATE
+& door : DOOR_STATE
+& gear : GEAR_STATE
+& /* @R6GearsDoorsHandleValvesControllerSwitch:r51 */ ((open_EV = TRUE or close_EV = TRUE or retract_EV = TRUE or extend_EV = TRUE) => general_EV = TRUE)
+& /* @R5GearsDoorsHandleValvesController:R41 */ not(open_EV = TRUE & close_EV = TRUE)
+& /* @R3GearsDoorsHandle:inv1 */ gears : POSITION --> GEAR_STATE
+& /* @R3GearsDoorsHandle:inv2 */ doors : POSITION --> DOOR_STATE
+& /* @R3GearsDoorsHandle:glued1 */ (door = closed <=> ran(doors) = {closed})
+& /* @R3GearsDoorsHandle:glued2 */ (door = open <=> ran(doors) = {open})
+& /* @R3GearsDoorsHandle:glueg1 */ (gear = extended <=> ran(gears) = {extended})
+& /* @R3GearsDoorsHandle:glueg2 */ (gear = retracted <=> ran(gears) = {retracted})
+& /* @R1GearDoor:safety_inv1 */ (gear = gear_moving => door = open)
+
+
+INITIALISATION
+ gears := POSITION * {extended} ||
+ doors := POSITION * {closed} ||
+ handle := down ||
+ valve_extend_gear := valve_closed ||
+ valve_retract_gear := valve_closed ||
+ valve_open_door := valve_closed ||
+ valve_close_door := valve_closed ||
+ open_EV := FALSE ||
+ close_EV := FALSE ||
+ retract_EV := FALSE ||
+ extend_EV := FALSE ||
+ shock_absorber := ground ||
+ general_EV := FALSE ||
+ general_valve := valve_closed ||
+ analogical_switch := switch_open ||
+ handle_move := FALSE ||
+ gear := extended ||
+ door := closed
+
+OPERATIONS
+
+ begin_flying =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:onground */ shock_absorber = ground
+ THEN
+ shock_absorber := flight
+ END;
+
+ land_plane =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:onground */ shock_absorber = flight
+ THEN
+ shock_absorber := ground
+ END;
+
+ open_valve_door_open =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_open */ valve_open_door = valve_closed
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ open_EV = TRUE
+ THEN
+ valve_open_door := valve_open
+ END;
+
+ close_valve_door_open =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_closed */ valve_open_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ open_EV = FALSE
+ THEN
+ valve_open_door := valve_closed
+ END;
+
+ open_valve_door_close =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_open */ valve_close_door = valve_closed
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ close_EV = TRUE
+ THEN
+ valve_close_door := valve_open
+ END;
+
+ close_valve_door_close =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_closed */ valve_close_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ close_EV = FALSE
+ THEN
+ valve_close_door := valve_closed
+ END;
+
+ open_valve_retract_gear =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_open */ valve_retract_gear = valve_closed
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ retract_EV = TRUE
+ THEN
+ valve_retract_gear := valve_open
+ END;
+
+ close_valve_retract_gear =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_closed */ valve_retract_gear = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ retract_EV = FALSE
+ THEN
+ valve_retract_gear := valve_closed
+ END;
+
+ open_valve_extend_gear =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_open */ valve_extend_gear = valve_closed
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ extend_EV = TRUE
+ THEN
+ valve_extend_gear := valve_open
+ END;
+
+ close_valve_extend_gear =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:valve_not_closed */ valve_extend_gear = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ extend_EV = FALSE
+ THEN
+ valve_extend_gear := valve_closed
+ END;
+
+ con_stimulate_open_door_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ open_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ close_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdh1 */ ((handle = down & not(ran(gears) = {extended})) or (handle = up & not(ran(gears) = {retracted}) & not(ran(doors) = {open} & shock_absorber = ground)))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ open_EV := TRUE
+ END;
+
+ con_stop_stimulate_open_door_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ open_EV = TRUE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd11 */ extend_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd12 */ retract_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdh1 */ ((handle = down & ran(gears) = {extended}) or (handle = up & (ran(gears) = {retracted} or shock_absorber = ground) & ran(doors) = {open}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ open_EV := FALSE
+ END;
+
+ con_stimulate_close_door_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ close_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ open_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd11 */ extend_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd12 */ retract_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdh1 */ ((handle = down & ran(gears) = {extended}) or (handle = up & (ran(gears) = {retracted} or shock_absorber = ground)))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grddoors */ not(ran(doors) = {closed})
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ close_EV := TRUE
+ END;
+
+ con_stop_stimulate_close_door_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ close_EV = TRUE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdh1 */ ((handle = down & ran(gears) = {extended} & ran(doors) = {closed}) or (handle = up & (ran(gears) = {retracted} or shock_absorber = ground) & ran(doors) = {closed}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ close_EV := FALSE
+ END;
+
+ con_stimulate_retract_gear_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ retract_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ extend_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ open_EV = TRUE
+ & handle = up
+ & not(ran(gears) = {retracted})
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdflight */ shock_absorber = flight
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grddoors */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ retract_EV := TRUE
+ END;
+
+ con_stop_stimulate_retract_gear_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ retract_EV = TRUE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdh1 */ (handle = down or ran(gears) = {retracted})
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ retract_EV := FALSE
+ END;
+
+ con_stimulate_extend_gear_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ extend_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ retract_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ open_EV = TRUE
+ & handle = down
+ & not(ran(gears) = {extended})
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grddoors */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ extend_EV := TRUE
+ END;
+
+ con_stop_stimulate_extend_gear_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ extend_EV = TRUE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grdh1 */ (handle = up or ran(gears) = {extended})
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_ev */ general_EV = TRUE
+ THEN
+ extend_EV := FALSE
+ END;
+
+ env_start_retracting_first(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_doors_open */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:handle_up */ handle = up
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:g1 */ gears(gr) = extended
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_retract_gear = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & /* @R2GearDoorHandle:g1 */ gear : {extended,gear_moving}
+ & /* @R2GearDoorHandle:door_open */ door = open
+ THEN
+ gears := gears <+ {gr |-> gear_moving} ||
+ gear := gear_moving
+ END;
+
+ env_retract_gear_skip(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_doors_open */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ gears[POSITION \ {gr}] /= {retracted}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:handle_up */ handle = up
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:g1 */ gears(gr) = gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ THEN
+ gears := gears <+ {gr |-> retracted}
+ END;
+
+ env_retract_gear_last(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_doors_open */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ gears[POSITION \ {gr}] = {retracted}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:handle_up */ handle = up
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:g1 */ gears(gr) = gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & /* @R2GearDoorHandle:g1 */ gear = gear_moving
+ & /* @R2GearDoorHandle:door_open */ door = open
+ THEN
+ gears := gears <+ {gr |-> retracted} ||
+ gear := retracted
+ END;
+
+ env_start_extending(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_doors_open */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:handle_down */ handle = down
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:g1 */ gears(gr) = retracted
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_extend_gear = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & /* @R2GearDoorHandle:g1 */ gear : {gear_moving,retracted}
+ & /* @R2GearDoorHandle:door_open */ door = open
+ THEN
+ gears := gears <+ {gr |-> gear_moving} ||
+ gear := gear_moving
+ END;
+
+ env_extend_gear_last(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_doors_open */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:handle_down */ handle = down
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ gears[POSITION \ {gr}] = {extended}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:g1 */ gears(gr) = gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & /* @R2GearDoorHandle:g1 */ gear = gear_moving
+ & /* @R2GearDoorHandle:door_open */ door = open
+ THEN
+ gears := gears <+ {gr |-> extended} ||
+ gear := extended
+ END;
+
+ env_extend_gear_skip(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_doors_open */ ran(doors) = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:handle_down */ handle = down
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ gears[POSITION \ {gr}] /= {extended}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:g1 */ gears(gr) = gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ THEN
+ gears := gears <+ {gr |-> extended}
+ END;
+
+ env_start_open_door(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & doors(gr) = closed
+ & gears(gr) /= gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:nomov */ gear_moving /: ran(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:h */ ((handle = down & ran(gears) = {retracted}) or (handle = up & ran(gears) = {extended}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_open_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & door : {closed,door_moving}
+ & gear /= gear_moving
+ & /* @R2GearDoorHandle:h */ ((handle = down & gear = retracted) or (handle = up & gear = extended))
+ THEN
+ doors := doors <+ {gr |-> door_moving} ||
+ door := door_moving
+ END;
+
+ env_open_door_last(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & doors(gr) = door_moving
+ & gears(gr) /= gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:nomov */ gear_moving /: ran(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ doors[POSITION \ {gr}] = {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:h */ ((handle = down & ran(gears) = {retracted}) or (handle = up & ran(gears) = {extended}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_open_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & door = door_moving
+ & gear /= gear_moving
+ & /* @R2GearDoorHandle:h */ ((handle = down & gear = retracted) or (handle = up & gear = extended))
+ THEN
+ doors := doors <+ {gr |-> open} ||
+ door := open
+ END;
+
+ env_open_door_skip(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & doors(gr) = door_moving
+ & gears(gr) /= gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:nomov */ gear_moving /: ran(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ doors[POSITION \ {gr}] /= {open}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:h */ ((handle = down & ran(gears) = {retracted}) or (handle = up & ran(gears) = {extended}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_open_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ THEN
+ doors := doors <+ {gr |-> open}
+ END;
+
+ env_start_close_door(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & doors(gr) = open
+ & gears(gr) /= gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:h */ ((handle = up & (ran(gears) = {retracted} or ran(gears) = {extended})) or (handle = down & ran(gears) = {extended}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_close_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ & door : {door_moving,open} & gear /= gear_moving & /* @R2GearDoorHandle:h */ ((handle = down & gear = extended) or (handle = up & gear : {extended,retracted}))
+ THEN
+ doors := doors <+ {gr |-> door_moving} ||
+ door := door_moving
+ END;
+
+ env_close_door(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & doors(gr) = door_moving & gears(gr) /= gear_moving & /* @R6GearsDoorsHandleValvesControllerSwitch:nomov */ gear_moving /: ran(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ doors[POSITION \ {gr}] = {closed}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:h */ ((handle = up & (ran(gears) = {retracted} or ran(gears) = {extended})) or (handle = down & ran(gears) = {extended}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_close_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:hground */ ((handle = up & ran(gears) = {extended}) => shock_absorber = ground)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open & door = door_moving & gear /= gear_moving
+ & /* @R2GearDoorHandle:h */ ((handle = down & gear = extended) or (handle = up & gear : {extended,retracted}))
+ THEN
+ doors := doors <+ {gr |-> closed} ||
+ door := closed
+ END;
+
+ env_close_door_skip(/* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr) =
+ SELECT /* @R6GearsDoorsHandleValvesControllerSwitch:gr */ gr : dom(gears)
+ & doors(gr) = door_moving
+ & gears(gr) /= gear_moving
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:nomov */ gear_moving /: ran(gears)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:all_others */ doors[POSITION \ {gr}] /= {closed}
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:h */ ((handle = up & (ran(gears) = {retracted} or ran(gears) = {extended})) or (handle = down & ran(gears) = {extended}))
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:gv */ valve_close_door = valve_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:hground */ ((handle = up & ran(gears) = {extended}) => shock_absorber = ground)
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:general_valve */ general_valve = valve_open
+ THEN
+ doors := doors <+ {gr |-> closed}
+ END;
+
+ toggle_handle_up =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:h */ handle = down
+ THEN
+ handle := up ||
+ handle_move := TRUE
+ END;
+
+ toggle_handle_down =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:h */ handle = up
+ THEN
+ handle := down ||
+ handle_move := TRUE
+ END;
+
+ con_stimulate_general_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ general_EV = FALSE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ handle_move = TRUE
+ THEN
+ general_EV := TRUE
+ END;
+
+ con_stop_stimulate_general_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ general_EV = TRUE
+ & open_EV = FALSE
+ & close_EV = FALSE
+ & retract_EV = FALSE
+ & extend_EV = FALSE
+ & close_EV = FALSE
+ & ((handle = up & ran(gears) = {retracted} & ran(doors) = {closed} & open_EV = FALSE) or (handle = down & ran(gears) = {extended} & ran(doors) = {closed} & open_EV = FALSE) or (handle = up & ran(gears) = {extended} & ran(doors) = {closed} & open_EV = FALSE))
+ THEN
+ general_EV := FALSE ||
+ handle_move := FALSE
+ END;
+
+ evn_open_general_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ general_EV = TRUE
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ general_valve = valve_closed
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd3 */ analogical_switch = switch_closed
+ THEN
+ general_valve := valve_open
+ END;
+
+ evn_close_general_valve =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ (general_EV = FALSE or analogical_switch = switch_open )
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ general_valve = valve_open
+ THEN
+ general_valve := valve_closed
+ END;
+
+ env_close_analogical_switch =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ analogical_switch = switch_open
+ & /* @R6GearsDoorsHandleValvesControllerSwitch:grd2 */ handle_move = TRUE
+ THEN
+ analogical_switch := switch_closed
+ END;
+
+ env_open_analogical_switch =
+ SELECT
+ /* @R6GearsDoorsHandleValvesControllerSwitch:grd1 */ analogical_switch = switch_closed
+ THEN
+ analogical_switch := switch_open
+ END
+
+END
diff --git a/Beispiele/Lift_MC.mch b/Beispiele/Lift_MC.mch
new file mode 100644
index 0000000000000000000000000000000000000000..3cb38062a84c46c5a8269a50ce82683f944be665
--- /dev/null
+++ b/Beispiele/Lift_MC.mch
@@ -0,0 +1,14 @@
+MACHINE Lift_MC
+
+VARIABLES floor
+
+INVARIANT floor >= 0 & floor <= 100
+
+INITIALISATION floor := 0
+
+OPERATIONS
+
+ inc = PRE floor<100 THEN floor := floor + 1 END ;
+ dec = PRE floor>0 THEN floor := floor - 1 END
+
+END
\ No newline at end of file
diff --git a/Beispiele/TrafficLight_MC.mch b/Beispiele/TrafficLight_MC.mch
new file mode 100644
index 0000000000000000000000000000000000000000..a7005d06a23ce4837473fc15c0c7292d8005bfce
--- /dev/null
+++ b/Beispiele/TrafficLight_MC.mch
@@ -0,0 +1,46 @@
+MACHINE TrafficLight_MC
+
+SETS colors = {red, redyellow, yellow, green}
+
+VARIABLES tl_cars, tl_peds
+
+INVARIANT tl_cars : colors &
+ tl_peds : {red, green} &
+ (tl_peds = red or
+ tl_cars = red)
+
+INITIALISATION tl_cars := red; tl_peds := red
+
+OPERATIONS
+
+cars_ry =
+ SELECT tl_cars = red & tl_peds = red THEN
+ tl_cars := redyellow
+ END;
+
+cars_y =
+ SELECT tl_cars = green & tl_peds = red THEN
+ tl_cars := yellow
+ END;
+
+cars_g =
+ SELECT tl_cars = redyellow & tl_peds = red THEN
+ tl_cars := green
+ END;
+
+cars_r =
+ SELECT tl_cars = yellow & tl_peds = red THEN
+ tl_cars := red
+ END;
+
+peds_r =
+ SELECT tl_peds = green & tl_cars = red THEN
+ tl_peds := red
+ END;
+
+peds_g =
+ SELECT tl_peds = red & tl_cars = red THEN
+ tl_peds := green
+ END
+
+END
\ No newline at end of file
diff --git a/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java
new file mode 100644
index 0000000000000000000000000000000000000000..ba4d5bb43aacae90177ab5a064c6de73393e13f8
--- /dev/null
+++ b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.java
@@ -0,0 +1,465 @@
+import de.hhu.stups.btypes.BRelation;
+import de.hhu.stups.btypes.BTuple;
+import de.hhu.stups.btypes.BSet;
+import de.hhu.stups.btypes.BObject;
+import de.hhu.stups.btypes.BBoolean;
+import java.util.Objects;
+import java.util.Arrays;
+import de.hhu.stups.btypes.BUtils;
+
+
+public class Train_1_beebook_deterministic_MC_POR_v2 {
+
+
+ private static BRelation<ROUTES, BLOCKS> fst;
+ private static BRelation<ROUTES, BLOCKS> lst;
+ private static BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>> nxt;
+ private static BRelation<BLOCKS, ROUTES> rtbl;
+
+
+ public enum BLOCKS implements BObject {
+ A,
+ B,
+ C,
+ D,
+ E,
+ F,
+ G,
+ H,
+ I,
+ J,
+ K,
+ L,
+ M,
+ N;
+
+ public BBoolean equal(BLOCKS o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(BLOCKS o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ public enum ROUTES implements BObject {
+ R1,
+ R2,
+ R3,
+ R4,
+ R5,
+ R6,
+ R7,
+ R8,
+ R9,
+ R10;
+
+ public BBoolean equal(ROUTES o) {
+ return new BBoolean(this == o);
+ }
+
+ public BBoolean unequal(ROUTES o) {
+ return new BBoolean(this != o);
+ }
+ }
+
+ private static BSet<BLOCKS> _BLOCKS = new BSet<BLOCKS>(BLOCKS.A, BLOCKS.B, BLOCKS.C, BLOCKS.D, BLOCKS.E, BLOCKS.F, BLOCKS.G, BLOCKS.H, BLOCKS.I, BLOCKS.J, BLOCKS.K, BLOCKS.L, BLOCKS.M, BLOCKS.N);
+ private static BSet<ROUTES> _ROUTES = new BSet<ROUTES>(ROUTES.R1, ROUTES.R2, ROUTES.R3, ROUTES.R4, ROUTES.R5, ROUTES.R6, ROUTES.R7, ROUTES.R8, ROUTES.R9, ROUTES.R10);
+
+ private BSet<BLOCKS> LBT;
+ private BRelation<BLOCKS, BLOCKS> TRK;
+ private BSet<ROUTES> frm;
+ private BSet<BLOCKS> OCC;
+ private BSet<BLOCKS> resbl;
+ private BSet<ROUTES> resrt;
+ private BRelation<BLOCKS, ROUTES> rsrtbl;
+
+ static {
+ fst = new BRelation<ROUTES, BLOCKS>(new BTuple<>(ROUTES.R1, BLOCKS.L), new BTuple<>(ROUTES.R2, BLOCKS.L), new BTuple<>(ROUTES.R3, BLOCKS.L), new BTuple<>(ROUTES.R4, BLOCKS.M), new BTuple<>(ROUTES.R5, BLOCKS.M), new BTuple<>(ROUTES.R6, BLOCKS.C), new BTuple<>(ROUTES.R7, BLOCKS.G), new BTuple<>(ROUTES.R8, BLOCKS.N), new BTuple<>(ROUTES.R9, BLOCKS.G), new BTuple<>(ROUTES.R10, BLOCKS.N));
+ lst = new BRelation<ROUTES, BLOCKS>(new BTuple<>(ROUTES.R1, BLOCKS.C), new BTuple<>(ROUTES.R2, BLOCKS.G), new BTuple<>(ROUTES.R3, BLOCKS.N), new BTuple<>(ROUTES.R4, BLOCKS.G), new BTuple<>(ROUTES.R5, BLOCKS.N), new BTuple<>(ROUTES.R6, BLOCKS.L), new BTuple<>(ROUTES.R7, BLOCKS.L), new BTuple<>(ROUTES.R8, BLOCKS.L), new BTuple<>(ROUTES.R9, BLOCKS.M), new BTuple<>(ROUTES.R10, BLOCKS.M));
+ nxt = new BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>>(new BTuple<>(ROUTES.R1, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.L, BLOCKS.A), new BTuple<>(BLOCKS.A, BLOCKS.B), new BTuple<>(BLOCKS.B, BLOCKS.C))), new BTuple<>(ROUTES.R2, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.L, BLOCKS.A), new BTuple<>(BLOCKS.A, BLOCKS.B), new BTuple<>(BLOCKS.B, BLOCKS.D), new BTuple<>(BLOCKS.D, BLOCKS.E), new BTuple<>(BLOCKS.E, BLOCKS.F), new BTuple<>(BLOCKS.F, BLOCKS.G))), new BTuple<>(ROUTES.R3, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.L, BLOCKS.A), new BTuple<>(BLOCKS.A, BLOCKS.B), new BTuple<>(BLOCKS.B, BLOCKS.D), new BTuple<>(BLOCKS.D, BLOCKS.K), new BTuple<>(BLOCKS.K, BLOCKS.J), new BTuple<>(BLOCKS.J, BLOCKS.N))), new BTuple<>(ROUTES.R4, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.M, BLOCKS.H), new BTuple<>(BLOCKS.H, BLOCKS.I), new BTuple<>(BLOCKS.I, BLOCKS.K), new BTuple<>(BLOCKS.K, BLOCKS.F), new BTuple<>(BLOCKS.F, BLOCKS.G))), new BTuple<>(ROUTES.R5, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.M, BLOCKS.H), new BTuple<>(BLOCKS.H, BLOCKS.I), new BTuple<>(BLOCKS.I, BLOCKS.J), new BTuple<>(BLOCKS.J, BLOCKS.N))), new BTuple<>(ROUTES.R6, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.C, BLOCKS.B), new BTuple<>(BLOCKS.B, BLOCKS.A), new BTuple<>(BLOCKS.A, BLOCKS.L))), new BTuple<>(ROUTES.R7, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.G, BLOCKS.F), new BTuple<>(BLOCKS.F, BLOCKS.E), new BTuple<>(BLOCKS.E, BLOCKS.D), new BTuple<>(BLOCKS.D, BLOCKS.B), new BTuple<>(BLOCKS.B, BLOCKS.A), new BTuple<>(BLOCKS.A, BLOCKS.L))), new BTuple<>(ROUTES.R8, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.N, BLOCKS.J), new BTuple<>(BLOCKS.J, BLOCKS.K), new BTuple<>(BLOCKS.K, BLOCKS.D), new BTuple<>(BLOCKS.D, BLOCKS.B), new BTuple<>(BLOCKS.B, BLOCKS.A), new BTuple<>(BLOCKS.A, BLOCKS.L))), new BTuple<>(ROUTES.R9, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.G, BLOCKS.F), new BTuple<>(BLOCKS.F, BLOCKS.K), new BTuple<>(BLOCKS.K, BLOCKS.I), new BTuple<>(BLOCKS.I, BLOCKS.H), new BTuple<>(BLOCKS.H, BLOCKS.M))), new BTuple<>(ROUTES.R10, new BRelation<BLOCKS, BLOCKS>(new BTuple<>(BLOCKS.N, BLOCKS.J), new BTuple<>(BLOCKS.J, BLOCKS.I), new BTuple<>(BLOCKS.I, BLOCKS.H), new BTuple<>(BLOCKS.H, BLOCKS.M))));
+ BRelation<BLOCKS, ROUTES> _ic_set_0 = new BRelation<BLOCKS, ROUTES>();
+ for(BLOCKS _ic_b_1 : _BLOCKS) {
+ for(ROUTES _ic_r_1 : _ROUTES) {
+ if((new BBoolean(nxt.domain().elementOf(_ic_r_1).booleanValue() && new BBoolean(nxt.functionCall(_ic_r_1).domain().elementOf(_ic_b_1).booleanValue() || nxt.functionCall(_ic_r_1).range().elementOf(_ic_b_1).booleanValue()).booleanValue())).booleanValue()) {
+ _ic_set_0 = _ic_set_0.union(new BRelation<BLOCKS, ROUTES>(new BTuple<>(_ic_b_1, _ic_r_1)));
+ }
+
+ }
+ }
+
+ rtbl = _ic_set_0;
+ }
+
+ public Train_1_beebook_deterministic_MC_POR_v2() {
+ resrt = new BSet<ROUTES>();
+ resbl = new BSet<BLOCKS>();
+ rsrtbl = new BRelation<BLOCKS, ROUTES>();
+ OCC = new BSet<BLOCKS>();
+ TRK = new BRelation<BLOCKS, BLOCKS>();
+ frm = new BSet<ROUTES>();
+ LBT = new BSet<BLOCKS>();
+ }
+
+
+ public Train_1_beebook_deterministic_MC_POR_v2(BRelation<ROUTES, BLOCKS> fst, BRelation<ROUTES, BLOCKS> lst, BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>> nxt, BRelation<BLOCKS, ROUTES> rtbl, BSet<BLOCKS> LBT, BRelation<BLOCKS, BLOCKS> TRK, BSet<ROUTES> frm, BSet<BLOCKS> OCC, BSet<BLOCKS> resbl, BSet<ROUTES> resrt, BRelation<BLOCKS, ROUTES> rsrtbl) {
+ this.fst = fst;
+ this.lst = lst;
+ this.nxt = nxt;
+ this.rtbl = rtbl;
+ this.LBT = LBT;
+ this.TRK = TRK;
+ this.frm = frm;
+ this.OCC = OCC;
+ this.resbl = resbl;
+ this.resrt = resrt;
+ this.rsrtbl = rsrtbl;
+ }
+
+
+ public void route_reservation(ROUTES r) {
+ BSet<ROUTES> _ld_resrt = resrt;
+ BRelation<BLOCKS, ROUTES> _ld_rsrtbl = rsrtbl;
+ BSet<BLOCKS> _ld_resbl = resbl;
+ resrt = _ld_resrt.union(new BSet<ROUTES>(r));
+ rsrtbl = _ld_rsrtbl.union(rtbl.rangeRestriction(new BSet<ROUTES>(r)));
+ resbl = _ld_resbl.union(rtbl.inverse().relationImage(new BSet<ROUTES>(r)));
+
+ }
+
+ public void route_freeing(ROUTES r) {
+ BSet<ROUTES> _ld_resrt = resrt;
+ BSet<ROUTES> _ld_frm = frm;
+ resrt = _ld_resrt.difference(new BSet<ROUTES>(r));
+ frm = _ld_frm.difference(new BSet<ROUTES>(r));
+
+ }
+
+ public void FRONT_MOVE_1(ROUTES r) {
+ BSet<BLOCKS> _ld_OCC = OCC;
+
+ BSet<BLOCKS> _ld_LBT = LBT;
+ OCC = _ld_OCC.union(new BSet<BLOCKS>(fst.functionCall(r)));
+ LBT = _ld_LBT.union(new BSet<BLOCKS>(fst.functionCall(r)));
+
+ }
+
+ public void FRONT_MOVE_2(BLOCKS b) {
+ OCC = OCC.union(new BSet<BLOCKS>(TRK.functionCall(b)));
+
+ }
+
+ public void BACK_MOVE_1(BLOCKS b) {
+ BSet<BLOCKS> _ld_OCC = OCC;
+
+ BSet<BLOCKS> _ld_LBT = LBT;
+ BRelation<BLOCKS, ROUTES> _ld_rsrtbl = rsrtbl;
+ BSet<BLOCKS> _ld_resbl = resbl;
+ OCC = _ld_OCC.difference(new BSet<BLOCKS>(b));
+ rsrtbl = _ld_rsrtbl.domainSubstraction(new BSet<BLOCKS>(b));
+ resbl = _ld_resbl.difference(new BSet<BLOCKS>(b));
+ LBT = _ld_LBT.difference(new BSet<BLOCKS>(b));
+
+ }
+
+ public void BACK_MOVE_2(BLOCKS b) {
+ BSet<BLOCKS> _ld_OCC = OCC;
+
+ BSet<BLOCKS> _ld_LBT = LBT;
+ BRelation<BLOCKS, ROUTES> _ld_rsrtbl = rsrtbl;
+ BSet<BLOCKS> _ld_resbl = resbl;
+ OCC = _ld_OCC.difference(new BSet<BLOCKS>(b));
+ rsrtbl = _ld_rsrtbl.domainSubstraction(new BSet<BLOCKS>(b));
+ resbl = _ld_resbl.difference(new BSet<BLOCKS>(b));
+ LBT = _ld_LBT.difference(new BSet<BLOCKS>(b)).union(new BSet<BLOCKS>(TRK.functionCall(b)));
+
+ }
+
+ public void point_positionning(ROUTES r) {
+ TRK = TRK.domainSubstraction(nxt.functionCall(r).domain()).rangeSubstraction(nxt.functionCall(r).range()).union(nxt.functionCall(r));
+
+ }
+
+ public void route_formation(ROUTES r) {
+ frm = frm.union(new BSet<ROUTES>(r));
+
+ }
+
+ public BRelation<ROUTES, BLOCKS> _get_fst() {
+ return fst;
+ }
+
+ public BRelation<ROUTES, BLOCKS> _get_lst() {
+ return lst;
+ }
+
+ public BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>> _get_nxt() {
+ return nxt;
+ }
+
+ public BRelation<BLOCKS, ROUTES> _get_rtbl() {
+ return rtbl;
+ }
+
+ public BSet<BLOCKS> _get_LBT() {
+ return LBT;
+ }
+
+ public BRelation<BLOCKS, BLOCKS> _get_TRK() {
+ return TRK;
+ }
+
+ public BSet<ROUTES> _get_frm() {
+ return frm;
+ }
+
+ public BSet<BLOCKS> _get_OCC() {
+ return OCC;
+ }
+
+ public BSet<BLOCKS> _get_resbl() {
+ return resbl;
+ }
+
+ public BSet<ROUTES> _get_resrt() {
+ return resrt;
+ }
+
+ public BRelation<BLOCKS, ROUTES> _get_rsrtbl() {
+ return rsrtbl;
+ }
+
+ public BSet<BLOCKS> _get__BLOCKS() {
+ return _BLOCKS;
+ }
+
+ public BSet<ROUTES> _get__ROUTES() {
+ return _ROUTES;
+ }
+
+
+ public BSet<ROUTES> _tr_route_reservation() {
+ BSet<ROUTES> _ic_set_1 = new BSet<ROUTES>();
+ for(ROUTES _ic_r_1 : _ROUTES.difference(resrt)) {
+ if((new BBoolean(rtbl.inverse().relationImage(new BSet<ROUTES>(_ic_r_1)).intersect(resbl).equal(new BSet<BLOCKS>()).booleanValue() && new BSet<ROUTES>().equal(resrt.difference(rsrtbl.range())).booleanValue())).booleanValue()) {
+ _ic_set_1 = _ic_set_1.union(new BSet<ROUTES>(_ic_r_1));
+ }
+
+ }
+ return _ic_set_1;
+ }
+
+ public BSet<ROUTES> _tr_route_freeing() {
+ BSet<ROUTES> _ic_set_2 = new BSet<ROUTES>();
+ for(ROUTES _ic_r_1 : resrt.difference(rsrtbl.range())) {
+ _ic_set_2 = _ic_set_2.union(new BSet<ROUTES>(_ic_r_1));
+
+ }
+ return _ic_set_2;
+ }
+
+ public BSet<ROUTES> _tr_FRONT_MOVE_1() {
+ BSet<ROUTES> _ic_set_3 = new BSet<ROUTES>();
+ for(ROUTES _ic_r_1 : frm) {
+ if((new BBoolean(new BBoolean(resbl.difference(OCC).elementOf(fst.functionCall(_ic_r_1)).booleanValue() && _ic_r_1.equal(rsrtbl.functionCall(fst.functionCall(_ic_r_1))).booleanValue()).booleanValue() && new BSet<ROUTES>().equal(resrt.difference(rsrtbl.range())).booleanValue())).booleanValue()) {
+ _ic_set_3 = _ic_set_3.union(new BSet<ROUTES>(_ic_r_1));
+ }
+
+ }
+ return _ic_set_3;
+ }
+
+ public BSet<BLOCKS> _tr_FRONT_MOVE_2() {
+ BSet<BLOCKS> _ic_set_4 = new BSet<BLOCKS>();
+ for(BLOCKS _ic_b_1 : OCC.intersect(TRK.domain())) {
+ if((OCC.notElementOf(TRK.functionCall(_ic_b_1))).booleanValue()) {
+ _ic_set_4 = _ic_set_4.union(new BSet<BLOCKS>(_ic_b_1));
+ }
+
+ }
+ return _ic_set_4;
+ }
+
+ public BSet<BLOCKS> _tr_BACK_MOVE_1() {
+ BSet<BLOCKS> _ic_set_5 = new BSet<BLOCKS>();
+ for(BLOCKS _ic_b_1 : LBT.difference(TRK.domain())) {
+ if((new BSet<ROUTES>().equal(resrt.difference(rsrtbl.range()))).booleanValue()) {
+ _ic_set_5 = _ic_set_5.union(new BSet<BLOCKS>(_ic_b_1));
+ }
+
+ }
+ return _ic_set_5;
+ }
+
+ public BSet<BLOCKS> _tr_BACK_MOVE_2() {
+ BSet<BLOCKS> _ic_set_6 = new BSet<BLOCKS>();
+ for(BLOCKS _ic_b_1 : LBT.intersect(TRK.domain())) {
+ if((new BBoolean(OCC.elementOf(TRK.functionCall(_ic_b_1)).booleanValue() && new BSet<ROUTES>().equal(resrt.difference(rsrtbl.range())).booleanValue())).booleanValue()) {
+ _ic_set_6 = _ic_set_6.union(new BSet<BLOCKS>(_ic_b_1));
+ }
+
+ }
+ return _ic_set_6;
+ }
+
+ public BSet<ROUTES> _tr_point_positionning() {
+ BSet<ROUTES> _ic_set_7 = new BSet<ROUTES>();
+ for(ROUTES _ic_r_1 : resrt.difference(frm)) {
+ if((new BSet<ROUTES>().equal(resrt.difference(rsrtbl.range()))).booleanValue()) {
+ _ic_set_7 = _ic_set_7.union(new BSet<ROUTES>(_ic_r_1));
+ }
+
+ }
+ return _ic_set_7;
+ }
+
+ public BSet<ROUTES> _tr_route_formation() {
+ BSet<ROUTES> _ic_set_8 = new BSet<ROUTES>();
+ for(ROUTES _ic_r_1 : resrt.difference(frm)) {
+ if((new BBoolean(nxt.functionCall(_ic_r_1).domainRestriction(rsrtbl.inverse().relationImage(new BSet<ROUTES>(_ic_r_1))).equal(TRK.domainRestriction(rsrtbl.inverse().relationImage(new BSet<ROUTES>(_ic_r_1)))).booleanValue() && new BSet<ROUTES>().equal(resrt.difference(rsrtbl.range())).booleanValue())).booleanValue()) {
+ _ic_set_8 = _ic_set_8.union(new BSet<ROUTES>(_ic_r_1));
+ }
+
+ }
+ return _ic_set_8;
+ }
+
+ public boolean _check_inv_1() {
+ return TRK.checkDomain(_BLOCKS).and(TRK.checkRange(_BLOCKS)).and(TRK.isFunction()).and(TRK.isPartial(_BLOCKS)).and(TRK.isInjection()).booleanValue();
+ }
+
+ public boolean _check_inv_2() {
+ BBoolean _ic_boolean_9 = new BBoolean(true);
+ for(ROUTES _ic_r_1 : resrt.difference(frm)) {
+ for(BSet<ROUTES> _ic_a_1 : Arrays.asList(new BSet<ROUTES>(_ic_r_1))) {
+ if(!(rtbl.rangeRestriction(_ic_a_1).equal(rsrtbl.rangeRestriction(_ic_a_1))).booleanValue()) {
+ _ic_boolean_9 = new BBoolean(false);
+ break;
+ }
+
+ }
+
+ }
+
+ return _ic_boolean_9.booleanValue();
+ }
+
+ public boolean _check_inv_3() {
+ BBoolean _ic_boolean_11 = new BBoolean(true);
+ for(BLOCKS _ic_x_1 : TRK.domain()) {
+ for(BLOCKS _ic_y_1 : TRK.relationImage(new BSet<BLOCKS>(_ic_x_1))) {
+ BBoolean _ic_boolean_10 = new BBoolean(false);
+ for(ROUTES _ic_r_1 : _ROUTES) {
+ if((nxt.functionCall(_ic_r_1).elementOf(new BTuple<>(_ic_x_1, _ic_y_1))).booleanValue()) {
+ _ic_boolean_10 = new BBoolean(true);
+ break;
+ }
+
+ }
+
+ if(!(_ic_boolean_10).booleanValue()) {
+ _ic_boolean_11 = new BBoolean(false);
+ break;
+ }
+
+ }
+ }
+
+ return _ic_boolean_11.booleanValue();
+ }
+
+ public boolean _check_inv_4() {
+ BBoolean _ic_boolean_12 = new BBoolean(true);
+ for(ROUTES _ic_r_1 : frm) {
+ for(BSet<BLOCKS> _ic_a_1 : Arrays.asList(rsrtbl.inverse().relationImage(new BSet<ROUTES>(_ic_r_1)))) {
+ if(!(nxt.functionCall(_ic_r_1).domainRestriction(_ic_a_1).equal(TRK.domainRestriction(_ic_a_1))).booleanValue()) {
+ _ic_boolean_12 = new BBoolean(false);
+ break;
+ }
+
+ }
+
+ }
+
+ return _ic_boolean_12.booleanValue();
+ }
+
+ public boolean _check_inv_5() {
+ return LBT.subset(OCC).booleanValue();
+ }
+
+ public boolean _check_inv_6() {
+ BBoolean _ic_boolean_13 = new BBoolean(true);
+ for(BLOCKS _ic_a_1 : rsrtbl.domain()) {
+ for(BLOCKS _ic_b_1 : LBT) {
+ for(ROUTES _ic_c_1 : Arrays.asList(rsrtbl.functionCall(_ic_b_1))) {
+ for(BRelation<BLOCKS, BLOCKS> _ic_d_1 : Arrays.asList(nxt.functionCall(_ic_c_1))) {
+ if(!(new BBoolean(!new BBoolean(_ic_d_1.range().elementOf(_ic_b_1).booleanValue() && _ic_a_1.equal(_ic_d_1.inverse().functionCall(_ic_b_1)).booleanValue()).booleanValue() || rsrtbl.functionCall(_ic_a_1).unequal(_ic_c_1).booleanValue())).booleanValue()) {
+ _ic_boolean_13 = new BBoolean(false);
+ break;
+ }
+
+ }
+
+ }
+
+ }
+ }
+
+ return _ic_boolean_13.booleanValue();
+ }
+
+ public boolean _check_inv_7() {
+ return rsrtbl.checkDomain(resbl).and(rsrtbl.checkRange(resrt)).and(rsrtbl.isFunction()).and(rsrtbl.isTotal(resbl)).booleanValue();
+ }
+
+ public boolean _check_inv_8() {
+ return rsrtbl.subset(rtbl).booleanValue();
+ }
+
+ public boolean _check_inv_9() {
+ return OCC.subset(resbl).booleanValue();
+ }
+
+ public boolean _check_inv_10() {
+ BBoolean _ic_boolean_14 = new BBoolean(true);
+ for(ROUTES _ic_r_1 : _ROUTES) {
+ for(BRelation<BLOCKS, BLOCKS> _ic_a_1 : Arrays.asList(nxt.functionCall(_ic_r_1))) {
+ for(BSet<BLOCKS> _ic_b_1 : Arrays.asList(rsrtbl.inverse().relationImage(new BSet<ROUTES>(_ic_r_1)))) {
+ for(BSet<BLOCKS> _ic_c_1 : Arrays.asList(_ic_b_1.difference(OCC))) {
+ if(!(new BBoolean(new BBoolean(_ic_a_1.relationImage(rtbl.inverse().relationImage(new BSet<ROUTES>(_ic_r_1)).difference(_ic_b_1)).intersect(_ic_c_1).equal(new BSet<BLOCKS>()).booleanValue() && _ic_a_1.relationImage(_ic_b_1).subset(_ic_b_1).booleanValue()).booleanValue() && _ic_a_1.relationImage(_ic_c_1).subset(_ic_c_1).booleanValue())).booleanValue()) {
+ _ic_boolean_14 = new BBoolean(false);
+ break;
+ }
+
+ }
+
+ }
+
+ }
+
+ }
+
+ return _ic_boolean_14.booleanValue();
+ }
+
+ public boolean _check_inv_11() {
+ return frm.subset(resrt).booleanValue();
+ }
+
+ public boolean _check_inv_12() {
+ 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 Train_1_beebook_deterministic_MC_POR_v2 _copy() {
+ return new Train_1_beebook_deterministic_MC_POR_v2(fst, lst, nxt, rtbl, LBT, TRK, frm, OCC, resbl, resrt, rsrtbl);
+ }
+
+
+
+
+}
diff --git a/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.json b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.json
new file mode 100644
index 0000000000000000000000000000000000000000..e1eabf3eb28a551a7518130cab8541f3c16cccef
--- /dev/null
+++ b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.json
@@ -0,0 +1,72 @@
+{
+ "machineName": "Train_1_beebook_deterministic_MC_POR_v2",
+ "variables": [
+ "_get_LBT",
+ "_get_TRK",
+ "_get_frm",
+ "_get_OCC",
+ "_get_resbl",
+ "_get_resrt",
+ "_get_rsrtbl"
+ ],
+ "operationFunctions": [
+ {
+ "opName": "route_reservation",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$ROUTES"
+ ]
+ },
+ {
+ "opName": "route_freeing",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$ROUTES"
+ ]
+ },
+ {
+ "opName": "FRONT_MOVE_1",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$ROUTES"
+ ]
+ },
+ {
+ "opName": "FRONT_MOVE_2",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$BLOCKS"
+ ]
+ },
+ {
+ "opName": "BACK_MOVE_1",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$BLOCKS"
+ ]
+ },
+ {
+ "opName": "BACK_MOVE_2",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$BLOCKS"
+ ]
+ },
+ {
+ "opName": "point_positionning",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$ROUTES"
+ ]
+ },
+ {
+ "opName": "route_formation",
+ "parameterTypes": [
+ "Train_1_beebook_deterministic_MC_POR_v2$ROUTES"
+ ]
+ }
+ ],
+ "transitionEvaluationFunctions": {
+ "point_positionning": "_tr_point_positionning",
+ "route_reservation": "_tr_route_reservation",
+ "FRONT_MOVE_1": "_tr_FRONT_MOVE_1",
+ "BACK_MOVE_1": "_tr_BACK_MOVE_1",
+ "FRONT_MOVE_2": "_tr_FRONT_MOVE_2",
+ "route_formation": "_tr_route_formation",
+ "route_freeing": "_tr_route_freeing",
+ "BACK_MOVE_2": "_tr_BACK_MOVE_2"
+ }
+}
diff --git a/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.mch b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.mch
new file mode 100644
index 0000000000000000000000000000000000000000..40a4dc747dda7a17e0f51b6ae90f4940fdc25c82
--- /dev/null
+++ b/Beispiele/Train_1_beebook_deterministic_MC_POR_v2.mch
@@ -0,0 +1,173 @@
+MACHINE Train_1_beebook_deterministic_MC_POR_v2
+SETS /* enumerated */
+ BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N};
+ ROUTES={R1,R2,R3,R4,R5,R6,R7,R8,R9,R10}
+CONCRETE_CONSTANTS
+ fst,
+ lst,
+ nxt,
+ rtbl
+ABSTRACT_VARIABLES
+ LBT,
+ TRK,
+ frm,
+ OCC,
+ resbl,
+ resrt,
+ rsrtbl
+/* PROMOTED OPERATIONS
+ route_reservation,
+ route_freeing,
+ FRONT_MOVE_1,
+ FRONT_MOVE_2,
+ BACK_MOVE_1,
+ BACK_MOVE_2,
+ point_positionning,
+ route_formation */
+PROPERTIES
+ /* @axm2 */ dom(rtbl) = BLOCKS
+ & /* @axm3 */ ran(rtbl) = ROUTES
+ & /* @axm4 */ nxt : ROUTES --> (BLOCKS >+> BLOCKS)
+ & /* @axm5 */ fst : ROUTES --> BLOCKS
+ & /* @axm6 */ lst : ROUTES --> BLOCKS
+ & /* @axm7 */ fst~ <: rtbl
+ & /* @axm8 */ lst~ <: rtbl
+ & /* @axm11 */ !(r).(r : ROUTES => fst(r) /= lst(r))
+ & /* @axm10 */ !(r).(r : ROUTES => !(S).(S <: ran(nxt(r)) & S <: nxt(r)[S] => S = {}))
+ & /* @axm9 */ !(r).(r : ROUTES => nxt(r) : (rtbl~)[{r}] \ {lst(r)} >->> (rtbl~)[{r}] \ {fst(r)})
+ & /* @axm12 */ !(r,s).((r : ROUTES & s : ROUTES) & r /= s => fst(r) /: (rtbl~)[{s}] \ {fst(s),lst(s)})
+ & /* @axm13 */ !(r,s).((r : ROUTES & s : ROUTES) & r /= s => lst(r) /: (rtbl~)[{s}] \ {fst(s),lst(s)})
+ & /* @compute_rtbl_from_nxt */ rtbl = {b,r|b : BLOCKS & r : ROUTES & (r : dom(nxt) & (b : dom(nxt(r)) or b : ran(nxt(r))))}
+ & /* @axm40 */ nxt = {R1 |-> {L |-> A,A |-> B,B |-> C},R2 |-> {L |-> A,A |-> B,B |-> D,D |-> E,E |-> F,F |-> G},R3 |-> {L |-> A,A |-> B,B |-> D,D |-> K,K |-> J,J |-> N},R4 |-> {M |-> H,H |-> I,I |-> K,K |-> F,F |-> G},R5 |-> {M |-> H,H |-> I,I |-> J,J |-> N},R6 |-> {C |-> B,B |-> A,A |-> L},R7 |-> {G |-> F,F |-> E,E |-> D,D |-> B,B |-> A,A |-> L},R8 |-> {N |-> J,J |-> K,K |-> D,D |-> B,B |-> A,A |-> L},R9 |-> {G |-> F,F |-> K,K |-> I,I |-> H,H |-> M},R10 |-> {N |-> J,J |-> I,I |-> H,H |-> M}}
+ & /* @axm41 */ fst = {R1 |-> L,R2 |-> L,R3 |-> L,R4 |-> M,R5 |-> M,R6 |-> C,R7 |-> G,R8 |-> N,R9 |-> G,R10 |-> N}
+ & /* @axm42 */ lst = {R1 |-> C,R2 |-> G,R3 |-> N,R4 |-> G,R5 |-> N,R6 |-> L,R7 |-> L,R8 |-> L,R9 |-> M,R10 |-> M}
+INVARIANT
+ /* @inv1 */ TRK : BLOCKS >+> BLOCKS
+
+ & /* @inv4 */ !(r,a).(r : resrt \ frm & a = {r} => rtbl |> a = rsrtbl |> a)
+ & /* @inv5 */ !(x,y).(x : dom(TRK) & y : TRK[{x}] => #(r).(r : ROUTES & x |-> y : nxt(r)))
+ & /* @inv6 */ !(r,a).(r : frm & a = (rsrtbl~)[{r}] => a <| nxt(r) = a <| TRK)
+ & /* @inv7 */ LBT <: OCC
+ & /* @inv8 */ !(a,b,c,d).(a : dom(rsrtbl) & b : LBT & c = rsrtbl(b) & d = nxt(c) &
+ (b : ran(d) & (a = (d~)(b))) => rsrtbl(a) /= c)
+ & /* @inv9 */ rsrtbl : resbl --> resrt
+ & /* @inv10 */ rsrtbl <: rtbl
+ & /* @inv11 */ OCC <: resbl
+ & /* @inv12 */ !(r,a,b,c).(r : ROUTES & a = nxt(r) & b = (rsrtbl~)[{r}] & c = b \ OCC =>
+ a[(rtbl~)[{r}] \ b] /\ c = {} &
+ a[b] <: b &
+ a[c] <: c)
+ & /* @inv2 */ frm <: resrt
+ & /* @inv3 */ rsrtbl[OCC] <: frm
+ASSERTIONS
+ /* @thm1 */ !(b).(b : OCC & b : dom(TRK) => nxt(rsrtbl(b))(b) = TRK(b));
+ /* @thm2 */ ran(lst) /\ dom(TRK) \ ran(fst) = {};
+ /* @thm3 */ ran(fst) /\ ran(TRK) \ ran(lst) = {}
+INITIALISATION
+ resrt := {}
+ ||
+ resbl := {}
+ ||
+ rsrtbl := {}
+ ||
+ OCC := {}
+ ||
+ TRK := {}
+ ||
+ frm := {}
+ ||
+ LBT := {}
+
+OPERATIONS
+ route_reservation(r) =
+
+ PRE
+ /* @grd1 */ r : ROUTES \ resrt
+ & /* @grd2 */ (rtbl~)[{r}] /\ resbl = {}
+ & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */
+ THEN
+ resrt := resrt \/ {r}
+ ||
+ rsrtbl := rsrtbl \/ (rtbl |> {r})
+ ||
+ resbl := resbl \/ (rtbl~)[{r}]
+ END;
+
+ route_freeing(r) =
+ PRE
+ /* @grd1 */ r : resrt \ ran(rsrtbl)
+ THEN
+ resrt := resrt \ {r}
+ ||
+ frm := frm \ {r}
+ END;
+
+ FRONT_MOVE_1(r) =
+ PRE
+ /* @grd1 */ r : frm
+ & /* @grd3 */ fst(r) : resbl \ OCC
+ & /* @grd2 */ r = rsrtbl(fst(r))
+ & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */
+ THEN
+ OCC := OCC \/ {fst(r)}
+ ||
+ LBT := LBT \/ {fst(r)}
+ END;
+
+ FRONT_MOVE_2(b) =
+ PRE
+ /* @grd1 */ b : OCC /\ dom(TRK)
+ & /* @grd2 */ TRK(b) /: OCC
+ THEN
+ OCC := OCC \/ {TRK(b)}
+ END;
+
+ BACK_MOVE_1(b) =
+ PRE
+ /* @grd1 */ b : LBT \ dom(TRK)
+ & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */
+ THEN
+ OCC := OCC \ {b}
+ ||
+ rsrtbl := {b} <<| rsrtbl
+ ||
+ resbl := resbl \ {b}
+ ||
+ LBT := LBT \ {b}
+ END;
+
+ BACK_MOVE_2(b) =
+ PRE
+ /* @grd1 */ b : LBT /\ dom(TRK)
+ & /* @grd2 */ TRK(b) : OCC
+ & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */
+ THEN
+ OCC := OCC \ {b}
+ ||
+ rsrtbl := {b} <<| rsrtbl
+ ||
+ resbl := resbl \ {b}
+ ||
+ LBT := LBT \ {b} \/ {TRK(b)}
+
+ END;
+
+ point_positionning(r) =
+ PRE
+ /* @grd1 */ r : resrt \ frm
+ & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */
+ THEN
+ TRK := ((dom(nxt(r)) <<| TRK) |>> ran(nxt(r))) \/ nxt(r)
+ END;
+
+ route_formation(r) =
+ PRE
+ /* @grd1 */ r : resrt \ frm
+ & /* @grd2 */ (rsrtbl~)[{r}] <| nxt(r) = (rsrtbl~)[{r}] <| TRK
+ & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */
+ THEN
+ frm := frm \/ {r}
+ END
+
+END
+
diff --git a/Beispiele/scheduler_deterministic_MC.mch b/Beispiele/scheduler_deterministic_MC.mch
new file mode 100644
index 0000000000000000000000000000000000000000..8447d8f18084c7c44f27d319d6c5626dafca7ff3
--- /dev/null
+++ b/Beispiele/scheduler_deterministic_MC.mch
@@ -0,0 +1,63 @@
+MACHINE scheduler_deterministic_MC
+
+SETS
+ PID = {process1,process2,process3}
+
+VARIABLES active, ready, waiting
+
+DEFINITIONS
+ ASSERT_LTL == "G([new]=> X e(del))"; /* This formula is true */
+
+INVARIANT active : POW(PID) & ready : POW(PID) & waiting: POW(PID) & /* the types */
+ /* and now the rest of the invariant */
+ active <: PID &
+ ready <: PID &
+ waiting <: PID &
+ (ready /\ waiting) = {} &
+ active /\ (ready \/ waiting) = {} &
+ card(active) <= 1
+
+INITIALISATION
+ active := {}; ready := {}; waiting := {}
+
+OPERATIONS
+
+new(pp) =
+ SELECT
+ pp : PID &
+ pp /: active &
+ pp /: (ready \/ waiting)
+ THEN
+ waiting := (waiting \/ { pp })
+ END;
+
+del(pp) =
+ SELECT
+ pp : waiting
+ THEN
+ waiting := waiting - { pp }
+ END;
+
+ready(rr) =
+ SELECT
+ rr : waiting
+ THEN
+ waiting := (waiting - {rr});
+ IF (active = {}) THEN
+ active := {rr}
+ ELSE
+ ready := ready \/ {rr}
+ END
+ END;
+
+swap(pp) =
+ PRE pp : PID & ((ready /= {}) => pp : ready) & active /= {} THEN
+ waiting := (waiting \/ active);
+ IF (ready = {}) THEN
+ active := {}
+ ELSE
+ active := {pp};
+ ready := ready - {pp}
+ END
+ END
+END
\ No newline at end of file
diff --git a/Beispiele/sort_m2_data100_MC.mch b/Beispiele/sort_m2_data100_MC.mch
new file mode 100644
index 0000000000000000000000000000000000000000..46b44c6b47dbaddf6928f3d71f8a1ab1f803dd93
--- /dev/null
+++ b/Beispiele/sort_m2_data100_MC.mch
@@ -0,0 +1,82 @@
+MACHINE sort_m2_data1000_MC
+// a version where some assertions and invariants are simplified/removed
+// so that TLC4B can infer a function type for f and g
+CONCRETE_CONSTANTS
+ n,
+ f
+ABSTRACT_VARIABLES
+ j,
+ k,
+ l,
+ g
+/* PROMOTED OPERATIONS
+ progress,
+ prog1,
+ prog2,
+ final_evt */
+PROPERTIES
+ n : INTEGER
+ & n = 100
+ & /* @sort_c0:axm1 */ n > 0
+ & /* @sort_c0:axm2 */ f : 1 .. n >-> NATURAL
+ & /* @sort_c0_data100:prob_f */ f = %i.(i : 1 .. n| 15000 - i)
+INVARIANT
+ /* @sort_m2:inv1_m2 */ j >= k & j <= n
+ & /* @sort_m2:inv2_m2 */ l >= k & j <= j
+ & /* @sort_m2:inv3_m2 */ g(l) = min(g[k .. j])
+ & /* @sort_m1:inv1_m1 */ g : 1 .. n >-> NATURAL
+
+INITIALISATION
+ BEGIN
+ g := f
+ ||
+ k := 1
+ ||
+ l := 1
+ ||
+ j := 1
+ END
+OPERATIONS
+ progress =
+ SELECT
+ /* @sort_m2_data100:grd1 */ k /= n
+ & /* @sort_m2_data100:grd2 */ j = n
+ THEN
+ g := g <+ ({k |-> g(l)} <+ {l |-> g(k)})
+ ||
+ k := k + 1
+ ||
+ j := k + 1
+ ||
+ l := k + 1
+ END;
+
+ prog1 =
+ SELECT
+ /* @sort_m2_data100:grd1 */ k /= n
+ & /* @sort_m2_data100:grd2 */ j /= n
+ & /* @sort_m2_data100:grd3 */ g(l) <= g(j + 1)
+ THEN
+ l := l
+ ||
+ j := j + 1
+ END;
+
+ prog2 =
+ SELECT
+ /* @sort_m2_data100:grd1 */ k /= n
+ & /* @sort_m2_data100:grd2 */ j /= n
+ & /* @sort_m2_data100:grd3 */ g(l) > g(j + 1)
+ THEN
+ j := j + 1
+ ||
+ l := j + 1
+ END;
+
+ final_evt =
+ SELECT
+ /* @sort_m2_data100:grd1 */ k = n
+ THEN
+ skip
+ END
+END
diff --git a/notes b/notes
index ea2ee9c4c5c25f33ac8e3a97557f64b2ab02339d..6b3654a5c7cdbb2f505da85e9711c11b5d00558d 100644
--- a/notes
+++ b/notes
@@ -4,5 +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
No Invariant Violations, No Deadlocks