ColorSort , 
, "  ", 
, " after moving to the right angle, move the cube into the heap [we're GOING]
 \n ", 
, " after the bottom motor finished moving, return to starting stage
 \n ", 
, " after the cube has been dropped into the heap, return to original position. Wait for the motor to finish returning before doing anything else
 \n ", 
, " after the cube has been kicked in, move to the right angle
 \n ", 
, " aside from the WAIT stage, botMotColor never changes
 \n ", 
, " aside from the WAIT stage, spec_currentColor never changes
 \n ", 
, " change the bottom motor's direction iff an edge has been reached
 \n ", 
, " equivalence of satisfaction
 \n ", 
, " ext haltButton: {PRESS, RELEASE};
 \n ", 
, " if a motor is in the middle of moving, all the other motors stop
 \n ", 
, " if the speed button is pressed, increase the speed by one level
 \n ", 
, " if the speed button is released, the speed remains the same
 \n ", 
, " if there are no more cubes, await a new input
 \n ", 
, " if there is no cube and we are not currently moving a cube, all motors sleep
 \n ", 
, " if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
 \n ", 
, " if we pause, this means no motors move and all the rest of the stats remain the same
 \n ", 
, " initial assignments: initial spec_state
 \n ", 
, " initial assignments: initial spec_state_1
 \n ", 
, " initial assignments: initial spec_state__seek
 \n ", 
, " initial assignments: initial spec_state_return
 \n ", 
, " initial assignments: initial spec_state_seek
 \n ", 
, " initial state
 \n ", 
, " motors are asleep at the start
 \n ", 
, " new spec_waiting_ack_bot_mot:boolean;
 \n ", 
, " no pause is eternal
 \n ", 
, " once seeing a cube, verMot kicks it in
 \n ", 
, " only \n ", 
, " only one motors moves at a time
 \n ", 
, " reduce the number of cubes left to soft iff a cycle has been finished
 \n ", 
, " safety this and next spec_state_1
 \n ", 
, " safety this and next spec_state__seek
 \n ", 
, " safety this and next spec_state_return
 \n ", 
, " safety this and next spec_state_seek
 \n ", 
, " seek the heap for the current cube until it is found
 \n ", 
, " spec_allsleep is true iff all motors sleep
 \n ", 
, " the cube ALWAYS falls into the correct heap ((detect = botMotColor) = p, (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) = q, (ack_ver_hor = MOVE & spec_stage = DROP) = r)
 \n ", 
, " the cube ALWAYS falls into the correct heap ((detect = spec_currentColor) = p, (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) = q, (ack_ver_hor = MOVE & spec_stage = DROP) = r)
 \n ", 
, " the dropping stage starts when we kick the cube in and ends when we drop it into its heap
 \n ", 
, " transitions
 \n ", 
, " we do not drop at the start, and the spped level starts at 1
 \n ", 
, " when the heap is found, drop the cube into it through the tray
 \n ", 
, " when you are back in the original position, reduce the current number of cubes to drop by 1
 \n ", 
, " while the bottom motor is moving, see if the color has been found [botMot STOPPED MOVING and the color has NOT been found; we're GOING]
 \n ", 
, " while the bottom motor is moving, see if the color has been found [botMot is MOVING and the color has NOT been found; we're GOING]
 \n ", 
, 
Elevator , 
, "  ", 
, " G (elevMot = BWD) -> next(obstacle = CLEAR); \n ", 
, " G (obstacle=BLOCKED -> !(elevMot = FWD & elevMot = FWD));
 \n ", 
, " LTLSPEC -- safety requirement
 \n ", 
, " LTLSPEC -- stop at floor
 \n ", 
, " LTLSPECENV
 \n ", 
, " change direction at lower floor
 \n ", 
, " change direction at upper floor
 \n ", 
, " ext \n ", 
, " ext doorMot : {FWD, BWD, STP};
 \n ", 
, " floor=LOWER & elevMot!=STOP | floor=UPPER & elevMot!=STOP -> elevMot=STOP;
 \n ", 
, " goal of forklift
 \n ", 
, " initial state
 \n ", 
