**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.