#!/usr/bin/env python
# coding: utf-8

# <center>
#     <h1>Part 2: Introduction to Storm</h1>
#     <h2>Matthias Volk</h2>
#     <br>
#     <br>
# <img src="attachment:storm_logo.png" width="500px"/></center>
# 
# **<center>[www.stormchecker.org](https://www.stormchecker.org)</center>**
# 
# <div align="right">Press <em>spacebar</em> to navigate</div>

# ## Storm
# A modern probabilistic model checker
# - **State-of-the-art**: best performance at [QComp 2020](http://qcomp.org/competition/2020/index.html)
# - **Modular**: dedicated solvers for each task, interchange libraries
# - Written in **C++**, **Python interface** via [stormpy](https://moves-rwth.github.io/stormpy/)
# - **Open-source**, developed since 2012, over 170,000 lines of code
# 
# ### Getting Storm
# - Native support for *Linux* and *macOS* (homebrew formula)
# - Virtual machine and Docker containers (also for *Windows*)

# ## Getting Storm for this presentation
# We use a [Docker container](https://www.docker.com/) based on [Jupyter Notebook](https://jupyter.org/) throughout this presentation.
# #### Installation steps:
# 1. Install [Docker](https://docs.docker.com/get-docker/) for your OS
# 2. Download (>1 GB) and start the container:
# ```bash
# docker run -it -p 8080:8080 --name stormpyter movesrwth/stormpyter:discotec2020
# ```
# 3. Open the Jupyter website indicated in the command line:
# [127.0.0.1:8080/...](http://127.0.0.1:8080)
# 4. Open file **discotec_storm.ipynb**
# 5. The presentation should start automatically

# ## Hands-on presentation
# 
# - This is an interactive presentation. You can **execute all commands by yourself**!
# - Navigate with *spacebar* and *shift+spacebar*
# - All interactive commands can be executed with *shift+enter*
# - Switch between presentation and notebook with *alt+r*
# 
# 

# ### Example

# In[ ]:


get_ipython().system('storm')


# You should see the Storm version information.
# 
# You can even **change the code**! Try adding the flag `--version`.

# ## Dining philosophers

# <center>
#     <img src="attachment:dining_philosophers.png" width="500px"/>
# <div style="font-size:10px">Source: <a href="https://en.wikipedia.org/wiki/File:An_illustration_of_the_dining_philosophers_problem.png">Benjamin D. Esham / Wikimedia Commons</a></div>
# </center>

# - Formulated in 1965 by Edsger Dijkstra
# - Philosophers become hungry from thinking
# - Every *hungry* philosophers wants to *eat*
# - Before eating, pick up *left* and *right fork*

# ## Dining philosophers
# 
# #### Problem
# No fully distributed and symmetric *deterministic* algorithm is possible (Lehmann, Rabin 1981)
#   - Deadlock if all philosophers first pick up left fork
# 
# 
# #### Solution
# &#10140; Use *randomized* algorithm
# 
# Algorithm by Lehmann and Rabin (POPL'81)
#   - Random choice whether first picking left or right fork
# 
# 

# ## Randomized dining philosophers (Lehmann, Rabin)

# 
# 1. thinking
# 2. hungry:
#     1. flip coin to choose first fork  
#     2. try to pick up first fork
#     3. if successful continue, else keep trying
#     4. try to pick up second fork
#     5. if successful continue, otherwise put down first fork and think again
# 3. eating
# 4. put down left and right fork and think again

# ```
# 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]("https://www.prismmodelchecker.org/casestudies/phil.php")

# ## Prism file for randomized dining philosophers
# Prism file specifying algorithm for 3 processes
# todo: add picture with prism code
#     
# 
# Source: [Prism Website](https://www.prismmodelchecker.org/casestudies/phil.php)

# ## Building model with Storm
# 
# Read prism file for 3 philosophers with Storm:

# In[ ]:


get_ipython().system('storm --prism examples/phil3.nm --buildfull')


# ## Model checking

# <img src="attachment:model_checking_overview.png" width="90%"/>

# - Model: randomized dining philosophers
# - Properties:
#     - Starvation freedom
#     - Mutual exclusion for forks
#     - Average waiting time
#     - ...

# ## Model checking DTMC
# - Assume scheduling of processes follows uniform distribution  
#   &#10140; Yields discrete-time Markov chain (DTMC)

# "*Probability that no philosopher is ever hungry*"

# In[ ]:


get_ipython().system('storm --prism examples/phil3.pm --prop \'P=? [G !"hungry"]\'  |tail -n+12')


# ## Model checking DTMC
# "*Percentage of time spent eating*"

# In[ ]:


get_ipython().system('storm --prism examples/phil3.pm --prop \'S=? ["eat"]\' |tail -4')


# ## Model checking DTMC
# Liveness: "*If a philosopher is hungry then eventually some philosopher eats"*

