Finding states that have only one self-loop

[Ali A. Noroozi]

Hi all,

Given a dtmc model, which is an instance of the ProbModel class, how can I find states with only one self-loop?

I know I can find states with no transition using:

JDD.Ref(trans01);
deadlocks = JDD.ThereExists(trans01, allDDColVars);
JDD.Ref(reach);
deadlocks = JDD.And(reach, JDD.Not(deadlocks));

I need to write such a code for finding those states that have only one self-loop.

[Ali A. Noroozi]

Is there anybody to help me with this?

[Joachim Klein]

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.

[Ali A. Noroozi]

Hi Joachim,

Yes, this is exactly what I was looking for. Thank you.

> an email to prismmodelchecker-dev+unsub...@googlegroups.com
> <mailto:prismmodelchecker-dev+unsub...@googlegroups.com>.