Untimed semantic model

[MattWindsor91]

This issue tracks the fact that, for some properties (often existential), the timed-traces semantic model is overly restrictive. It requires time to be considered as part of the trace, which then means that cold occurrences without duration bounds permit a set of traces parameterised by every possible number of tocks before the occurrence; situations where the model performs actions urgently require a large amount of duration(0) applying.

Could we just hide tock on both ends? Or would we need to use the untimed semantic model of RoboChart?