Counterexample generation

[Jingyi Wang]

Hello,

I'm trying to do some counterexample analysis for DTMCs and PRISM is the first choice of course. Does PRISM support it now? Say given a specification and a PCTL safety property, output the counterexample ([as Han, Katoen, 2007]) if the property is not satisfied. If not, is there a decent tool for doing this to your knowledge?

Thanks for the help.

Best regards,

Jingyi

[Dave Parker]

Hi Jingyi,

We have an implementation of this that is currently being integrated
into the main version. For now, it's available as a separate version.
Contact me off-list and I'll send you details.

Best wishes,

Dave.

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Anastasia Mavridou]

Hello,

Is this available currently in the main version? If not, can I also get details about the separate version?

Thank you,

Anastasia