Skip to content

Using STAMINA

Jump to bottom
Josh Jeppson edited this page May 24, 2022 · 1 revision

Required input

STAMINA/C++ supports models written in the PRISM modeling language, and will in the future probably support other languages like JANI. There are two files you need to pass into STAMINA:

  • Module/Model File: The file which contains the description of your PRISM model. Currently, STAMINA only supports models of type ctmc
  • CSL Properties File: The file which contains the properties you want to be checked.

The usage for STAMINA is as follows:

stamina [MODEL FILE] [PROPERTIES FILE] <Options>

Options

Within the <Options> you can specify the following relevant options:

  • κ (The probability reachability threshold)
  • rκ (The reduction factor for κ)

The STAMINA software and state-truncation algorithm are developed at Utah State University within Dr. Zhen Zhang's research group. STAMINA/C++ is primarily developed by Joshua Jeppson, BS.

This wiki is outdated! Please visit https://staminachecker.org/documentation/wiki/ for full up-to-date wiki.

Clone this wiki locally