Advanced Examples

This guide is a collection of examples meant to bridge the gap between the getting started guide and the API.

Contents:

• Analysis
  • Background
  • Qualitative Analysis
  • Adapting the model checking engine
  • Adapting model checking algorithms
• Building Models
  • Background
  • Building different formalisms
• Discrete-time Markov chains (DTMCs)
  • Background
  • Transition Matrix
  • Labeling
  • Reward Models
  • Building the Model
• Markov decision processes (MDPs)
  • Background
  • Transition Matrix
  • Labeling
  • Reward models
  • Building the Model
  • Partially observable Markov decision process (POMDPs)
• Continuous-time Markov chains (CTMCs)
  • Background
  • Transition Matrix
  • Labeling
  • Building the Model
• Markov automata (MAs)
  • Background
  • Transition Matrix
  • Markovian States
  • Building the Model
• Engines
  • Background
  • Sparse engine
  • Symbolic engine
  • Hybrid engine
• Exploring Models
  • Background
  • Reading MDPs
  • Reading POMDPs
  • Sorting states
  • Reading MAs
• Working with Simulators
  • Model-based simulation
  • Program-level simulator
• Reward Models
  • Exploring reward models
• Working with Schedulers
  • Examining Schedulers for MDPs
  • Examining Schedulers for Markov automata
• Working with Shortest Paths
  • Background
  • Examining Shortest Paths
• Parametric Models
  • Instantiating parametric models
  • Checking parametric models
  • Collecting information about the parametric models
• Dynamic Fault Trees
  • Building DFTs
  • Analyzing DFTs
• Generalized Stochastic Petri Nets
  • Loading GSPNs
  • Building GSPNs