(O)XSTS statement-based witness trace

[arminzavada]

The current witness generation generates a true witness, however, the exact operations executed are encoded implicitly in the model using pre- and post-conditions. It would be valuable to have an explicit representation as well, that explicitly states the exact path the model checker took.

Tasks:

• Design the trace representation
• Implement Semantifyr and Backend trace generation

[arminzavada]

Idea for the trace: introduce a new trace keyword, that constructs new instances whenever executed. These instances are placed into a steps feature of the resulting witness type.

Each constructed step instance encodes one specific step of the execution, executing them in the execution order replays the trace.

Separate the steps into Big and Small steps. A big step is an exact execution of a full transition. Small steps are the internal steps in a big step, specifying some parts of the execution with semantic meaning.

For example, in a state machine the big step is the full processing of the incoming event. The internal small steps are the intricate details, such as checking the guard condition, executing the exit action, firing the transition, and finally executing the entry action.

The Big and Small step separetion should be done automatically, making sure that the resulting witness target is a semantically accurate refinement of the original model.