MODIFICATIONS
The orignal SEDL code produced by the
translator ada_to_sedl was modified as follows. When an
artist unregisters for an event, we add a declaration (dead
...) telling the model builder that we think that slot of the
event array is now dead. The model builder will set the slot to a
fixed value (thus reducing the number of states), but will also check
to make sure the slot is not read again before it is written (i.e.,
was really dead).
(type a_id_type (enumerated
"art1"
"art2"))
(type e_kind (enumerated
"e1"
"e2"))
(type list_size (range 0 2))
(type i_range (range 1 3))
(constant number_of_artists 2)
(constant number_of_events 2)
(task a1 (
(entry start_artist)
(entry notify_client_event
(by-value event e_kind))
(entry terminate_artist)
(variable notify_event e_kind)
(entry terminate_artist-end))
(
(accept start_artist)
(call dispatcher register_event
"art1"
"e1")
(call dispatcher register_event
"art1"
"e2")
(call artist_manager a1_registered)
(loop
(select
(when t
(accept notify_client_event (
(assign notify_event event))))
(when t
(accept terminate_artist (
(call dispatcher unregister_event
"art1"
"e1")
(call dispatcher unregister_event
"art1"
"e2")
(accept terminate_artist-end)))
((exit)))))))
(task a2 (
(entry start_artist)
(entry notify_client_event
(by-value event e_kind))
(entry terminate_artist)
(variable notify_event e_kind)
(entry terminate_artist-end))
(
(accept start_artist)
(call dispatcher register_event
"art2"
"e1")
(call artist_manager a2_registered)
(loop
(select
(when t
(accept notify_client_event (
(assign notify_event event))))
(when t
(accept terminate_artist (
(call dispatcher unregister_event
"art2"
"e1")
(accept terminate_artist-end)))
((exit)))))))
(task adt_wrapper (
(entry start_wrapper))
(
(accept start_wrapper)
(loop
(call dispatcher notify_artists
(choose e_kind))
(call dispatcher notify_artists-end))))
(task artist_manager (
(entry start_manager)
(entry a1_registered)
(entry a2_registered)
(entry start_manager-end))
(
(accept start_manager (
(call a1 start_artist)
(call a2 start_artist)
(accept a1_registered)
(accept a2_registered)
(accept start_manager-end)))
(while
(choose (boolean))
(
(null)))
(call a1 terminate_artist)
(call a1 terminate_artist-end)
(call a2 terminate_artist)
(call a2 terminate_artist-end)))
(task client_init ()
(
(call artist_manager start_manager)
(call artist_manager start_manager-end)
(call adt_wrapper start_wrapper)))
(task dispatcher (
(entry register_event
(by-value a_id a_id_type)
(by-value event_kind e_kind))
(entry unregister_event
(by-value a_id a_id_type)
(by-value event_kind e_kind))
(entry notify_artists
(by-value event e_kind))
(variable e1_lst
(array (range 1 number_of_artists) a_id_type))
(variable e2_lst
(array (range 1 number_of_artists) a_id_type))
(variable e1_sz list_size 0)
(variable e2_sz list_size 0)
(variable i i_range)
(entry notify_artists-end))
(
(loop
(select
(when t
(accept register_event (
(case event_kind
("e1" (
(assign i 1)
(loop
(if (> i e1_sz)
(
(assign e1_sz (+ e1_sz 1))
(assign
(index e1_lst i) a_id)
((exit))))
(if (=
(index e1_lst i) a_id)
(
((exit))))
(assign i (+ i 1)))))
("e2" (
(assign i 1)
(loop
(if (> i e2_sz)
(
(assign e2_sz (+ e2_sz 1))
(assign
(index e2_lst i) a_id)
((exit))))
(if (=
(index e2_lst i) a_id)
(
((exit))))
(assign i (+ i 1)))))))))
(when t
(accept unregister_event (
(case event_kind
("e1" (
(if (= e1_sz 0)
(
(null))
(
(assign i 1)
(while
(<= i e1_sz)
(
(if (=
(index e1_lst i) a_id)
(
(while
(< i e1_sz)
(
(assign
(index e1_lst i)
(index e1_lst (+ i 1)))
(assign i (+ i 1))))
(assign e1_sz (- e1_sz 1))))
(assign i (+ i 1))))
(dead (index e1_lst (+ e1_sz 1)))))))
("e2" (
(if (= e2_sz 0)
(
(null))
(
(assign i 1)
(while
(<= i e2_sz)
(
(if (=
(index e2_lst i) a_id)
(
(while
(< i e2_sz)
(
(assign
(index e2_lst i)
(index e2_lst (+ i 1)))
(assign i (+ i 1))))
(assign e2_sz (- e2_sz 1))))
(assign i (+ i 1))))
(dead (index e2_lst (+ e2_sz 1)))))))))))
(when t
(accept notify_artists (
(case event
("e1" (
(for i 1 e1_sz (
(case
(index e1_lst i)
("art1" (
(call a1 notify_client_event
"e1")))
("art2" (
(call a2 notify_client_event
"e1"))))))))
("e2" (
(for i 1 e2_sz (
(case
(index e2_lst i)
("art1" (
(call a1 notify_client_event
"e2")))
("art2" (
(call a2 notify_client_event
"e2")))))))))
(accept notify_artists-end))))
(when t
(terminate))))))
Back to SEDL Source for Chiron Original Dispatcher (2 artists, 2 events)