progirep
commented
6 years ago If you extract a symbolic strategy, then the output is a file describing a BDD in the format used by the "dddmp" extension of the CUDD Binary Decision Diagram Library. CUDD supports constant-time complementation -- a negative root ID thus represents that the BDD asked for is the complement of the one described in the file. Note that CUDD features complemented "else"-edges. Thus, complementation can happen multiple times along a path from the root to the sinks. You shouldn't need to worry about this if you use the dddmp extension of CUDD to read the BDD from a file.
As far as your second question is concerned: There are two different symbolic strategy computation modes. The "--symbolicStrategy" parameter enables the standard mode. In it, two sets of extra variables in addition to the standard input/output variables are used:
- The "jx..." variables -- these encode the number of the liveness goal that the controller is currently trying to reach.
- The "strat_type" variable that encodes whether along a transition, a goal has been reached or not.
If you execute a strategy generated with this mode, you need to iterate through all system goals in your strategy executor. If you use the "--simpleSymbolicStrategy" option, you will get a post-copy of the "jx..." variables as well. Furthermore, the "strat_type" bit will disappear, so the strategy is easier to execute.
Dear tool maintainer,
I've been trying to use your tool in my work. However, I'm a little confused about how to interpret the output of slugs.
For a very simple example
[OUTPUT] g [SYS_TRANS] g->!g' !g->g'
When I used --symbolicStrategy parameter I get the following dddmp dump file
.ver DDDMP-2.0 .mode A .varinfo 0 .nnodes 5 .nvars 4 .nsuppvars 3 .suppvarnames g g' _jx_b0 .orderedvarnames g g' _jx_b0 strat_type .ids 0 1 2 .permids 0 1 2 .auxids 0 1 2 .nroots 1 .rootids -5 .nodes 1 T 1 0 0 2 2 2 1 -1 3 1 1 1 2 4 1 1 2 1 5 0 0 3 4 .end
My question is