Open
Description
Describe the bug
A clear and concise description of what the bug is.
My issue is in:
- STAMINA CLI (
sstamina
) - STAMINA GUI (
xstamina
)
I was using the...
- STAMINA 2.0 Algorithm (Re-exploring,
-J
) - STAMINA 2.5 Algorithm (Iterative,
-I
) - STAMINA 3.0 Algorithm (Priority, `-P)
- I didn't use the
--rare
or--common
flags. - I used the
--rare
flag - I used the
--common
flag
- I didn't use the
To Reproduce
Steps to reproduce the behavior:
Correct the typo "Stochiastic" in the following message printed by STAMINA: "STAMINA -- The STochiastic Approximate Model-checker, for INfinite-state Analysis". Also, remove comma.
Expected behavior
A clear and concise description of what you expected to happen.
Screenshots
If applicable, add screenshots to help explain your problem.
Desktop (please complete the following information):
- OS:
- Version:
- Git Hash (if known):
Additional context
Add any other context about the problem here.
Logs
========================================================================================
�[1mSTAMINA -- The STochiastic Approximate Model-checker, for INfinite-state Analysis�[0m
========================================================================================
(C) 2023 Fluent Verification Research Group -- Licensed freely under the GPLv3 license
Version: 2.2.5
Developers: J Jeppson, Z Zhang, R Roberts, T Neupane, and others.
Website: https://staminachecker.org
Repository: https://github.com/fluentverification/stamina-storm
========================================================================================
Model checker: Storm (https://stormchecker.org) - Licensed under the GPLv3
Storm Authors: C Hensel, S Junges, J Katoen, T Quatmann, M Volk
========================================================================================
WARN (Program.cpp:238): The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.
WARN (Program.cpp:1633): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1633): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1633): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
Labeling:
4 labels
* Absorbing -> 1 item(s)
* deadlock -> 9 item(s)
* init -> 1 item(s)
* (akg >= 5) -> 1353 item(s)
========================================================================================
RESULTS
========================================================================================
Property: "1": P=? [true U<=15 (akg >= 5)];
Probability Minimum: 0.014735521018
Probability Maximum: 0.014737205629
Window: 0.000001684611
========================================================================================
Model: 217812 states with 1 initial.
========================================================================================
Metadata
Metadata
Assignees
Labels
No labels