Matthias Volk
Matthias Volk
Currently, some parts of the code are still using `std::cout`. We should revise them to use our custom macros such as `STORM_LOG_INFO` or `STORM_PRINT_AND_LOG`. In addition, we opt to use...
@Vescatur found that using the abstraction engine always prints an error. However, the model-checking query can still be successfully executed. The problem is that `canHandle` in [utility/Engine.cpp](https://github.com/moves-rwth/storm/blob/master/src/storm/utility/Engine.cpp#L107) is missing the...
The file `model-handling.h` requires the library `storm-counterexamples` for e.g. printing counterexamples. I am wondering if we could remove this dependency and move the support for counterexamples into the dedicated library.
At least in two instances, preprocessing is only transforming the model but not the properties: - [model-handling.h#L550](https://github.com/moves-rwth/storm/blob/master/src/storm-cli-utilities/model-handling.h#L550) - [model-handling.h#L591](https://github.com/moves-rwth/storm/blob/master/src/storm-cli-utilities/model-handling.h#L591)
I get different runtimes for CTMC modelchecking when computing the transient probability of reaching a label compared to avoiding the label. I attached a [minimal CTMC](https://github.com/moves-rwth/storm/files/5267284/ctmc.txt) modeling a phase-type distribution...
When using Xcode for the Storm compilation the tests cannot be compiled because the googletest library is not found. The expected location would be `build_xcode/resources/3rdparty/gtest-1.10.0/lib/libgtest.a` but the generated library from...
Parsing of `RationalFunction` in the DRN format is slow. Profiling revealed that the main issue lies in the following line: https://github.com/moves-rwth/storm/blob/2433671b7d08d069cdcf0feee0971d1783d9ef26/src/storm-parsers/parser/ValueParser.cpp#L23 For an example profiling run, 97.5% of the total...
We currently download Spot from https://spot.lrde.epita.fr/. At the moment of writing, the site is down. This problem also sporadically occurred before (usually noticeable when the CI failed). If the issue...
Checking whether a model is acyclic should be quite helpful. Note that the current implementation first needs to find and exclude all states with self-loops, because the underlying Storm function...
(Issue was originally raised in https://github.com/moves-rwth/stormpy/issues/28#issuecomment-1271835119) Pass the Storm location (`storm_dir `) as a HINT to CMake in https://github.com/moves-rwth/stormpy/blob/f19e657eec9cbb439a6934a3ea78a13cdba26d97/cmake/CMakeLists.txt#L3