Improve bounded response check performance by checking only a single order

Idea

The idea is to check only a single order in the bounded response check, rather than every order. And, to allow executing multiple events per 'cycle' (e.g., PLC cycle). This should adhere to the 'transition execution order' being defined in #970 (closed).

It would improve performance greatly. It would also reduce the bounds significantly.

Note that more CIF to CIF transformations and other tools may then need to remove the controller properties annotation, as they may affect the transition execution order and thus invalidate the result of the bounded response check.

Origin

This has been discussed in issue #911. The idea was first posited at #911 (comment 2749009):

9. So far, we have assumed we can't change the problem we're solving. If we do allow for that, we could assume more about the execution of the controller. That is, if we assume to know the order in which the events are considered during execution (in the two loops), then we could exploit this for the bounded response check. The problem of the bounded response check as we currently do it, as that we try to compute the bound for all possible orders in which the execution may try them. This blows up exponentially in the different orders. If we assume a fixed order in which they are tried, we only have to consider that order. This would likely blow up considerably less, and prevent the exponential increase.

There is some follow-up discussion there. It was also tried out a bit, see #911 (comment 2812127):

I did a quick experiment with using a specific order (not sure if it is the exact same order as PLCgen):

• It can be computed in less than a second for the waterway lock model.
• The bound is then '1' rather than '34':

  • I was puzzled a bit by this at first, but it makes some sense. We start from any reachable state. We then take one step for each controllable event. Typically, a controllable event enables or disables an actuator. And typically the actuator then can't be switched again, unless something else happens first. That is, some sensor needs to change, uncontrollable events need to happen, and only then new control decisions are possible.

  • Thus, it is likely that a bound of '1' is enough for a lot of models in practice. If there are requirement automata that enforce some order for some controllable events, then the bound may increase beyond '1'.

  • I think RWS for instance often only uses state/event exclusion requirements, so they may not even get bounds higher than '1'.

And some follow-up discussion after that.

Addresses #970 (closed), #911, #892