motSpeed = LEVEL1 & !spec_dropping
!spec_dropping & motSpeed = LEVEL1 & spec_pausing = GO & direction = RIGHT
!spec_waiting_ack_ver_mot
!spec_waiting_ack_hor_mot
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor))
spec_state=S0
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=go,(spec_haltButtonValidPressed=true))
motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = go
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=GO,(spec_haltButtonValidPressed=true))
motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = GO
!spec_dropping & motSpeed = LEVEL1
store_place = false & motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = go
motSpeed = LEVEL1
respondsTo(color!=BLACK,(detect=spec_currentColor&horMot=MOVE))
spec_state_1=S0
spec_state__seek=S0
spec_state_return=S0
spec_state_seek=S0
elevMot=STOP
balancer=STP
spec_blockedState=S0
spec_mode=AUTO
balancerSpeed=REGULAR
spec_moveAwayFromFrontObstacleState=S0
spec_moveAwayFromBackObstacleState=S0
spec_forwardingState=S0
spec_backwardingState=S0
spec_specState = Q0
spec_turnState = T0
spec_nextMoveMode = FWD
spec_search = M0
search = M0 & spec_state = Q0
spec_nextHead = SO
respondsTo((Noise=NOISE),(Heading=spec_nextHead))
specState = Q0
turnState = T0
nextHead = SO
nextMoveMode = FWD
respondsTo((Noise=NOISE),(Heading=nextHead))
( spec_policy=SEEKING )
( policy=SEEKING )
( policy=SEEKING)
spec_b2f=S0
spec_f2b=S0
spec_policy=SEEKING & !spec_park
respondsTo(!(spec_policy=PARKED),!(throttle=STOP))
( spec_policy=SEEKING |( spec_policy=MEASURING & parkCommand = START))
( spec_policy=SEEKING)
(carStatus = SEEKING_FOR_PS & sensorMot = FWD & spec_counter = 0)
respondsTo(carStatus=MEASURE_PARKING,(carStatus=PREPARE_FOR_PARALLEL_PARKING|carStatus=ALIGN_BEFORE_PARKING))
respondsTo(carStatus=PREPARE_FOR_PARALLEL_PARKING,(spec_counter=preparingParallelSteps))
respondsTo((carStatus=ALIGN_BEFORE_PARKING),(carStatus=PERPENDICULAR|carStatus=PARALLEL))
respondsTo(carStatus=MEASURE_PARKING,(carStatus=PREPARE_FOR_PARALLEL_PARKING|carStatus=PERPENDICULAR))
respondsTo((carStatus=BYPASSING),(carStatus=SEEKING_FOR_PS))
stopping & !doorReq & !startTechnicalJob
stopping & doorReq=NIL
pRespondsToS(noRequests & readyToBaseStation, atBaseStation)
stopping & doorReq=NIL & !startTechnicalJob & noRequests
pRespondsToS(noRequests & longTimeWithoutRequests, atBaseStation)
stopping & doorReq=NIL & noRequests & !startTechnicalJob
pRespondsToS(forwarding, noRequestsFwd)
pRespondsToS(backwarding, noRequestsBwd)
stopping & doorReq=NIL & noRequests 
stopping & noTasks
stopping
stopping & countTimeSinceReqs
stopping & countTimeSinceReqs & !doorReq
stopping & !doorReq
stopping & !accelerating & !slowingDown
pHolds_afterQuntilR(openningDoors,doorsAreClosed,doorsAreFullyOpened)
pHolds_afterQuntilR(closingDoors,doorsAreFullyOpened,doorsAreClosed)
pHolds_afterQuntilR(goingUp,floor0,floor1)
pHolds_afterQuntilR(goingDown,floor1,floor0)
(!moving) & (keepDoorsState) & (!lightIsOn) 
pHolds_afterQuntilR(!openningDoors,firstStateAtDesignatedFloor,seconds3)
pHolds_afterQuntilR(openningDoors,firstStateAtDesignatedFloor&seconds3,doorsAreFullyOpened)
pHolds_afterQuntilR(keepDoorsState,doorsAreFullyOpened,seconds5)
(stayInPlace) & (keepDoorsState)
!sound_c
(stayingSameHeigt)&(keepDoorsState)&(!lightIsOn)&(!anyCalls)
pRespondsToS(calls_c[0],floor0)
(stayingSameHeigt)&(keepDoorsState)&(!lightIsOn)
(!memCalls[0])&(!memCalls[1])&(!memCalls[2])&(!memCalls[3])
pRespondsToS(calls_c[1],floor1)
(!moving)&(keepDoorsState)&(!lightIsOn)
pRespondsToS(calls_c[2],floor2)
pRespondsToS(calls_c[3],floor3)
pBecomesTrue_betweenQandR(floor0,returnTo0,goingUp|!moving)
pBecomesTrue_betweenQandR(doorsAreFullyOpened,atFloorThatCalled&(!moving),moving|keepDoorsState|closingDoors)
(!memCalls[0]) & (!memCalls[1]) & (!memCalls[2]) & (!memCalls[3]) 
pRespondsToS (calls_c[0], floor0) 
pRespondsToS (calls_c[1], floor1) 
pRespondsToS (calls_c[2], floor2) 
pRespondsToS (calls_c[3], floor3) 
pBecomesTrue_betweenQandR (floor0&doorsAreClosed, returnTo0,goingUp|!moving|openningDoors|keepDoorsState) 
pBecomesTrue_betweenQandR(doorsAreFullyOpened, justStoppedAtDesignatedFloor,moving|closingDoors|(keepDoorsState&seconds3)) 
pHolds_afterQuntilR(goingUp,floor0,floor3)
pHolds_afterQuntilR(goingDown,floor3,floor0)
pHolds_afterQuntilR(!moving,atDesignatedFloor,!atDesignatedFloor)
pHolds_afterQuntilR(!openningDoors,firstMomentAtDesignatedFloor,seconds3)
pHolds_afterQuntilR(openningDoors,firstMomentAtDesignatedFloor&seconds3,doorsAreFullyOpened)
mode = PARKING & driveMotor = STOP & steeringMotor = STRAIGHT & velocity=0
mode = PARKING & driveMotor = STOP & steeringMotor = STRAIGHT
stopping & senseMotor = REVERSE
mode = SEARCHING & stopping & steeringMotor = STRAIGHT
mode = SEARCHING & senseMotor = SIDE & steeringMotor = STRAIGHT
mode = SEARCHING & senseMotor = SIDE & steeringMotor = STRAIGHT & stopping
pRespondsToS(deepEnoughtToPark, reverseParking)
pRespondsToS(wideEnoughtToPark, parallelParking)
parkingMode = NONE
pRespondsToS(foundAParallelSpot, parallelParking)
pRespondsToS(foundAReverseSpot, reverseParking)
senseMotor = DRIVE
stopping & senseMotor = DRIVE & parkingMode = NONE & steeringMotor = 45
stopping & senseMotor = SCANNING & steeringMotor = STRAIGHT
stopping & steeringMotor = STRAIGHT & senseMotor = REVERSE
mode = SEARCHING & steeringMotor = STRAIGHT & stopping
pRespondsToS( ((mode = SEARCHING | mode = SCANNING) & (sideSense > 1)), mode != SEARCHING | mode != SCANNING | sideSense = 1)
mode = INIT
!initDone
a!=b
from != to
assign(from, fromColor)
assign(to, toColor)
hanoiAssign(hanoiFrom, hanoiFromColor)
hanoiAssign(hanoiTo, hanoiToColor)
!secondStep