# In[ ]:


get_ipython().system('storm --prism examples/phil3.pm --prop \'filter(forall, P>=1 [F "eat"], "hungry")\' |tail -4')


# ## Model checking MDP
# - Allow arbitrary scheduling of processes now  
#   &#10140; Yields Markov decision process (MDP) containing non-determinism

# "*(Minimal/Maximal) Probability that no philosopher is ever hungry*"

# In[ ]:


get_ipython().system('storm --prism examples/phil3.nm --prop \'Pmin=? [G !"hungry"];Pmax=? [G !"hungry"]\' |tail -n+12')


# ## Model checking MDP
# Liveness: "*If a philosopher is hungry then eventually some philosopher eats"*

# In[ ]:


get_ipython().system('storm --prism examples/phil3.nm --prop \'filter(forall, P>=1 [F "eat"], "hungry")\' |tail -3')


# ## Model checking MDP
# **Problem**: unfair schedulers avoid scheduling hungry philosophers  
# **Solution**: use adapted algorithm without fairness assumptions (Duflot, Fribourg, Picaronny, 2004)

# In[ ]:


get_ipython().system('storm --prism examples/phil-nofair3.nm --prop \'filter(forall, P>=1 [F "eat"], "hungry")\' |tail -3')


# ## Model checking deterministic algorithm
# 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);`

# In[ ]:


get_ipython().system('storm --prism examples/phil-nofair-det3.nm --prop \'filter(forall, P>=1 [F "eat"], "hungry")\' |tail -3')


# ## Computing waiting times for philosophers
# "*Probability that a hungry philosopher eats within 10 steps*"

# In[ ]:


get_ipython().system('storm --prism examples/phil-nofair3.nm --prop \'filter(min, Pmin=? [F<=10 "eat"], "hungry");filter(avg, Pmin=? [F<=10 "eat"], "hungry")\' |tail -7')


# ## Computing waiting times for philosophers
# "*Expected number of steps (in the worst-case) that a hungry philosopher needs to take before eating*"

# In[ ]:


get_ipython().system('storm --prism examples/phil-nofair3.nm --prop \'filter(max, Rmax=? [F "eat"], "hungry")\' |tail -3')


# ## Modularity of Storm
# 
# <center>
#     <img src="attachment:storm_architecture.png" width="60%"/>
# </center>
# 
# - Use different input formats  
# - Modularity allows to use different solvers and libraries

# ## Input formats
# - Storm supports a variety of input formats:
#     - [Prism language](https://www.prismmodelchecker.org/manual/ThePRISMLanguage/Introduction)
#     - [Jani modelling language](http://www.jani-spec.org/)
#     - Explicit format
#     - Generalized stochastic Petri nets

# In[ ]:


get_ipython().system('storm --jani examples/phil-nofair3.jani -jprop |tail -7')


# ## Computing exact values
# - Floating point arithmetic and convergence criteria might not be precise  
#   &#10140; use exact (rational) numbers and sound algorithms off-the-shelf
# - Drawback: performance might decrease

# In[ ]:


get_ipython().system('storm --prism examples/phil-nofair3.nm --prop \'filter(max, Rmax=? [F "eat"], "hungry")\' |tail -2')


# In[ ]:


get_ipython().system('storm --prism examples/phil-nofair3.nm --prop \'filter(max, Rmax=? [F "eat"], "hungry")\' --exact |tail -2')


# ## Engines in Storm
# Storm supports different model representations:
# - **Sparse matrix**:
#     - Model building is time and memory intensive
#     - Fast numerical computations
# - **Binary Decision Diagrams (BDD)**:
#     - Fast and memory efficient model building if model is structured
#     - Slower numerical computations
# - **Hybrid** approach:
#     - Build with BDD, use sparse matrix for numerical computations
# - ...

# ## Engines in Storm

# In[ ]:


get_ipython().system("storm --engine sparse --prism examples/phil-nofair5.nm --prop 'Pmax=? [F no_eat>1]' |tail -n+7")


# In[ ]:


get_ipython().system("storm --engine dd --prism examples/phil-nofair5.nm --prop 'Pmax=? [F no_eat>1]' --ddlib cudd |tail -n+7")


# ## Bisimulation minimization
# - Reduces state-space size without loosing information
# - Exploits symmetries

# In[ ]:


get_ipython().system('storm --bisimulation --prism examples/phil-nofair3.nm --prop \'filter(forall, P>=1 [F "eat"], "hungry")\' |tail -n+7')


# ## Summary
# - Basic introduction to **Storm command-line interface**
# - Correctness of **dining philosophers** algorithm
# - Storm supports broad range of **models and properties**
# - Different **engines** allow tailored analysis per model and property
# 
# ### Next:
# **Stormpy**: Python bindings for Storm  
# &#10140; Easy and rapid prototyping for probabilistic model checking

# In[ ]: