Document and use a consistent transition execution order for CIF tools that use it
Several tools use a transition execution order, or will use it, and these should be consistent.
This issue supersedes issue #628 (closed), which was only about having two loops (for uncontrollable and controllable events). This issue includes that, but includes more things that affect the execution order.
Steps
-
Document the order properly in the CIF controller properties checker documentation. (!1050 (merged)) -
Use the order consistently in relevant tools: -
PLCgen (!1050 (merged)) -
CIF code generator (!1050 (merged)) -
Bounded response check (#971 (closed))
-
Follow-ups
- Optional 'execution mode' of the CIF simulator (#1045 (closed))
The order
- Assumptions:
- All events are either controllable or uncontrollable. So, no kindless events and no 'tau' events.
- Pre-processing:
- Any component definitions/instantiations are eliminated, using the 'Eliminate component definition/instantiation' CIF to CIF transformation.
- Any state/event exclusion invariants are eliminated, using the 'Eliminate state/event exclusion invariants' CIF to CIF transformation. We do need to consider consistency between 'Eliminate state/event exclusion invariants' and what CIF to BDD does. But, maybe it doesn't matter, as this always synchronizes with the rest, so then the order is not relevant. Automaton order is only relevant for channel senders/receivers, I think (see below).
- Transition execution order:
- There is code generated from the CIF specification that is regularly executed (at fixed or variable time intervals), completing one execution before the next (e.g., PLC cycles).
- The code has three parts, that are executed in order:
- The values of the input variables are read from the environment.
- Execute transitions: first one loop for transitions for uncontrollable events, then one for transitions for controllable events.
- The outputs are written to the environment.
- Per loop:
- The events are ordered in some way (see event order below).
- For each event, in order, at most one transition is executed.
- If the event is enabled, one transition is executed for it. If the event is disabled, it is skipped.
- After each event, regardless of whether it was enabled and a transition was executed for it, the next event is considered, and so on for all the events of the particular loop.
- Once all events have been considered once, if for any of the events a transition was executed, then another iteration of the loop is performed.
- The loop is executed as many times as necessary, until no event is enabled anymore. However, a limit may be set and then the loop is executed as most as many times as the limit indicates.
- Per event:
- If the event is a channel, the first enabled sender automaton for that channel participates in the transition (see automaton order below).
- If the event is a channel, the first enabled receiver automaton for that channel participates in the transition (see automaton order below).
- For each participating automaton for the event (sender, receiver, monitor or non-monitor synchronizing automaton), the first enabled edge participates in the transition (see location and edge orders below).
- For a monitor automaton for the event, if there is no enabled edge in the current location of the automaton, the automaton is ignored for that transition.
- CIF object orders:
- In general, there are several way to order things, with pros and cons. Some things to consider:
- Sorting objects is maybe the most stable, as we can do that explicitly after collecting objects. But, users can't influence it then.
- Model order can be influenced by user, but there could be many places we need to make consistent. We also need to define how to walk over the model (breadth-first, depth-first, collect locally first or recursively first, etc).
- The order affects the order that PLC code is generated and thus readability. It also affects the BDD edge order, and thus can have an impact on the synthesis performance.
- Automata of the specification:
- Alternative 1: Sorted on names (see sorting notes below).
- Alternative 2: Order produced by
CifCollectUtils.collectAutomata
. Would need to be documented then in the method's JavaDoc, and likely needs unit tests to ensure it never changes later on. Also, the order may not be super logical as it is now.
- Events:
- Alternative 1: Alphabet of the specification (send/receive/sync alphabet), sorted on names (see sorting notes below).
- Alternative 2: Order produced by
CifCollectUtils.collectEvents
. Would need to be documented then in the method's JavaDoc, and likely needs unit tests to ensure it never changes later on. Also, the order may not be super logical as it is now. Also, this gives all declarations, which may be more than the alphabet of the specification, so it would need to be restricted to the alphabet of the specification. - Alternative 3: Order as PLCgen has it now, which is per automaton either the explicit alphabet, or the order that events are encountered by going through the locations, edges and edge events, followed by the monitor events as specified. Note that this is further affected by the 'Simplify others' CIF to CIF transformation that is done as pre-processing, which removes duplicate events of alphabets, monitors and on edges.
- Locations: order as defined in the automaton (model order).
- Edges: order as defined in the location (model order).
- Edge events are not relevant. For each edge event on an edge, the guards/updates are the same. They either concern different events and then the event order is relevant. Or they are duplicate events that only need to be considered once.
- In general, there are several way to order things, with pros and cons. Some things to consider:
- Sorting of CIF objects (if we go for that):
- Sort the objects alphabetically in increasing order on their absolute non-escaped names, based on the ASCII characters in the absolute names.
- Automata can't contain automata, and also events can't contain events. But, one may still be a prefix of another, for instance
event1
andevent1b
. We thus need to define how it sorts in those cases. - We could partition on '.' and 'number to non-number' and 'non-number to number' boundaries, and then sort number parts numerically and rest ASCII compare. This would solve '10' before '2' issues.
- We could sort non-numeric parts first non-case-sensitive and then case sensitive, like
org.eclipse.escet.common.java.Strings.SORTER
. But, is that always better?
Some choices thus still need to be made about the automata and event orders.
Controller checker annotation instead of documented order
We could also opt not to document the execution order, but instead have the controller checker indicate the order in the controller properties annotation, or some other annotation. However, then we may need to have a list of event and a list of automata in there. Annotation arguments are type checked as expressions. Expressions don't allow event references, as we only allow them in specific places (like on edges and in invariants). Component references are allowed in expressions (for instance to switch over automata), but a list with a component type as element type is not allowed. So, this would require changes to annotations, if we were to go for this. For now, let's start with just documenting it and making it compatible.