Skip to content
Snippets Groups Projects
Commit bb26543f authored by Fabian Vu's avatar Fabian Vu
Browse files

Add Landing Gear, Train, and original B models

parent 5ae06cb9
No related branches found
No related tags found
No related merge requests found
Showing with 3429 additions and 0 deletions
File moved
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
/******************************************************************************
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
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);
}
}
{
"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"
}
}
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
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
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
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);
}
}
{
"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"
}
}
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
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
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
...@@ -4,5 +4,7 @@ Scheduler: 35 states, 144 transitions ...@@ -4,5 +4,7 @@ Scheduler: 35 states, 144 transitions
Sorting Algorithm: 5050 states, 5050 transitions Sorting Algorithm: 5050 states, 5050 transitions
Cruise Controller: 1360 states, 26148 transitions Cruise Controller: 1360 states, 26148 transitions
CAN BUS: 132598 states, 340264 transitions CAN BUS: 132598 states, 340264 transitions
Landing Gear: 131328 states, 884369 transitions
Train: 672174 states, 2244486 transitions
No Invariant Violations, No Deadlocks No Invariant Violations, No Deadlocks
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment