Groups
Conversations
All groups and messages
Send feedback to Google
Help
Training
Sign in
Groups
PRISM model checker
Conversations
About
Problem with multiple conjunction (operator &)
6 views
Skip to first unread message
gab.la...@gmail.com
unread,
Jul 9, 2015, 4:56:22 AM
7/9/15
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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 AM
7/9/15
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Sign in to report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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