Finding states that have only one self-loop

16 views
Skip to first unread message

Ali A. Noroozi

unread,
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:
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

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

Joachim Klein

unread,
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(),
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

unread,
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
Forward
0 new messages