Question regarding the format of the slug output

[bbiiggppiigg]

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

1. How should I interpret this output ? What does it mean to have a negative rootid ?
2. Why don't we need a primed version of the variable _jx_b0 and strat_type ?

[progirep]

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.