, 
GyroLTL , 
, "  ", 
, " !G ((bluetoothCmd=AUTO) -> ((distSense=BLOCKED & balancer=STP & isReady) -> next(!(balancer=STP)))); // maybe remove and replace with env assumptions
 \n ", 
, " !LTLSPEC
 \n ", 
, " //////////////////////////////////////////////////////////
 \n ", 
, " ////////////////////////////////////////////////////////// \n ", 
, " Any non driving command from the bluetooth controller saves the last manual mode command
 \n ", 
, " Back surface becomes blocked responds to continuously moving backward
 \n ", 
, " Back surface becomes clear responds to continuously moving away from obstacle.
 \n ", 
, " Changing speed logic:
 \n ", 
, " Connecting bluetooth command to manual command local variable
 \n ", 
, " Eventually the robot will be ready to move.
 \n ", 
, " Front surface becomes blocked responds to continuously moving forward.
 \n ", 
, " Front surface becomes clear responds to continuously moving away from obstacle.
 \n ", 
, " G ((bluetoothCmd=AUTO) -> ((balancer=FWD) -> next((bluetoothCmd=AUTO) -> !(balancer=TURN_RIGHT | balancer=TURN_LEFT)))); 
 \n ", 
, " G F (balancer=FWD);
 \n ", 
, " Initial \n ", 
, " Initial file contents for AspectLTL aspect file (*.altl)
 \n ", 
, " Initial state.
 \n ", 
, " LTLSPEC
 \n ", 
, " Manual mode specifications:
 \n ", 
, " Move backward only when there are no obstacles behind.
 \n ", 
, " Move forward only when there are no obstacles ahead.
 \n ", 
, " Pattern #20 for: turning happens when blocked until clear
 \n ", 
, " Pattern for: back surface becomes blocked responds to continuously moving backward
 \n ", 
, " Pattern for: back surface becomes clear responds to continuously moving away from obstacle
 \n ", 
, " Pattern for: front surface becomes blocked responds to continuously moving forward
 \n ", 
, " Pattern for: front surface becomes clear responds to continuously moving away from obstacle
 \n ", 
, " Pattern for: turning happens when blocked until clear
 \n ", 
, " Robot starts when not blocked forward and backward
 \n ", 
, " Stop while the robot is not ready to move.
 \n ", 
, " Switching between auto and manual modes logic:
 \n ", 
, " The robot needs to be stabilized at first and it is not ready to move.
 \n ", 
, " The robot will start in auto mode.
 \n ", 
, " When in auto mode, always move forward when there are no obstacles ahead.
 \n ", 
, " When in auto mode, eventually move forward.
 \n ", 
, " When the robot is ready, it will stay that way.
 \n ", 
, " equivalence of satisfaction
 \n ", 
, " goal of gyro
 \n ", 
, " initial assignments: initial state
 \n ", 
, " initial state
 \n ", 
, " new spec_drivingMode : {AUTO, MANUAL};
 \n ", 
, " new spec_prevspec_drivingMode : boolean;
 \n ", 
, " safety requirement
 \n ", 
, " safety this and next blockedState
 \n ", 
, " safety this and next state
 \n ", 
, " spec_drivingMode=AUTO;
 \n ", 
, 
HumanoidLTL , 
, "  ", 
, " ////////////
 \n ", 
, " ////////////////////////// 
 \n ", 
, " ////////////////////////////////////////////
 \n ", 
, " ///////////////////////////////////////////////
 \n ", 
, " //////////////////////////////////////////////////////////////
 \n ", 
, " ////////////////////////////////////////////////////////////// 
 \n ", 
, " Don't go the long path
 \n ", 
, " G ((nextMoveMode = TURN_LEFT_2 & Obstacle = BLOCKED) -> next(nextMoveMode = TURN_LEFT_1));
 \n ", 
, " G ((spec_nextMoveMode = TURN_LEFT_2 & Obstacle = BLOCKED) -> next(spec_nextMoveMode = TURN_LEFT_1));
 \n ", 
, " G ((spec_nextMoveMode = TURN_LEFT_2) -> F(spec_nextMoveMode = TURN_LEFT_2 & Obstacle = CLEAR));
 \n ", 
