Hi Ali,
so, you want to obtain the set of states that only have transitions back
to themselves, and none to other states?
You can use JDD.Identity(rowVars,colVars) to obtain a BDD for the
transitions that are to the same state. The following should do the trick:
JDDNode selfloopTrans01 = JDD.And(trans01.copy(),
JDD.Identity(allDDRowVars, allDDColVars));
// states with self-loops
JDDNode selfloopStates = JDD.ThereExists(selfloopTrans01.copy(),
allDDColVars);
JDDNode outgoingTrans01 = JDD.And(trans01.copy(), JDD.Not(selfLoopTrans01));
// states with outgoing transitions to other states
JDDNode outgoingStates = JDD.ThereExists(outgoingTrans01, allDDColVars);
JDDNode onlySelfloopStates = JDD.And(selfloopStates,
JDD.Not(outgoingStates));
I didn't test this code, so there might be small typos, but the
principle should be clear :)
Cheers,
Joachim
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to
prismmodelchecke...@googlegroups.com
> <mailto:
prismmodelchecke...@googlegroups.com>.
> To post to this group, send email to
>
prismmodel...@googlegroups.com
> <mailto:
prismmodel...@googlegroups.com>.
> Visit this group at
https://groups.google.com/group/prismmodelchecker-dev.