fluentverification / stamina-storm Goto Github PK

STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.

Home Page: https://staminachecker.org

License: GNU General Public License v3.0

C++ 95.51% CMake 2.01% Shell 0.29% Python 0.64% C 1.46% Dockerfile 0.08%

ctmc formal-methods formal-verification graph-theory model-checking transient-analysis markov-chain dtmc

stamina-storm's Introduction

STAMINA (STORM Integration)

Parent Repository

To get both STAMINA/PRISM and STAMINA/STORM, please clone the parent repository, at https://github.com/fluentverification/stamina

Description

Introducing STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis

STAMINA is a powerful software tool designed to analyze infinite-sized Continuous-Time Markov Chains (CTMCs) and provide valuable insights for probabilistic model checking. With its C++ implementation, which interfaces seamlessly with the Storm probabilistic model checking engine, STAMINA offers a highly efficient and accelerated analysis process.

Key Features:

Efficient CTMC Analysis: STAMINA leverages its cutting-edge algorithms to analyze infinite-sized CTMCs with remarkable speed and accuracy.
Truncation Techniques: The software employs advanced truncation techniques to focus on the most significant areas of probability mass, ensuring an optimal balance between precision and computational complexity.
Probability Bounds: STAMINA delivers both an absolute minimum probability (Pmin) and an absolute maximum probability (Pmax) for the analyzed CTMCs. These bounds guarantee that the difference (Pmax - Pmin) remains within a user-specified tightness bound (w), allowing you to estimate the actual probability with high confidence.
C++ Implementation: The C++ version of STAMINA has been carefully optimized for performance, significantly surpassing its predecessor written in Java. The new implementation offers enhanced speed and efficiency, making it the preferred choice for conducting high-speed model checking tasks.

Note: While the Java version of STAMINA, which interfaced with the PRISM model checking engine, remains available, it is no longer actively maintained. Users are encouraged to adopt the C++ version for improved performance and feature updates.

Get started with STAMINA today and unlock the potential of analyzing infinite-sized CTMCs with speed, accuracy, and comprehensive probability bounds that converge within the specified tightness bound.

For detailed usage instructions, installation guidelines, and further information, please refer to the project's GitHub repository, website, or the project wiki

Website

Check out our website at https://staminachecker.org or view the website's source code on GitHub.

To compile:

Please see our wiki page for more information, dependency list, etc. However, assuming you have the dependencies (most notably, Storm) installed:

On Linux and Mac:

git clone https://github.com/fluentverification/stamina-storm
cd bin
cmake .. -DSTORM_PATH=<PATH TO STORM DIRECTORY> -DCMAKE_CXX_COMPILER=/usr/bin/clang-cpp
make

Both GCC and CLang are supported, but we recommend CLang as it's STL implementation for certain hashed datasets is slightly faster.

On Windows:

Windows is not officially supported but if Storm, CMake, Git, etc., are installed then it is possible to install STAMINA on windows. Simply invoke CMake as you would on Linux and Mac and then build the project.

To run:

The basic syntax of running STAMINA is as follows:

./sstamina MODEL_FILE PROPERTIES_FILE [OPTIONS...]

GUI (Work in Progress)

A new GUI is being written using QtWidgets5. This GUI will be called xstamina and will feature comprehensive access to all of the features of STAMINA, and will also include a few extra "goodies", such as help creating CSL properties and PRISM models.

Some features of this new GUI include: - PRISM File editing/CSL Properties editing - Syntax highlighting for PRISM model files - Direct "Check" button included in the GUI - (Planned) CSL Properties wizard - Label Editor - State viewer - (Planned) Counterexample viewer (to integrate with the other FLUENT projects)

To compile with the GUI, you will need the following dependencies: - QtWidgets v5+ - KF5

You can compile the xstamina executable using the BUILD_GUI cmake option.

cmake .. [OTHER CMAKE OPTIONS] -DBUILD_GUI=ON

stamina-storm's People

Contributors

Stargazers

Watchers

Forkers

gerbs-11 shivamganwani

stamina-storm's Issues

In some cases, initial states not generated, causing an assertion error in `storm::builder::StateAndChoiceInformationBuilder::addMarkovianState`

To reproduce in gdb:

gdb --args ./stamina-cplusplus PATH_TO_CASE_STUDIES/case-studies/HazardCct/Circuit0x8E_Two_Inverter/Glitch\ Zero/Unbounded/Circuit0x8E_TI_010to100_unbounded.sm PATH_TO_CASE_STUDIES/case-studies/HazardCct/Circuit0x8E_Two_Inverter/Glitch\ Zero/Unbounded/pro.csl

Gets the following output:

[INFO]: Starting STAMINA with kappa = 1.000000 and reduction factor = 2.000000
[INFO]: Stamina version is: 0.1
[DEBUG MESSAGE]: Checking property in properties vector.
[WARNING]: This property (1) is a probability path formula.
[INFO]: 0: dequeued state
[MESSAGE]: Finished exploration of state space and state truncation (with permReachability 0) in 18 seconds,
        Explored 0 states. Transition matrix has 1 rows.
[ERROR]: STAMINA encountered the following (possibly recoverable) error: 
        Initial states are empty!
[INFO]: Exploring state with id 0.

