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.