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?
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
tockon both ends? Or would we need to use the untimed semantic model of RoboChart?