stamina-cplusplus: /home/josh/Documents/Work/stamina-cplusplus/storm/src/storm/builder/StateAndChoiceInformationBuilder.cpp:96: void storm::builder::StateAndChoiceInformationBuilder::addMarkovianState(uint_fast64_t): Assertion `_buildMarkovianStates' failed.

Program received signal SIGABRT, Aborted.

Actually deploy dockerized STAMINA to Azure

Here's a place to discuss deployment to Azure. This issue will close when that is done.

Remove `auto` keywords

Remove auto keywords and replace them with proper datatypes. This will probably not be done immediately, since we should get the codebase working first, and a lot of the missing functionality implemented. However, a lot of the auto keywords have been put there because:

The storm API we are using doesn't have the same types as the prism API the Java version uses, meaning that even types like State, ProbState, and others don't have storm analogs.
We're not sure what type a method returns, but we know from translating from the Java version that it probably has some attribute which we need to modify. If we can figure out the type, we can figure out what methods or attributes it has and it will be easier to debug when we eventually get to the compile/testing stage

(dev branch)

`multithreading` branch idles forever

I'm not sure why but no threads are explored, but all idle forever.

State Space Truncation

The current dev branch functionally performs truncation, but slowly, so I am attempting to optimize it in the optimize branch, but the optimized version doesn't quite match.

Incorrect Results for Pmin and Pmax even though state space is correct

The current property modification code for some reason does not directly work. The values of P_min and P_max are incorrect even though the state space is properly truncated.

Not exploring any states

There is an issue with the next state generation. For some reason, no next states are being generated. It may be that we are missing a self-loop.

Transitions from cross exploration: how best to insert?

Need to figure out how to insert the transitions when the "from" state is owned by one thread, and the "to" state is owned by another thread. The ControlThread object has a requestInsertTransition, which requires the following parameters:

Thread Index: this should probably be the thread index of the state who owns the "to" state
From State (index): the column of the transition matrix, index of the "from" state
To State (index): the row of the transition matrix, index of the "to" state
Transition Rate/Transition Probability

What should probably be done:

During requestCrossExploration methods, we should take the transition rate and index of the "from" state and also place it in the crossExplorationQueue.

Not getting parsed modules file

stamina is not currently reading modules file correctly, and I'm not sure why since this is a storm API call. I've looked at the files I'm passing in, and they're not incorrect.

As of current, the error gotten is as follows:

[INFO]: Starting STAMINA with kappa = 1.000000 and reduction factor = 2.000000
[INFO]: Stamina version is: 0.1
[ERROR]: STAMINA encountered the following error and will now exit: 
        Got error when reading modules or properties file:
                WrongFormatException: Parsing error at 12:5:  expecting "endmodule", here:
                TetR : int init 0;
            ^

This corresponds to the following code in Stamina.cpp:

83    // Load modules file and properties file
84    try {
85        modulesFile = storm::parser::PrismParser::parse(options->model_file, true);
86        propertiesVector = storm::api::parsePropertiesForPrismProgram(options->properties_file, modulesFile);
87        modelChecker->initialize(&modulesFile, &propertiesVector);
88    }
89    catch (const std::exception& e) {
90        // Uses stringstream because std::to_string(e) throws an error with storm's exceptions
91        std::stringstream msg;
92        msg << "Got error when reading modules or properties file:\n\t\t" << e.what();
93        errorAndExit(msg.str());
94    }

Exception in `StaminaModelBuilder::build()`

Backtrace:

#0  __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:50
#1  0x00007ffff4fe1859 in __GI_abort () at abort.c:79
#2  0x00007ffff5267911 in ?? () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#3  0x00007ffff527338c in ?? () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#4  0x00007ffff52733f7 in std::terminate() () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#5  0x00007ffff52736a9 in __cxa_throw () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#6  0x00007ffff61a9bbc in storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >::assertValidityOfComponents(storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> > const&) const [clone .cold] () from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#7  0x00007ffff6efd521 in storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >::Model(storm::models::ModelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) () from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#8  0x00007ffff6efd65d in storm::models::sparse::DeterministicModel<double, storm::models::sparse::StandardRewardModel<double> >::DeterministicModel(storm::models::ModelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) () from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#9  0x00007ffff70187bf in storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> >::Ctmc(storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) ()
   from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#10 0x00007ffff702b385 in std::shared_ptr<storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> > > storm::utility::builder::buildModelFromComponents<double, storm::models::sparse::StandardRewardModel<double> >(storm::models::ModelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<double> >&&) ()
   from /path/to/stamina/stamina-cplusplus/storm/lib/libstorm.so
#11 0x00005555555aaea0 in stamina::StaminaModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::build (this=0x5555558cf110)
    at /path/to/stamina/stamina-cplusplus/src/StaminaModelBuilder.cpp:111
#12 0x00005555555da091 in stamina::StaminaModelChecker::modelCheckProperty (this=0x55555582c220, prop=..., modulesFile=...) at /path/to/stamina/stamina-cplusplus/src/StaminaModelChecker.cpp:157
#13 0x0000555555590c0a in stamina::Stamina::run (this=0x7fffffffd560) at /path/to/stamina/stamina-cplusplus/src/Stamina.cpp:53
#14 0x0000555555577301 in main (argc=3, argv=0x7fffffffdaa8) at /path/to/stamina/stamina-cplusplus/src/main.cpp:37

Unknown Issue -- Perimeter Reachability spikes after several iterations

Output (Annotated):

=====================================================================================
Data is correct here: (checked against the Java version)
=====================================================================================
[INFO]: Starting STAMINA with kappa = 1.000000 and reduction factor = 1.250000
[INFO]: Stamina version is: 0.1
[INFO]: There are the following number of state labels: 0
P=? [true U[0, 2100] ((LacI < 20) & (TetR > 40))]
[WARNING]: This property (1) is a probability path formula.
[INFO]: Approximation [Refine Iterations: 0, kappa = 1.000000]
piHat = 1 and w/approx = 0.0005
[INFO]: Perimeter reachability: 1.000000
At this iteration, kappa = 1
[INFO]: Finished state space truncation. Explored 4 states in total.
At this iteration, the following states are terminal:3
piHat = 3 and w/approx = 0.0005
[INFO]: Perimeter reachability: 3.000000
At this iteration, kappa = 0.8
[INFO]: Finished state space truncation. Explored 10 states in total.
At this iteration, the following states are terminal:7
piHat = 5.6 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.600000
At this iteration, kappa = 0.64
[INFO]: Finished state space truncation. Explored 16 states in total.
At this iteration, the following states are terminal:11
piHat = 7.04 and w/approx = 0.0005
[INFO]: Perimeter reachability: 7.040000
At this iteration, kappa = 0.512
[INFO]: Finished state space truncation. Explored 22 states in total.
At this iteration, the following states are terminal:15
piHat = 7.68 and w/approx = 0.0005
[INFO]: Perimeter reachability: 7.680000
At this iteration, kappa = 0.4096
[INFO]: Finished state space truncation. Explored 28 states in total.
At this iteration, the following states are terminal:19
piHat = 7.7824 and w/approx = 0.0005
[INFO]: Perimeter reachability: 7.782400
At this iteration, kappa = 0.32768
[INFO]: Finished state space truncation. Explored 31 states in total.
At this iteration, the following states are terminal:21
piHat = 6.88128 and w/approx = 0.0005
[INFO]: Perimeter reachability: 6.881280
At this iteration, kappa = 0.262144
[INFO]: Finished state space truncation. Explored 35 states in total.
At this iteration, the following states are terminal:23
piHat = 6.02931 and w/approx = 0.0005
[INFO]: Perimeter reachability: 6.029312
At this iteration, kappa = 0.209715
[INFO]: Finished state space truncation. Explored 39 states in total.
At this iteration, the following states are terminal:25
piHat = 5.24288 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.242880
At this iteration, kappa = 0.167772
[INFO]: Finished state space truncation. Explored 45 states in total.
At this iteration, the following states are terminal:28
piHat = 4.69762 and w/approx = 0.0005
[INFO]: Perimeter reachability: 4.697620
At this iteration, kappa = 0.134218
[INFO]: Finished state space truncation. Explored 49 states in total.
At this iteration, the following states are terminal:30
piHat = 4.02653 and w/approx = 0.0005
[INFO]: Perimeter reachability: 4.026532
At this iteration, kappa = 0.107374
[INFO]: Finished state space truncation. Explored 53 states in total.
At this iteration, the following states are terminal:32
piHat = 3.43597 and w/approx = 0.0005
[INFO]: Perimeter reachability: 3.435974
=====================================================================================
This is where the data becomes incorrect below this iteration
=====================================================================================
At this iteration, kappa = 0.0858993
[INFO]: Finished state space truncation. Explored 119 states in total.
At this iteration, the following states are terminal:69
piHat = 5.92705 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.927055
At this iteration, kappa = 0.0687195
[INFO]: Finished state space truncation. Explored 181 states in total.
At this iteration, the following states are terminal:114
piHat = 7.83402 and w/approx = 0.0005
[INFO]: Perimeter reachability: 7.834020
At this iteration, kappa = 0.0549756
[INFO]: Finished state space truncation. Explored 210 states in total.
At this iteration, the following states are terminal:130
piHat = 7.14683 and w/approx = 0.0005
[INFO]: Perimeter reachability: 7.146826
At this iteration, kappa = 0.0439805
[INFO]: Finished state space truncation. Explored 237 states in total.
At this iteration, the following states are terminal:147
piHat = 6.46513 and w/approx = 0.0005
[INFO]: Perimeter reachability: 6.465128
At this iteration, kappa = 0.0351844
[INFO]: Finished state space truncation. Explored 288 states in total.
At this iteration, the following states are terminal:183
piHat = 6.43874 and w/approx = 0.0005
[INFO]: Perimeter reachability: 6.438740
At this iteration, kappa = 0.0281475
[INFO]: Finished state space truncation. Explored 338 states in total.
At this iteration, the following states are terminal:217
piHat = 6.10801 and w/approx = 0.0005
[INFO]: Perimeter reachability: 6.108007
At this iteration, kappa = 0.022518
[INFO]: Finished state space truncation. Explored 383 states in total.
At this iteration, the following states are terminal:240
piHat = 5.40432 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.404320
At this iteration, kappa = 0.0180144
[INFO]: Finished state space truncation. Explored 441 states in total.
At this iteration, the following states are terminal:269
piHat = 4.84587 and w/approx = 0.0005
[INFO]: Perimeter reachability: 4.845873
At this iteration, kappa = 0.0144115
[INFO]: Finished state space truncation. Explored 589 states in total.
At this iteration, the following states are terminal:357
piHat = 5.14491 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.144912
At this iteration, kappa = 0.0115292
[INFO]: Finished state space truncation. Explored 709 states in total.
At this iteration, the following states are terminal:430
piHat = 4.95756 and w/approx = 0.0005
[INFO]: Perimeter reachability: 4.957562
At this iteration, kappa = 0.00922337
[INFO]: Finished state space truncation. Explored 923 states in total.
At this iteration, the following states are terminal:550
piHat = 5.07285 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.072855
At this iteration, kappa = 0.0073787
[INFO]: Finished state space truncation. Explored 1183 states in total.
At this iteration, the following states are terminal:683
piHat = 5.03965 and w/approx = 0.0005
[INFO]: Perimeter reachability: 5.039650
At this iteration, kappa = 0.00590296
[INFO]: Finished state space truncation. Explored 1446 states in total.
At this iteration, the following states are terminal:792
piHat = 4.67514 and w/approx = 0.0005
[INFO]: Perimeter reachability: 4.675143
At this iteration, kappa = 0.00472237

Segmentation fault during `carl::MonomialPool::~MonomialPool`

Neither GDB or Valgrind will give me a complete stacktrace (something about a messed up program counter) but we get a segmentation fault with a stacktrace that looks like this:

Program received signal SIGSEGV, Segmentation fault.
__GI___libc_free (mem=0x2821) at malloc.c:3102
3102    malloc.c: No such file or directory.
(gdb) bt
#0  __GI___libc_free (mem=0x2821) at malloc.c:3102
#1  0x00007ffff471cec1 in __gnu_cxx::new_allocator<std::__detail::_Hash_node_base*>::deallocate (
    this=0x7fffffffd987, __p=0x2821, __t=0) at /usr/include/c++/10/ext/new_allocator.h:133
#2  0x00007ffff4718fa6 in std::allocator_traits<std::allocator<std::__detail::_Hash_node_base*> >::deallocate (
    __a=..., __p=0x2821, __n=0) at /usr/include/c++/10/bits/alloc_traits.h:492
#3  0x00007ffff4a048d6 in std::__detail::_Hashtable_alloc<std::allocator<std::__detail::_Hash_node<carl::MonomialPool::PoolEntry, true> > >::_M_deallocate_buckets (
    this=0x7ffff7f72a00 <carl::Singleton<carl::MonomialPool>::getInstance()::t+96>, __bkts=0x2821, __bkt_count=0)
    at /usr/include/c++/10/bits/hashtable_policy.h:2099
#4  0x00007ffff4a0334e in std::_Hashtable<carl::MonomialPool::PoolEntry, carl::MonomialPool::PoolEntry, std::allocator<carl::MonomialPool::PoolEntry>, std::__detail::_Identity, carl::MonomialPool::equal, carl::MonomialPool::hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::_M_deallocate_buckets (
    this=0x7ffff7f72a00 <carl::Singleton<carl::MonomialPool>::getInstance()::t+96>, __bkts=0x2821, __bkt_count=0)
    at /usr/include/c++/10/bits/hashtable.h:407
#5  0x00007ffff4a01fac in std::_Hashtable<carl::MonomialPool::PoolEntry, carl::MonomialPool::PoolEntry, std::allocator<carl::MonomialPool::PoolEntry>, std::__detail::_Identity, carl::MonomialPool::equal, carl::MonomialPool::hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::_M_deallocate_buckets (
    this=0x7ffff7f72a00 <carl::Singleton<carl::MonomialPool>::getInstance()::t+96>)
    at /usr/include/c++/10/bits/hashtable.h:412
#6  0x00007ffff4a0109e in std::_Hashtable<carl::MonomialPool::PoolEntry, carl::MonomialPool::PoolEntry, std::allocator<carl::MonomialPool::PoolEntry>, std::__detail::_Identity, carl::MonomialPool::equal, carl::MonomialPool::hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, true, true> >::~_Hashtable (
    this=0x7ffff7f72a00 <carl::Singleton<carl::MonomialPool>::getInstance()::t+96>, __in_chrg=<optimized out>)
    at /usr/include/c++/10/bits/hashtable.h:1388
#7  0x00007ffff49f6732 in std::unordered_set<carl::MonomialPool::PoolEntry, carl::MonomialPool::hash, carl::MonomialPool::equal, std::allocator<carl::MonomialPool::PoolEntry> >::~unordered_set (
    this=0x7ffff7f72a00 <carl::Singleton<carl::MonomialPool>::getInstance()::t+96>, __in_chrg=<optimized out>)
    at /usr/include/c++/10/bits/unordered_set.h:97
#8  0x00007ffff49f68ee in carl::MonomialPool::~MonomialPool (
    this=0x7ffff7f729a0 <carl::Singleton<carl::MonomialPool>::getInstance()::t>, __in_chrg=<optimized out>)
    at /home/josh/Documents/work/dev/storm/build/resources/3rdparty/carl_download/source_dir/src/carl/core/MonomialPool.h:88
#9  0x00007ffff03acac6 in __cxa_finalize (d=0x7fffeecbabc0) at cxa_finalize.c:83
#10 0x00007fffeec581f3 in __do_global_dtors_aux () from /usr/local/lib/libcarl.so.14.22
#11 0x00007fffffffdbc0 in ?? ()
#12 0x00007ffff7fe2373 in _dl_fini () at dl-fini.c:138

This is weird because:
a) This doesn't happen on the master branch, even with the same versions of both Storm and Carl. However, it does happen in multithreading and priority
b) This isn't even in STAMINA. The stacktrace doesn't even show any of our functions

Therefore, I am extremely confused.

Add implementations of methods

I figured a GitHub issue would be a good place to keep track of what has and hasn't been implemented yet.

Methods that need to be implemented by Class:

InfCTMCModelGenerator needs the following methods:

getGlobalStateSet()
computeTransitionTarget()

Results

getResultsString()

This list will be updated as I find more. Additionally, I will mark when I've implemented something as well.

(dev branch)

Multithreading in `stateMap`

Insertion into stateMap and the entirety of generator->expand() are rather slow compared to the Java version. I think this is because the Java version automatically offloads hashing and hashmap insertion to another thread.

Idea:

Create a second thread in the StateIndexArray for insertion and whenever there is an insert, that happens on that thread

Issues with insertion into `mainExplorationQueue`

How best to insert? We need to make sure enqueueSuccessors is called in stateToIdCallback, so we will have to bind our callback method within the exploration thread. Additionally, the method must exist within that exploration thread, so some code moving around will be necessary.

Dockerfile: Bad Storm version

Unexpected behavior from the Storm version in the docker image.

Unknown label for chained atomic state formulas
Not returning the right number of states
Same commit as works on threadripper

Problem regarding several properties in one file

Stamina produces the following error when a user is attempting to check several properties at once.

ERROR (Model.cpp:58): Invalid item count (0) of state labeling (states: 1).
[ERROR]: STAMINA encountered the following (possibly recoverable) error:
STAMINA encountered the following error (possibly in the interface with STORM) in the function StaminaModelBuilder::build():
IllegalArgumentException: Invalid item count (0) of state labeling (states: 1).
Segmentation fault

Contents of property file being inserted:
P=? [ true U[0,60000] ((!valid) & (!ack) & (!done) & (!rdy)) ]; //0000//
P=? [ true U[0,60000] ((!valid) & (!ack) & (!done) & (rdy)) ]; //0001//
P=? [ true U[0,60000] ((!valid) & (!ack) & (done) & (!rdy)) ]; //0010//
P=? [ true U[0,60000] ((!valid) & (!ack) & (done) & (rdy)) ]; //0011//
P=? [ true U[0,60000] ((!valid) & (ack) & (!done) & (!rdy)) ]; //0100//
P=? [ true U[0,60000] ((!valid) & (ack) & (!done) & (rdy)) ]; //0101//
P=? [ true U[0,60000] ((!valid) & (ack) & (done) & (!rdy)) ]; //0110//
P=? [ true U[0,60000] ((!valid) & (ack) & (done) & (rdy)) ]; //0111//
P=? [ true U[0,60000] ((valid) & (!ack) & (!done) & (!rdy)) ]; //1000//
P=? [ true U[0,60000] ((valid) & (!ack) & (!done) & (rdy)) ]; //1001//
P=? [ true U[0,60000] ((valid) & (!ack) & (done) & (!rdy)) ]; //1010//
P=? [ true U[0,60000] ((valid) & (!ack) & (done) & (rdy)) ]; //1011//
P=? [ true U[0,60000] ((valid) & (ack) & (!done) & (!rdy)) ]; //1100//
P=? [ true U[0,60000] ((valid) & (ack) & (!done) & (rdy)) ]; //1101//
P=? [ true U[0,60000] ((valid) & (ack) & (done) & (!rdy)) ]; //1110//
P=? [ true U[0,60000] ((valid) & (ack) & (done) & (rdy)) ]; //1111//

Empty Behaviors from Storm API

Several times during program run, Storm will provide us with an empty state behavior on attempted expansion. Should we treat these states as deadlock, with a self-loop, or ignore them?

Multithreading branch: not achieving lock in `ExplorationThread::mainLoop`

For some reason, none of the exploration threads are achieving the lock of the shared mutex on the cross exploration queue. See lines 124-168 in IterativeExplorationThread.cpp:

if (!this->crossExplorationQueue.empty() && this->xLock.owns_lock()) {
	STAMINA_DEBUG_MESSAGE("Exploring from the cross exploration queue");
	std::lock_guard<decltype(this->xLock)> lockGuard(this->xLock);
	auto stateDeltaPiPair = this->crossExplorationQueue.front();
	this->crossExplorationQueue.pop_front();
	auto s = stateDeltaPiPair.first;
	double deltaPi = stateDeltaPiPair.second;
	StateType stateIndex = this->parent->getStateIndexOrAbsorbing(s);
	StateProbability stateProbability(
		s            // State values
		, stateIndex // State Index
		, deltaPi    // Delta Pi
	);

	// Update the estimated reachability of s
	// auto probabilityState = this->parent->getStateMap().get(stateIndex);
	// probabilityState->pi += deltaPi;
	exploreState(stateProbability);
}
else if (!this->mainExplorationQueue.empty()) {
	STAMINA_DEBUG_MESSAGE("Exploring from main exploration queue");
	// If we are dequeuing from the main exploration queue, then
	// the state we are enqueuing doesn't have a delta pi
	auto s = this->mainExplorationQueue.front();
	this->mainExplorationQueue.pop_front();
	StateProbability stateProbability(
		s.second
		, s.first->index
	);
	exploreState(stateProbability);
}
else if (!this->xLock.owns_lock()) {
	STAMINA_DEBUG_MESSAGE("Size of cross exploration queue: " << this->crossExplorationQueue.size());
	STAMINA_DEBUG_MESSAGE("Thread " << this->threadIndex << " is idling...");
	if (!this->crossExplorationQueue.empty() && !this->xLock.owns_lock()) {
		STAMINA_DEBUG_MESSAGE("Cross-exploration queue is not emply, but lock has not been achieved.");
	}
	else if (this->mainExplorationQueue.empty()) {
		// STAMINA_DEBUG_MESSAGE("Both main and cross exploration queue are empty");
	}
	this->idling = true;
}
else {
	this->idling = false;
}

Because the lock is never achieved, no exploration occurs.

Templatization issue with `StaminaModelBuilder` => `StaminaIterativeModelBuilder` => `StaminaThreadedIterativeModelBuilder`

Not entirely sure what is causing this, but there is an issue on compilation in the multithreading:HEAD branch, with multiple functional override issues.

In file included from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.h:6,
                 from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.cpp:6:
/home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/StaminaIterativeModelBuilder.h: In instantiation of ‘class stamina::builder::StaminaIterativeModelBuilder<double>’:
/usr/include/c++/10/bits/shared_ptr.h:584:23:   required from ‘std::shared_ptr<_Tp> std::static_pointer_cast(const std::shared_ptr<_Tp>&) [with _Tp = stamina::builder::StaminaModelBuilder<double>; _Up = stamina::builder::StaminaIterativeModelBuilder<double>]’
/home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.cpp:117:82:   required from here
/home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/StaminaIterativeModelBuilder.h:60:14: error: conflicting return type specified for ‘StateType stamina::builder::StaminaIterativeModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(const CompressedState&) [with ValueType = double; RewardModelType = storm::models::sparse::StandardRewardModel<double>; StateType = unsigned int; storm::generator::CompressedState = storm::storage::BitVector]’
   60 |    StateType getOrAddStateIndex(CompressedState const& state) override;
      |              ^~~~~~~~~~~~~~~~~~
In file included from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.h:5,
                 from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.cpp:6:
/home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/StaminaModelBuilder.h:163:22: note: overridden function is ‘StateType stamina::builder::StaminaModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(const CompressedState&) [with StateType = double; RewardModelType = storm::models::sparse::StandardRewardModel<double>; ValueType = unsigned int; storm::generator::CompressedState = storm::storage::BitVector]’
  163 |    virtual StateType getOrAddStateIndex(CompressedState const& state);
      |                      ^~~~~~~~~~~~~~~~~~
In file included from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.h:6,
                 from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.cpp:6:
/home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/StaminaIterativeModelBuilder.h:66:72: error: invalid covariant return type for ‘storm::storage::sparse::ModelComponents<CValueType, CRewardModelType> stamina::builder::StaminaIterativeModelBuilder<ValueType, RewardModelType, StateType>::buildModelComponents() [with ValueType = double; RewardModelType = storm::models::sparse::StandardRewardModel<double>; StateType = unsigned int]’
   66 |    storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents() override;
      |                                                                        ^~~~~~~~~~~~~~~~~~~~
In file included from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.h:5,
                 from /home/josh/Documents/work/dev/stamina-storm/src/stamina/core/StaminaModelChecker.cpp:6:
/home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/StaminaModelBuilder.h:220:80: note: overridden function is ‘storm::storage::sparse::ModelComponents<ValueType, RewardModelType> stamina::builder::StaminaModelBuilder<ValueType, RewardModelType, StateType>::buildModelComponents() [with StateType = double; RewardModelType = storm::models::sparse::StandardRewardModel<double>; ValueType = unsigned int]’
  220 |    virtual storm::storage::sparse::ModelComponents<ValueType, RewardModelType> buildModelComponents() = 0;
      |

I'm not sure why this is the case, since the return type for getOrAddStateIndex is StateType which is specified in all cases to be forward-declared as uint32_t

Multuthreading Issue with Either STORM or `boost`

Bug description: there appears to be some sort of issue with how STAMINA (single-threaded) interacts with either the STORM or boost APIs (which I assume are multithreaded). Determined by noting different output from terminal vs. in GDB using libthread_db.

To reproduce:

Test in GDB using gdb --args ./stamina-cplusplus $CASE_STUDIES_DIRECTORY/HazardCct/Circuit0x8E_Two_Inverter/Glitch\ Zero/Unbounded/Circuit0x8E_TI_010to100_unbounded.sm $CASE_STUDIES_DIRECTORY/HazardCct/Circuit0x8E_Two_Inverter/Glitch\ Zero/Unbounded/pro.csl
Test in terminal using ./stamina-cplusplus $CASE_STUDIES_DIRECTORY/HazardCct/Circuit0x8E_Two_Inverter/Glitch\ Zero/Unbounded/Circuit0x8E_TI_010to100_unbounded.sm $CASE_STUDIES_DIRECTORY/HazardCct/Circuit0x8E_Two_Inverter/Glitch\ Zero/Unbounded/pro.csl

Output in GDB using libthread_db

[Thread debugging using libthread_db enabled]
Using host libthread_db library "/usr/lib/libthread_db.so.1".
[INFO]: Starting STAMINA with kappa = 1.000000 and reduction factor = 2.000000
[INFO]: Stamina version is: 0.1
[DEBUG MESSAGE]: Checking property in properties vector.
[WARNING]: This property (1) is a probability path formula.
[INFO]: 0: dequeued state
[MESSAGE]: Finished exploration of state space and state truncation (with permReachability 0) in 19 seconds,
        Explored 0 states. Transition matrix has 1 rows.
[ERROR]: STAMINA encountered the following (possibly recoverable) error: 
        Initial states are empty!
[INFO]: Exploring state with id 0.
[INFO]: Exploring state with id 100000.
[INFO]: Exploring state with id 200000.
[INFO]: Exploring state with id 300000.
[INFO]: Exploring state with id 400000.
[INFO]: Exploring state with id 500000.
^C
Program received signal SIGINT, Interrupt.

Output in terminal:

[INFO]: Starting STAMINA with kappa = 1.000000 and reduction factor = 2.000000
[INFO]: Stamina version is: 0.1
[DEBUG MESSAGE]: Checking property in properties vector.
[WARNING]: This property (1) is a probability path formula.
[INFO]: 0: dequeued state
stamina-cplusplus: /home/josh/Documents/Work/stamina-cplusplus/storm/src/storm/storage/BitVectorHashMap.cpp:162: std::pair<bool, long unsigned int> storm::storage::BitVectorHashMap<ValueType, Hash>::findBucket(const storm::storage::BitVector&) const [with ValueType = unsigned int; Hash = storm::storage::Murmur3BitVectorHash<unsigned int>]: Assertion `key.size() == bucketSize' failed.
zsh: abort (core dumped)  ./stamina-cplusplus

