Welcome to the SMC Storm documentation!

smc_storm is a statistical model checker for discrete time Markov chains (DTMCs) and Markov decision processes (MDPs). As the name suggests, it builds up on STORM, and supports both probability and reward properties.

Contents

• Installation Guide
  • How to install smc_storm
  • Verify the installation works
• Tutorials
  • How to use smc_storm
• API
  • Class Hierarchy
  • File Hierarchy
  • Full API