Documentation for BDDs used in NondetModel and ProbModel

[Ramneet Singh]

I am trying to understand how the symbolic engine handles MDPs. I found the various BDDs and BDDVars used in NondetModel and ProbModel (which is a parent) to be a bit confusing. In particular, NondetModel has the following members:

```
protected JDDNode nondetMask; // mask for nondeterministic choices
protected JDDVars allDDSynchVars; // synch actions dd vars
protected JDDVars allDDSchedVars; // scheduler dd vars
protected JDDVars allDDChoiceVars; // local nondet choice dd vars
protected JDDVars allDDNondetVars; // all nondet dd vars (union of two above)
protected JDDNode transInd; // BDD for independent part of trans
protected JDDNode transSynch[]; // BDD for parts of trans from each action
protected JDDNode transReln; // BDD for the transition relation (no action encoding)
```

What is the difference between synch actions, scheduler choices, and local choices? Also, I assume these variables are the ones created to encode synch actions, scheduler choices and local choices, respectively (is it like an n-var encoding for 2^n choices or something different?)?

Also, which variables are transInd, each of the transSynch and the transReln BDDs over? Are they binary-valued or real-valued?

I have similar questions for the dd members in ProbModel:

```
protected JDDNode trans; // transition matrix dd
protected JDDNode trans01; // 0-1 transition matrix dd
protected JDDNode start; // start state dd
protected JDDNode reach; // reachable states dd
protected JDDNode deadlocks; // deadlock states dd (may have been fixed)
protected JDDNode stateRewards[]; // state rewards dds
protected JDDNode transRewards[]; // transition rewards dds
protected JDDNode transActions; // dd for transition action labels (MDPs)
protected JDDNode transPerAction[]; // dds for transition action labels (D/CTMCs)
```

Sorry about the long-winded and perhaps naive question, but where can I find more information about what exactly all these DDs mean so I can better understand how they are used in the algorithms?

Thanks for your help.
Best,

Ramneet