Native expression modification in STORM API rather than string-based property modification

Rather than using the ModelModify class to change property modification, we could use something within storm::logic::Formula or storm::*::Expression. This was originally written in a (somewhat buried) commit, but was not used because there were some issues with passing that expression into the model checker. If we were able to get this to work, it would present these benefits:

Reduced memory footprint in CompressedStates (by 1 bit per state)
Reduced code complexity in stamina::util::ModelModify
Reduced hard drive impact (minor)

This is marked as "enhancement" as it does not affect the results of STAMINA/STORM

Priority Method: on deque, the destructor for `ProbabilityStatePair` invokes destructor for `BitVector`, causing a segfault

Need to make it so that ~BitVector() is not called on statePriorityQueue.pop()

Autobuild STORM in CMakeLists.txt

STORM is able to do this using a resources folder with just a CMakeLists.txt for each third party resources. I'm not sure yet how to do this, but this would be a good contribution, especially for our GitHub workflows.

Duplicate Entries in Transition Matrix

Issue is most likely in StaminaModelBuilder::flushToTransitionMatrix

Multithreading branch: control thread not waiting for all threads to finish

This could be causing the segfaults. With -j2, after a while, if you type info threads, you get:

(gdb) info threads
  Id   Target Id                                    Frame 
  1    Thread 0x7ffff0531bc0 (LWP 22083) "sstamina" 0x00007ffff469fae1 in clone ()
   from /lib/x86_64-linux-gnu/libc.so.6
  3    Thread 0x7fffe7746700 (LWP 22085) "sstamina" 0x00007ffff51274e8 in stamina::builder::threads::IterativeExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::exploreState (
    this=0x555555809af0, stateProbability=...)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:274
