Skip to content

[USER SUBMITTED BUG] Correct typo in the output message produced by STAMINA CLI #54

Open
@zgzn

Description

@zgzn

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

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

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions