RE: Filter Property Specification

[Geeta Mahala]

Hello Dave,

I would like to extend my research work using PRISM. But I have some doubts regarding filter option to specify properties.

When I run filter(min, Pmin=? [ F<=16 pollution<=100 ], pollution>=200) , I am getting result=0.0. ( Output is mentioned below :-).

Model checking: filter(min, Pmin=? [ F<=16 pollution<=100 ], pollution>=200)

Building model...

Computing reachable states...

Reachability (BFS): 24 iterations in 0.25 seconds (average 0.010417, setup 0.00)

Time for model construction: 1.502 seconds.

Type:        MDP

States:      14125 (1 initial)

Transitions: 29790

Choices:     14125

Transition matrix: 77320 nodes (35 terminal), 29790 minterms, vars: 23r/23c/1nd

Prob0E: 1 iterations in 0.01 seconds (average 0.005000, setup 0.00)

yes = 670, no = 13455, maybe = 0

States satisfying filter pollution>=200: 8853

Minimum value over states satisfying filter: 0.0

There are 8853 states with (approximately) this value.

The first 10 states are displayed below. To view them all, enable verbose mode or use a print filter.

136:(0,370,205)

205:(0,409,215)

216:(0,413,214)

261:(0,433,201)

265:(0,434,218)

272:(0,436,218)

282:(0,440,208)

288:(0,442,205)

291:(0,443,225)

300:(0,446,204)

Time for model checking: 0.022 seconds.

Result: 0.0 (minimum value over states satisfying filter)

Q1. My question is  Even for filter(max, Pmin=? [ F<=16 pollution<=100 ], pollution>=200)  and filter(range, Pmin=? [ F<=16 pollution<=100 ], pollution>=200) are 0.0. But If I run   filter(print, Pmin=? [ F<=16 pollution<=100 ], pollution>=200) then result is 1.0 ( Output is mentioned below) why?

Model checking: filter(print, Pmin=? [ F<=16 pollution<=100 ], pollution>=200)

Building model...

Computing reachable states...

Reachability (BFS): 24 iterations in 0.25 seconds (average 0.010417, setup 0.00)

Time for model construction: 1.486 seconds.

Type:        MDP

States:      14125 (1 initial)

Transitions: 29790

Choices:     14125

Transition matrix: 77320 nodes (35 terminal), 29790 minterms, vars: 23r/23c/1nd

Prob0E: 1 iterations in 0.01 seconds (average 0.005000, setup 0.00)

yes = 670, no = 13455, maybe = 0

States satisfying filter pollution>=200: 8853

Results (non-zero only) for filter pollution>=200:

(all zero)

Value in the initial state: 1.0

Time for model checking: 0.015 seconds.

Result: 1.0 (value in the initial state)

Q2.  What does mean by yes = 670, no = 13455, maybe = 0.

Thank you so much.

[Gethin Norman]

Geeta,

for Q1 in the output for the filter it states

> Results (non-zero only) for filter pollution>=200:
> (all zero)

So this is consistent all the filters are returning 0 for all the states satisfying “pollution>=200” in the output it also states:

> Result: 1.0 (value in the initial state)

this should probably not be printed to avoid confusion, but as it states this is the normal model checking result for the initial state in which “pollution>=200” does not hold.

Q2.

yes are the number of states that satisfy the formula with probability 1
no are the number of states that satisfy the formula with probability 0
maybe are the number of states that satisfy the formula with a probability p where 0<p<1

The notation comes from the model checking algorithms that use the notation S^yes, S^no and S^maybe for these sets of states that can be found by graph-based algorithms

thanks

Gethin

> --
> 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.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker-dev/7dc4b20f-46db-4f35-9e81-bf0980753842n%40googlegroups.com.

[Geeta Mahala]

Hello Gethin,

Thank you so much for reply.

I have some more questions :

1. Can we generate counter example for mdp in current version of PRISM.

2. If we use prism source code then we can generate mdp.dot file and can visualize the model. Is it possible to visualize using the graph same as we can see complete mdp model if a property is satisfied or not satisfied ?

3. Is it true that we can not generate adv.tra for bounded property in PRISM.