* 4    Thread 0x7fffef746700 (LWP 22086) "sstamina" stamina::builder::threads::IterativeExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::exploreState (this=0x55555580a520, 
    stateProbability=...)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:274
  5    Thread 0x7fffeff47700 (LWP 22093) "sstamina" 0x00007ffff469fae1 in clone ()
   from /lib/x86_64-linux-gnu/libc.so.6
  6    Thread 0x7fffeef45700 (LWP 22095) "sstamina" 0x00007ffff469fae1 in clone ()
   from /lib/x86_64-linux-gnu/libc.so.6

There should be a max of 4 threads here because there is:

The starter thread
The Control Thread
Exploration Thread 1
Exploration Thread 2

Mismatched size of transition matrix

For some reason the size of the transition matrix is not correct:

[ERROR]: STAMINA encountered the following (possibly recoverable) error: 
        STAMINA encountered the following error (possibly in the interface with STORM) in the function StaminaModelBuilder::build():
        IllegalArgumentException: Can not create deterministic model: Number of rows of transition matrix does not match state count.
zsh: segmentation fault (core dumped)  ./stamina-cplusplus $MODEL_FILE $PROPERTIES_FILE

xSTAMINA (STAMINA GUI) - Laundry List

Current list of XStamina Bugs:

Cannot build model multiple times. Crashes.
Does not handle PRISM syntax error. Crashes.
Does not handle any exceptions thrown in Storm. Crashes.
- Will need to edit StaminaMessages::errorAndExit because GUI should not exit.
Sometimes after saving model file, properties file indicates it's been "saved" although it has not.

