A modern probabilistic model checker
We use a Docker container based on Jupyter Notebook throughout this presentation.
docker run -it -p 8080:8080 --name stormpyter movesrwth/stormpyter:discotec2020
127.0.0.1:8080/... 4. Open file discotec_storm.ipynb 5. The presentation should start automatically
!storm
You should see the Storm version information.
You can even change the code! Try adding the flag --version
.
No fully distributed and symmetric deterministic algorithm is possible (Lehmann, Rabin 1981)
➜ Use randomized algorithm
Algorithm by Lehmann and Rabin (POPL'81)
s=0 -> (s'=0); //stay thinking
s=0 -> (s'=1); //trying
// draw randomly
s=1 -> 0.5 : (s'=2) + 0.5 : (s'=3);
s=2 & lfree -> (s'=4); //pick up left
s=2 & !lfree -> (s'=2); //left not free
...
// Finished eating
s=9 -> (s'=10); //put down left
s=10 -> (s'=0); //go back to thinking
Source: Prism Website
Prism file specifying algorithm for 3 processes todo: add picture with prism code
Source: Prism Website
Read prism file for 3 philosophers with Storm:
!storm --prism examples/phil3.nm --buildfull
"Probability that no philosopher is ever hungry"
!storm --prism examples/phil3.pm --prop 'P=? [G !"hungry"]' |tail -n+12
"Percentage of time spent eating"
!storm --prism examples/phil3.pm --prop 'S=? ["eat"]' |tail -4
Liveness: "If a philosopher is hungry then eventually some philosopher eats"
!storm --prism examples/phil3.pm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -4
"(Minimal/Maximal) Probability that no philosopher is ever hungry"
!storm --prism examples/phil3.nm --prop 'Pmin=? [G !"hungry"];Pmax=? [G !"hungry"]' |tail -n+12
Liveness: "If a philosopher is hungry then eventually some philosopher eats"
!storm --prism examples/phil3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -3
Problem: unfair schedulers avoid scheduling hungry philosophers
Solution: use adapted algorithm without fairness assumptions (Duflot, Fribourg, Picaronny, 2004)
!storm --prism examples/phil-nofair3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -3
Consider (wrong) deterministic algorithm where always left fork is picked first.
Before: s=1 -> 0.5 : (s'=2) + 0.5 : (s'=3);
After: s=1 -> 1 : (s'=2);
!storm --prism examples/phil-nofair-det3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -3
"Probability that a hungry philosopher eats within 10 steps"
!storm --prism examples/phil-nofair3.nm --prop 'filter(min, Pmin=? [F<=10 "eat"], "hungry");filter(avg, Pmin=? [F<=10 "eat"], "hungry")' |tail -7
"Expected number of steps (in the worst-case) that a hungry philosopher needs to take before eating"
!storm --prism examples/phil-nofair3.nm --prop 'filter(max, Rmax=? [F "eat"], "hungry")' |tail -3
!storm --jani examples/phil-nofair3.jani -jprop |tail -7
!storm --prism examples/phil-nofair3.nm --prop 'filter(max, Rmax=? [F "eat"], "hungry")' |tail -2
!storm --prism examples/phil-nofair3.nm --prop 'filter(max, Rmax=? [F "eat"], "hungry")' --exact |tail -2
Storm supports different model representations:
!storm --engine sparse --prism examples/phil-nofair5.nm --prop 'Pmax=? [F no_eat>1]' |tail -n+7
!storm --engine dd --prism examples/phil-nofair5.nm --prop 'Pmax=? [F no_eat>1]' --ddlib cudd |tail -n+7
!storm --bisimulation --prism examples/phil-nofair3.nm --prop 'filter(forall, P>=1 [F "eat"], "hungry")' |tail -n+7
Stormpy: Python bindings for Storm
➜ Easy and rapid prototyping for probabilistic model checking