Promela model for 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()
|