SEDL Source for Chiron Decomposed Dispatcher (2 artists, 2 events)

The SEDL code was generated from the Ada source code using ada_to_sedl. The resulting code had to be modified slightly to be used my INCA and by INCA-SPIN and INCA-SMV. In both cases, different modifications were made for (a) Property 1 and (b) the remaining properties. In addition, SEDL predicate definitions must be given when using INCA to generate SPIN and SMV input.

• Original SEDL source code
• Modified SEDL for INCA
  • Modified for Property 1
  • Modified for the remaining properties
• Modified SEDL for INCA-SPIN and INCA-SMV
  • Modified for Property 1
  • Modified for the remaining properties
• Predicate Definitions for INCA-SPIN and INCA-SMV
  • Predicate Definitions for Property 1
  • Predicate Definitions for the remaining properties

Back to Chiron Decomposed Dispatcher (2 artists, 2 events)