10
0
mirror of https://github.com/LCPQ/quantum_package synced 2024-12-22 20:35:19 +01:00
quantum_package/promela/slave.pml

30 lines
539 B
Promela
Raw Normal View History

2017-05-02 17:41:58 +02:00
proctype slave() {
req_message msg;
rep_message reply;
byte task;
byte state;
send_req(CONNECT, 0);
assert (reply.m == OK);
state = reply.value;
send_req(GETPSI, 0);
assert (reply.m == PSI);
task=255;
do
:: (task == 0) -> break;
:: else ->
send_req( GETTASK, 0);
if
:: (reply.m == NONE) -> task = 0;
:: (reply.m == TASK) ->
task = reply.value;
/* Compute task */
send_req( TASKDONE, task);
assert (reply.m == OK);
pull_socket ! task;
fi
od
}