Add Casper Visser's automatic edge ordering algorithm to CIF data-based synthesis tool
This is a direct follow-up of #426 (closed), where this was already discussed.
From the description of that issue:
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).
[...] 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). [...]For this simple example, the computational gain seems limited, but for larger systems, it could help a lot.
From #426 (comment 1020808):
Let's imagine we have a counter model which could count from 0 to 5 (marked 0). And an actuator that may turn on or off (marked off). Suppose the actuator may only turn off when the counter counts 5 and it may only turn on when it counts 0. Our models look like this:
Requirements:
Actuator.off
\implies
Counter.5Actuator.on
\implies
Counter.0First of all, I decide what would be an ideal edge order for every plant model. For the counter we get:
decrease
,decrease
,decrease
,decrease
,decrease
,increase
,increase
,increase
,increase
,increase
For the actuator we get:off
,on
.From this I make the following conclusions:
increase
may never occur beforedecrease
andon
not beforeoff
in the event order.Secondly, to determine the order between plant models, I consider the requirements. The first requirement specifies that
off
can only occur when the counter is at 5. This location is flagged as nonblocking after the fivedecrease
edges. So I placeoff
after the fivedecrease
edges. The second requirement restricts eventon
. This event may only happen when the counter is at 0. Soon
should be placed after five timesincrease
. In the end, it gives the edge order:decrease
,decrease
,decrease
,decrease
,decrease
,off
,increase
,increase
,increase
,increase
,increase
,on
.If I draw the synchronous product of the plant and requirement model, it shows that the edge order is indeed the fastest to conclude the nonblocking check.
[...]
From #426 (comment 1020854):
First of all, I decide what would be an ideal edge order for every plant model. ... Secondly, to determine the order between plant models, I consider the requirements.
[...] it would seem that some automation to determine the order automatically would also be possible, by analyzing the plant/requirement models, given that you already sketch a partial structured approach. [...]
From #426 (comment 1020876):
it would seem that some automation to determine the order automatically would also be possible, by analyzing the plant/requirement models, given that you already sketch a partial structured approach.
In my Master's thesis, I am proposing this specific method to order the edges for any arbitrary model (currently only for FAs and event-based requirements (needs)). But I won't be able to make automatically in the month I have left for my project. As you said, it should be possible to do it automatically. But I was saving this ordering method for another issue because I am not entirely happy with the current version.
[...]
Did you already implement your proposed change, or how did you conclude this?
Right now, I did it all by my hand (500+ events) with the same logical deduction as explained but without the same event multiple times in a single loop.
From #426 (comment 1054097):
[...] I asked my supervisor this morning and unfortunately, I am not allowed to share the entire thesis with you or anyone else. Even publishing chapter 6 on its own is not desired. Which means I have to write a separate document describing the method once I have the time for it. Writing the separate document is definitely not happening before February.