One issue with the timed semantic model (see also #125) is that RoboChart actions tend to induce urgency or other interesting timing behaviour into models. RoboCert has no special support for communications coming through actions vs those coming through transitions; this issue tracks whether it should.
One issue is that the semantics does not visibly distinguish between actions and transitions, so we would need to make this visible to reason about it.
One issue with the timed semantic model (see also #125) is that RoboChart actions tend to induce urgency or other interesting timing behaviour into models. RoboCert has no special support for communications coming through actions vs those coming through transitions; this issue tracks whether it should.
One issue is that the semantics does not visibly distinguish between actions and transitions, so we would need to make this visible to reason about it.