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.
Back to Chiron Decomposed Dispatcher (2 artists, 2 events)