Promela model for process_poll()

process_poll

1	proctype process_poll(chan process_poll_sync_chan;chan params_chan) // ---process.c\process_poll:370-380
2	{
3	int p;
4	params_chan ? p;
5	if
6	::p != NULL ->
7	if //process.c\process_poll:374-378
8	::(processes[p].state==PROCESS_STATE_RUNNING)\|\|(processes[p].state== PROCESS_STATE_CALLED) ->
9	processes[p].needspoll = 1;
10	poll_requested = True;
11	:: else -> skip;
12	fi; //End of process.c\process_poll:374-378
13	:: else -> skip;
14	fi;
15	process_poll_sync_chan ! 0;
16	} // ---End of process.c\process_poll:370-380

Control flow abstraction of process_poll()

Promela model of process_poll()

Dr.Elham Mahmoudzadeh