Process Bancone { int nbomb = 0; long tick = 0, alarm = -1; bool butta = false; entry friggi_i(out int rimasti); entry friggi_f; entry servi_cliente_i; entry servi_cliente_f; entry scaduti; entry clock; entry wait_timer; entry set_timer (in long n); do [] nbomb == 0 or butta; accept friggi_i(out nrimasti); nrimasti = nbomb; [] ; accept friggi_f() -> nbomb = 30; alarm = tick + minuti(60); butta = false; [] nbomb > 0 and !butta; accept servi_cliente_i(); [] ; accept servi_cliente_f() -> nbomb--; [] ; accept clock(); -> tick++; [] tick >= alarm and alarm != -1; accept wait_timer() -> butta = true; nbomb = 0; alarm = -1; [] ; accept set_timer(in long n) -> alarm = tick + n; [] ; accept scaduti -> butta = true; od; } Process Mario { int nrimasti; while(true){ call Bancone.friggi_i(nrimasti); if(nrimasti) < butta >; < friggi bomboloni > call Bancone.set_timer(60); call Bancone.friggi_f(); } } Process Piero { while(true){ < attendi cliente > call Bancone.servi_cliente_i(); < servi cliente > call Bancone.servi_cliente_f(); } } Process Rosa { while(true){ call Bancone.wait_timer(); call Bancone.butta(); } } Process Clock { while(true){ < hardware clock ticks > call Bancone.clock(); } }