MODIFICATIONS
SEDL code (a) was further modified as
follows. Once we've verified that artists cannot register when they
are already registered, we add an (assume nil) statement
to the code that would be reached in the dispatcher if this were to
occur. This statement tells the model builder that the behavior along
this branch is to be pruned, resulting in a smaller FSA for the
dispatcher. In particular, in dispatcher FSA states where an artist
has registered for an event, there will be no accept events for that
artist registering for that event (since that branch was pruned).
In addition, we have inserted a line
(assert (< e1_sz number_of_artists))which is used for verifying Property 8.
(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)
(
(assert (< e1_sz number_of_artists))
(assign e1_sz (+ e1_sz 1))
(assign
(index e1_lst i) a_id)
((exit))))
(if (=
(index e1_lst i) a_id)
(
(assume nil)))
(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)
(
(assume nil)))
(assign i (+ i 1)))))))))
(when t
(accept unregister_event (
(case event_kind
("e1" (
(if (= e1_sz 0)
(
(assume nil))
(
;; Begin inserted section
(assign i 1)
(while (<= i e1_sz)
(if (= (index e1_lst i) a_id)
(exit)
(assign i (+ i 1))))
(if (> i e1_sz) (assume nil))
;; End inserted section
(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)
(
(assume nil))
(
;; Begin inserted section
(assign i 1)
(while (<= i e2_sz)
(if (= (index e2_lst i) a_id)
(exit)
(assign i (+ i 1))))
(if (> i e2_sz) (assume nil))
;; End inserted section
(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)