Native Promela Code for Chiron Decomposed Dispatcher
(2 artists, 2 events)
/* Promela specification for Chiron generated by make_npmdisp.pl
Multiple Dispatcher Version
Name: disp.prom
Created on: Fri Oct 22 09:49:28 EDT 1999
Number of artists: 2
Number of events: 2
Configuration: 11 10
*/
#define number_of_artists 2
mtype = {art1,
art2,
e1,
e2,
register, unregister, notify,
start_artist, notify_client_event, terminate_artist,
start_wrapper,
start_manager,
a1_registered,
a2_registered,
end}
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 dispatch_e1_chan = [0] of {mtype, mtype};
chan dispatch_e2_chan = [0] of {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;
end_select:
do
:: dispatcher_chan?register,a_id,event ->
if
:: (event == e1) ->
dispatch_e1_chan!register,a_id
:: (event == e2) ->
dispatch_e2_chan!register,a_id
fi;
dispatcher_chan?register,end,_;
if
:: ((event == e1) && (a_id == art2)) ->
aftrega2e1:
skip
:: else
fi
:: dispatcher_chan?unregister,a_id,event ->
if
:: (event == e1) ->
dispatch_e1_chan!unregister,a_id
:: (event == e2) ->
dispatch_e2_chan!unregister,a_id
fi;
dispatcher_chan?unregister,end,_
:: dispatcher_chan?notify,event,_ ->
if
:: (event == e1) ->
dispatch_e1_chan!notify;
dispatch_e1_chan!notify,end
:: (event == e2) ->
dispatch_e2_chan!notify;
dispatch_e2_chan!notify,end
fi;
dispatcher_chan?notify,end,_
od
}
proctype dispatch_e1() {
mtype a_id;
byte i;
end_select:
do
:: atomic {
dispatch_e1_chan?register,a_id ->
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;
a_id = art1; i = 0
}
:: atomic {
dispatch_e1_chan?unregister,a_id ->
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;
a_id = art1; i = 0
}
:: dispatch_e1_chan?notify,_ ->
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;
atomic{
dispatch_e1_chan?notify,end;
a_id = art1; i = 0
}
od
}
proctype dispatch_e2() {
mtype a_id;
byte i;
end_select:
do
:: atomic {
dispatch_e2_chan?register,a_id ->
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;
a_id = art1; i = 0
}
:: atomic {
dispatch_e2_chan?unregister,a_id ->
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;
a_id = art1; i = 0
}
:: dispatch_e2_chan?notify,_ ->
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;
atomic{
dispatch_e2_chan?notify,end;
a_id = art1; i = 0
}
od
}
proctype a1() {
mtype notify_event, event;
a1_chan?start_artist,_;
rega1e1:
dispatcher_chan!register,art1,e1;
dispatcher_chan!register,end;
rega1e2:
dispatcher_chan!register,art1,e2;
dispatcher_chan!register,end;
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,art1,e1;
dispatcher_chan!unregister,end;
unrega1e2:
dispatcher_chan!unregister,art1,e2;
dispatcher_chan!unregister,end;
a1_chan?terminate_artist,end;
break
fi
od;
atomic{notify_event = e1; event = e1}
}
proctype a2() {
mtype notify_event, event;
a2_chan?start_artist,_;
rega2e1:
dispatcher_chan!register,art2,e1;
dispatcher_chan!register,end;
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,art2,e1;
dispatcher_chan!unregister,end;
a2_chan?terminate_artist,end;
break
fi
od;
atomic{notify_event = e1; event = e1}
}
proctype adt_wrapper() {
adt_wrapper_chan?start_wrapper;
do
:: if
:: true -> dispatcher_chan!notify,e1;
notarte1:
dispatcher_chan!notify,end;
aftnotarte1:
skip
:: true -> dispatcher_chan!notify,e2;
notarte2:
dispatcher_chan!notify,end
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;
/*
do
:: true -> skip
:: true -> break
od;
*/
a1_chan!terminate_artist;
a1_chan!terminate_artist,end;
a2_chan!terminate_artist;
a2_chan!terminate_artist,end;
end_artist_manager:
0
}
proctype client_init() {
artist_manager_chan!start_manager;
artist_manager_chan!end;
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 */
run dispatch_e1(); /* pid 7 */
run dispatch_e2(); /* pid 8 */
}
}
#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 dispatch_e1[7]@notclievta1e1
#define notifyclienteventa1e2 dispatch_e2[8]@notclievta1e2
#define notifyclienteventa2e1 dispatch_e1[7]@notclievta2e1
#define notifyclienteventa2e2 dispatch_e2[8]@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 Decomposed Dispatcher (2
artists, 2 events)