only initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state_1
 safety this and next spec_state_1
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 if a motor is in the middle of moving, all the other motors stop
 the dropping stage starts when we kick the cube in and ends when we drop it into its heap
 we do not drop at the start, and the spped level starts at 1
 if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
 change the bottom motor's direction iff an edge has been reached
 seek the heap for the current cube until it is found
 when the heap is found, drop the cube into it through the tray
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if we pause, this means no motors move and all the rest of the stats remain the same
 initial state
 transitions
 initial state
 transitions
 no pause is eternal
 if we pause, this means no motors move and all the rest of the stats remain the same
 aside from the WAIT stage, spec_currentColor never changes
 only one motors moves at a time
 spec_allsleep is true iff all motors sleep
 motors are asleep at the start
 if there is no cube and we are not currently moving a cube, all motors sleep
 once seeing a cube, verMot kicks it in
 after the cube has been kicked in, move to the right angle
 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]
 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]
 after moving to the right angle, move the cube into the heap [we're GOING]
 after the cube has been dropped into the heap, return to original position. Wait for the motor to finish returning before doing anything else
 after the bottom motor finished moving, return to starting stage
 reduce the number of cubes left to soft iff a cycle has been finished
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 only one motors moves at a time
 motors are asleep at the start
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state__seek
 safety this and next spec_state__seek
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 only one motors moves at a time
 if a motor is in the middle of moving, all the other motors stop
 the dropping stage starts when we kick the cube in and ends when we drop it into its heap
 we do not drop at the start, and the spped level starts at 1
 if there are no more cubes, await a new input
 when you are back in the original position, reduce the current number of cubes to drop by 1
 if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
 seek the heap for the current cube until it is found
 when the heap is found, drop the cube into it through the tray
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 only one motors moves at a time
 if a motor is in the middle of moving, all the other motors stop
 the dropping stage starts when we kick the cube in and ends when we drop it into its heap
 we do not drop at the start, and the spped level starts at 1
 if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
 seek the heap for the current cube until it is found
 when the heap is found, drop the cube into it through the tray
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 only one motors moves at a time
 initial assignments: initial spec_state_seek
 safety this and next spec_state_seek
 equivalence of satisfaction
 initial assignments: initial spec_state_return
 safety this and next spec_state_return
 equivalence of satisfaction
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 initial state
 transitions
 initial state
 transitions
 initial assignments: initial spec_state
 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)
 equivalence of satisfaction
 no pause is eternal
 if we pause, this means no motors move and all the rest of the stats remain the same
 aside from the WAIT stage, botMotColor never changes
 only one motors moves at a time
 spec_allsleep is true iff all motors sleep
 motors are asleep at the start
 if there is no cube and we are not currently moving a cube, all motors sleep
 once seeing a cube, verMot kicks it in
 after the cube has been kicked in, move to the right angle
 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]
 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]
 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]
 after moving to the right angle, move the cube into the heap [we're GOING]
 after the cube has been dropped into the heap, return to original position. Wait for the motor to finish returning before doing anything else
 after the bottom motor finished moving, return to starting stage
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 only one motors moves at a time
 if a motor is in the middle of moving, all the other motors stop
 the dropping stage starts when we kick the cube in and ends when we drop it into its heap
 we do not drop at the start, and the spped level starts at 1
 if there are no more cubes, await a new input
 when you are back in the original position, reduce the current number of cubes to drop by 1
 if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
 seek the heap for the current cube until it is found
 when the heap is found, drop the cube into it through the tray
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is pressed, increase the speed by one level
 if the speed button is released, the speed remains the same
 initial state
 transitions
 initial state
 transitions
