diff --git a/.gitmodules b/.gitmodules index 0d54a84c27..2f1dadf575 100644 --- a/.gitmodules +++ b/.gitmodules @@ -980,6 +980,9 @@ [submodule "vendor/grammars/sublime-pony"] path = vendor/grammars/sublime-pony url = https://github.com/CausalityLtd/sublime-pony +[submodule "vendor/grammars/sublime-promela-spin"] + path = vendor/grammars/sublime-promela-spin + url = https://github.com/corbanmailloux/sublime-promela-spin.git [submodule "vendor/grammars/sublime-q"] path = vendor/grammars/sublime-q url = https://github.com/komsit37/sublime-q diff --git a/grammars.yml b/grammars.yml index efffb487cd..da6a4f2ecc 100644 --- a/grammars.yml +++ b/grammars.yml @@ -864,6 +864,8 @@ vendor/grammars/sublime-opal: - source.opalsysdefs vendor/grammars/sublime-pony: - source.pony +vendor/grammars/sublime-promela-spin: +- source.promela vendor/grammars/sublime-q: - source.q - source.q_output diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index 74368ef5a5..39f686e6cf 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -4633,6 +4633,14 @@ Prolog: tm_scope: source.prolog ace_mode: prolog language_id: 295 +Promela: + type: programming + color: "#de0000" + tm_scope: source.promela + ace_mode: text + extensions: + - ".pml" + language_id: 441858312 Propeller Spin: type: programming color: "#7fa2a7" diff --git a/samples/Promela/Session.pml b/samples/Promela/Session.pml new file mode 100644 index 0000000000..5d4029e5be --- /dev/null +++ b/samples/Promela/Session.pml @@ -0,0 +1,44 @@ +#include "Supervisor.pml" +/* Supervisor.pml includes Thread.pml (which includes Invariants.prp) */ + +init +{ + byte i = 0; + assert_all(i, 0, 0); + sv_ctor(i); + i = 0; + assert_all(i, READY, CONTINUE); + printf("Init starts Supervisor...\n"); + sv_start_sync(); + do + :: if + :: get_state(0) == RUNNING -> + printf("Init pauses Supervisor...\n"); + if + :: true -> pause(0, true) + :: true -> pause(0, false) + fi + :: get_state(0) == PAUSED -> + printf("Init resumes Supervisor...\n"); + if + :: true -> resume(0, true) + :: true -> resume(0, false) + fi + :: true -> skip + fi + :: break + od + if + :: printf("Init stops Supervisor...\n"); + if + :: true -> stop(0, true) + :: true -> stop(0, false) + fi + :: true -> skip + fi + wait_for_HALT_mask(0); + i = 0; + sv_dtor(i); + i = 0; + assert_all(i, 0, 0) +} diff --git a/samples/Promela/Supervisor.pml b/samples/Promela/Supervisor.pml new file mode 100644 index 0000000000..24cb127e0a --- /dev/null +++ b/samples/Promela/Supervisor.pml @@ -0,0 +1,347 @@ +#include "./Thread.pml" + +/** + * Supervisor propagates commands in serial mode if and only if this variable is + * set to true. As of ADAPRO 5.0.0, Supervisor keeps querying a configuration + * parameter corresponding with this condition during runtime. + */ +bool serialize_commands; + +/** + * Should be true if and only if all Workers have entered the state STOPPED. + * This is a private field of Supervisor, but modeled as a global variable to + * enable more precise simulation of constructors. + */ +bool all_workers_stopped; + +/** + * Should be true if and only if one or more Workers have entered the state + * ABORTED. This is a private field of Supervisor, but modeled as a global + * variable to enable more precise simulation of constructors. + */ +bool exists_aborted_worker; + +/** + * Supervisor sets this true when calling its transition callback on CONTINUE + * for the first time. This is used for the mechanism that prevents Supervisor + * for propagating the CONTINUE command when starting. Doing so would prevent + * Workers from starting in the state PAUSED. This is a private field of + * Supervisor, but modeled as a global variable to enable more precise + * simulation of constructors. + */ +bool supervisor_started; + +/** + * Asserts that all the threads from k to N are in the given state with the + * given command. Mutates the value of k, leaving it 0 at the end. + */ +inline assert_all(k, state, command) +{ + d_step + { + do + :: k < N -> + assert(get_state(k) == state); + assert(get_command(k) == command); + k++ + :: else -> + break + od + k = 0 + } +} + +/** Sends the given command to Worker number j. Waits iff wait == true. */ +inline send_command(j, command, wait) +{ + if + :: command == START -> + start(j, wait) + :: command == PAUSE -> + pause(j, wait) + :: command == CONTINUE -> + resume(j, wait) + :: command == STOP || command == ABORT -> + stop(j, wait) + fi +} + +/** + * Propagates the given command in covariant order, i.e. by iterating through + * Workers in increasing order. Blocks if and only if wait is true. + */ +inline covariant_propagation(command, wait) +{ + do + :: j < N -> + send_command(j, command, wait); + j++ + :: else -> + j = 1; + break + od +} + +/** + * Propagates the given command in contravariant order, i.e. by iterating + * through Workers in decreasing order. + */ +inline contravariant_propagation(command) +{ + j = N - 1; + do + :: j > 0 -> + send_command(j, command, true); + j-- + :: else -> + j = 1; + break + od +} + +/** + * Propagates the given command to all Workers, using the command propagate mode + * determined by the value of the global variable serialize_commands. + */ +inline propagate_command(command) +{ + if + :: command == CONTINUE && !supervisor_started -> + printf("Supervisor doesn't propagate the first CONTINUE command.\n"); + supervisor_started = true + :: else -> + if + :: serialize_commands -> propagate_command_in_lifo(command) + :: else -> propagate_command_in_parallel(command) + fi + fi +} + +/** + * Sends the given command to all Workers using serial command propagation + * mode. This means sending every command in the blocking way. + */ +inline propagate_command_in_lifo(command) +{ + if + :: command == START || command == PAUSED -> + covariant_propagation(command, true) + :: else -> + contravariant_propagation(command) + fi +} + +/** + * Sends the given command to all Workers using parallel command propagation + * mode. This means sending commands asynchronously first to every Worker, and + * then waiting for them move to an appropriate state. + */ +inline propagate_command_in_parallel(command) +{ + printf("Supervisor propagating command %e...\n", command); + covariant_propagation(command, false); + do + :: j < N -> + if + :: command == START -> wait_for_START_mask(j) + :: command == CONTINUE -> wait_for_RESUME_mask(j) + :: command == PAUSE -> wait_for_PAUSE_mask(j) + :: command == STOP -> wait_for_HALT_mask(j) + fi + j++ + :: else -> + j = 1; + break + od +} + +/** + * Checks whether of not there all Workers have moved to the state STOPPED or if + * there exists a worker in state ABORTED and sets the appropriate booleans. + */ +inline check_worker_states() +{ + all_workers_stopped = true; + do + :: j < N -> + all_workers_stopped = + all_workers_stopped && get_state(j) == STOPPED; + exists_aborted_worker = + exists_aborted_worker || get_state(j) == ABORTED; + j++ + :: else -> + j = 1; + break + od +} + +inline sv_start_sync() +{ + set_command(0, START); + run Supervisor(); + wait_for_START_mask(0); +} + +/** + * Models the method ADAPRO::Control::Supervisor::prepare. + */ +inline sv_prepare() +{ + propagate_command(START); +} + +/** + * Models the method ADAPRO::Control::Supervisor::execute. + */ +inline sv_execute() +{ + executing[0] = true; + check_worker_states(); + if + :: all_workers_stopped -> + printf("Supervisor will stop because all Workers have stopped...\n"); + stop(0, false) + :: exists_aborted_worker -> + printf("Supervisor will stop because some Workers have aborted...\n"); + stop(0, false) + :: else -> + skip + fi + executing[0] = false +} + +/** Models the transition callback of ADAPRO::Control::Supervisor. */ +inline sv_trans_cb(s) +{ + if + :: s == RUNNING -> + propagate_command(CONTINUE) + :: s == PAUSED -> + propagate_command(PAUSE) + :: s == ABORTING || s == STOPPING -> + propagate_command(STOP) + :: else -> + skip + fi +} + +inline sv_covariant_transition(state, command, next) +{ + print_state_transition(0, state, command, next); + set_state(0, next); + sv_trans_cb(next) +} + +inline sv_contravariant_transition(state, command, next) +{ + sv_trans_cb(next); + print_state_transition(0, state, command, next); + set_state(0, next) +} + +/** + * Models the constructor of Supervisor, which first sets its own state and + * command and then calls the Worker constructors. + */ +inline sv_ctor(i) +{ + d_step + { + if + :: true -> serialize_commands = true + :: true -> serialize_commands = false + fi + all_workers_stopped = false; + exists_aborted_worker = false; + supervisor_started = false; + do + :: i < N -> + ctor(i); + i++ + :: else -> + break + od + } +} + +/** + * Models the destructor of Supervisor. + */ +inline sv_dtor(i) +{ + d_step + { + do + :: i < N -> + dtor(i); + i++ + :: else -> + break + od + } +} + +/** Models the ADAPRO Supervisor Thread. */ +proctype Supervisor() +{ + /** + * The variable j is a local index variable that Supervisor uses for + * iterating over Workers. Supervisor itself is the Thread number 0, so + * this variable needs to always stay in the open interval ]0,N[. + */ + byte j = 1; + + /* Startup: */ + get_command(0) == START; + sv_covariant_transition(READY, START, STARTING); + set_command(0, CONTINUE); + sv_prepare(); + + /* Execution: */ + do + :: get_command(0) == CONTINUE -> + assert(get_state(0) == STARTING || get_state(0) == RUNNING || + get_state(0) == PAUSED); + if + :: get_state(0) == STARTING -> + sv_covariant_transition(STARTING, CONTINUE, RUNNING) + :: get_state(0) == PAUSED -> + sv_covariant_transition(PAUSED, CONTINUE, RUNNING) + :: else -> + skip + fi + sv_execute() + :: get_command(0) == PAUSE -> + if + :: get_state(0) == PAUSED -> + get_command(0) != PAUSED + :: else -> + assert(get_state(0) == STARTING || get_state(0) == RUNNING || + get_state(0) == STARTING); + if + :: get_state(0) == STARTING || get_state(0) == RUNNING -> + sv_contravariant_transition(RUNNING, PAUSE, PAUSED) + :: else -> + skip + fi + fi + :: get_command(0) == STOP || get_command(0) == ABORT -> + break + od + + /* Shutdown: */ + if + :: get_command(0) == STOP -> + assert(get_state(0) == STARTING || get_state(0) == RUNNING || + get_state(0) == PAUSED); + sv_covariant_transition(get_state(0), STOP, STOPPING); + sv_contravariant_transition(STOPPING, STOP, STOPPED) + :: get_command(0) == ABORT -> + assert(get_state(0) == STARTING || get_state(0) == RUNNING || + get_state(0) == STOPPING); + sv_covariant_transition(get_state(0), ABORT, ABORTING); + sv_contravariant_transition(ABORTING, ABORT, ABORTED) + :: else -> + assert(false) + fi +} diff --git a/samples/Promela/TCP.pml b/samples/Promela/TCP.pml new file mode 100644 index 0000000000..d763f5927a --- /dev/null +++ b/samples/Promela/TCP.pml @@ -0,0 +1,103 @@ +mtype = { SYN, FIN, ACK, SYN_ACK } + +chan AtoN = [1] of { mtype }; +chan NtoA = [1] of { mtype }; +chan BtoN = [1] of { mtype }; +chan NtoB = [1] of { mtype }; + +int state[2]; +int pids[2]; + +#define ClosedState 0 +#define ListenState 1 +#define SynSentState 2 +#define SynRecState 3 +#define EstState 4 +#define FinW1State 5 +#define CloseWaitState 6 +#define FinW2State 7 +#define ClosingState 8 +#define LastAckState 9 +#define TimeWaitState 10 +#define EndState -1 + +#define leftConnecting (state[0] == ListenState && state[1] == SynSentState) +#define leftEstablished (state[0] == EstState) +#define rightEstablished (state[1] == EstState) +#define leftClosed (state[0] == ClosedState) + +proctype TCP(chan snd, rcv; int i) { + pids[i] = _pid; +CLOSED: + state[i] = ListenState; + if + /* Passive open */ + :: goto LISTEN; + /* Active open */ + :: snd ! SYN; goto SYN_SENT; + /* Terminate */ + :: goto end; + fi +LISTEN: + state[i] = ListenState; + if + :: rcv ? SYN -> snd ! SYN_ACK; goto SYN_RECEIVED; + /* Simultaneous LISTEN */ + :: timeout -> goto CLOSED; + /* recently added the 'timout.' - Max */ + fi +SYN_SENT: + state[i] = SynSentState; + if + /* Simultaneous open */ + :: rcv ? SYN -> snd ! ACK; goto SYN_RECEIVED; + /* Standard behavior */ + :: rcv ? SYN_ACK -> snd ! ACK; goto ESTABLISHED; + /* Timeout */ + :: timeout -> goto CLOSED; + fi +SYN_RECEIVED: + state[i] = SynRecState; + rcv ? ACK; goto ESTABLISHED; + /* We may want to consider putting a timeout -> CLOSED here. */ +ESTABLISHED: + state[i] = EstState; + if + /* Close - initiator sequence */ + :: snd ! FIN; goto FIN_WAIT_1; + /* Close - responder sequence */ + :: rcv ? FIN -> snd ! ACK; goto CLOSE_WAIT; + fi +FIN_WAIT_1: + state[i] = FinW1State; + if + /* Simultaneous close */ + :: rcv ? FIN -> snd ! ACK; goto CLOSING; + /* Standard close */ + :: rcv ? ACK -> goto FIN_WAIT_2; + fi +CLOSE_WAIT: + state[i] = CloseWaitState; + snd ! FIN; goto LAST_ACK; +FIN_WAIT_2: + state[i] = FinW2State; + rcv ? FIN -> snd ! ACK; goto TIME_WAIT; +CLOSING: + state[i] = ClosingState; + rcv ? ACK -> goto TIME_WAIT; +LAST_ACK: + state[i] = LastAckState; + rcv ? ACK -> goto CLOSED; +TIME_WAIT: + state[i] = TimeWaitState; + goto CLOSED; +end: + state[i] = EndState; +} + +init { + state[0] = ClosedState; + state[1] = ClosedState; + run TCP(AtoN, NtoA, 0); + run TCP(BtoN, NtoB, 1); +} \ No newline at end of file diff --git a/samples/Promela/Thread.pml b/samples/Promela/Thread.pml new file mode 100644 index 0000000000..453936a9a3 --- /dev/null +++ b/samples/Promela/Thread.pml @@ -0,0 +1,401 @@ +#include "./Theory.prp" +/* TODO: Rename Thread to Worker, as Supervisor has its own Promela file. */ + +/** The number of Threads, including Supervisor as Thread no. 0, to simulate. */ +#define N 3 + +/** + * The numerical values of the states are: + * ABORTED = 1, + * ABORTING = 2, + * STOPPED = 3, + * STOPPING = 4, + * PAUSED = 5, + * RUNNING = 6, + * STARTING = 7, + * READY = 8 + */ +mtype = {READY, STARTING, RUNNING, PAUSED, STOPPING, STOPPED, ABORTING, ABORTED}; + +/** + * The numerical values of the commands are: + * ABORT = 9, + * STOP = 10, + * PAUSE = 11, + * CONTINUE = 12, + * START = 13 + */ +mtype = {START, CONTINUE, PAUSE, STOP, ABORT}; + +/** + * It seems that mtype declarations have "big endian" ordering, which I find + * counterintuitive. Hence, this definition: + */ +#define LT(x, y) x > y + +/** + * Prettyprints the state transition for Thread number i. For automatic state + * transitions, the command should be set to 0, in which case an underscore + * ('_') will be printed instead of a command name. + */ +inline print_state_transition(i, state, command, next) +{ + if + :: i == 0 && command == 0 -> + printf("Supervisor: (%e, _) -> %e\n", state, next) + :: i == 0 && command > 0 -> + printf("Supervisor: (%e, %e) -> %e\n", state, command, next) + :: i > 0 && command == 0 -> + printf("Worker %d: (%e, _) -> %e\n", i, state, next) + :: i > 0 && command > 0 -> + printf("Worker %d: (%e, %e) -> %e\n", i, state, command, next) + fi +} + +/********************************** PRIVATE ***********************************/ + +/** States of the Threads. Index 0 is reserved for the Supervisor. */ +mtype states[N]; + +/** Commands of the Threads. Index 0 is reserved for the Supervisor. */ +mtype commands[N]; + +/** The array of Threads currently executing. */ +bool executing[N]; + +/** See the documentation for ADAPRO::Control::Thread::set_state. */ +#define set_state(i, state) states[i] = state + +/** See the documentation for ADAPRO::Control::Thread::set_command. */ +#define set_command(i, command) \ + atomic \ + { \ + if \ + :: command == START && commands[i] == CONTINUE -> \ + assert(get_state(i) == READY); \ + commands[i] = START \ + :: command == PAUSE && commands[i] == CONTINUE -> \ + assert(get_state(i) == STARTING || get_state(i) == RUNNING); \ + commands[i] = PAUSE \ + :: command == CONTINUE && \ + (commands[i] == START || commands[i] == PAUSE) -> \ + assert(get_state(i) == STARTING || get_state(i) == PAUSED); \ + commands[i] = CONTINUE \ + :: command == STOP && \ + (commands[i] == CONTINUE || commands[i] == PAUSE) -> \ + assert(get_state(i) == STARTING || get_state(i) == RUNNING || \ + get_state(i) == PAUSED); \ + commands[i] = STOP \ + :: command == ABORT -> \ + assert(get_state(i) != READY); \ + commands[i] = ABORT \ + :: else -> printf("Thread %d ignores command %e.\n", i, commands[i]) \ + fi \ + } + +/********************************** PUBLIC ************************************/ + +/** See the documentation for ADAPRO::Control::Thread::get_state. */ +#define get_state(i) states[i] + +/** See the documentation for ADAPRO::Control::Thread::get_command. */ +#define get_command(i) commands[i] + +/********************************* PROTECTED **********************************/ + +/** + * Models the method ADAPRO::Control::Thread::prepare by non-deterministically + * choosing between aborting, pausing, and doing nothing. + */ +inline prepare(i) +{ + if + :: true -> abort(i) + :: true -> set_command(i, PAUSE) + :: true -> set_command(i, STOP) + :: true -> skip + fi +} + +/** + * Models the method ADAPRO::Control::Thread::execute by non-deterministically + * choosing between aborting, pausing, stopping, and doing nothing. + */ +inline execute(i) +{ + executing[i] = true; + if + :: true -> abort(i) + /* :: true -> set_command(i, PAUSE) */ + :: true -> set_command(i, STOP) + :: true -> skip + fi + executing[i] = false +} + +/** + * Models the method ADAPRO::Control::Thread::finish by non-deterministically + * choosing between aborting and doing nothing. + */ +inline finish(i) +{ + if + :: true -> abort(i) + :: true -> skip + fi +} + +/** Aborts the Thread number i. Always non-blocking. */ +inline abort(i) +{ + assert(_pid != 1); /* Supervisor is not allowed to abort Workers. */ + set_command(i, ABORT); +} + +/********************************** PRIVATE ***********************************/ + +/** + * Simulates the Thread class constructor by initializing the state and + * commmand of thread number i Thread with their legal default values. + */ +inline ctor(i) +{ + d_step + { + states[i] = READY; + commands[i] = CONTINUE + } +} + +inline dtor(i) +{ + d_step + { + states[i] = 0; + commands[i] = 0; + executing[i]= false + } +} + +/** Models the default transition callback of a Thread that does nothing. */ +inline trans_cb(s) +{ + skip +} + +inline covariant_transition(state, command, next) +{ + print_state_transition(k, state, command, next); + set_state(k, next); + /*trans_cb(next)*/ +} + +inline contravariant_transition(state, command, next) +{ + /*trans_cb(next);*/ + print_state_transition(k, state, command, next); + set_state(k, next) +} + +/** Models the ADAPRO::Control::Thread::run method. */ +proctype Thread(byte k) +{ + /* Startup: */ + get_command(k) == START; + covariant_transition(READY, START, STARTING); + set_command(k, CONTINUE); + prepare(k); + + /* Execution: */ + do + :: get_command(k) == CONTINUE -> + assert(get_state(k) == STARTING || get_state(k) == RUNNING || + get_state(k) == PAUSED); + if + :: get_state(k) == STARTING -> + covariant_transition(STARTING, CONTINUE, RUNNING) + :: get_state(k) == PAUSED -> + covariant_transition(PAUSED, CONTINUE, RUNNING) + :: else -> + skip + fi + execute(k) + :: get_command(k) == PAUSE -> + if + :: get_state(k) == PAUSED -> + get_command(k) != PAUSED + :: else -> + assert(get_state(k) == STARTING || get_state(k) == RUNNING || + get_state(k) == STARTING); + if + :: get_state(k) == STARTING || get_state(k) == RUNNING -> + contravariant_transition(RUNNING, PAUSE, PAUSED) + :: else -> + skip + fi + fi + :: get_command(k) == STOP || get_command(k) == ABORT -> + break + od + + /* Shutdown: */ + if + :: get_command(k) == STOP -> + assert(get_state(k) == STARTING || get_state(k) == RUNNING || + get_state(k) == PAUSED); + covariant_transition(get_state(k), STOP, STOPPING); + finish(k); + contravariant_transition(STOPPING, STOP, STOPPED) + :: get_command(k) == ABORT -> + assert(get_state(k) == STARTING || get_state(k) == RUNNING || + get_state(k) == STOPPING); + covariant_transition(get_state(k), ABORT, ABORTING); + contravariant_transition(ABORTING, ABORT, ABORTED) + :: else -> + assert(false) + fi +} + +/********************************** PUBLIC ************************************/ + +/** Models Control::Thread::wait_for_state_mask(Data::State::START_MASK). */ +inline wait_for_START_mask(i) +{ + if + :: _pid == 0 -> + printf("Init is waiting for START mask on Thread %d...\n", i) + :: _pid == 1 -> + printf("Supervisor is waiting for START mask on Thread %d...\n", i) + :: _pid > 1 -> + printf("Worker %d is waiting for START mask on Thread %d...\n", _pid - 1, i) + fi + get_state(i) == RUNNING || + get_state(i) == PAUSED || + get_state(i) == STOPPING || + get_state(i) == STOPPED || + get_state(i) == ABORTING || + get_state(i) == ABORTED; + printf("Waiting ended.\n") +} + +/** Models Control::Thread::wait_for_state_mask(Data::State::PAUSE_MASK). */ +inline wait_for_PAUSE_mask(i) +{ + if + :: _pid == 0 -> + printf("Init is waiting for PAUSED mask on Thread %d...\n", i) + :: _pid == 1 -> + printf("Supervisor is waiting for PAUSED mask on Thread %d...\n", i) + :: _pid > 1 -> + printf("Worker %d is waiting for PAUSED mask on Thread %d...\n", _pid - 1, i) + fi + get_state(i) == PAUSED || + get_state(i) == STOPPING || + get_state(i) == STOPPED || + get_state(i) == ABORTING || + get_state(i) == ABORTED; + printf("Waiting ended.\n") +} + +/** Models Control::Thread::wait_for_state_mask(Data::State::RESUME_MASK). */ +inline wait_for_RESUME_mask(i) +{ + if + :: _pid == 0 -> + printf("Init is waiting for RESUME mask on Thread %d...\n", i) + :: _pid == 1 -> + printf("Supervisor is waiting for RESUME mask on Thread %d...\n", i) + :: _pid > 1 -> + printf("Worker %d is waiting for RESUME mask on Thread %d...\n", _pid - 1, i) + fi + get_state(i) == RUNNING || + get_state(i) == STOPPING || + get_state(i) == STOPPED || + get_state(i) == ABORTING || + get_state(i) == ABORTED; + printf("Waiting ended.\n") +} + +/** Models Control::Thread::wait_for_state_mask(Data::State::HALT_MASK). */ +inline wait_for_HALT_mask(i) +{ + if + :: _pid == 0 -> + printf("Init is waiting for HALT mask on Thread %d...\n", i) + :: _pid == 1 -> + printf("Supervisor is waiting for HALT mask on Thread %d...\n", i) + :: _pid > 1 -> + printf("Worker %d is waiting for HALT mask on Thread %d...\n", _pid - 1, i) + fi + get_state(i) == STOPPED || + get_state(i) == ABORTED; + printf("Waiting ended.\n") +} + +/** Models Control::Thread::wait_for_state_mask(Data::State::ABORT_MASK). */ +inline wait_for_ABORT_mask(i) +{ + if + :: _pid == 0 -> + printf("Init is waiting for ABORTED mask on Thread %d...\n", i) + :: _pid == 1 -> + printf("Supervisor is waiting for ABORTED mask on Thread %d...\n", i) + :: _pid > 1 -> + printf("Worker %d is waiting for ABORTED mask on Thread %d...\n", _pid - 1, i) + fi + get_state(i) == ABORTED; + printf("Waiting ended.\n") +} + +/** + * Starts the Thread number i. If wait is true, then this macro blocks until + * the Thread has entered a state greater than or equal to RUNNING. + */ +inline start(i, wait) +{ + set_command(i, START); + run Thread(i); + if + :: wait -> wait_for_START_mask(i) + :: else -> skip + fi +} + +/** + * Pauses the Thread number i. If wait is true, then this macro blocks until the + * Thread has entered a state greater than or equal to PAUSED. + */ +inline pause(i, wait) +{ + set_command(i, PAUSE); + if + :: wait -> wait_for_PAUSE_mask(i) + :: else -> skip + fi +} + +/** + * Resumes the Thread number i. If wait is true, then this macro blocks until + * the Thread has entered a state greater than or equal to RUNNING. + */ +inline resume(i, wait) +{ + set_command(i, CONTINUE); + if + :: wait -> wait_for_RESUME_mask(i) + :: else -> skip + fi +} + +/** + * Stops the Thread number i. If wait is true, then this macro blocks until + * the Thread has entered the state STOPPED or ABORTED. + */ +inline stop(i, wait) +{ + set_command(i, STOP); + if + :: wait -> wait_for_HALT_mask(i) + :: else -> skip + fi +} diff --git a/samples/Promela/attacker_4_FINITE.pml b/samples/Promela/attacker_4_FINITE.pml new file mode 100644 index 0000000000..47a308d608 --- /dev/null +++ b/samples/Promela/attacker_4_FINITE.pml @@ -0,0 +1,55 @@ +/* spin -t4 -s -r experiment1_4_True_daisy_check.pml */ +active proctype attacker() { + + NtoA ! ACK; + NtoB ! SYN; + BtoN ? SYN_ACK; + NtoB ! ACK; + BtoN ? FIN; + NtoB ! ACK; + NtoB ! FIN; + BtoN ? ACK; + NtoB ! SYN; + BtoN ? SYN_ACK; + NtoB ! ACK; +// recovery to N +// N begins here ... + + do + :: AtoN ? SYN -> + if + :: NtoB ! SYN; + fi unless timeout; + :: BtoN ? SYN -> + if + :: NtoA ! SYN; + fi unless timeout; + :: AtoN ? FIN -> + if + :: NtoB ! FIN; + fi unless timeout; + :: BtoN ? FIN -> + if + :: NtoA ! FIN; + fi unless timeout; + :: AtoN ? ACK -> + if + :: NtoB ! ACK; + fi unless timeout; + :: BtoN ? ACK -> + if + :: NtoA ! ACK; + fi unless timeout; + :: AtoN ? SYN_ACK -> + if + :: NtoB ! SYN_ACK; + fi unless timeout; + :: BtoN ? SYN_ACK -> + if + :: NtoA ! SYN_ACK; + fi unless timeout; + :: _nr_pr < 3 -> break; + od +end: + +} \ No newline at end of file diff --git a/samples/Promela/bare_signals.pml b/samples/Promela/bare_signals.pml new file mode 100644 index 0000000000..bffa7fcf7e --- /dev/null +++ b/samples/Promela/bare_signals.pml @@ -0,0 +1,40 @@ +inline bare_signals_0_transition(id) +{ + int transition_id; + transition_id = id; + do + ::(transition_id == -1)-> + break; + ::(transition_id == 0)-> + bare_signals_0_state = bare_signals_0_state_1; + transition_id = -1; + ::(transition_id == 1)-> + bare_signals_0_state = bare_signals_0_state_2; + transition_id = -1; + ::(transition_id == 2)-> + bare_signals_0_state = bare_signals_0_state_1; + transition_id = -1; + od; +} +inline bare_signals_0_init() +{ + bare_signals_0_transition(0); +} +inline bare_signals_0_PI_0_signal_1() +{ + if + ::(bare_signals_0_state == bare_signals_0_state_1)-> + bare_signals_0_transition(1); + ::else-> + break; + fi; +} +inline bare_signals_0_PI_0_signal_2() +{ + if + ::(bare_signals_0_state == bare_signals_0_state_2)-> + bare_signals_0_transition(2); + ::else-> + break; + fi; +} diff --git a/samples/Promela/ex.1.pml b/samples/Promela/ex.1.pml new file mode 100644 index 0000000000..057ac71694 --- /dev/null +++ b/samples/Promela/ex.1.pml @@ -0,0 +1,49 @@ +mtype = { Wakeme, Running } + +bit lk, sleep_q +bit r_lock, r_want +mtype State = Running + +active proctype client() { + sleep: // sleep routine + atomic { (lk == 0) -> lk = 1 } // spinlock(&lk) + do // while r->lock + :: (r_lock == 1) -> // r->lock == 1 + r_want = 1 + State = Wakeme + lk = 0 // freelock(&lk) + (State == Running) // wait for wakeup + :: else -> // r->lock == 0 + break + od; + progress: + assert(r_lock == 0) // should still be true + r_lock = 1 // consumed resource + lk = 0 // freelock(&lk) + goto sleep +} + +active proctype server() { // interrupt routine + wakeup: // wakeup routine + r_lock = 0 // r->lock = 0 + (lk == 0) // waitlock(&lk) + if + :: r_want -> // someone is sleeping + atomic { // spinlock on sleep queue + (sleep_q == 0) -> sleep_q = 1 + } + r_want = 0 + + #ifdef PROPOSED_FIX + (lk == 0) // waitlock(&lk) + #endif + if + :: (State == Wakeme) -> + State = Running + :: else -> + fi; + sleep_q = 0 + :: else -> + fi + goto wakeup + } diff --git a/vendor/README.md b/vendor/README.md index deed83c704..b8bf9c93c5 100644 --- a/vendor/README.md +++ b/vendor/README.md @@ -365,6 +365,7 @@ This is a list of grammars that Linguist selects to provide syntax highlighting - **Prisma:** [prisma/vscode-prisma](https://github.com/prisma/vscode-prisma) - **Processing:** [textmate/processing.tmbundle](https://github.com/textmate/processing.tmbundle) - **Prolog:** [alnkpa/sublimeprolog](https://github.com/alnkpa/sublimeprolog) +- **Promela:** [corbanmailloux/sublime-promela-spin](https://github.com/corbanmailloux/sublime-promela-spin) - **Propeller Spin:** [bitbased/sublime-spintools](https://github.com/bitbased/sublime-spintools) - **Protocol Buffer:** [zxh0/vscode-proto3](https://github.com/zxh0/vscode-proto3) - **Pug:** [davidrios/jade-tmbundle](https://github.com/davidrios/jade-tmbundle) diff --git a/vendor/grammars/sublime-promela-spin b/vendor/grammars/sublime-promela-spin new file mode 160000 index 0000000000..e96c52c08f --- /dev/null +++ b/vendor/grammars/sublime-promela-spin @@ -0,0 +1 @@ +Subproject commit e96c52c08f9d63164f8817b3170c12bf73d37432 diff --git a/vendor/licenses/git_submodule/sublime-promela-spin.dep.yml b/vendor/licenses/git_submodule/sublime-promela-spin.dep.yml new file mode 100644 index 0000000000..7a5c603a89 --- /dev/null +++ b/vendor/licenses/git_submodule/sublime-promela-spin.dep.yml @@ -0,0 +1,31 @@ +--- +name: sublime-promela-spin +version: e96c52c08f9d63164f8817b3170c12bf73d37432 +type: git_submodule +homepage: https://github.com/corbanmailloux/sublime-promela-spin.git +license: mit +licenses: +- sources: LICENSE.txt + text: | + The MIT License (MIT) + + Copyright (c) 2016 Corban Mailloux + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +notices: []