Problem with multiple conjunction (operator &)

6 views
Skip to first unread message

gab.la...@gmail.com

unread,
Jul 9, 2015, 4:56:22 AM7/9/15
to prismmod...@googlegroups.com
Hello everybody!
I'm new in this forum and I just started to use PRISM. 
I defined a model and I was trying to check some properties on it by using CTL semantics.
I realized that the model checker returns me "false" when I try to check a property defined as a triple conjunction as follows:

!P<=0[G ("phi0") & (!P<=0[X "chi1"]) & (!P<=0[X(!P<=0[X "phi1"])])]

I tried with other properties and every time I use the logic operator "&" two times, it doesn't return me true even though it should.
Do you know if this is a kind of limitation of PRISM or I'm using the syntax in a wrong way?

Thanks a lot!

Dave Parker

unread,
Jul 9, 2015, 7:08:41 AM7/9/15
to prismmod...@googlegroups.com, gab.la...@gmail.com
Hi,

I don't see any problem with the "&"s.

However, while this equivalence is true:

E[X "phi"] === !P<=0[X "phi"]

this is one is *not*:

E[G "phi"] === !P<=0[G "phi"]

This is because you can have a single path satisfying G "phi", but which
has probability 0.

PRISM has partial support for CTL, for example it does E[G], but not
E[X]. So try:

E[G ("phi0") & (!P<=0[X "chi1"]) & (!P<=0[X(!P<=0[X "phi1"])])]

instead of

!P<=0[G ("phi0") & (!P<=0[X "chi1"]) & (!P<=0[X(!P<=0[X "phi1"])])]

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.
Reply all
Reply to author
Forward
0 new messages