Chiron User Interface with Decomposed Dispatcher
2 artists, 2 events


In this sample Chiron Interface, there are two artists and two events. The first artist begins by registering for both events, and the second artist registers for the first, but not the second. After this, for an undertermined period, the dispatcher receives events and passes them along to the appropriate artist or artists. Then both artists unregister for each of the events for which they have registered, and the program terminates.



Back to Chiron User Interface

Back to Example Repository for Finite State Verification Tools