CIF simulator trace input mode: can't replay trace exactly for non-deterministic events

The problem

In case of non-deterministic events, currently either there are two options:

• strict mode on: don't allow non-deterministic events when replaying the trace file.
• strict mode off: allow non-deterministic events and let the automatic input component choose.

In the former, non-deterministic events are not at all supported, and in the latter the automatic input component may not choose what we want. To be able to faithfully replay an earlier execution, we should have enough information in the trace file to choose.

Proposed solution

I propose:

• Add a state command:
  • Syntax: state <var_1>=<value_1> <aut_2=loc_2> ... <var_n>=<value_n>.
  • Indicates the state of the model at the moment the command is present in the trace file. If the state does not match these values of variable and locations of automata, an error occurs in replaying the trace.
  • The variable names, automata names, location names, and values, use the same syntax as we use in state annotations. We may allow a bit more in the simulator, we'll have to see about the details. It should match CIF literal syntax, and ideally we can use the CIF value parser that we also use for initial values of input variables and discrete variables with multiple potential initial values.
  • Not all variables or automata need to be specified. Only the ones that are specified need to match. There are no restrictions on the other variables and automata.
  • Depending on the configured time mode, time may or may not pass before a state command.
• In case of a non-deterministic choice for an event e:
  • The event command is not followed by a state command: the behavior is as before.
  • The event command is followed by one or more state commands:
    • If there multiple state commands concern different variables, they together form a more complete state. If they specify the same values for the same variable, that still holds. If they have conflicting values for the same variable, the first one 'wins'. The later state command with conflicting value may lead to an error when it is later executed itself.
    • If strict mode is on: there must be exactly one possible transitions for e that leads to the given state. That one is chosen. If there is not exactly one such transition, it is still an error.
    • If strict mode is off: from the possible transitions for e, those that lead to the given state are selected and passed to the automatic input component to choose from.

Alternative

An alternative to using the state command after an event command, is to combine them. For instance, something like:

• event e to state <var_1>=<value_1> <aut_2=loc_2> ... <var_n>=<value_n>.

This idea is based on #710.

Open issues

• Real value precision: To represent states, the difficulty is likely real numbers. The values of continuous variables will likely be slightly different due to numeric precision, ODE solving, etc. How to match states to make sure a state command is 'satisfied' is non-trivial. Similarly, matching possible end states of event transitions to 'filter' them has the same issues.