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
(internal "after_accept_notify_artists_e1")which allows us to create a predicate representing the code reaching that point.
(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-end)
(call dispatcher register_event
"art1"
"e2")
(call dispatcher register_event-end)
(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-end)
(call dispatcher unregister_event
"art1"
"e2")
(call dispatcher unregister_event-end)
(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 dispatcher register_event-end)
(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")
(call dispatcher unregister_event-end)
(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 dispatch_e1 (
(entry register_e1
(by-value a_id a_id_type))
(entry unregister_e1
(by-value a_id a_id_type))
(entry notify_e1)
(variable e1_lst
(array (range 1 number_of_artists) a_id_type))
(variable e1_sz list_size 0)
(variable i i_range)
(entry notify_e1-end))
(
(loop
(select
(when t
(accept register_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)
(
(assume nil)))
(assign i (+ i 1))))))
(when t
(accept unregister_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))))))))
(when t
(accept notify_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"))))))
(accept notify_e1-end))))
(when t
(terminate))))))
(task dispatch_e2 (
(entry register_e2
(by-value a_id a_id_type))
(entry unregister_e2
(by-value a_id a_id_type))
(entry notify_e2)
(variable e2_lst
(array (range 1 number_of_artists) a_id_type))
(variable e2_sz list_size 0)
(variable i i_range)
(entry notify_e2-end))
(
(loop
(select
(when t
(accept register_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_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_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_e2-end))))
(when t
(terminate))))))
(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))
(entry register_event-end)
(entry unregister_event-end)
(entry notify_artists-end))
(
(loop
(select
(when t
(accept register_event (
(case event_kind
("e1" (
(call dispatch_e1 register_e1
a_id)))
("e2" (
(call dispatch_e2 register_e2
a_id))))
(accept register_event-end))))
(when t
(accept unregister_event (
(case event_kind
("e1" (
(call dispatch_e1 unregister_e1
a_id)))
("e2" (
(call dispatch_e2 unregister_e2
a_id))))
(accept unregister_event-end))))
(when t
(accept notify_artists (
(case event
("e1" (
(internal "after_accept_notify_artists_e1")
(call dispatch_e1 notify_e1)
(call dispatch_e1 notify_e1-end)))
("e2" (
(call dispatch_e2 notify_e2)
(call dispatch_e2 notify_e2-end))))
(accept notify_artists-end))))
(when t
(terminate))))))
Back to SEDL Source for Chiron Original Dispatcher (2 artists, 2 events)