Unimplemented:

Log viewer. If you need STAMINA's logs you can still open xstamina from a terminal and monitor your terminal. I don't know ~~how~~ the best way to capture output from StaminaMessages into a QPlainTextEdit.
Several of the actions/Menubar buttons don't yet have implementation behind them, although most of the core functionality is there
The "model tree" to the left of the model file editor is not yet populated with information about the model
Label editor
Constants editor
Early-terminated states viewer
Most of the preferences not related to model-checking
Stamina config file to save preferences to.

Reduce and test memory impact

Reduce memory impact wherever possible and test the memory impact of using a std::unordered_map<StateType, ProbabilityState> vs. a stamina::util::StateIndexArray. Additionally, test memory impact against STAMINA/PRISM 2.0

Segmentation fault(s): various places in `multithreading` branch

Current stack trace of segfault:

#0  0x00007ffff62239f1 in storm::generator::NextStateGenerator<double, unsigned int>::load(storm::storage::BitVector const&) () from /usr/local/lib/libstorm.so
#1  0x00007ffff51275eb in stamina::builder::threads::IterativeExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::exploreState (this=0x55555580a520, stateProbability=...)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:274
#2  0x00007ffff51272a0 in stamina::builder::threads::IterativeExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::exploreStates (this=0x55555580a520)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:231
#3  0x00007ffff5126d3f in stamina::builder::threads::ExplorationThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::mainLoop (this=0x55555580a520)
    at /home/josh/Documents/work/dev/stamina-storm/src/stamina/builder/threads/ExplorationThread.cpp:82
