CIF event-based toolset: add state annotations to output CIF models
We recently added an option to add state annotations to the output CIF models generated by the CIF explorer (see #687 (closed)). It would be very useful for our research if the event-based toolset applications that output a CIF model, would do so as well.
The following tools from the event-based toolset generate a CIF model as output:
- Event-based automaton abstraction
- Event-based automaton projection
- Event-based DFA minimization
- Event-based NFA to DFA automaton conversion
- Event-based supervisor synthesis
- Event-based synchronous product
- Event-based trim
Some notes:
- All these applications use
org.eclipse.escet.cif.eventbased.apps.conversion.ConvertFromEventBased.convertAutomaton
to generate the output CIF automaton. So, adding the annotations there should be sufficient. - We may want to add an option, like the CIF explorer has, to allow adding or not adding the state annotations.
- It should be relatively easy to determine the state annotation(s) to add, since a
org.eclipse.escet.cif.eventbased.automata.Location
has anorigin
, which is an instance ofCifOrigin
, which tracks the origin information. There may be multiple original locations that became one location in the result of the tool (LocationSetOrigin
,StateOrigin
), and hence there may be multiple state annotations for a single output location. This information should be sufficient to determine the state annotations to add.