Skip to content

GitLab

Commit 54ad3bf0 authored by Hernán Gagliardi's avatar Hernán Gagliardi
Browse files

spec translator

parent 68220e2a
Hide whitespace changes
Inline Side-by-side
Showing with 5 additions and 3428 deletions
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL2TAG_789_ColorSort.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} color ;
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {YES, NO} starting_pos ;
env {YES, NO} edge ;
env {PRESS, RELEASE} speedButton;
env {PRESS, RELEASE} haltButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {RIGHT, LEFT} direction ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
sys boolean spec_pauseButtonValidPressed ;
sys {PAUSE, GO} spec_pausing ;
define
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define
verhor_dontmove := ack_ver = SLEEP & ack_hor = SLEEP;
define
onlybotmoves := verhor_dontmove & ack_bot = MOVE;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- if a motor is in the middle of moving, all the other motors stop
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
-- currentColor keeps its value unless a new cube is kicked
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (verMot = MOVE -> color = next(spec_currentColor));
guarantee -- the dropping stage starts when we kick the cube in and ends when we drop it into its heap
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & horMot = SLEEP);
-- this is how the colorsort works when given a cube
guarantee -- we do not drop at the start, and the spped level starts at 1
motSpeed = LEVEL1 & !spec_dropping;
guarantee
!spec_dropping & motSpeed = LEVEL1 & spec_pausing = GO & direction = RIGHT;
guarantee -- if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
G (spec_pausing = GO & !spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN);
-- if we are not in the dropping stage and are at the initial position, drop a cube iff you see one
guarantee
G (!spec_dropping & starting_pos = YES & color = BLACK -> allsleep);
guarantee
G (color = BLACK | spec_dropping -> verMot = SLEEP);
guarantee
G (spec_pausing = GO & !spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE);
guarantee -- change the bottom motor's direction iff an edge has been reached
G (edge = YES <-> direction != next(direction));
guarantee -- seek the heap for the current cube until it is found
G (spec_pausing = GO & spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK);
guarantee -- when the heap is found, drop the cube into it through the tray
G (spec_pausing = GO & spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE);
-- the speed button
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL1 -> next(motSpeed = LEVEL2));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL2 -> next(motSpeed = LEVEL3));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL3 -> next(motSpeed = LEVEL1));
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed -> motSpeed = next(motSpeed));
-- the pause button
guarantee
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_pauseButtonValidPressed);
-- we pause if the button was pressed and we were going, or if it were not pressed and we were pausing already. Vice versa for going
guarantee
G ((spec_pauseButtonValidPressed & spec_pausing = GO) | (!spec_pauseButtonValidPressed & spec_pausing = PAUSE)
-> next(spec_pausing) = PAUSE);
guarantee
G ((!spec_pauseButtonValidPressed & spec_pausing = GO) | (spec_pauseButtonValidPressed & spec_pausing = PAUSE)
-> next(spec_pausing) = GO);
assumption -- no pause is eternal
respondsTo(spec_pausing=PAUSE,(spec_pausing=GO));
guarantee -- if we pause, this means no motors move and all the rest of the stats remain the same
G (spec_pausing = PAUSE -> allsleep);
-- environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
assumption
GF (ack_hor=MOVE);
-- some interesting guarantees
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL2_621_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver_hor ;
env {MOVE, SLEEP} ack_bot ;
env {NOEDGE, EDGE} atEdge ;
env {ZERO, NOTZERO} num_of_cubes;
env {PRESS, RELEASE} haltButton;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {RIGHT, LEFT, STOP, INITPOS} botMot ;
sys boolean spec_allsleep ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {REDUCE, NOTREDUCE} reduce_num_of_cubes;
sys { S0, S1, S2} spec_state ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys {WAIT, KICK, TOANGLERIGHT, TOANGLELEFT, DROP, FROMANGLE} spec_stage ;
sys boolean spec_finished_cycle;
sys boolean spec_speedButtonValidPressed ;
sys boolean spec_haltButtonValidPressed ;
sys {pause, go} spec_pausing ;
guarantee -- initial assignments: initial spec_state
spec_state=S0;
guarantee -- 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)
G ((spec_state=S0 & ((!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(detect = spec_currentColor)) | ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP)) | (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = spec_currentColor)) | (!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP) & (detect = spec_currentColor))) & next(spec_state=S0)) |
(spec_state=S0 & ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = spec_currentColor)) & next(spec_state=S1)) |
(spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = spec_currentColor)) & next(spec_state=S0)) |
(spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = spec_currentColor)) & next(spec_state=S1)) |
(spec_state=S1 & ((ack_ver_hor = MOVE & spec_stage = DROP)) & next(spec_state=S2)) |
(spec_state=S2 & next(spec_state=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state=S0|spec_state=S1);
guarantee
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed = true);
guarantee
G ((spec_haltButtonValidPressed = true & spec_pausing = go) | (spec_haltButtonValidPressed = false & spec_pausing = pause)
-> next(spec_pausing) = pause);
guarantee
G ((spec_haltButtonValidPressed = false & spec_pausing = go) | (spec_haltButtonValidPressed = true & spec_pausing = pause)
-> next(spec_pausing) = go);
guarantee -- no pause is eternal
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=go,(spec_haltButtonValidPressed=true));
guarantee -- if we pause, this means no motors move and all the rest of the stats remain the same
G (spec_pausing = pause | ack_ver_hor = MOVE ->
spec_allsleep = true & next(spec_stage) = spec_stage);
guarantee --aside from the WAIT stage, spec_currentColor never changes
G (spec_stage != WAIT -> next(spec_currentColor) = spec_currentColor);
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- spec_allsleep is true iff all motors sleep
G (spec_allsleep = true <-> verMot = SLEEP & horMot = SLEEP & botMot = STOP);
guarantee -- motors are asleep at the start
motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = go;
-- THIS IS HOW THE ROBOT WORKS WHEN NOT PAUSED
-- prior to heap search
guarantee -- if there is no cube and we are not currently moving a cube, all motors sleep
G ((color = BLACK | num_of_cubes = ZERO) & spec_stage = WAIT ->
spec_allsleep = true & next(spec_stage) = WAIT);
guarantee -- once seeing a cube, verMot kicks it in
G (color != BLACK & num_of_cubes != ZERO & spec_stage = WAIT & spec_pausing = go ->
verMot = MOVE & color = next(spec_currentColor) & next(spec_stage) = KICK);
guarantee -- after the cube has been kicked in, move to the right angle
G (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go ->
botMot = RIGHT & next(spec_stage) = TOANGLERIGHT);
-- heap search
guarantee -- 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]
G (atEdge != EDGE & spec_stage = TOANGLERIGHT & detect != spec_currentColor & spec_pausing = go ->
botMot = RIGHT & next(spec_stage) = TOANGLERIGHT);
guarantee -- 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]
G (atEdge = EDGE & spec_stage = TOANGLERIGHT & spec_pausing = go & detect != spec_currentColor ->
botMot = LEFT & next(spec_stage) = TOANGLELEFT);
guarantee -- 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]
G (spec_stage = TOANGLELEFT & spec_pausing = go & detect != spec_currentColor ->
botMot = LEFT & next(spec_stage) = TOANGLELEFT);
guarantee -- after moving to the right angle, move the cube into the heap [we're GOING]
G ((spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = spec_currentColor ->
verMot = SLEEP & horMot = MOVE & botMot = STOP & next(spec_stage) = DROP );
-- return to initial position
guarantee -- after the cube has been dropped into the heap, return to original position. Wait for the motor to finish returning before doing anything else
G (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = pause))) & spec_stage = FROMANGLE)) & spec_pausing = go ->
botMot = INITPOS & next(spec_stage) = FROMANGLE);
guarantee
G (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go);
guarantee -- after the bottom motor finished moving, return to starting stage
G (spec_finished_cycle -> spec_allsleep = true & next(spec_stage) = WAIT);
guarantee -- reduce the number of cubes left to soft iff a cycle has been finished
G (spec_finished_cycle <-> reduce_num_of_cubes = REDUCE);
-- speed button
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed = true);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
assumption -- after starting to move, we will sleep eventually
respondsTo(ack_ver_hor=MOVE,(ack_ver_hor=SLEEP));
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption
G (spec_stage != KICK & spec_stage != DROP -> ack_ver_hor = SLEEP);
assumption -- we will always finish sorting the given number of cubes
respondsTo(num_of_cubes!=ZERO,(num_of_cubes=ZERO));
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL2_794_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver_hor ;
env {MOVE, SLEEP} ack_bot ;
env {NOEDGE, EDGE} atEdge ;
env {ZERO, NOTZERO} num_of_cubes;
env {PRESS, RELEASE} haltButton;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {RIGHT, LEFT, STOP, INITPOS} botMot ;
sys boolean spec_allsleep ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {REDUCE, NOTREDUCE} reduce_num_of_cubes;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys {WAIT, KICK, TOANGLERIGHT, TOANGLELEFT, DROP, FROMANGLE} spec_stage ;
sys boolean spec_finished_cycle;
sys boolean spec_speedButtonValidPressed ;
sys boolean spec_haltButtonValidPressed ;
sys {PAUSE, GO} spec_pausing ;
guarantee
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed = true);
guarantee
G ((spec_haltButtonValidPressed = true & spec_pausing = GO) | (spec_haltButtonValidPressed = false & spec_pausing = PAUSE)
-> next(spec_pausing) = PAUSE);
guarantee
G ((spec_haltButtonValidPressed = false & spec_pausing = GO) | (spec_haltButtonValidPressed = true & spec_pausing = PAUSE)
-> next(spec_pausing) = GO);
guarantee -- no pause is eternal
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=GO,(spec_haltButtonValidPressed=true));
guarantee -- if we pause, this means no motors move and all the rest of the stats remain the same
G (spec_pausing = PAUSE | ack_ver_hor = MOVE ->
spec_allsleep = true & next(spec_stage) = spec_stage);
guarantee --aside from the WAIT stage, spec_currentColor never changes
G (spec_stage != WAIT -> next(spec_currentColor) = spec_currentColor);
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- spec_allsleep is true iff all motors sleep
G (spec_allsleep = true <-> verMot = SLEEP & horMot = SLEEP & botMot = STOP);
guarantee -- motors are asleep at the start
motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = GO;
-- THIS IS HOW THE ROBOT WORKS WHEN NOT PAUSED
-- prior to heap search
guarantee -- if there is no cube and we are not currently moving a cube, all motors sleep
G ((color = BLACK | num_of_cubes = ZERO) & spec_stage = WAIT ->
spec_allsleep = true & next(spec_stage) = WAIT);
guarantee -- once seeing a cube, verMot kicks it in
G (color != BLACK & num_of_cubes != ZERO & spec_stage = WAIT & spec_pausing = GO ->
verMot = MOVE & color = next(spec_currentColor) & next(spec_stage) = KICK);
guarantee -- after the cube has been kicked in, move to the right angle
G (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = GO ->
botMot = RIGHT & next(spec_stage) = TOANGLERIGHT);
-- heap search
guarantee -- 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]
G (atEdge != EDGE & (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & detect != spec_currentColor & spec_pausing = GO ->
(spec_stage = TOANGLERIGHT -> botMot = RIGHT) & (spec_stage = TOANGLELEFT -> botMot = LEFT) & next(spec_stage) = spec_stage);
guarantee -- 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]
G (atEdge = EDGE & (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = GO & detect != spec_currentColor ->
(spec_stage = TOANGLERIGHT -> botMot = LEFT & next(spec_stage) = TOANGLELEFT) & (spec_stage = TOANGLELEFT -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT));
/*
LTLSPEC -- 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]
G (spec_stage = TOANGLELEFT & spec_pausing = GO & detect != spec_currentColor ->
botMot = LEFT & next(spec_stage) = TOANGLELEFT);
*/
guarantee -- after moving to the right angle, move the cube into the heap [we're GOING]
G ((spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = GO & detect = spec_currentColor ->
verMot = SLEEP & horMot = MOVE & botMot = STOP & next(spec_stage) = DROP );
-- return to initial position
guarantee -- after the cube has been dropped into the heap, return to original position. Wait for the motor to finish returning before doing anything else
G (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = PAUSE))) & spec_stage = FROMANGLE)) & spec_pausing = GO ->
botMot = INITPOS & next(spec_stage) = FROMANGLE);
guarantee
G (spec_finished_cycle <-> ack_bot = SLEEP & PREV(spec_pausing = GO) & spec_stage = FROMANGLE & spec_pausing = GO);
guarantee -- after the bottom motor finished moving, return to starting stage
G (spec_finished_cycle -> spec_allsleep = true & next(spec_stage) = WAIT);
guarantee -- reduce the number of cubes left to soft iff a cycle has been finished
G (spec_finished_cycle <-> reduce_num_of_cubes = REDUCE);
-- speed button
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed = true);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
assumption -- after starting to move, we will sleep eventually
respondsTo(ack_ver_hor=MOVE,(ack_ver_hor=SLEEP));
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption
G (spec_stage != KICK & spec_stage != DROP -> ack_ver_hor = SLEEP);
assumption -- we will always finish sorting the given number of cubes
respondsTo(num_of_cubes!=ZERO,(num_of_cubes=ZERO));
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3TAG_787_ColorSort.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} color ;
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {YES, NO} starting_pos ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define
verhor_dontmove := ack_ver = SLEEP & ack_hor = SLEEP;
define
onlybotmoves := verhor_dontmove & ack_bot = MOVE;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- if a motor is in the middle of moving, all the other motors stop
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
-- currentColor keeps its value unless a new cube is kicked
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (verMot = MOVE -> color = next(spec_currentColor));
guarantee -- the dropping stage starts when we kick the cube in and ends when we drop it into its heap
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & horMot = SLEEP);
-- this is how the colorsort works when given a cube
guarantee -- we do not drop at the start, and the spped level starts at 1
!spec_dropping & motSpeed = LEVEL1;
guarantee -- if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
G (!spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN);
-- if we are not in the dropping stage and are at the initial position, drop a cube iff you see one
guarantee
G (!spec_dropping & starting_pos = YES & color = BLACK -> allsleep);
guarantee
G (color = BLACK | spec_dropping -> verMot = SLEEP);
guarantee
G (!spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE);
guarantee -- seek the heap for the current cube until it is found
G (spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK);
guarantee -- when the heap is found, drop the cube into it through the tray
G (spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE);
-- the speed button
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL1 -> next(motSpeed = LEVEL2));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL2 -> next(motSpeed = LEVEL3));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL3 -> next(motSpeed = LEVEL1));
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed -> motSpeed = next(motSpeed));
-- environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
assumption
GF (ack_hor=MOVE);
-- some interesting guarantees
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_621_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver_hor ;
env {MOVE, SLEEP} ack_bot ;
env {NOEDGE, EDGE} atEdge ;
env boolean color_seen ;
env {PRESS, RELEASE} haltButton;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {PLACE, RIGHT, LEFT, STOP, INITPOS} botMot ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} botMotColor ;
sys boolean store_place ;
sys boolean spec_allsleep ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2} spec_state ;
sys {WAIT, KICK, TOANGLEPLACE, TOANGLERIGHT, TOANGLELEFT, DROP, FROMANGLE} spec_stage ;
sys boolean spec_speedButtonValidPressed ;
sys boolean spec_haltButtonValidPressed ;
sys {pause, go} spec_pausing ;
guarantee -- initial assignments: initial spec_state
spec_state=S0;
guarantee -- 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)
G ((spec_state=S0 & ((!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(detect = botMotColor)) | ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP)) | (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = botMotColor)) | (!(ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & (ack_ver_hor = MOVE & spec_stage = DROP) & (detect = botMotColor))) & next(spec_state=S0)) |
(spec_state=S0 & ((ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go) & !(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = botMotColor)) & next(spec_state=S1)) |
(spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & (detect = botMotColor)) & next(spec_state=S0)) |
(spec_state=S1 & (!(ack_ver_hor = MOVE & spec_stage = DROP) & !(detect = botMotColor)) & next(spec_state=S1)) |
(spec_state=S1 & ((ack_ver_hor = MOVE & spec_stage = DROP)) & next(spec_state=S2)) |
(spec_state=S2 & next(spec_state=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state=S0|spec_state=S1);
guarantee
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed = true);
guarantee
G ((spec_haltButtonValidPressed = true & spec_pausing = go) | (spec_haltButtonValidPressed = false & spec_pausing = pause)
-> next(spec_pausing) = pause);
guarantee
G ((spec_haltButtonValidPressed = false & spec_pausing = go) | (spec_haltButtonValidPressed = true & spec_pausing = pause)
-> next(spec_pausing) = go);
guarantee -- no pause is eternal
respondsTo(spec_haltButtonValidPressed=true&spec_pausing=go,(spec_haltButtonValidPressed=true));
guarantee -- if we pause, this means no motors move and all the rest of the stats remain the same
G (spec_pausing = pause | ack_ver_hor = MOVE ->
spec_allsleep = true & next(spec_stage) = spec_stage);
guarantee --aside from the WAIT stage, botMotColor never changes
G (spec_stage != WAIT -> next(botMotColor) = botMotColor);
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- spec_allsleep is true iff all motors sleep
G (spec_allsleep = true <-> verMot = SLEEP & horMot = SLEEP & botMot = STOP);
guarantee -- motors are asleep at the start
store_place = false & motSpeed = LEVEL1 & spec_stage = WAIT & spec_pausing = go;
-- THIS IS HOW THE ROBOT WORKS WHEN NOT PAUSED
-- prior to heap search
guarantee -- if there is no cube and we are not currently moving a cube, all motors sleep
G (color = BLACK & spec_stage = WAIT ->
spec_allsleep = true & next(spec_stage) = WAIT);
guarantee -- once seeing a cube, verMot kicks it in
G (color != BLACK & spec_stage = WAIT & spec_pausing = go ->
verMot = MOVE & color = next(botMotColor) & next(spec_stage) = KICK);
guarantee -- after the cube has been kicked in, move to the right angle
G (ack_ver_hor = SLEEP & spec_stage = KICK & spec_pausing = go & color_seen = false ->
(color_seen = false -> botMot = RIGHT & next(spec_stage) = TOANGLERIGHT) & (color_seen = true -> botMot = PLACE & next(spec_stage) = TOANGLERIGHT));
-- placement in case the heap's location is already known
guarantee
G (ack_bot = MOVE & spec_stage = TOANGLEPLACE & spec_pausing = go ->
botMot = PLACE & next(spec_stage) = TOANGLERIGHT);
guarantee
G (ack_bot = SLEEP & spec_stage = TOANGLEPLACE & spec_pausing = go ->
horMot = MOVE & next(spec_stage) = DROP);
-- heap search
guarantee -- 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]
G (atEdge != EDGE & spec_stage = TOANGLERIGHT & detect != botMotColor & spec_pausing = go ->
botMot = RIGHT & next(spec_stage) = TOANGLERIGHT);
guarantee -- 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]
G (atEdge = EDGE & spec_stage = TOANGLERIGHT & spec_pausing = go & detect != botMotColor ->
botMot = LEFT & next(spec_stage) = TOANGLELEFT);
guarantee -- 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]
G (spec_stage = TOANGLELEFT & spec_pausing = go & detect != botMotColor ->
botMot = LEFT & next(spec_stage) = TOANGLELEFT);
guarantee -- after moving to the right angle, move the cube into the heap [we're GOING]
G ((spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = botMotColor ->
horMot = MOVE & next(spec_stage) = DROP);
guarantee
G (store_place = true <-> (spec_stage = TOANGLERIGHT | spec_stage = TOANGLELEFT) & spec_pausing = go & detect = botMotColor);
-- return to initial position
guarantee -- after the cube has been dropped into the heap, return to original position. Wait for the motor to finish returning before doing anything else
G (((ack_ver_hor = SLEEP & spec_stage = DROP) | ((ack_bot = MOVE | (ack_bot = SLEEP & PREV(spec_pausing = pause))) & spec_stage = FROMANGLE)) & spec_pausing = go ->
botMot = INITPOS & next(spec_stage) = FROMANGLE);
guarantee -- after the bottom motor finished moving, return to starting stage
G (ack_bot = SLEEP & PREV(spec_pausing = go) & spec_stage = FROMANGLE & spec_pausing = go ->
spec_allsleep & next(spec_stage) = WAIT);
-- speed button
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed = true);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = true & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed = false & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
assumption -- after starting to move, we will sleep eventually
respondsTo(ack_ver_hor=MOVE,(ack_ver_hor=SLEEP));
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption
G (spec_stage != KICK & spec_stage != DROP -> ack_ver_hor = SLEEP);
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_638_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys { S0, S1, S2} spec_state_1 ;
sys { S0, S1, S2} spec_state_2 ;
sys boolean spec_speedButtonValidPressed ;
define -- spec_allsleep is true iff all motors sleep
spec_allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- spec_nonemove is true iff no motor moves
spec_nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee -- motors are asleep at the start
motSpeed = LEVEL1;
-- this is how the robot works. MAY GOD HELP US ALL
guarantee
G (color = BLACK & spec_nonemove & spec_allsleep -> spec_allsleep);
/*
LTLSPEC
G (color != BLACK & spec_nonemove & spec_allsleep -> verMot = MOVE & next(spec_currentColor) = color);
LTLSPEC -- initial assignments: initial spec_state_1
spec_state_1=S0;
LTLSPEC -- safety this and next spec_state_1
G ((spec_state_1=S0 & ((!(verMot = MOVE) & !(ack_ver = SLEEP -> botMot = SEEK)) | ((verMot = MOVE) & (detect = spec_currentColor)) | (!(detect = spec_currentColor) & (ack_ver = SLEEP -> botMot = SEEK)) | (!(verMot = MOVE) & (detect = spec_currentColor) & (ack_ver = SLEEP -> botMot = SEEK))) & next(spec_state_1=S0)) |
(spec_state_1=S0 & ((verMot = MOVE) & !(detect = spec_currentColor) & !(ack_ver = SLEEP -> botMot = SEEK)) & next(spec_state_1=S2)) |
(spec_state_1=S1 & TRUE & next(spec_state_1=S1)) |
(spec_state_1=S2 & (!(detect = spec_currentColor) & (ack_ver = SLEEP -> botMot = SEEK)) & next(spec_state_1=S0)) |
(spec_state_1=S2 & ((detect = spec_currentColor)) & next(spec_state_1=S1)) |
(spec_state_1=S2 & (!(detect = spec_currentColor) & !(ack_ver = SLEEP -> botMot = SEEK)) & next(spec_state_1=S2)));
LTLSPECENV -- equivalence of satisfaction
(G F (spec_state_1=S0));
LTLSPEC
G (detect = spec_currentColor & PREV(botMot) = SEEK -> horMot = MOVE);
LTLSPEC -- initial assignments: initial spec_state_2
spec_state_2=S0;
LTLSPEC -- safety this and next spec_state_2
G ((spec_state_2=S0 & ((!(horMot = MOVE) & !(ack_hor = SLEEP -> botMot = RETURN)) | ((horMot = MOVE) & (ack_bot = SLEEP)) | (!(ack_bot = SLEEP) & (ack_hor = SLEEP -> botMot = RETURN)) | (!(horMot = MOVE) & (ack_bot = SLEEP) & (ack_hor = SLEEP -> botMot = RETURN))) & next(spec_state_2=S0)) |
(spec_state_2=S0 & ((horMot = MOVE) & !(ack_bot = SLEEP) & !(ack_hor = SLEEP -> botMot = RETURN)) & next(spec_state_2=S2)) |
(spec_state_2=S1 & TRUE & next(spec_state_2=S1)) |
(spec_state_2=S2 & (!(ack_bot = SLEEP) & (ack_hor = SLEEP -> botMot = RETURN)) & next(spec_state_2=S0)) |
(spec_state_2=S2 & ((ack_bot = SLEEP)) & next(spec_state_2=S1)) |
(spec_state_2=S2 & (!(ack_bot = SLEEP) & !(ack_hor = SLEEP -> botMot = RETURN)) & next(spec_state_2=S2)));
LTLSPECENV -- equivalence of satisfaction
(G F (spec_state_2=S0));
LTLSPEC
G ((ack_hor = SLEEP & PREV(ack_hor) = MOVE) | (PREV(botMot) = RETURN & PREV(ack_bot) = MOVE) -> botMot = RETURN);
LTLSPEC
G (PREV(botMot) = RETURN & PREV(ack_bot) = SLEEP -> spec_allsleep);
*/
-- speed button
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- an interesting guarantee
guarantee
respondsTo(color!=BLACK,(detect=spec_currentColor&horMot=MOVE));
guarantee
GF (horMot=MOVE);
-- Some environment specifications
assumption -- after starting to move, we will sleep eventually
respondsTo(ack_ver=MOVE,(ack_ver=SLEEP));
assumption -- after starting to move, we will sleep eventually
respondsTo(ack_hor=MOVE,(ack_hor=SLEEP));
assumption -- after starting to move, we will sleep eventually
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_645_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys { S0, S1, S2} spec_state_1 ;
sys { S0, S1, S2} spec_state_2 ;
sys boolean spec_speedButtonValidPressed ;
define -- spec_allsleep is true iff all motors sleep
spec_allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- spec_nonemove is true iff no motor moves
spec_nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor) & spec_dropping = next(spec_dropping));
-- running the robot
guarantee
G (spec_dropping -> verMot = SLEEP);
guarantee
G (horMot = MOVE <-> spec_dropping & detect = spec_currentColor);
guarantee
G (color = BLACK & !spec_dropping -> spec_allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color & next(spec_dropping));
guarantee -- initial assignments: initial spec_state_1
spec_state_1=S0;
guarantee -- safety this and next spec_state_1
G ((spec_state_1=S0 & ((!(verMot = MOVE) & !(detect = spec_currentColor)) | ((detect = spec_currentColor))) & next(spec_state_1=S0)) |
(spec_state_1=S0 & ((verMot = MOVE) & !(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S1)) |
(spec_state_1=S0 & ((verMot = MOVE) & (botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S2)) |
(spec_state_1=S1 & next(spec_state_1=S1)) |
(spec_state_1=S2 & ((detect = spec_currentColor)) & next(spec_state_1=S0)) |
(spec_state_1=S2 & (!(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S1)) |
(spec_state_1=S2 & ((botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state_1=S2)));
assumption -- equivalence of satisfaction
GF (spec_state_1=S0|spec_state_1=S2);
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
assumption -- there will always be a cube
GF (color!=BLACK);
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_646_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2} spec_state__seek ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- spec_allsleep is true iff all motors sleep
spec_allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- spec_nonemove is true iff no motor moves
spec_nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(PREV(botMot = RETURN) & ack_bot = SLEEP));
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> spec_allsleep);
assumption
G (!spec_dropping -> spec_nonemove);
assumption
G (ack_hor = MOVE <-> detect = spec_currentColor & (PREV(horMot = MOVE) | PREV(ack_hor = MOVE)));
assumption
G (horMot = MOVE -> PREV(ack_ver = SLEEP));
-- running the robot
guarantee
G (spec_dropping -> verMot = SLEEP);
guarantee
G (!spec_dropping -> botMot = STOP & horMot = SLEEP);
guarantee
G (color = BLACK & !spec_dropping -> spec_allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color & next(spec_dropping));
guarantee
G (ack_ver = SLEEP & PREV(ack_ver = MOVE) & spec_dropping -> botMot = SEEK);
guarantee -- initial assignments: initial spec_state__seek
spec_state__seek=S0;
guarantee -- safety this and next spec_state__seek
G ((spec_state__seek=S0 & ((!(botMot = SEEK) & !(detect = spec_currentColor)) | ((detect = spec_currentColor))) & next(spec_state__seek=S0)) |
(spec_state__seek=S0 & ((botMot = SEEK) & !(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S1)) |
(spec_state__seek=S0 & ((botMot = SEEK) & (botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S2)) |
(spec_state__seek=S1 & next(spec_state__seek=S1)) |
(spec_state__seek=S2 & ((detect = spec_currentColor)) & next(spec_state__seek=S0)) |
(spec_state__seek=S2 & (!(botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S1)) |
(spec_state__seek=S2 & ((botMot = SEEK) & !(detect = spec_currentColor)) & next(spec_state__seek=S2)));
assumption -- equivalence of satisfaction
GF (spec_state__seek=S0|spec_state__seek=S2);
guarantee
G (spec_dropping & detect = spec_currentColor & PREV(botMot != STOP) <-> horMot = MOVE);
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
assumption -- there will always be a cube
GF (color!=BLACK);
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_662_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2} spec_state__return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP );
/* */
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color & next(spec_dropping));
guarantee
G ((nonemove & spec_dropping) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) -> horMot = MOVE);
/*
LTLSPEC
G (nonemove & PREV(ack_hor) = MOVE & spec_dropping -> botMot = RETURN);
LTLSPEC -- initial assignments: initial spec_state__return
spec_state__return=S0;
LTLSPEC -- safety this and next spec_state__return
G ((spec_state__return=S0 & ((!(botMot = RETURN) & !(ack_bot = SLEEP)) | ((ack_bot = SLEEP))) & next(spec_state__return=S0)) |
(spec_state__return=S0 & ((botMot = RETURN) & !(botMot = RETURN) & !(ack_bot = SLEEP)) & next(spec_state__return=S1)) |
(spec_state__return=S0 & ((botMot = RETURN) & (botMot = RETURN) & !(ack_bot = SLEEP)) & next(spec_state__return=S2)) |
(spec_state__return=S1 & TRUE & next(spec_state__return=S1)) |
(spec_state__return=S2 & ((ack_bot = SLEEP)) & next(spec_state__return=S0)) |
(spec_state__return=S2 & (!(botMot = RETURN) & !(ack_bot = SLEEP)) & next(spec_state__return=S1)) |
(spec_state__return=S2 & ((botMot = RETURN) & !(ack_bot = SLEEP)) & next(spec_state__return=S2)));
LTLSPECENV -- equivalence of satisfaction
(G F (spec_state__return=S0 | spec_state__return=S2));
LTLSPEC
G (PREV(botMot) = RETURN & ack_bot = SLEEP -> allsleep & next(spec_dropping) = FALSE);
*/
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
assumption -- there will always be a cube
GF (color!=BLACK);
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_674_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G(spec_prevBotMotReturn<->PREV(botMot = RETURN));
sys boolean spec_prevBotMotReturn ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & nonemove));
/* */
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) | (PREV(botMot = SEEK) & onlybotmoves & detect != spec_currentColor) -> botMot = SEEK);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P19
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true between (spec_prevBotMotReturn & ack_bot = MOVE) and (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE)) | ((spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_prevBotMotReturn & ack_bot = MOVE))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S3)) |
(spec_state_return=S1 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S1)) |
(spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S3)) |
(spec_state_return=S2 & next(spec_state_return=S2)) |
(spec_state_return=S3 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S3 & (!(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S1|spec_state_return=S3);
/*
LTLSPEC
G (spec_dropping & PREV(botMot) = RETURN & nonemove -> allsleep);
*/
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_675_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2, S3} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & nonemove));
/* */
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G ((nonemove & spec_dropping & PREV(ack_hor != MOVE)) -> botMot = SEEK);
-- P19
-- (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P19
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true between (spec_prevBotMotReturn & ack_bot = MOVE) and (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE)) | ((spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_prevBotMotReturn & ack_bot = MOVE))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S3)) |
(spec_state_return=S1 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S1)) |
(spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S3)) |
(spec_state_return=S2 & next(spec_state_return=S2)) |
(spec_state_return=S3 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S3 & (!(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S1|spec_state_return=S3);
/*
LTLSPEC
G (spec_dropping & PREV(botMot) = RETURN & nonemove -> allsleep);
*/
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
//new spec_waiting_ack_bot_mot:boolean;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPEC -- initial state
!spec_waiting_ack_bot_mot; -- not waiting for acknowledgement (only sleeping is allowed)
LTLSPEC -- transitions
G(!spec_waiting_ack_bot_mot & botMot=STOP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (!spec_waiting_ack_bot_mot & botMot!=STOP -> next(spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot=SLEEP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot!=SLEEP -> next(spec_waiting_ack_bot_mot));
LTLSPECENV -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_bot_mot -> ack_bot=SLEEP);
LTLSPECENV -- if we are waiting motor has to eventually acknowledge finishing
G(spec_waiting_ack_bot_mot -> F(ack_bot=SLEEP));
*/
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_678_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2, S3} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP));
/* */
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G (nonemove & spec_dropping & PREV(ack_hor != MOVE)-> botMot = SEEK);
-- P19
-- (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & onlybotmoves & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P19
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true between (spec_prevBotMotReturn & ack_bot = MOVE) and (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE)) | ((spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_prevBotMotReturn & ack_bot = MOVE))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & (spec_prevBotMotReturn & ack_bot = MOVE)) & next(spec_state_return=S3)) |
(spec_state_return=S1 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & (spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S1)) |
(spec_state_return=S1 & (!(spec_prevBotMotReturn & ack_bot = SLEEP) & !(spec_dropping & onlybotmoves -> botMot = RETURN)) & next(spec_state_return=S3)) |
(spec_state_return=S2 & next(spec_state_return=S2)) |
(spec_state_return=S3 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S3 & (!(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S1|spec_state_return=S3);
/*
LTLSPEC
G (spec_dropping & PREV(botMot) = RETURN & nonemove -> allsleep);
*/
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
//new spec_waiting_ack_bot_mot:boolean;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPEC -- initial state
!spec_waiting_ack_bot_mot; -- not waiting for acknowledgement (only sleeping is allowed)
LTLSPEC -- transitions
G(!spec_waiting_ack_bot_mot & botMot=STOP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (!spec_waiting_ack_bot_mot & botMot!=STOP -> next(spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot=SLEEP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot!=SLEEP -> next(spec_waiting_ack_bot_mot));
LTLSPECENV -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_bot_mot -> ack_bot=SLEEP);
LTLSPECENV -- if we are waiting motor has to eventually acknowledge finishing
G(spec_waiting_ack_bot_mot -> F(ack_bot=SLEEP));
*/
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_679_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP));
/* */
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK);
-- P19
-- (spec_dropping & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P20
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true after (spec_prevBotMotReturn & ack_bot = MOVE) until (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) | ((spec_prevBotMotReturn & ack_bot = SLEEP))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & (spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S1 & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S2 & (!(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S2);
guarantee
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep);
/**/
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
//new spec_waiting_ack_bot_mot:boolean;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPEC -- initial state
!spec_waiting_ack_bot_mot; -- not waiting for acknowledgement (only sleeping is allowed)
LTLSPEC -- transitions
G(!spec_waiting_ack_bot_mot & botMot=STOP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (!spec_waiting_ack_bot_mot & botMot!=STOP -> next(spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot=SLEEP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot!=SLEEP -> next(spec_waiting_ack_bot_mot));
LTLSPECENV -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_bot_mot -> ack_bot=SLEEP);
LTLSPECENV -- if we are waiting motor has to eventually acknowledge finishing
G(spec_waiting_ack_bot_mot -> F(ack_bot=SLEEP));
*/
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_681_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP));
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
/*
LTLSPEC
G (spec_prevBotMotSeek & ack_bot = MOVE -> F (spec_prevBotMotSeek & detect = spec_currentColor));
LTLSPEC
G F (horMot = MOVE);
*/
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK);
-- P19
-- (spec_dropping & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P20
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true after (spec_prevBotMotReturn & ack_bot = MOVE) until (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) | ((spec_prevBotMotReturn & ack_bot = SLEEP))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & (spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S1 & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S2 & (!(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S2);
guarantee
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep);
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
//new spec_waiting_ack_bot_mot:boolean;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPEC -- initial state
!spec_waiting_ack_bot_mot; -- not waiting for acknowledgement (only sleeping is allowed)
LTLSPEC -- transitions
G(!spec_waiting_ack_bot_mot & botMot=STOP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (!spec_waiting_ack_bot_mot & botMot!=STOP -> next(spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot=SLEEP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot!=SLEEP -> next(spec_waiting_ack_bot_mot));
LTLSPECENV -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_bot_mot -> ack_bot=SLEEP);
LTLSPECENV -- if we are waiting motor has to eventually acknowledge finishing
G(spec_waiting_ack_bot_mot -> F(ack_bot=SLEEP));
*/
assumption
respondsTo(ack_ver=MOVE,(ack_ver=SLEEP));
assumption
respondsTo(ack_hor=MOVE,(ack_hor=SLEEP));
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_682_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP));
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
/* */
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK);
-- P19
-- (spec_dropping & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P20
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true after (spec_prevBotMotReturn & ack_bot = MOVE) until (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) | ((spec_prevBotMotReturn & ack_bot = SLEEP))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & (spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S1 & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S2 & (!(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S2);
guarantee
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep);
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
//new spec_waiting_ack_bot_mot:boolean;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPEC -- initial state
!spec_waiting_ack_bot_mot; -- not waiting for acknowledgement (only sleeping is allowed)
LTLSPEC -- transitions
G(!spec_waiting_ack_bot_mot & botMot=STOP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (!spec_waiting_ack_bot_mot & botMot!=STOP -> next(spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot=SLEEP -> next(!spec_waiting_ack_bot_mot));
LTLSPEC
G (spec_waiting_ack_bot_mot & ack_bot!=SLEEP -> next(spec_waiting_ack_bot_mot));
LTLSPECENV -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_bot_mot -> ack_bot=SLEEP);
LTLSPECENV -- if we are waiting motor has to eventually acknowledge finishing
G(spec_waiting_ack_bot_mot -> F(ack_bot=SLEEP));
*/
assumption
respondsTo(ack_ver=MOVE,(ack_ver=SLEEP));
assumption
respondsTo(ack_hor=MOVE,(ack_hor=SLEEP));
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption
GF (ack_hor=MOVE);
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_687_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
//ext haltButton: {PRESS, RELEASE};
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
/*ext spec_haltButtonValidPressed : boolean;
ext spec_pausing : {PAUSE, GO};*/
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP));
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
/* */
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK);
-- P19
-- (spec_dropping & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P20
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true after (spec_prevBotMotReturn & ack_bot = MOVE) until (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) | ((spec_prevBotMotReturn & ack_bot = SLEEP))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & (spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S1 & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S2 & (!(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S2);
guarantee
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep);
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
/*
-- pause button
LTLSPEC
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed);
LTLSPEC
G ((spec_haltButtonValidPressed & spec_pausing = GO) | (!spec_haltButtonValidPressed & spec_pausing = PAUSE)
-> next(spec_pausing) = PAUSE);
LTLSPEC
G ((!spec_haltButtonValidPressed & spec_pausing = GO) | (spec_haltButtonValidPressed & spec_pausing = PAUSE)
-> next(spec_pausing) = GO);
LTLSPECENV -- no pause is eternal
G (spec_pausing = PAUSE -> F (spec_pausing = GO));
*/
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption --
G(horMot=MOVE -> next(ack_hor=MOVE));
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPECENV
G (ack_ver = MOVE -> F (ack_ver = SLEEP));
LTLSPECENV
G (ack_hor = MOVE -> F (ack_hor = SLEEP));*/
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
assumption
GF (ack_hor=MOVE);
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTL3_688_ColorSort_fixed.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} color ;
env {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
//ext haltButton: {PRESS, RELEASE};
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys { S0, S1, S2, S3} spec_state_seek ;
sys { S0, S1, S2} spec_state_return ;
sys {RED, GREEN, BLUE, BLACK, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
/*ext spec_haltButtonValidPressed : boolean;
ext spec_pausing : {PAUSE, GO};*/
define -- allsleep is true iff all motors sleep
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define -- nonemove is true iff no motor moves
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define -- nonemove is true iff no motor moves
onlybotmoves := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = MOVE;
guarantee
G (spec_prevBotMotReturn<->PREV(botMot = RETURN));
guarantee
G (spec_prevBotMotSeek<->PREV(botMot = SEEK));
sys boolean spec_prevBotMotReturn ;
sys boolean spec_prevBotMotSeek ;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & !(spec_prevBotMotReturn & ack_bot = SLEEP));
guarantee
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
assumption
G (!spec_dropping -> nonemove);
/* */
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
-- running the robot
guarantee
G (color = BLACK & !spec_dropping -> allsleep);
guarantee
G (color != BLACK & !spec_dropping -> verMot = MOVE & next(spec_currentColor) = color);
guarantee
G (nonemove & spec_dropping & PREV(ack_ver = MOVE)-> botMot = SEEK);
-- P19
-- (spec_dropping & detect != spec_currentColor -> botMot = SEEK) is true between (spec_prevBotMotSeek & ack_bot = MOVE) and (spec_prevBotMotSeek & detect = spec_currentColor)
guarantee -- initial assignments: initial spec_state_seek
spec_state_seek=S0;
guarantee -- safety this and next spec_state_seek
G ((spec_state_seek=S0 & ((!(spec_prevBotMotSeek & ack_bot = MOVE)) | ((spec_prevBotMotSeek & detect = spec_currentColor) & (spec_prevBotMotSeek & ack_bot = MOVE))) & next(spec_state_seek=S0)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S1)) |
(spec_state_seek=S0 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK) & (spec_prevBotMotSeek & ack_bot = MOVE)) & next(spec_state_seek=S3)) |
(spec_state_seek=S1 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S0)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & (spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S1)) |
(spec_state_seek=S1 & (!(spec_prevBotMotSeek & detect = spec_currentColor) & !(spec_dropping & detect != spec_currentColor -> botMot = SEEK)) & next(spec_state_seek=S3)) |
(spec_state_seek=S2 & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & ((spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S2)) |
(spec_state_seek=S3 & (!(spec_prevBotMotSeek & detect = spec_currentColor)) & next(spec_state_seek=S3)));
guarantee -- equivalence of satisfaction
GF (spec_state_seek=S0|spec_state_seek=S1|spec_state_seek=S3);
guarantee
G (spec_dropping & onlybotmoves & detect = spec_currentColor & PREV(botMot = SEEK) <-> horMot = MOVE);
guarantee
G (nonemove & PREV(ack_hor = MOVE) & spec_dropping -> botMot = RETURN);
-- P20
-- (spec_dropping & onlybotmoves -> botMot = RETURN) is true after (spec_prevBotMotReturn & ack_bot = MOVE) until (spec_prevBotMotReturn & ack_bot = SLEEP)
guarantee -- initial assignments: initial spec_state_return
spec_state_return=S0;
guarantee -- safety this and next spec_state_return
G ((spec_state_return=S0 & ((!(spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) | ((spec_prevBotMotReturn & ack_bot = SLEEP))) & next(spec_state_return=S0)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & !(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S0 & ((spec_prevBotMotReturn & ack_bot = MOVE) & (spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)) |
(spec_state_return=S1 & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S0)) |
(spec_state_return=S2 & (!(spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S1)) |
(spec_state_return=S2 & ((spec_dropping & onlybotmoves -> botMot = RETURN) & !(spec_prevBotMotReturn & ack_bot = SLEEP)) & next(spec_state_return=S2)));
guarantee -- equivalence of satisfaction
GF (spec_state_return=S0|spec_state_return=S2);
guarantee
G (spec_prevBotMotReturn & ack_bot = SLEEP -> allsleep);
-- speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL3);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL1);
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL1) -> motSpeed = LEVEL1);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL2) -> motSpeed = LEVEL2);
guarantee -- if the speed button is pressed, increase the speed by one level
G (!spec_speedButtonValidPressed & PREV(motSpeed = LEVEL3) -> motSpeed = LEVEL3);
/*
-- pause button
LTLSPEC
G (haltButton = PRESS & PREV(haltButton = RELEASE) <-> spec_haltButtonValidPressed);
LTLSPEC
G ((spec_haltButtonValidPressed & spec_pausing = GO) | (!spec_haltButtonValidPressed & spec_pausing = PAUSE)
-> next(spec_pausing) = PAUSE);
LTLSPEC
G ((!spec_haltButtonValidPressed & spec_pausing = GO) | (spec_haltButtonValidPressed & spec_pausing = PAUSE)
-> next(spec_pausing) = GO);
LTLSPECENV -- no pause is eternal
G (spec_pausing = PAUSE -> F (spec_pausing = GO));
*/
-- Some environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- on move command acknowledge moving
G(verMot=MOVE -> next(ack_ver=MOVE));
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- on move command acknowledge moving
G(horMot=MOVE -> next(ack_hor=MOVE));
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
/*
LTLSPECENV
G (ack_ver = MOVE -> F (ack_ver = SLEEP));
LTLSPECENV
G (ack_hor = MOVE -> F (ack_hor = SLEEP));*/
assumption
respondsTo(ack_bot=MOVE,(ack_bot=SLEEP));
/*
LTLSPECENV
G (botMot = MOVE & spec_)
*/
/*
LTLSPECENV
G F (ack_hor = MOVE);
*/
assumption -- there will always be a cube
GF (color!=BLACK);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTLTAG_788_ColorSort.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} color ;
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {YES, NO} starting_pos ;
env {ZERO, NOTZERO} num_of_cubes;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {REDUCE, NOTREDUCE} reduce_num_of_cubes;
sys {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define
verhor_dontmove := ack_ver = SLEEP & ack_hor = SLEEP;
define
onlybotmoves := verhor_dontmove & ack_bot = MOVE;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- if a motor is in the middle of moving, all the other motors stop
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
-- currentColor keeps its value unless a new cube is kicked
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (verMot = MOVE -> color = next(spec_currentColor));
guarantee -- the dropping stage starts when we kick the cube in and ends when we drop it into its heap
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & horMot = SLEEP);
-- this is how the colorsort works when given a cube
guarantee -- we do not drop at the start, and the spped level starts at 1
!spec_dropping & motSpeed = LEVEL1;
guarantee -- if there are no more cubes, await a new input
G (num_of_cubes = ZERO -> allsleep);
guarantee -- when you are back in the original position, reduce the current number of cubes to drop by 1
G (!spec_dropping & starting_pos = YES & PREV(botMot = RETURN) <-> reduce_num_of_cubes = REDUCE);
guarantee -- if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
G (num_of_cubes = NOTZERO & !spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN);
-- if we are not in the dropping stage and are at the initial position, drop a cube iff you see one
guarantee
G (!spec_dropping & starting_pos = YES & color = BLACK -> allsleep);
guarantee
G (color = BLACK | spec_dropping -> verMot = SLEEP);
guarantee
G (num_of_cubes = NOTZERO & !spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE);
guarantee -- seek the heap for the current cube until it is found
G (num_of_cubes = NOTZERO & spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK);
guarantee -- when the heap is found, drop the cube into it through the tray
G (num_of_cubes = NOTZERO & spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE);
-- the speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL1 -> next(motSpeed = LEVEL2));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL2 -> next(motSpeed = LEVEL3));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL3 -> next(motSpeed = LEVEL1));
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed -> motSpeed = next(motSpeed));
-- environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
assumption
GF (ack_hor=MOVE);
-- some interesting guarantees
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/ColorSortLTLTAG_792_ColorSort.spectra deleted 100644 → 0
View file @ 68220e2a
module ColorSort
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} color ;
env {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} detect ;
env {MOVE, SLEEP} ack_ver ;
env {MOVE, SLEEP} ack_hor ;
env {MOVE, SLEEP} ack_bot ;
env {YES, NO} starting_pos ;
env {ZERO, NOTZERO} num_of_cubes;
env {PRESS, RELEASE} speedButton;
sys {MOVE, SLEEP} verMot ;
sys {MOVE, SLEEP} horMot ;
sys {SEEK, STOP, RETURN} botMot ;
sys {LEVEL1, LEVEL2, LEVEL3} motSpeed;
sys {REDUCE, NOTREDUCE} reduce_num_of_cubes;
sys {GREEN, BLACK, RED, BLUE, YELLOW , WHITE} spec_currentColor;
sys boolean spec_dropping ;
sys boolean spec_speedButtonValidPressed ;
define
allsleep := verMot = SLEEP & horMot = SLEEP & botMot = STOP;
define
nonemove := ack_ver = SLEEP & ack_hor = SLEEP & ack_bot = SLEEP;
define
verhor_dontmove := ack_ver = SLEEP & ack_hor = SLEEP;
define
onlybotmoves := verhor_dontmove & ack_bot = MOVE;
guarantee -- only one motors moves at a time
G (verMot = MOVE -> (botMot = STOP & horMot = SLEEP));
guarantee
G (horMot = MOVE -> (botMot = STOP & verMot = SLEEP));
guarantee
G (botMot != STOP -> (verMot = SLEEP & horMot = SLEEP));
guarantee -- if a motor is in the middle of moving, all the other motors stop
G (ack_ver = MOVE | ack_hor = MOVE -> allsleep);
-- currentColor keeps its value unless a new cube is kicked
guarantee
G (verMot = SLEEP -> spec_currentColor = next(spec_currentColor));
guarantee
G (verMot = MOVE -> color = next(spec_currentColor));
guarantee -- the dropping stage starts when we kick the cube in and ends when we drop it into its heap
G (spec_dropping = next(spec_dropping) <-> verMot = SLEEP & horMot = SLEEP);
-- this is how the colorsort works when given a cube
guarantee -- we do not drop at the start, and the spped level starts at 1
!spec_dropping & motSpeed = LEVEL1;
guarantee -- if there are no more cubes, await a new input
G (num_of_cubes = ZERO -> allsleep);
guarantee -- when you are back in the original position, reduce the current number of cubes to drop by 1
G (!spec_dropping & starting_pos = YES & PREV(botMot = RETURN) <-> reduce_num_of_cubes = REDUCE);
guarantee -- if we are not in the dropping stage and the vertical and horizontal motors are still, return to the initial position
G (num_of_cubes = NOTZERO & !spec_dropping & starting_pos = NO & verhor_dontmove <-> botMot = RETURN);
-- if we are not in the dropping stage and are at the initial position, drop a cube iff you see one
guarantee
G (!spec_dropping & starting_pos = YES & color = BLACK -> allsleep);
guarantee
G (color = BLACK | spec_dropping -> verMot = SLEEP);
guarantee
G (num_of_cubes = NOTZERO & !spec_dropping & starting_pos = YES & nonemove & color != BLACK <-> verMot = MOVE);
guarantee -- seek the heap for the current cube until it is found
G (num_of_cubes = NOTZERO & spec_dropping & detect != spec_currentColor & verhor_dontmove <-> botMot = SEEK);
guarantee -- when the heap is found, drop the cube into it through the tray
G (num_of_cubes = NOTZERO & spec_dropping & detect = spec_currentColor & verhor_dontmove <-> horMot = MOVE);
-- the speed button
guarantee
motSpeed = LEVEL1 & !spec_dropping;
guarantee
G (speedButton = PRESS & PREV(speedButton = RELEASE) <-> spec_speedButtonValidPressed);
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL1 -> next(motSpeed = LEVEL2));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL2 -> next(motSpeed = LEVEL3));
guarantee -- if the speed button is pressed, increase the speed by one level
G (spec_speedButtonValidPressed & motSpeed = LEVEL3 -> next(motSpeed = LEVEL1));
guarantee -- if the speed button is released, the speed remains the same
G (!spec_speedButtonValidPressed -> motSpeed = next(motSpeed));
-- environment specifications
sys boolean spec_waiting_ack_ver_mot;
sys boolean spec_waiting_ack_hor_mot;
guarantee -- initial state
!spec_waiting_ack_ver_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_ver_mot & verMot!=MOVE -> next(!spec_waiting_ack_ver_mot));
guarantee
G (!spec_waiting_ack_ver_mot & verMot=MOVE -> next(spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver=SLEEP -> next(!spec_waiting_ack_ver_mot));
guarantee
G (spec_waiting_ack_ver_mot & ack_ver!=SLEEP -> next(spec_waiting_ack_ver_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_ver_mot -> ack_ver=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_ver_mot,(ack_ver=SLEEP));
guarantee -- initial state
!spec_waiting_ack_hor_mot; -- not waiting for acknowledgement (only sleeping is allowed)
guarantee -- transitions
G(!spec_waiting_ack_hor_mot & horMot!=MOVE -> next(!spec_waiting_ack_hor_mot));
guarantee
G (!spec_waiting_ack_hor_mot & horMot=MOVE -> next(spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor=SLEEP -> next(!spec_waiting_ack_hor_mot));
guarantee
G (spec_waiting_ack_hor_mot & ack_hor!=SLEEP -> next(spec_waiting_ack_hor_mot));
assumption -- while we are not waiting motor can only acknowledge sleeping
G(!spec_waiting_ack_hor_mot -> ack_hor=SLEEP);
assumption -- if we are waiting motor has to eventually acknowledge finishing
respondsTo(spec_waiting_ack_hor_mot,(ack_hor=SLEEP));
assumption -- there will always be a cube
GF (color!=BLACK);
assumption
GF (ack_hor=MOVE);
assumption -- there will always be an input from the user that is not zero
GF (num_of_cubes!=ZERO);
assumption -- the number of cubes will always eventually become zero
respondsTo(num_of_cubes!=ZERO,(num_of_cubes=ZERO));
-- some interesting guarantees
guarantee
respondsTo(color!=BLACK,(horMot=MOVE&detect=spec_currentColor));
guarantee
GF (horMot=MOVE);
pattern respondsTo(trigger, response) {
var boolean responded;
responded;
G (next(responded) iff (response or responded and !trigger));
GF (responded);
}
maven-root/mtsa/src/main/SPECTRATranslator/SYNTECH15/DP.spectra
View file @ 54ad3bf0
import "DwyerPatterns.spectra"
spec DiningPhilosophers
spec DP
type State = {FREE, LEFT, RIGHT};
define N := 2;
define N := 5;
env boolean[N] hungry;
sys State[N] forks;
predicate hasTwoForks(Int(0..(N-1)) i):
......@@ -12,7 +13,7 @@ asm initialNoHungry: ini forall i in Int(0..(N-1)) . !hungry[i];
asm keepBeingHungry: always forall i in Int(0..(N-1)) . (hungry[i] & !hasTwoForks(i)) -> next(hungry[i]);
asm stopsEating{Int(0..(N-1)) i}: S_responds_to_P_globally(!hungry[i], hasTwoForks(i));
//asm stopsEating{Int(0..(N-1)) i}: S_responds_to_P_globally(!hungry[i], hasTwoForks(i));
gar initialForksFree: ini forall i in Int(0..(N-1)) . forks[i] = FREE;
......@@ -24,10 +25,4 @@ gar mustPutDownFork: always forall i in Int(0..(N-1)) . (forks[i] = LEFT -> next
gar dontGiveForkIfNoHungry: always forall i in Int(0..(N-1)) . (!hungry[i] -> (next(forks[i] != RIGHT) & next(forks[(i+1)%N] != LEFT)));
gar eventuallyEats{Int(0..(N-1)) i}: S_responds_to_P_globally(hasTwoForks(i), hungry[i]);
// Vacuous Guarantees
//gar adjacentNeverEatTogether: always forall i in Int(0..(N-1)) . hasTwoForks(i) -> (!hasTwoForks(i+1) & !(hasTwoForks(i-1)));
//gar eventuallyNotEating{Int(0..(N-1)) i}: alwEv !hasTwoForks(i);
// gar eventuallyEats{Int(0..(N-1)) i}: S_responds_to_P_globally(hasTwoForks(i), hungry[i]);
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment