Promela model for process list

process_run

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