#4  0x00007ffff50f840c in std::__invoke_impl<void, void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> (
    __f=@0x555555872e50: &virtual stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::mainLoop(), __t=@0x555555872e48: 0x55555580a520)
    at /usr/include/c++/10/bits/invoke.h:73
#5  0x00007ffff50f834f in std::__invoke<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> (
--Type <RET> for more, q to quit, c to continue without paging--
    __fn=@0x555555872e50: &virtual stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::mainLoop()) at /usr/include/c++/10/bits/invoke.h:95
#6  0x00007ffff50f82bf in std::thread::_Invoker<std::tuple<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> >::_M_invoke<0ul, 1ul> (this=0x555555872e48)
    at /usr/include/c++/10/thread:264
#7  0x00007ffff50f8278 in std::thread::_Invoker<std::tuple<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> >::operator() (this=0x555555872e48)
    at /usr/include/c++/10/thread:271
#8  0x00007ffff50f825c in std::thread::_State_impl<std::thread::_Invoker<std::tuple<void (stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>::*)(), stamina::builder::threads::BaseThread<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>*> > >::_M_run (
    this=0x555555872e40) at /usr/include/c++/10/thread:215
#9  0x00007ffff4860ed0 in ?? () from /lib/x86_64-linux-gnu/libstdc++.so.6
#10 0x00007ffff2dc5ea7 in start_thread () from /lib/x86_64-linux-gnu/libpthread.so.0
#11 0x00007ffff469faef in clone () from /lib/x86_64-linux-gnu/libc.so.6

