Native Promela Code for Chiron Original Dispatcher
(2 artists, 2 events)
/* 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"
Back to Chiron Original Dispatcher (2
artists, 2 events)