Stormvogel Documentation

Stormvogel provides easy and user-friendly APIs for creating, visualizing, and debugging probabilistic Markov models.

Get started here!

Getting Started

• Welcome to Stormvogel!

Source Code Repository and Issue Tracker:

GitHub Repository

PyPI Package:

PyPI Package

Documentation Index:

Model Construction

• Building DTMCs
  • The Knuth die
  • Simple communication
• Building MDPs
  • The study dilemma
  • Grid model
• Building CTMCs
• Building POMDPs
• Parametric models
• Stormpy Conversion
• Parallel composition
  • m1
  • m2
  • Quotient model
• Parametric models

Visualization

• Model visualization
  • Basic editing
  • Advanced editing
  • Javascript injection
• Generating GIFs

Model Analysis

• Model checking (using Storm)
• Visual value iteration and Markov Chain evolution
  • Value iteration
  • DTMC evolution
• Policy iteration
• Simulator

Reinforcement Learning

• Gymnasium integration
  • FrozenLake
  • CliffWalking
  • Taxi
• Gymnasium sampling
  • FrozenLake
  • Blackjack
  • Acrobot

Tools and Utilities

• Debugging models
  • Showing Maximal End Components
  • Showing Prob01 sets
• End component elimination
• Implementation details
  • Communication server remark
• Visualization
  • Note on debugging
  • Python
  • Javascript/HTML
• API Reference
  • stormvogel

Version info:

Last update: Jul 21, 2025.

Current version: 0.9.2.

Search for a specific page:

• Index

• Module Index

• Search Page