Promela model for process list
|
|
| 1 |
#define max_nProcesses 32 |
| 2 |
#define NULL -1 |
| 3 |
mtype: boolType = {False,True}; |
| 4 |
mtype: proc_state { PROCESS_STATE_NONE, PROCESS_STATE_CALLED, PROCESS_STATE_RUNNING } |
| 5 |
typedef process { |
| 6 |
int next; |
| 7 |
byte name[9]; |
| 8 |
int thread; |
| 9 |
mtype: boolType needspoll; |
| 10 |
mtype: proc_state state; |
| 11 |
}; |
| 12 |
process processes[max_nProcesses]; |
| 13 |
int process_list=NULL; |
|
|
Structure of process list
|
Promela model of process list
|