(As of commit 036d155)

Many state transitions in `priority` method

Priority method:

[INFO]: Finished state space truncation.
        Explored 8134 states in total.
        Got 24992 transitions.

Iterative method:

[INFO]: Finished state space truncation.
        Explored 8163 states in total.
        Got 401 transitions.

Combined CTMC Analysis

In stamina::checker::StaminaModelChecker, two transient analysis are being performed, one for $P_{min}$ and one for $P_{max}$. If we have already performed the model-checking, we should have all of the state probabilities for a given time-bound. Therefore, we should be able to only perform checking once, and then find the values as follows, given $s_a$ the absorbing state, and $p(s_a)$ the (normalized) reachability of $s_a$. (Note, this is not $\pi(s_a)$!)

Note that $P_{min}$ is normally calculated as follows:

$$P_{min} = P_{=?}[\psi\ U^I\ \phi\ \wedge\ \neg\ \hat{s}]$$
but it should be able to be calculated as follows:

$$ P_{min} = P_{max} - p(s_a) $$

So we can use the typical $P_{max}$ computation:

$$
P_{max} = P_{=?}[\psi\ U^I\ \phi\ \vee\ \hat{s}]
$$
And then get $p(s_a)$ from the CheckResult (not sure how yet)

This occurs at StaminaModelChecker.cpp:214

