1 //— process.c/process_run:301-313 2 proctype process run(chan process run sync ch) 3 { chan ret chan = [0] of int; 4 int tmp; 5 if//– Begin of process.c/process_run:305-307 6 :: (poll requested == True) -> 7 run do poll(ret chan); //– Begin process.c/process_run:306 8 ret chan ? tmp;//– End of process.c/process_run:306 9 ::else->skip; 10 fi;//– End of process.c/process_run:305-307 11 run do event(ret chan); //Begin of process.c/process_run:310 12 ret chan ? tmp; //End of process.c/process_run:310 13 end: process run sync ch poll requested+nevents; //process.c/process_run:312 14 } //— End of process.c/process_run:301-313 Control flow abstraction of process_run() Promela model of process_run()
