Run STAMINA/STORM on the cloud

Looking for a job you already started? Try this page.

Upload your own... Use a preset...
Create job Web user
No File Selected...
Learn how to write a model file
No File Selected...
Learn about the types of properties STAMINA can check
Presets coming soon! For now, you can download our case study files from here.

The reachability threshold, also called κ, is the threshold by which states are either fully included in the model, or truncated (their successors ignored and an artificial transition sent to an absorbing state). Read more...
Between iterations of truncation, κ is reduced to allow for more states to be explored if the results are not accurate enough. The next κ is calculated as κ / rκ. Read more...
The accuracy bound, w is defined as Pmax - Pmin. When this window is specified, STAMINA guarantees that the actual probability will be somewhere within that window. Read more...

☰ Advanced Options


Use multithreading protocol (may prevent timeout).
Create .tra file which contains all of the states used in the final model.

Report the labels created and the number of states created with each label.
Enforce absolute state limit at states.
API URL: Change
For online users, STAMINA will time-out after 5 seconds. If you wish to check larger models than that, please download and install STAMINA.
STAMINA Information FLUENT Information Papers and Research
STAMINA/STORM State-space truncation (STAMINA) Google Scholar
STAMINA/PRISM
Contact Developers
Fluent Website
Contact Fluent
STAMINA is developed at Utah State University and is part of the tools developed by the FLUENT Team. The STAMINA tool is licensed under the GPLv3 license, and the model checkers it integrates with, STORM and PRISM, are under the GPL 3.0 and 2.0 licenses respectively.
This website is designed and developed by hand by Josh Jeppson. The content and design of this website is licensed under the CC-BY-SA-NC license. This website uses the Breeze Icons from KDE licensed under the GPL3.