auto result_lower = checker->check(
	// env,
	storm::modelchecker::CheckTask<>(*(propMin.getRawFormula()), true)
);
min_results->result = result_lower->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];
auto result_upper = checker->check(
	// env,
	storm::modelchecker::CheckTask<>(*(propMax.getRawFormula()), true)
);
max_results->result = result_upper->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];

This could be changed to something like

auto result_upper = checker->check(
	// env,
	storm::modelchecker::CheckTask<>(*(propMax.getRawFormula()), true)
);
max_results->result = result_upper->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];
min_results->result = max_results->result - /* Wherever to get p(s_a) */;

I tried result_upper->asExplicitQuantitativeCheckResult<double>()[0], as well as a number of other things, (since the absorbing state index is 0), but this didn't work.

Replace several `bool` values in `ProbabilityState` with a single `uint8_t status` to save space.

Currently there are a bunch of boolean values in the ProbabilityState class which could be condensed into something smaller:

class ProbabilityState {
public:
...
	bool assignedInRemapping;
	bool isNew;
	bool wasPutInTerminalQueue;
	bool preTerminated;
	bool deadlock;
...
// More code here
}

We could use a single uint8_t status to hold all of these values, with bit 0 being assignedInRemapping, bit 1 being isNew, etc... and use bitwise math to get the values like so:

// Somewhere Above
const uint8_t ASSIGNED_IN_REMAPPING_INDEX = 0;
const uint8_t IS_NEW_INDEX = 1;
...
void 
ProbabilityState::setAssignedInRemapping(bool value) {
    // Create bitmask and zero out the desired bit
    status &= ~(0x1 << ASSIGNED_IN_REMAPPING_INDEX);
    // Set the desired bit to the desired value
    status |= (uint8_t) value << ASSIGNED_IN_REMAPPING_INDEX;
}
bool
ProbabilityState::wasAssignedInRemapping() {
    return (status >> ASSIGNED_IN_REMAPPING_INDEX) & 0x1;
}

If anyone wants to help out on this, I think this would be a good first issue for a newcomer.

State Exploration Multithreading

Part of the improvements for STAMINA 2.5 involve asynchronous multithreaded exploration of states by multiple threads as requested by the user. Commit c099b02 creates skeleton for this, but I have a couple of ideas/concerns.

Should the threads be in their own namespace?
Should they be in the same file as the builders?