Finding states that have only one self-loop

Skip to first unread message

Ali A. Noroozi

Jan 30, 2019, 8:43:38 AM1/30/19
to PRISM model checker developers
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:
deadlocks = JDD.ThereExists(trans01, allDDColVars);
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

Feb 26, 2019, 7:59:42 AM2/26/19
to PRISM model checker developers
Is there anybody to help me with this?

Joachim Klein

Feb 26, 2019, 8:16:49 AM2/26/19
to Ali A. Noroozi, PRISM model checker developers
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(),

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,

I didn't test this code, so there might be small typos, but the
principle should be clear :)

> --
> 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
> <>.
> To post to this group, send email to
> <>.
> Visit this group at

Ali A. Noroozi

Feb 26, 2019, 9:23:47 AM2/26/19
to PRISM model checker developers
Hi Joachim,

Yes, this is exactly what I was looking for. Thank you.
Reply all
Reply to author
0 new messages