, " G (nextMoveMode = TURN_RIGHT <-> (next(turnState) = T1 | next(turnState) = T2));
 \n ", 
, " G (spec_nextMoveMode = TURN_LEFT <-> (next(spec_turnState) = T1 | next(spec_turnState) = T2));
 \n ", 
, " G (spec_turnState = T1 -> (F(spec_turnState) = T0));
 \n ", 
, " G (spec_turnState = T2 -> (Obstacle = CLEAR));
 \n ", 
, " G F (Button = PRESSED);
 \n ", 
, " G F (search = M0); // finally head to the right direction
 \n ", 
, " G F(Obstacle = CLEAR);
 \n ", 
, " G(!(Y(spec_specState = Q2) & Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = BWD));
 \n ", 
, " G(!(Y(spec_state = Q2) & Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = BWD));
 \n ", 
, " G(((nextMoveMode = FWD | nextMoveMode = BWD)) -> next(Heading) = Heading);
 \n ", 
, " G((Y(Y(spec_nextMoveMode = TURN_LEFT_2)) & Y(spec_nextMoveMode = FWD)) -> Obstacle = CLEAR);
 \n ", 
, " G((Y(Y(spec_spec_nextMoveMode = TURN_LEFT_2)) & Y(spec_spec_nextMoveMode = FWD)) -> Obstacle = CLEAR);
 \n ", 
, " G((Y(spec_specState = Q0) & Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = BWD) -> spec_specState = Q1);
 \n ", 
, " G((Y(spec_state = Q0) & Y(spec_nextMoveMode = FWD) & spec_nextMoveMode = BWD) -> spec_state = Q1);
 \n ", 
, " G((next(Obstacle = BLOCKED) & !((Y(spec_nextMoveMode = TURN_LEFT_2)))) -> next(!(spec_nextMoveMode = FWD)));
 \n ", 
, " G((nextMoveMode != FWD) -> F(Obstacle = CLEAR));
 \n ", 
, " G((spec_nextMoveMode != FWD) -> F(Obstacle = CLEAR));
 \n ", 
, " G(Y((spec_specState = Q1) & Y(spec_nextMoveMode = BWD) & spec_nextMoveMode = FWD) -> spec_specState = Q2);
 \n ", 
, " G(Y((spec_state = Q1) & Y(spec_nextMoveMode = BWD) & spec_nextMoveMode = FWD) -> spec_state = Q2);
 \n ", 
, " LTLSPEC
 \n ", 
, " LTLSPECENV
 \n ", 
, " calibrate after turn
 \n ", 
, " calibrate before turn
 \n ", 
, " check if needed
 \n ", 
, " ext Button : {FREE, PRESSED};
 \n ", 
, " ext Noise : {QUIET, NOISE};
 \n ", 
, " new search : {M0,M1};
 \n ", 
, " search = M0;
 \n ", 
, " state = Q0;
 \n ", 
, " to prevant robot from going FWD<-->BWD indefinitely 
 \n ", 
, " turn to degree
 \n ", 
, 
PcarLTL_394_PCar , 
, "  ", 
, " G ( (throttle = BWD & steer = LEFT) -> next(!(throttle = FWD & steer = LEFT)));
 \n ", 
, " G ( (throttle = BWD & steer = RIGHT) -> next(!(throttle = FWD & steer = RIGHT)));
 \n ", 
, " G (((obstacle = CLEAR) & (sideSense = BLOCKED)) -> !((throttle = FWD) & (steer=RIGHT)));
 \n ", 
, " Initial \n ", 
, " LTLSPEC
 \n ", 
, 
V2-SelfParkingSmartCarLTL , 
, "  ", 
, " /**********************************************************************************/
 \n ", 
, " /************************align before parking parallel ****************************/
 \n ", 
, " Initial \n ", 
, " Initial file contents for AspectLTL aspect file (*.altl)
 \n ", 
, 
V3-SelfParkingSmartCarLTL , 
, "  ", 
, " );
 \n ", 
, " -> (keepCounterValue)
 \n ", 
, " G((carStatus = PREPARE_FOR_PARALLEL_PARKING & obstacle = BLOCKED)
 \n ", 
, " Initial \n ", 
, " LTLSPEC
 \n ", 
, 
