"Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe" - Supporting Material

Paper: "Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe"
Hubert Garavel, Holger Hermanns and David Parker

Models, properties and scripts

We include here the files and scripts to analyse the mainframe model in PRISM and Storm.

The model is also now included in the PRISM Benchmark Suite.

See this page for the equivalent files for analysis with CADP.

• PRISM model: erlangen.prism
• Properties: erlangen.props
  
  
• PRISM model (syntactically reduced): erlangen-merged.prism
  
  
• Script (figures): expt-plots.sh
• Script (comparison): expt-prism-vs-storm.sh
• Script (Table 3): expt-bisim.sh