/* Promela specification for Chiron generated by make_npdisp.pl Single Dispatcher Version Name: disp.prom Created on: Thu Oct 21 14:46:38 EDT 1999 Number of artists: 2 Number of events: 2 Configuration: 11 10 */ #define number_of_artists 2 mtype = {art1, art2, e1, e2, register_event, unregister_event, notify_artists, start_artist, notify_client_event, terminate_artist, start_wrapper, start_manager, a1_registered, a2_registered, end_rendezvous} mtype e1_lst[number_of_artists]; mtype e2_lst[number_of_artists]; byte e1_sz = 0; byte e2_sz = 0; chan dispatcher_chan = [0] of {mtype, mtype, mtype}; chan a1_chan = [0] of {mtype, mtype}; chan a2_chan = [0] of {mtype, mtype}; chan adt_wrapper_chan = [0] of {mtype}; chan artist_manager_chan = [0] of {mtype}; proctype dispatcher() { mtype a_id; mtype event; byte i; end_select: do :: atomic { dispatcher_chan?register_event,a_id,event -> if :: (event == e1) -> i = 1; do :: if :: (i > e1_sz) -> e1_sz++; e1_lst[i-1] = a_id; break :: else fi; if :: (e1_lst[i-1] == a_id) -> break :: else fi; i++ od :: (event == e2) -> i = 1; do :: if :: (i > e2_sz) -> e2_sz++; e2_lst[i-1] = a_id; break :: else fi; if :: (e2_lst[i-1] == a_id) -> break :: else fi; i++ od fi }; /* The following if...fi clause is here just to define the predicate afterregistera2e1. */ if :: ((event == e1) && (a_id == art2)) -> aftrega2e1: skip :: else fi; atomic{a_id = art1; event = e1; i = 0} :: atomic { dispatcher_chan?unregister_event,a_id,event -> if :: (event == e1) -> if :: (e1_sz == 0) -> skip :: else -> i = 1; do :: (i > e1_sz) -> break :: else -> if :: (e1_lst[i-1] == a_id) -> do :: (i >= e1_sz) -> break :: else -> e1_lst[i-1] = e1_lst[i]; i++ od; e1_sz-- :: else fi; i++ od; e1_lst[e1_sz] = 0 fi :: (event == e2) -> if :: (e2_sz == 0) -> skip :: else -> i = 1; do :: (i > e2_sz) -> break :: else -> if :: (e2_lst[i-1] == a_id) -> do :: (i >= e2_sz) -> break :: else -> e2_lst[i-1] = e2_lst[i]; i++ od; e2_sz-- :: else fi; i++ od; e2_lst[e2_sz] = 0 fi fi; a_id = art1; event = e1; i = 0 } :: dispatcher_chan?notify_artists,event,_ -> if :: (event == e1) -> i = 1; do :: (i > e1_sz) -> break :: else -> if :: (e1_lst[i-1] == art1) -> notclievta1e1: a1_chan!notify_client_event,e1 :: (e1_lst[i-1] == art2) -> notclievta2e1: a2_chan!notify_client_event,e1 fi od :: (event == e2) -> i = 1; do :: (i > e2_sz) -> break :: else -> if :: (e2_lst[i-1] == art1) -> notclievta1e2: a1_chan!notify_client_event,e2 :: (e2_lst[i-1] == art2) -> notclievta2e2: a2_chan!notify_client_event,e2 fi od fi; atomic{ dispatcher_chan?notify_artists,end_rendezvous,_; a_id = art1; event = e1; i = 0 } od } proctype a1() { mtype notify_event, event; a1_chan?start_artist,_; rega1e1: dispatcher_chan!register_event,art1,e1; rega1e2: dispatcher_chan!register_event,art1,e2; artist_manager_chan!a1_registered; do :: if :: atomic { a1_chan?notify_client_event,event -> notify_event = event } :: a1_chan?terminate_artist,_ -> unrega1e1: dispatcher_chan!unregister_event,art1,e1; unrega1e2: dispatcher_chan!unregister_event,art1,e2; a1_chan?end_rendezvous,_; break fi od; atomic{notify_event = e1; event = e1} } proctype a2() { mtype notify_event, event; a2_chan?start_artist,_; rega2e1: dispatcher_chan!register_event,art2,e1; artist_manager_chan!a2_registered; do :: if :: atomic { a2_chan?notify_client_event,event -> notify_event = event } :: a2_chan?terminate_artist,_ -> unrega2e1: dispatcher_chan!unregister_event,art2,e1; a2_chan?end_rendezvous,_; break fi od; atomic{notify_event = e1; event = e1} } proctype adt_wrapper() { adt_wrapper_chan?start_wrapper; do :: if :: true -> dispatcher_chan!notify_artists,e1; notarte1: dispatcher_chan!notify_artists,end_rendezvous; aftnotarte1: skip :: true -> dispatcher_chan!notify_artists,e2; notarte2: dispatcher_chan!notify_artists,end_rendezvous fi od } proctype artist_manager() { artist_manager_chan?start_manager; a1_chan!start_artist; a2_chan!start_artist; artist_manager_chan?a1_registered; artist_manager_chan?a2_registered; artist_manager_chan?end_rendezvous; /* do :: true -> skip :: true -> break od; */ a1_chan!terminate_artist; a1_chan!end_rendezvous; a2_chan!terminate_artist; a2_chan!end_rendezvous; end_artist_manager: 0 } proctype client_init() { artist_manager_chan!start_manager; artist_manager_chan!end_rendezvous; adt_wrapper_chan!start_wrapper } init { /* pid 0 */ atomic { run dispatcher(); /* pid 1 */ run a1(); /* pid 2 */ run a2(); /* pid 3 */ run adt_wrapper(); /* pid 4 */ run artist_manager(); /* pid 5 */ run client_init() /* pid 6 */ } } #define registera1e1 a1[2]@rega1e1 #define unregistera1e1 a1[2]@unrega1e1 #define registera1e2 a1[2]@rega1e2 #define unregistera1e2 a1[2]@unrega1e2 #define registera2e1 a2[3]@rega2e1 #define unregistera2e1 a2[3]@unrega2e1 #define afterregistera2e1 dispatcher[1]@aftrega2e1 #define isregistereda1e1 \ (((e1_sz >= 1) && (e1_lst[0] == art1)) || \ ((e1_sz >= 2) && (e1_lst[1] == art1))) #define isregistereda1e2 \ (((e2_sz >= 1) && (e2_lst[0] == art1)) || \ ((e2_sz >= 2) && (e2_lst[1] == art1))) #define isregistereda2e1 \ (((e1_sz >= 1) && (e1_lst[0] == art2)) || \ ((e1_sz >= 2) && (e1_lst[1] == art2))) #define notifyartistse1 adt_wrapper[4]@notarte1 #define notifyartistse2 adt_wrapper[4]@notarte2 #define afternotifyartistse1 adt_wrapper[4]@aftnotarte1 #define notifyclienteventa1e1 dispatcher[1]@notclievta1e1 #define notifyclienteventa1e2 dispatcher[1]@notclievta1e2 #define notifyclienteventa2e1 dispatcher[1]@notclievta2e1 #define notifyclienteventa2e2 dispatcher[1]@notclievta2e2 #define e1szEQ0 (e1_sz == 0) #define e1szGT0 (e1_sz > 0) #define e2szGT0 (e2_sz > 0) #define registereda1a2e1 \ ((e1_sz >= 2) && (e1_lst[1] == art2) && (e1_lst[0] == art1)) #define term artist_manager[5]@end_artist_manager #include "disp.never"