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.
Different STAMINA hosts may have different rate limitations and timeouts. If you wish to check larger models than the current host will allow, please download and install STAMINA.
API URL: Change