Allow multiple occurrences of events in a single backward reachability iteration
For my Master's project, I am currently using the feature from issue #197 (closed) to order events manually for the data-based synthesis. For my project, ordering events manually dramatically improves the computational effort (from not being able to synthesize to being able to synthesize).
I would like to propose an addition to the feature from #197 (closed). Right now it is not possible to have the same event occur twice (or more) in the event order. ESCET outputs the error: ERROR: Invalid edge order: "<event-name>" is included more than once.
. Having an event occur more than once, could in some cases reduces the number of backward reachability iterations. Especially when the event is used in multiple edges. In the end, it should reduce the computational effort and reduce the synthesis time.
To illustrate the benefit of having the same event occur multiple times in an iteration, consider the following (simple) example:
The "ideal" edge order is c
, c
, b
, a
. This would require two iterations to complete the backward reachability check (after 1 iteration every state is flagged nonblocking). However, I may only input event order c
, b
, a
. Which requires three iterations. Where only locations 1
and 4
are flagged nonblocking after 1 iteration. After 2 iterations, every location is flagged nonblocking. (A "non-ideal" edge order is a
, b
, c
, (c
) (4 iterations).)
For this simple example, the computational gain seems limited, but for larger systems, it could help a lot.