10
0
mirror of https://github.com/LCPQ/quantum_package synced 2024-12-23 04:43:50 +01:00
quantum_package/promela/model.pml
2017-05-02 22:53:59 +02:00

36 lines
854 B
Promela

#define NPROC 3
#define BUFSIZE 2
#define NTASKS 4
mtype = { NONE, OK, WRONG_STATE, TERMINATE, GETPSI, PUTPSI, NEWJOB, ENDJOB, SETRUNNING,
SETWAITING, SETSTOPPED, CONNECT, DISCONNECT, ADDTASK, DELTASK, TASKDONE, GETTASK,
PSI, TASK, PUTPSI_REPLY, WAITING, RUNNING, STOPPED
}
#define send_req( MESSAGE, VALUE ) atomic { msg.m=MESSAGE ; msg.value=VALUE ; msg.state=state; } ; rep_socket ! msg; msg.reply ? reply
/* Request/Reply pattern */
typedef rep_message {
mtype m = NONE;
byte value = 0;
}
typedef req_message {
mtype m = NONE;
byte state = 0;
byte value = 0;
chan reply = [BUFSIZE] of { rep_message };
}
/* Channels */
chan rep_socket = [NPROC] of { req_message };
chan pull_socket = [NPROC] of { byte };
#include "task_server.pml"
#include "fortran.pml"
#include "collector.pml"
#include "slave.pml"