Skip to content

The GUI

Jump to bottom
Josh Jeppson edited this page May 24, 2022 · 6 revisions

Introduction

This wiki page will give you an introduction to using xstamina, the STAMINA GUI. The STAMINA GUI is compatible with both STAMINA/STORM and STAMINA/PRISM, although both must be installed. The name xstamina comes from the fact that on most *nix systems, the dominant windowing system is Xorg. Please note that XStamina runs on any windowing system as it uses Qt/PyQt5, whether that windowing system be Xorg, Wayland, etc. It has not been tested on Windows.

Quick Tip

Even if you have already compiled STAMINA (both STAMINA/STORM and STAMINA/PRISM), you may have to add them to your PATH variable in order to use XStamina.

Pre-requisites

You will need python3 and PyQt5. PyQt5 is best installed via pip using python3 -m pip pyqt5. If you would like xstamina to be installed, please run the following commands to move XStamina to your local bin folder:

sudo cp xstamina.py /usr/local/bin/xstamina
sudo cp MoreOptions.py /usr/local/bin

This can be uninstalled using:

sudo rm /usr/local/bin/xstamina
sudo rm /usr/local/bin/MoreOptions.py

Usage

The main GUI

image

  1. Model/Modules file. The file which contains the modules which in their entirety, describe the PRISM model.
  2. Properties file: The file with the list of CSL properties to use
  3. Undefined constants: PRISM allows you to specify constants at runtime, and therefore STAMINA/JAVA does as well
  4. The file to export the output of STAMINA to.
  5. The choice of whether to use STAMINA/STORM or STAMINA/PRISM
  6. The output window where STAMINA will dump log and results.
  7. Opens the "More Options" window
  8. Analyzes the model

The "More Options" Dialog

image

  1. Reduction factor (κ)
  2. Kappa reduction factor (rκ)
  3. Approximation factor
  4. Required maximal probability window for STAMINA to terminate
  5. The maximum number of refinement iterations
  6. Will there be property refinement?
  7. Export the modified model file with the Absorbing module (generally used for debugging and proof)
  8. Export the modified CSL properties (generally used for debugging and proof)
  9. Use rank transitions 10-14. Method to use
  10. Set defaults
  11. Finish (checks validity of options)

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