CounterExamples/Witnessess in PRISM

[sobi khan]

Hi,

I am trying to verify the properties like A [G "inv"]  and the result is not true also  E [F "goal"] for which the result is true. 

As It is mentioned in one section of the Manual that PRISM generates counter examples/witness to path which is displayed in the simulator tab (as can be seen in the attached snapshot). But I did not find any such option in my case. I am using PRISM 4.7, can anyone please guide me  exactly where  can I find the counter example or the witness ?

[Dave Parker]

Hi Sobia,

For A[G] and E[F], this should work, either from the command line or
GUI. For example, from the command line this:

bin/prism ../prism-examples/simple/dice/dice.pm -pf 'E[F d=6]'

finally displays this:

Counterexample/witness:
(0,0)
(2,0)
(6,0)
(7,6)

If you verify the same property in the usual way (right click +
"Verify") from the GUI, you are prompted whether you want to see the
resulting path loaded into the simulator.

Best wishes,

Dave

[sobi khan]

Hi Dave,

Many thanks for your response.

When I try to verify the same property you mentioned for dice.pm example using the GUI. 

I get the error path loading failed at step2 as can be seen in the attached snapshot.

I also tried to verify various other examples and I get similar errors as error path loading failed at step 4 etc.

Please guide me on what could be the possible reason for this error?

I get the same error in both PRISM4.6 and 4.7.

Thanks

[Dave Parker]

Thanks. I can reproduce this behaviour. It was a bug, for which I have
now pushed a fix to our main code repo on github:

https://github.com/prismmodelchecker/prism/

That version should resolve the issue (but you will need to compile
PRISM from source, if you were not already). Alternatively, the
command-line version of counterexample generation from my previous email
should work in any of these releases.

Best wishes,

Dave

> bin/prism ../prism-examples/simple/dice/dice.pm <http://dice.pm> -pf

> 'E[F d=6]'
>
> finally displays this:
>
> Counterexample/witness:
> (0,0)
> (2,0)
> (6,0)
> (7,6)
>
> If you verify the same property in the usual way (right click +
> "Verify") from the GUI, you are prompted whether you want to see the
> resulting path loaded into the simulator.
>
> 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 view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/c542db2e-333c-4ecf-b41d-c3678ccf9a4bn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/c542db2e-333c-4ecf-b41d-c3678ccf9a4bn%40googlegroups.com?utm_medium=email&utm_source=footer>.

[sobi khan]

Hi Dave,

 I am trying to verify the two different properties using the PRISM 4.7, terminal. The resulting logs are attached as a .txt file below.

In one case property holds and the PRISM generated a witness path as can be seen in the file(witness.txt), while in the other case the property is false but it does not generate any counterexample(No witness.txt). 

Can you please guide me on what could be the reason for this?

Thanks

[Dave Parker]

Hi Sobia,

There are two reasons for this.

Firstly, we only show either a witness if E[F"target"] is true, or a
counterexample if A[G"stay"] is false. In your case, the result of
E[F"target"] is false, so there is no witnessing path that can be
generated to show this.

Secondly, even if there was such a path, we have not yet added
counterexample generation for LTL formulas, just the simpler
reachability properties used in your first case.

Hope that helps,

Dave

> <http://dice.pm> example

> <http://dice.pm <http://dice.pm>> -pf

> > 'E[F d=6]'
> >
> > finally displays this:
> >
> > Counterexample/witness:
> > (0,0)
> > (2,0)
> > (6,0)
> > (7,6)
> >
> > If you verify the same property in the usual way (right click +
> > "Verify") from the GUI, you are prompted whether you want to see the
> > resulting path loaded into the simulator.
> >
> > 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 view this discussion on the web, visit
> >
> https://groups.google.com/d/msgid/prismmodelchecker/c542db2e-333c-4ecf-b41d-c3678ccf9a4bn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/c542db2e-333c-4ecf-b41d-c3678ccf9a4bn%40googlegroups.com>
>
> >

> <https://groups.google.com/d/msgid/prismmodelchecker/c542db2e-333c-4ecf-b41d-c3678ccf9a4bn%40googlegroups.com?utm_medium=email&utm_source=footer
> <https://groups.google.com/d/msgid/prismmodelchecker/c542db2e-333c-4ecf-b41d-c3678ccf9a4bn%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
>
> --
> 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 view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/10d92a76-4570-4a12-b662-05e50a6955c7n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/10d92a76-4570-4a12-b662-05e50a6955c7n%40googlegroups.com?utm_medium=email&utm_source=footer>.