The storm from moves-rwth

Segfault for PRISM model where variables are optimized away

If I run the attached model with

bin/storm --prism from_pta.txt

I get a segmentation fault:

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff6188750 in storm::expressions::BaseExpression::getManager (this=0x0) at storm/storm-trunk.github/src/storm/storage/expressions/BaseExpression.cpp:102
102                 return manager;
(gdb) bt
#0  0x00007ffff6188750 in storm::expressions::BaseExpression::getManager (this=0x0) at storm/storm-trunk.github/src/storm/storage/expressions/BaseExpression.cpp:102
#1  0x00007ffff6197b4a in storm::expressions::Expression::getManager (this=0x7fffffff8d80) at storm/storm-trunk.github/src/storm/storage/expressions/Expression.cpp:156
#2  0x00007ffff4fa486b in storm::adapters::Z3ExpressionAdapter::translateExpression (this=0x5555558d27f0, expression=...) at storm/storm-trunk.github/src/storm/adapters/Z3ExpressionAdapter.cpp:20
#3  0x00007ffff5eb0b6f in storm::solver::Z3SmtSolver::add (this=0x555555887af0, assertion=...) at storm/storm-trunk.github/src/storm/solver/Z3SmtSolver.cpp:105
#4  0x00007ffff5328655 in storm::generator::PrismNextStateGenerator<double, unsigned int>::getInitialStates(std::function<unsigned int (storm::storage::BitVector const&)> const&) (this=0x555555884e50, stateToIdCallback=...)
    at storm/storm-trunk.github/src/storm/generator/PrismNextStateGenerator.cpp:145
...

From a bit of debugging it looks like the variables are optimized away in

storm/src/storm/storage/prism/Program.cpp

Line 1240 in 13982b4

Program Program::simplify() {

and then in

storm/src/storm/storage/prism/Program.cpp

Line 456 in 13982b4

storm::expressions::Expression Program::getInitialStatesExpression() const {

the result expression does not get initialized, as there are no variables anymore.

I guess it would suffice to return a true expression if there are no variables in that function?

Test case from https://github.com/prismmodelchecker/prism-tests/blob/master/bugfixes/ptaalphabet.nm, translated using PRISM's digital clock conversion.

Model: from_pta.txt

storm compilation error

Hi,

I am trying to install storm on osx. I have tried to use brew and I get the following compilation error:

Last 15 lines from /Users/ochipara/Library/Logs/Homebrew/stormchecker/02.make:
^
/tmp/stormchecker-20190508-86606-mclz9y/storm-1.3.0/src/storm/builder/DdJaniModelBuilder.cpp:902:24: note: in instantiation of member function 'storm::builder::CombinedEdgesSystemComposer<storm::dd::DdType::Sylvan, carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::buildAutomatonDd' requested here
return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast<ActionInstantiations const&>(data), inputEnabledActionIndices);
^
/tmp/stormchecker-20190508-86606-mclz9y/storm-1.3.0/src/storm/builder/DdJaniModelBuilder.cpp:2090:58: note: in instantiation of member function 'storm::builder::CombinedEdgesSystemComposer<storm::dd::DdType::Sylvan, carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::visit' requested here
CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables);
^
/tmp/stormchecker-20190508-86606-mclz9y/storm-1.3.0/src/storm/storage/dd/DdManager.h:68:30: note: declared as a non-template here
Bdd getBddZero() const;
^
4 errors generated.
make[2]: *** [src/storm/CMakeFiles/storm.dir/builder/DdJaniModelBuilder.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[1]: *** [src/storm/CMakeFiles/storm.dir/all] Error 2
make: *** [all] Error 2

Attached is the error log showing additional details from the compilation process. I get the same error if I try to compile from source.

02.make.log

Jani Dd Model Builder builds incorrect model

For this Jani model
I would expect 3 states and a resulting probability of 0.6. The sparse engine and mcsta confirm this. However, the dd engine yields the following:

storm --jani ddbug.jani -jprop -e dd
Storm 1.3.1 (dev)

Date: Tue Oct 15 14:50:27 2019
Command line arguments: --jani ddbug.jani -jprop -e dd
Current working directory: /Users/tim/storm/build/bin

Time for model input parsing: 0.000s.

 WARN (DdJaniModelBuilder.cpp:1521): Guard of an edge in a DTMC overlaps with previous guards.
Time for model construction: 0.012s.

-------------------------------------------------------------- 
Model type: 	DTMC (symbolic)
States: 	5 (4 nodes)
Transitions: 	11 (19 nodes)
Reward Models:  none
Variables: 	rows: 2 meta variables (3 DD variables), columns: 2 meta variables (3 DD variables)
Labels: 	2
   * deadlock -> 1 state(s) (4 nodes)
   * init -> 1 state(s) (4 nodes)
-------------------------------------------------------------- 

Model checking property "1": Pmin=? [F (X = 1)] ...
Result (for initial states): 0.7999998746
Time for model checking: 0.001s.

The warning is a little suspicious, as there are in fact no overlapping guards.
The problem does not occur if we remove the action labels.

Support for z3 version 4.4.1

Dear all,

what is the minimal z3 version that storm currently supports?
In particular, on Ubuntu 18.04 with z3 4.4.1, we get the following error which, I think, stems from the z3 version.

In member function ‘storm::expressions::Expression storm::adapters::Z3ExpressionAdapter::translateExpression(const z3::expr&)’:
.../storm/adapters/Z3ExpressionAdapter.cpp:148:80: error: invalid conversion from ‘storm::adapters::Z3_SIGNED_INTEGER* {aka long long int*}’ to ‘int64_t* {aka long int*}’ [-fpermissive]
if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) {

vector::_M_range_check exception for bounded until in CTMC

When running

bin/storm --prism ctmc-until.sm --prop 'P=? [ !"down" U>=0 "fail_sensors" ]' --prismcompat --constants MAX_COUNT=2

on ctmc-until.sm from the PRISM test suite, I get

...
ERROR (storm.cpp:17): An unexpected exception occurred and caused Storm to terminate. The message of this exception is: vector::_M_range_check: __n (which is 0) >= this->size() (which is 0)

when compiled for release,

...
storm: /home/klein/Projekte/storm/storm-trunk.github/src/storm/logic/BoundedUntilFormula.cpp:19: storm::logic::BoundedUntilFormula::BoundedUntilFormula(const std::shared_ptr<const storm::logic::Formula>&, const std::shared_ptr<const storm::logic::Formula>&, const std::vector<boost::optional<storm::logic::TimeBound> >&, const std::vector<boost::optional<storm::logic::TimeBound> >&, const std::vector<storm::logic::TimeBoundReference>&): Assertion `timeBoundReferences.size() == upperBound.size()' failed.

when compiled with Debug.

Seems to be related to the bounded until.

Function floor in Prism source-file should be of type int

If the function floor and the init statement are used in a prism source file, the parser throws the following error:

ERROR (BaseExpression.cpp:45): Unable to evaluate expression as integer.
ERROR (storm.cpp:14): An exception caused Storm to terminate. The message of the exception is: Unable to evaluate expression as integer.

In the minimal example below we can actually observe two issues. First (1.) if a constant is used in the variable definition and second, if floor is directly used in the definition.

mdp

const int MAX_output_ctr = floor(2.5);

init
  true
endinit

module output_chan
  output_ctr : [0 .. MAX_output_ctr];  // 1.
  //  output_ctr : [0 .. floor(2.5)];  // 2.

  [tick] true -> true;
endmodule

Different output when using a label or the underlying expression

When using storm-pomdp to create a pMC from a POMDP I get different results when I'm using a labelled expression than when I'm just using the expression. To the best of my knowledge, both outputs should be equal.

The label is defined as label "crash" = a=s1;

Command 1: storm-pomdp --prism shields-warehouse/storm-pomdp-model.prism --parametric-drn shields-warehouse/storm-pmdp-model.drn --prop "Pmax=? [ (! \"crash\") U a = 21 ]"

Storm-pomdp 1.3.1 (dev)

Date: Thu Jul 18 14:14:41 2019
Command line arguments: --prism shields-warehouse/storm-pomdp-model.prism --parametric-drn shields-warehouse/storm-pmdp-model.drn --prop 'Pmax=? [ (! "crash") U a = 21 ]'
Current working directory: /home/jeremy/study/internship

Time for model input parsing: 0.210s.

Time for model construction: 0.141s.

-------------------------------------------------------------- 
Model type: 	POMDP (sparse)
States: 	441
Transitions: 	3481
Choices: 	2541
Observations: 	21
Reward Models:  none
State Labels: 	4 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * (a = 21) -> 21 item(s)
   * crash -> 21 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 
Analyzing property 'Pmax=? [!("crash") U (a = 21)]'
Assumming memoryless schedulers.
Transforming memoryless POMDP to pMC... done.
-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	441
Transitions: 	2367
Reward Models:  none
State Labels: 	4 labels
   * deadlock -> 0 item(s)
   * init -> 1 item(s)
   * (a = 21) -> 21 item(s)
   * crash -> 21 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 
Simplifying pMC... done.
-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	402
Transitions: 	2192
Reward Models:  none
State Labels: 	3 labels
   * init -> 1 item(s)
   * (a = 21) -> 1 item(s)
   * crash -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 
Exporting pMC...Write to file shields-warehouse/storm-pmdp-model.drn.
 done.

Command 2: storm-pomdp --prism shields-warehouse/storm-pomdp-model.prism --parametric-drn shields-warehouse/storm-pmdp-model.drn --prop "Pmax=? [ (! (a = s1)) U a = 21 ]"

Storm-pomdp 1.3.1 (dev)

Date: Thu Jul 18 14:16:51 2019
Command line arguments: --prism shields-warehouse/storm-pomdp-model.prism --parametric-drn shields-warehouse/storm-pmdp-model.drn --prop 'Pmax=? [ (! (a = s1)) U a = 21 ]'
Current working directory: /home/jeremy/study/internship

Time for model input parsing: 0.206s.

Time for model construction: 0.134s.

-------------------------------------------------------------- 
Model type: 	POMDP (sparse)
States: 	441
Transitions: 	3336
Choices: 	2441
Observations: 	21
Reward Models:  none
State Labels: 	4 labels
   * deadlock -> 0 item(s)
   * !((a = s1)) -> 420 item(s)
   * init -> 1 item(s)
   * (a = 21) -> 21 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 
Analyzing property 'Pmax=? [!((a = s1)) U (a = 21)]'
Assumming memoryless schedulers.
Transforming memoryless POMDP to pMC...ERROR (ApplyFiniteSchedulerToPomdp.cpp:64): Number of choices must be equal for every state with same number of actions
storm-pomdp: /home/jeremy/study/internship/storm/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp:64: std::unordered_map<unsigned int, std::vector<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA> >, true> > > storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType>::getObservationChoiceWeights(storm::transformer::PomdpFscApplicationMode) const [with ValueType = __gmp_expr<__mpq_struct [1], __mpq_struct [1]>]: Assertion `it == res.end() || it->second.size() == pomdp.getNumberOfChoices(state)' failed.
Aborted (core dumped)

You can find the POMDP file here.

Two tests fail after successfully building Storm 1.3.1 on Ubuntu 18.04 LTS with Gurobi, MathSAT and TBB

I've built Storm 1.3.1 on an Ubuntu 18.04 LTS VM with Gurobi, MathSAT and Intel TBB support successfully, but the model checking test times out and the permissive scheduler test fails, bin/test-permissiveschedulers returns the following:

[==========] Running 1 test from 1 test case.
[----------] Global test environment set-up.
[----------] 1 test from SmtPermissiveSchedulerTest
[ RUN      ] SmtPermissiveSchedulerTest.DieSelection
unknown file: Failure
C++ exception with description "bad_weak_ptr" thrown in the test body.
[  FAILED  ] SmtPermissiveSchedulerTest.DieSelection (2 ms)
[----------] 1 test from SmtPermissiveSchedulerTest (2 ms total)

[----------] Global test environment tear-down
[==========] 1 test from 1 test case ran. (2 ms total)
[  PASSED  ] 0 tests.
[  FAILED  ] 1 test, listed below:
[  FAILED  ] SmtPermissiveSchedulerTest.DieSelection

 1 FAILED TEST

Running bin/test-modelchecker raises CPU load to 100% for 1 core and does not proceed after the first step (no error here, I manually terminated it after around 20 minutes):

[==========] Running 300 tests from 87 test cases.
[----------] Global test environment set-up.
[----------] 5 tests from SparseMdpPcaaMultiObjectiveModelCheckerTest
[ RUN      ] SparseMdpPcaaMultiObjectiveModelCheckerTest.consensus

Here's the output from make test:

Test project /usr/local/bin/storm/build
      Start  1: run-test-abstraction
 1/14 Test  #1: run-test-abstraction .............   Passed   21.79 sec
      Start  2: run-test-adapter
 2/14 Test  #2: run-test-adapter .................   Passed    1.45 sec
      Start  3: run-test-builder
 3/14 Test  #3: run-test-builder .................   Passed  134.49 sec
      Start  4: run-test-logic
 4/14 Test  #4: run-test-logic ...................   Passed    0.16 sec
      Start  5: run-test-modelchecker
 5/14 Test  #5: run-test-modelchecker ............***Timeout 1500.01 sec
      Start  6: run-test-parser
 6/14 Test  #6: run-test-parser ..................   Passed    0.56 sec
      Start  7: run-test-permissiveschedulers
 7/14 Test  #7: run-test-permissiveschedulers ....***Failed    0.13 sec
      Start  8: run-test-solver
 8/14 Test  #8: run-test-solver ..................   Passed    0.80 sec
      Start  9: run-test-storage
 9/14 Test  #9: run-test-storage .................   Passed   48.05 sec
      Start 10: run-test-transformer
10/14 Test #10: run-test-transformer .............   Passed    0.21 sec
      Start 11: run-test-utility
11/14 Test #11: run-test-utility .................   Passed   11.12 sec
      Start 12: run-test-pars-modelchecker
12/14 Test #12: run-test-pars-modelchecker .......   Passed   16.20 sec
      Start 13: run-test-pars-utility
13/14 Test #13: run-test-pars-utility ............   Passed    0.21 sec
      Start 14: run-test-dft-api
14/14 Test #14: run-test-dft-api .................   Passed    1.06 sec

86% tests passed, 2 tests failed out of 14

Total Test time (real) = 1736.44 sec

The VM has got 4 vCPUs with a total of 16 cores and 16GB of RAM, model checking should not have timed out, considering the other tests were quite quick to finish. How would I go about troubleshooting this issue?

Feature Request: Scheduler extraction in step-bounded reachability analysis

Given an MDP in the explicit format, for reachability formulas involving G , F{op}k or U{op}k, the model checking result returns a vector with the maximum probability of satisfying the formulas but not the associated scheduler.

It would be nice to support scheduler extraction for reachability analysis in MDP.

See also this issue: moves-rwth/stormpy#3

Failed test step when installing storm

Hi, I'm trying to install Storm in my MacBook from source. Everything worked, however when I run the test step "make check", it shows that

93% tests passed, 1 tests failed out of 14

Total Test time (real) = 371.69 sec

The following tests FAILED:
11 - run-test-utility (Failed)
Errors while running CTest
make[3]: *** [CMakeFiles/check] Error 8
make[2]: *** [CMakeFiles/check.dir/all] Error 2
make[1]: *** [CMakeFiles/check.dir/rule] Error 2
make: *** [check] Error 2

What might be the reason that fails the test and how to fix the problem?

Thanks

Error when parsing very large integer constants

Hi everyone,

parsing the following prism program with storm

`dtmc
const N = 10000000000;
module chain

c : [0..N] init 0;
f : bool init false;

[] (c < N) -> (0.000000001): (f'=true) + (0.99999999) : (c'=c+1);

endmodule
label "goal" = f=true;`

causes the error

expecting < integer expression >, here:
const N = 10000000000;
^

For N=10^9, however, everything works fine.

Best regards,
Kevin

Gurobi get_target_property with non-existent target

When I change the cmake settings (with ccmake) to enable the use of Gurobi with -DSTORM_USE_GUROBI=ON and -DGUROBI_ROOT=/opt/gurobi702/linux64, I get the following errors when running cmake:

$ cmake ..
CMAKE_INSTALL_DIR: lib/CMake/storm
-- Storm - Building DEBUG version.
-- Storm - Using ccache
-- Storm - Detected operating system Linux.
-- Assuming extension for shared libraries: .so
-- Assuming extension for static libraries: .a
-- Build static libraries.
-- Storm - Using compiler configuration gcc (ccache) 5.4.0.
-- Storm - CXX Flags:  -mpopcnt -std=c++14 -pedantic -Wall -Wextra -Wno-unknown-pragmas -Wno-unused-local-typedefs
-- Storm - CXX Debug Flags: -g
-- Storm - CXX Release Flags: -O3 -DNDEBUG -flto -fprefetch-loop-arrays -ffast-math -fno-finite-math-only -flto -march=native
-- Storm - Build type: DEBUG
-- storm - Using boost 106100 (library version 1_61).
-- storm - Including ExprTk.
-- storm - Including Sparsepp.
-- storm - Including ModernJSON.
-- storm - Linking with Z3. (Z3 version supports optimization)
-- storm - Using system version of glpk.
-- storm - Linking with glpk 4.57
-- storm - Linking with Gurobi.
CMake Error at resources/3rdparty/CMakeLists.txt:179 (add_imported_library):
  add_imported_library Macro invoked with incorrect arguments for macro
  named: add_imported_library
Call Stack (most recent call first):
  CMakeLists.txt:327 (include)


-- storm - Linking with CUDD 3.0.0.
-- storm - Linking with cpptemplate.
-- storm - Use system version of carl.
-- storm - Linking with carl 17.04 (CARL_USE_CLN_NUMBERS: ON).
-- storm - Use system version of xerces.
-- storm - Linking with xercesc.
-- storm - Using shipped version of sylvan.
-- storm - Linking with sylvan.
-- storm - Linking with hwloc .
-- Storm - version is 1.0.0 (0 commits ahead of tag), building from git: 44dc3e7d8ddfe80dadfb2d5d967bef4f9a953477 (dirty: true).
-- Registered with cmake
CMake Error at resources/cmake/macros/imported.cmake:29 (get_target_property):
  get_target_property() called with non-existent target "Gurobi".
Call Stack (most recent call first):
  resources/cmake/macros/export.cmake:12 (export_target)
  CMakeLists.txt:414 (include)


-- Configuring incomplete, errors occurred!
See also "/home/dan/Research/storm/build/CMakeFiles/CMakeOutput.log".
See also "/home/dan/Research/storm/build/CMakeFiles/CMakeError.log".

I no longer get the first error if I add SHARED as an argument to add_imported_library() on line 179 of resources/3rdparty/CMakeLists.txt, but this does not fix the second error.

Negative rewards

When specifying negative rewards in a PRISM model, there is no error message but weird values are computed. According to Christian Hensel, negative rewards shall never be specified.

Installing storm on Amazon AWS

Hello,

I am trying to install storm on an Amazon AWS client, and I am running into errors while executing cmake .. command in the build folder. I am attaching the message on the terminal:

[ec2-user@ip-172-31-14-157 build]$ cmake ..
-- Storm - CMake install dir: /usr/local/lib/CMake/storm
-- Storm - Building RELEASE version.
-- Storm - Could not find ccache.
-- Storm - Detected operating system Linux.
-- Storm - Assuming extension for shared libraries: .so
-- Storm - Assuming extension for static libraries: .a
-- Storm - Build static libraries.
-- Storm - Enabling link-time optimizations.
-- Storm - Using compiler configuration gcc 7.3.1.
CMake Warning at /usr/local/share/cmake-3.7/Modules/FindBoost.cmake:744 (message):
Imported targets not available for Boost version 107000
Call Stack (most recent call first):
/usr/local/share/cmake-3.7/Modules/FindBoost.cmake:848 (_Boost_COMPONENT_DEPENDENCIES)
/usr/local/share/cmake-3.7/Modules/FindBoost.cmake:1435 (_Boost_MISSING_DEPENDENCIES)
resources/3rdparty/CMakeLists.txt:62 (find_package)
CMakeLists.txt:386 (include)

CMake Warning at /usr/local/share/cmake-3.7/Modules/FindBoost.cmake:744 (message):
Imported targets not available for Boost version 107000
Call Stack (most recent call first):
/usr/local/share/cmake-3.7/Modules/FindBoost.cmake:848 (_Boost_COMPONENT_DEPENDENCIES)
/usr/local/share/cmake-3.7/Modules/FindBoost.cmake:1435 (_Boost_MISSING_DEPENDENCIES)
resources/3rdparty/CMakeLists.txt:62 (find_package)
CMakeLists.txt:386 (include)

-- Storm - Using boost 107000 (library version 1_70).
-- Storm - Including ExprTk.
-- Storm - Including Sparsepp.
-- Storm - Including ModernJSON.
-- Could NOT find z3 (missing: Z3_LIBRARY Z3_INCLUDE_DIR)
CMake Warning at resources/3rdparty/CMakeLists.txt:180 (message):
Storm - Z3 not found. Building of Prism/JANI models will not be supported.
Call Stack (most recent call first):
CMakeLists.txt:386 (include)

-- Storm - Using shipped version of glpk.
-- Storm - Linking with glpk 4.57
-- Storm - Linking with CUDD 3.0.0.
CMake Error at resources/3rdparty/CMakeLists.txt:241 (message):
File /home/ec2-user/storm/build/resources/3rdparty/carl/libcarl.so.14.18
does not exist, did you build carl?
Call Stack (most recent call first):
CMakeLists.txt:386 (include)

-- Storm - Found carl using master14 branch.
-- Storm - Use system version of carl.
-- Storm - Linking with preinstalled carl 14.18.10-g2c4f69a1 (include: /home/ec2-user/storm/build/resources/3rdparty/carl_download/source_dir/src, library lib_carl, CARL_USE_CLN_NUMBERS: ON, CARL_USE_GINAC: ON).
-- Storm - Use shipped version of xerces.
-- Storm - Linking with xercesc.
-- Storm - Using shipped version of sylvan.
-- Storm - Linking with sylvan.
-- Storm - Linking with hwloc .
-- Storm - Version is 1.3.1 (dev) (version 1.3.0 + 3 commits), building from git: 4b56fb1 (dirty: false).
-- Registered with cmake
-- Configuring incomplete, errors occurred!

I am also attaching the output from CMakeError.log:

Determining if the pthread_create exist failed with the following output:
Change Dir: /home/ec2-user/storm/build/CMakeFiles/CMakeTmp

Run Build Command:"/usr/bin/gmake" "cmTC_db370/fast"
/usr/bin/gmake -f CMakeFiles/cmTC_db370.dir/build.make CMakeFiles/cmTC_db370.dir/build
gmake[1]: Entering directory /home/ec2-user/storm/build/CMakeFiles/CMakeTmp' Building C object CMakeFiles/cmTC_db370.dir/CheckSymbolExists.c.o /usr/bin/cc -o CMakeFiles/cmTC_db370.dir/CheckSymbolExists.c.o -c /home/ec2-user/storm/build/CMakeFiles/CMakeTmp/CheckSymbolExists.c Linking C executable cmTC_db370 /usr/local/bin/cmake -E cmake_link_script CMakeFiles/cmTC_db370.dir/link.txt --verbose=1 /usr/bin/cc -rdynamic CMakeFiles/cmTC_db370.dir/CheckSymbolExists.c.o -o cmTC_db370 -rdynamic CMakeFiles/cmTC_db370.dir/CheckSymbolExists.c.o: In function main':
CheckSymbolExists.c:(.text+0x16): undefined reference to pthread_create' collect2: error: ld returned 1 exit status gmake[1]: *** [cmTC_db370] Error 1 gmake[1]: Leaving directory /home/ec2-user/storm/build/CMakeFiles/CMakeTmp'
gmake: *** [cmTC_db370/fast] Error 2

File /home/ec2-user/storm/build/CMakeFiles/CMakeTmp/CheckSymbolExists.c:
/* */
#include <pthread.h>

int main(int argc, char** argv)
{
(void)argv;
#ifndef pthread_create
return ((int*)(&pthread_create))[argc];
#else
(void)argc;
return 0;
#endif
}

Determining if the function pthread_create exists in the pthreads failed with the following output:
Change Dir: /home/ec2-user/storm/build/CMakeFiles/CMakeTmp

Run Build Command:"/usr/bin/gmake" "cmTC_6f752/fast"
/usr/bin/gmake -f CMakeFiles/cmTC_6f752.dir/build.make CMakeFiles/cmTC_6f752.dir/build
gmake[1]: Entering directory /home/ec2-user/storm/build/CMakeFiles/CMakeTmp' Building C object CMakeFiles/cmTC_6f752.dir/CheckFunctionExists.c.o /usr/bin/cc -DCHECK_FUNCTION_EXISTS=pthread_create -o CMakeFiles/cmTC_6f752.dir/CheckFunctionExists.c.o -c /usr/local/share/cmake-3.5/Modules/CheckFunctionExists.c Linking C executable cmTC_6f752 /usr/local/bin/cmake -E cmake_link_script CMakeFiles/cmTC_6f752.dir/link.txt --verbose=1 /usr/bin/cc -DCHECK_FUNCTION_EXISTS=pthread_create -rdynamic CMakeFiles/cmTC_6f752.dir/CheckFunctionExists.c.o -o cmTC_6f752 -rdynamic -lpthreads /usr/bin/ld: cannot find -lpthreads collect2: error: ld returned 1 exit status gmake[1]: *** [cmTC_6f752] Error 1 gmake[1]: Leaving directory /home/ec2-user/storm/build/CMakeFiles/CMakeTmp'
gmake: **

Thanks a lot for the help.

Floating point exception in exact Rmin computation

When running
bin/storm --prism robot.nm --prop 'Rmin=? [ F "goal2" ]' --exact
for functionality/verify/mdps/rewards/robot.nm from the PRISM test suite, I get a floating-point exception:

Model checking property R[exp]min=? [F "goal2"] ...
 WARN (MinMaxLinearEquationSolver.cpp:161): Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method.
 WARN (SparseMdpPrctlHelper.cpp:407): Results of reward computation may be too low, because of zero-reward loops.
Floating point exception

Looks like an unhandled division-by-zero in the SparseLU processing.

Might be related to the handling of improper schedulers in Rmin policy iteration?

Bug with Markov Automata PRISM file input

The following file:

ma
 
module M 
 
s:[0..2] init 0;

[](s=0) -> 0.06:(s'=1) + 0.94:(s'=2);

endmodule

when input with storm --prism file.ma returns the following error:

ERROR (MarkovAutomaton.cpp:160): Entries of transition matrix do not sum up to one for (non-Markovian) choice 0 of state 0 (sum is 1). ERROR (storm.cpp:14): An exception caused Storm to terminate. The message of the exception is: Entries of transition matrix do not sum up to one for (non-Markovian) choice 0 of state 0 (sum is 1).

If I change the probabilities to 0.05 & 0.95 or 0.04 & 0.96 for example, the model is successfully built. Additionally, if I change the model at the top of the file from ma to mdp, the model also successfully builds.

Installation via brew fails on OSX 10.13.4

I have troubles to install storm via homebrew. To set up a clean environment, I create a dedicated user account and removed macports temporarily. It seems to be related to Carl (, again). Do you need further information to debug that issue?

homebrew$ brew install stormchecker
==> Installing stormchecker from moves-rwth/storm
==> Installing dependencies for moves-rwth/storm/stormchecker: moves-rwth/misc/carl
==> Installing moves-rwth/storm/stormchecker dependency: moves-rwth/misc/carl
==> Downloading https://github.com/smtrat/carl/archive/17.12.zip
Already downloaded: /Users/homebrew/Library/Caches/Homebrew/carl-17.12.zip
==> cmake /private/tmp/carl-20180418-75318-588i2n/carl-17.12 -DCMAKE_C_FLAGS_RELEASE=-DNDEBUG -DCMAKE_CXX_FLAGS_RELEASE=-DNDEBUG -DCMAKE_INSTALL_PREFIX=/Users/homebrew/bin/homebrew/
==> make install
Last 15 lines from /Users/homebrew/Library/Logs/Homebrew/carl/02.make:
[ 50%] Built target gtest
Scanning dependencies of target gtest_main
[ 75%] Building CXX object googlemock/gtest/CMakeFiles/gtest_main.dir/src/gtest_main.cc.o
[100%] Linking CXX static library libgtest_main.a
[100%] Built target gtest_main
cd /tmp/carl-20180418-75318-e97jjv/resources/src/GTest-EP-build && 
/Users/homebrew/bin/homebrew/Cellar/cmake/3.11.1/bin/cmake -E touch /tmp/carl-20180418-75318-e97jjv/resources/src/GTest-EP-stamp/GTest-EP-build
[  8%] No install step for 'GTest-EP'
cd /tmp/carl-20180418-75318-e97jjv/resources/src/GTest-EP-build && 
/Users/homebrew/bin/homebrew/Cellar/cmake/3.11.1/bin/cmake -E echo_append
cd /tmp/carl-20180418-75318-e97jjv/resources/src/GTest-EP-build && 
/Users/homebrew/bin/homebrew/Cellar/cmake/3.11.1/bin/cmake -E touch /tmp/carl-20180418-75318-e97jjv/resources/src/GTest-EP-stamp/GTest-EP-install
[  8%] Completed 'GTest-EP'
/Users/homebrew/bin/homebrew/Cellar/cmake/3.11.1/bin/cmake -E make_directory /tmp/carl-20180418-75318-e97jjv/CMakeFiles
/Users/homebrew/bin/homebrew/Cellar/cmake/3.11.1/bin/cmake -E touch /tmp/carl-20180418-75318-e97jjv/CMakeFiles/GTest-EP-complete
/Users/homebrew/bin/homebrew/Cellar/cmake/3.11.1/bin/cmake -E touch /tmp/carl-20180418-75318-e97jjv/resources/src/GTest-EP-stamp/GTest-EP-done
[  8%] Built target GTest-EP
make: *** [all] Error 2

If reporting this issue please do so at (not Homebrew/brew or Homebrew/core):
https://github.com/moves-rwth/homebrew-misc/issues

DRN parser does not check validity of the model

The DRN parser currently reads models that are invalid.
For example, a model in which the outgoing probabilities sum to more than one is parsed without any exception. This behaviour is unwanted. In particular, speed should not be a main concern as the DRN parser is slow anyway.

Prism to JANI conversion error: InvalidJaniException: Expression variable 'X' not known in Jani data structures.

When trying to convert the following PRISM model and property to JANI, I get the error shown below.

The model and property are valid PRISM. Adding --globalvars --prismcompat parameters gives the same error. I'm working with the current master version.

Property:

// p_bounded_until_S
Pmin=? [ true U<=10 some_property ]

Model:


mdp

module server

	state : [0..4] init 0;
	some_property: bool init false;
	
	[go] state=0 -> 1:(state'=1);
	[risk] state=1 -> 0.5:(state'=2) + 0.5:(state'=3);
	[safe] state=1 -> 0.6:(state'=0) + 0.3:(state'=2) + 0.1:(state'=3);
	[finish] state=2 -> (state'=2); 
	[close] state=3 -> (state'=3);
	[reset] state=3 -> (state'=0);
	
endmodule

Error:

hans@debian:~/storm/build/bin$ ./storm-conv --prism ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.nm --tojani ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.jani --prop ../../../Documents/testcases/nested_pctl_1/properties.props
Storm-conv 1.3.1 (dev)

Date: Tue Apr  9 09:10:34 2019
Command line arguments: --prism ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.nm --tojani ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.jani --prop ../../../Documents/testcases/nested_pctl_1/properties.props
Current working directory: /home/hans/storm/build/bin

Parsing PRISM input ...  done. (0.001s seconds).
Converting PRISM Program to JANI model ...  done. (0.000s seconds).
Exporting JANI model ... ERROR (JSONExporter.cpp:683): Expression variable 'some_property' not known in Jani data structures.
ERROR (storm-conv.cpp:335): An exception caused Storm-conv to terminate. The message of the exception is: InvalidJaniException: Expression variable 'some_property' not known in Jani data structures.

Can not compute Boolean combination of long-run probability thresholds

When running
bin/storm --prism HG-04.pm --prop 'S<=0.166667 [ x=7 ]&S>=0.166665 [ x=7 ]'
on HG-04.pm from the PRISM test suite, I get:

...
Model checking property (LRA<=166667/1000000 [(x = 7)] & LRA>=33333/200000 [(x = 7)]) ...
ERROR (AbstractModelChecker.cpp:199): Expected qualitative results.
ERROR (storm.cpp:14): An exception caused Storm to terminate. The message of the exception is: Expected qualitative results.

For a single S-property with threshold, I get a Boolean result.

As far as I can see, the condition at

storm/src/storm/modelchecker/AbstractModelChecker.cpp

Line 265 in e3eb667

if (checkTask.isBoundSet()) {

is somehow false, so the result does not get converted to a qualitative result.

storm does not handle absolute property paths properly

When calling storm with something like

storm --prism /Users/linda/some_model --prop /Users/linda/some_props
it fails with
ERROR (FormulaParser.cpp:101): Could not parse formula.
ERROR (storm.cpp:14): An exception caused Storm to terminate. The message of the exception is: Could not parse formula

However, everything works fine when using a relative path for the properties file

storm --prism /Users/linda/some_model --prop ./some_props
or when naming the properties file with some arbitrary suffix
storm --prism /Users/linda/some_model --prop /Users/linda/some_props.abcd
For the models file, every format seems to be OK.

I guess this comes from storm interpreting '/Users/linda/some_props' as a property, not a path to a properties file?

MDP support

Hi,

I am interested in checking time-bounded reachability for an mdp model. An example is shown below:

mdp
const double ps;
module active
s : [0 .. 3] init 0;
[] s = 0 -> ps : (s'=1) + (1 - ps) : (s'=0);
[] s = 0 -> ps : (s'=2) + (1 - ps) : (s'=0);
[] s = 1 -> ps : (s'=3) + (1 - ps) : (s'=1);
[] s = 2 -> ps : (s'=3) + (1 - ps) : (s'=1);
endmodule

rewards "progress"
s = 0: 0;
s = 1: 1;
s = 2: 1;
s = 3: 2;
endrewards

I want to check system properties of the form: P=? [true U<=5 (s = 3)]. Is there support in storm built for evaluating such properties?

jit always links with carl

Jit currently seems to link with all the glory of Carl, which is not necessary if ValueType is double. Fixing this should reduce build times for jit.

Feature request: Option to disable graph-preserving constraints

In some use cases it may not be desirable to preserve the graph of a pMC.

For example, when using storm-pars go check the property P=? [ G ! crash ] on the following model

state 0 init
	action 0
		0 : p1
		1 : 1 - p1
state 1 crash
	action 0
		1 : 1

The result of the query is 0 (as is shown below).

$ storm-pars --prop "P=? [ G ! \"crash\" ]" --explicit-drn storm-pmc-model-test.drn --resultfile storm-pmc-test-results.txt
Storm-pars 1.3.1 (dev)

Date: Mon Jul 22 17:23:04 2019
Command line arguments: --prop 'P=? [ G ! "crash" ]' --explicit-drn storm-pmc-model-test.drn --resultfile storm-pmc-test-results.txt
Current working directory: /home/jeremy/study/internship

Time for model construction: 0.018s.

-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	2
Transitions: 	3
Reward Models:  none
State Labels: 	2 labels
   * crash -> 1 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "1": P=? [G !("crash")] ...
Result (initial states): 0
Time for model checking: 0.007s.

Write to file storm-pmc-test-results.txt.

The result is 0 since a graph-preserving constrain prohibits p1 = 1. However, when synthesizing an optimal strategy for this problem it may not be necessary to keep the transition from state 0 to 1 as a possibility.

There is of course a workaround by using z3 only on the well-formedness constraints, but it would be nice if storm-pars also offered the possibility to disable the graph-preserving constraints. In addition, it may not always be easy to determine which formula to optimize under these constraints.

My theoretical knowledge is not deep enough to know if this causes problems in some other cases (since it may cause graph components to become disconnected).

Problems with changes to commit #3f0afe

With regards to the commit 3f0afe9, I'm not sure why it was necessary as ExprTk already supports '_' and '. in symbol names.

More information can be found here:
https://github.com/ArashPartow/exprtk/blob/master/readme.txt#L4055

The change made in the commit will cause problems with expressions. As a simple example the following expression: ".123" will result in two tokens which are a symbol: "." and a number: "123" neither of which is correct.

In exact mode, MDP result is not exact

For lec15mdp.nm from the PRISM test suite (stable branch):

storm --prism ./pmc/lec15mdp.nm --prop 'Pmax=? [ F s=1|s=3|s=4 ]'  --exact --verbose
Storm 1.1.1 (dev)

[...]
Model checking property Pmax=? [F (((s = 1) | (s = 3)) | (s = 4))] ...
 INFO (SparseMdpPrctlHelper.cpp:125): Found 4 'no' states.
 INFO (SparseMdpPrctlHelper.cpp:126): Found 1 'yes' states.
 INFO (SparseMdpPrctlHelper.cpp:127): Found 1 'maybe' states.
 INFO (IterativeMinMaxLinearEquationSolver.cpp:421): Iterative solver converged after 27 iterations.
 INFO (cli.cpp:622): Result (for initial states):
Result (for initial states):  INFO (cli.cpp:564): 11175859456989514707/14901161193847656250 (approx. 0.749999)
11175859456989514707/14901161193847656250 (approx. 0.7499992324) INFO (cli.cpp:610):

When I select policy iteration as the minmax method, the correct value is obtained:

storm --prism ./pmc/lec15mdp.nm --prop 'Pmax=? [ F s=1|s=3|s=4 ]'  --exact --method pi --verbose

Storm 1.1.1 (dev)

[...]
Model checking property Pmax=? [F (((s = 1) | (s = 3)) | (s = 4))] ...
 INFO (SparseMdpPrctlHelper.cpp:125): Found 4 'no' states.
 INFO (SparseMdpPrctlHelper.cpp:126): Found 1 'yes' states.
 INFO (SparseMdpPrctlHelper.cpp:127): Found 1 'maybe' states.
 INFO (EigenLinearEquationSolver.cpp:321): Solving linear equation system (1 rows) with with rational numbers using LU factorization (Eigen library).
 INFO (EigenLinearEquationSolver.cpp:321): Solving linear equation system (1 rows) with with rational numbers using LU factorization (Eigen library).
 INFO (IterativeMinMaxLinearEquationSolver.cpp:421): Iterative solver converged after 2 iterations.
 INFO (cli.cpp:622): Result (for initial states):
Result (for initial states):  INFO (cli.cpp:564): 3/4 (approx. 0.75)
3/4 (approx. 0.75) INFO (cli.cpp:610):

My guess would be that somehow the standard value iteration setting is not changed to policy iteration?

Maximum expected rewards not calculated correctly with non-transient variables in Jani model

In the following Jani model, we get an incorrect result for the maximum expected reward when the reward variable is not declared as a transient variable. When the reward is not declared as transient, Storm reports that the maximum expected reward is 0.

Conceptual Image:

Command line arguments:

--jani ../../../Documents/testcases/bug_storm.jani --janiproperty '--minmax:method' svi
Current working directory: /home/hans/storm/build/bin

Jani model where reward is not transient:

{
	"jani-version": 1,
	"name": "bug_storm",
	"type": "mdp",
	"variables": [
		{
			"name": "reward",
			"type": "int",
			"initial-value": 0
		},
		{
			"name": "goal",
			"type": "bool",
			"initial-value": false
		}
	],
	"properties": [ {
		"name": "Test",
		"expression": {
			"op": "filter",
			"fun": "max",
			"values": {
				"op": "Emax",
				"exp": "reward",
				"accumulate": [
					"steps"
				],
				"reach": "goal"
			},
			"states": {
				"op": "initial"
			}
		}
	} ],
	"automata": [
		{
			"name": "Main",
			"locations": [
				{
					"name": "loc_1"
				},
				{
					"name": "loc_0"
				}
			],
			"initial-locations": [ "loc_1" ],
			"edges": [
				{
					"location": "loc_1",
					"destinations": [
						{
							"location": "loc_0",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							},
							"assignments": [
								{
									"ref": "reward",
									"value": 1
								},
								{
									"ref": "goal",
									"value": true
								}
							]
						},
						{
							"location": "loc_0",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							},
							"assignments": [ {
								"ref": "goal",
								"value": true
							} ]
						}
					]
				}
			]
		}
	],
	"system": {
		"elements": [ {
			"automaton": "Main"
		} ]
	}
}

Jani model where reward is transient:

{
	"jani-version": 1,
	"name": "bug_storm",
	"type": "mdp",
	"variables": [
		{
			"name": "reward",
			"type": "int",
			"initial-value": 0,
			"transient": true
		},
		{
			"name": "goal",
			"type": "bool",
			"initial-value": false
		}
	],
	"properties": [ {
		"name": "Test",
		"expression": {
			"op": "filter",
			"fun": "max",
			"values": {
				"op": "Emax",
				"exp": "reward",
				"accumulate": [
					"steps"
				],
				"reach": "goal"
			},
			"states": {
				"op": "initial"
			}
		}
	} ],
	"automata": [
		{
			"name": "Main",
			"locations": [
				{
					"name": "loc_1"
				},
				{
					"name": "loc_0"
				}
			],
			"initial-locations": [ "loc_1" ],
			"edges": [
				{
					"location": "loc_1",
					"destinations": [
						{
							"location": "loc_0",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							},
							"assignments": [
								{
									"ref": "reward",
									"value": 1
								},
								{
									"ref": "goal",
									"value": true
								}
							]
						},
						{
							"location": "loc_0",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							},
							"assignments": [ {
								"ref": "goal",
								"value": true
							} ]
						}
					]
				}
			]
		}
	],
	"system": {
		"elements": [ {
			"automaton": "Main"
		} ]
	}
}

Make check fails for 3 tests because of z3

run-test-builder, run-test-modelchecker, run-test-storage was raising exception as to child process killed.

Improve performance of ExpressionEvaluator for RationalFunction

Parsing of RationalFunction in the DRN format is slow.

Profiling revealed that the main issue lies in the following line:

storm/src/storm-parsers/parser/ValueParser.cpp

Line 23 in 2433671

    
           storm::RationalFunction rationalFunction = evaluator.asRational(parser.parseFromString(value));

For an example profiling run, 97.5% of the total time was spent in this line. Out of this time, 78.4% was spent in ExpressionEvaluator::asRational and 18.8% in ExpressionParser::parseFromString.

Using the placeholders introduced in 8b77f7f did shorten the parsing time by a factor of 100 for some files, because we only need to parse each RationalFunction once. For the moment this helps, but in the long term we should improve the performance of the ExpressionEvalulator.

Error building Z3ExpressionAdapter

I hope this is the righ forum to ask for this kind of help in.

I am trying to build storm, but I getting compilation errors. I have attached output of cmake .. and make binaries below.

cmake outputt
make binaries output

The problem appears to be Z3ExpressionAdapter.

I have tried to use g++ version 5.4 instead of gcc 8, but the same problem appears. I have z3 version 4.7.1 installed.

Cannot convert unterminated properties

The file below is a valid PRISM property file. However when trying to convert it with storm we get an error saying that formula could not be parsed.

In a PRISM property file, properties aren't required to be seperated by an ';'. It seems as the converter has this as an (implicit) requirement.

Properties

// property_1
Pmin=? [ F state = 1 ]

// property_2
Pmin=? [ F state = 2 ]

Error:

hans@debian:~/storm/build/bin$ ./storm-conv --prism ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.nm --tojani ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.jani --prop ../../../Documents/testcases/nested_pctl_1/properties.props
Storm-conv 1.3.1 (dev)

Date: Tue Apr  9 09:44:05 2019
Command line arguments: --prism ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.nm --tojani ../../../Documents/testcases/nested_pctl_1/prism_pctl_benchmark.jani --prop ../../../Documents/testcases/nested_pctl_1/properties.props
Current working directory: /home/hans/storm/build/bin

Parsing PRISM input ... ERROR (FormulaParser.cpp:91): Could not parse formula.
ERROR (storm-conv.cpp:338): An unexpected exception occurred and caused Storm-conv to terminate. The message of this exception is: std::exception

Missing exportJani module

In previous releases, there was an exportJani module with --jani-output option, in the new (1.3.0) version I can't find it. I used it with --prism2jani option to convert my prism models into jani language.

What should I do? The prism2jani option is still available, but it seems it has no effect standing by alone.

NaN probability from constant

(with Linda Leuschner)

Consider the following PRISM DTMC:

dtmc

const double p  = pow(1 - 1E-7, 50);

module error
x : [0..2] init 0;

[] true  ->
     0.5 : true
  +  0.5 : (x' = 1)
  +  p*0 : (x' = 2);
endmodule

With the explicit engine, this results in a non-stochastic matrix, as the p*0 expression is translated to NaN during model building. If one plugs in the pow(...) expression directly in the transition, i.e.,

  +  pow(1 - 1E-7, 50)*0 : (x' = 2);

everything works fine. Exact evaluation of both variants generates the expected model as well.

From some debugging it looks like the constant expression is simplified to a rational number (RationalLiteralExpression, the value looks fine) and then somehow in the conversion to double / evaluation of p*0 something goes wrong. The *0 is not necessary for triggering this bug, p and 1-p as the transition probabilities are both evaluated to NaN as well... The value of p is ~0.999995, so there should be no problem with storage as a double. However, as a rational number, p has a large numerator and denominator.

Apart from fixing the concrete evaluation bug, it would probably make sense to add checks that the likelihood values generated in the model builders are not one of the infinities or NaN.

SparseMatrix: trivialRowGrouping & rowGroupIndices logic

The SparseMatrix ctor initializes trivialRowGroupings as !rowGroupIndices. Clearly the direction ¬rowGroupIndices ⇒ trivialRowGroupings is sound, but the other direction is not (i.e., it is possible and seemingly allowed to have a “custom” yet trivial row grouping).

As a result, trivialRowGroupings is currently sometimes falsely negative (e.g., model instantiator DTMCs).

I see the following possibilities:

Put the burden on the caller by documenting that the passed rowGroupIndices must be non-trivial, or by explicitly passing the flag.
Actually check whether the given row groups are trivial. This raises a further question:
- What is the relationship between rowCount == columnCount and trivialRowGroupings? Are terminal states allowed?

[Build System] libclang/image not found

The following message occurs on Mac Os during building, without explanation.

dyld: Library not loaded: @rpath/libclang.dylib
Referenced from: /usr/local/bin/doxygen
Reason: image not found

State labels in explicit-drn are parsed incorrectly

When using storm-pomdp to transform a POMDP to a pMC without (user created) labels, states in the resulting explicit-drn file will be labeled with the expression from the property (e.g. when using [F a = b] as a prop, a state in the resulting file may be labeled with (a = b).

When the resulting file is parsed by storm-pars, the parentheses are not taken into account. Alternatively, this could be considered a bug in storm-pomdp (since it introduces the spaces) or it can be considered bad practice not to use labels.

For example (is used a = s1 in the prop):

$ storm-pars --explicit-drn shields-warehouse/storm-pmc-g-no-crash.drn
Storm-pars 1.3.1 (dev)

Date: Thu Jul 18 17:33:53 2019
Command line arguments: --explicit-drn shields-warehouse/storm-pmc-g-no-crash.drn
Current working directory: /home/jeremy/study/internship

Time for model construction: 1.946s.

-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	441
Transitions: 	2457
Reward Models:  none
State Labels: 	4 labels
   * s1) -> 420 item(s)
   * init -> 1 item(s)
   * (a -> 420 item(s)
   * != -> 420 item(s)
Choice Labels: 	none
--------------------------------------------------------------

I can add more info/source files if it's needed.

(Counter)Example Generation

The tool paper "A Storm is Coming: A Modern Probabilistic Model Checker" describes a counterex engine (cp. Fig. 1), which is currently neither documented online nor available for use with the -e switch.

I would like to obtain examples of paths/states where a verified property either holds or is violated, especially in a non-deterministic MDP.
Is the aforementioned engine implemented and could be used for this purpose?
If not, what other approaches could lead to solving this issue, which data is either already available or could be exposed by Storm that could help with this cause?

Segfault when checking always property with nesting

Problem:
When checking always properties with nesting, storm produces a segfault. I did not obtain segfaults when checking similar eventually properties.

Model:

Command Line Arguments:
/home/hans/storm/build/bin# ./storm --jani ../../../Documents/testcases/nested_pctl_1/always.jani --janiproperty

Example Property Which Crashes:
Pmin([] (Pmin(<> (global_state == 1)) >= 0.5));

JANI File - example property

{
	"jani-version": 1,
	"name": "always",
	"type": "mdp",
	"features": [ "derived-operators" ],
	"actions": [
		{
			"name": "start"
		},
		{
			"name": "finish"
		},
		{
			"name": "close"
		},
		{
			"name": "reset"
		},
		{
			"name": "risk"
		},
		{
			"name": "safe"
		}
	],
	"variables": [ {
		"name": "global_state",
		"type": "int",
		"initial-value": 0
	} ],
	"properties": [
		{
			"name": "p_ap_eq",
			"expression": {
				"op": "filter",
				"fun": "min",
				"values": {
					"op": "Pmin",
					"exp": {
						"op": "G",
						"exp": {
							"op": "≥",
							"left": {
								"op": "Pmin",
								"exp": {
									"op": "F",
									"exp": {
										"op": "=",
										"left": "global_state",
										"right": 1
									}
								}
							},
							"right": {
								"op": "/",
								"left": 1,
								"right": 2
							}
						}
					}
				},
				"states": {
					"op": "initial"
				}
			}
		}
	],
	"automata": [
		{
			"name": "Server",
			"locations": [
				{
					"name": "loc_1"
				},
				{
					"name": "loc_26"
				},
				{
					"name": "loc_31"
				},
				{
					"name": "loc_30"
				},
				{
					"name": "loc_29"
				},
				{
					"name": "loc_28"
				},
				{
					"name": "loc_27"
				}
			],
			"initial-locations": [ "loc_1" ],
			"variables": [ {
				"name": "state",
				"type": "int",
				"initial-value": 0
			} ],
			"edges": [
				{
					"location": "loc_1",
					"action": "start",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 0
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 1
							},
							{
								"ref": "global_state",
								"value": 1
							}
						]
					} ]
				},
				{
					"location": "loc_1",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 1
						}
					},
					"destinations": [
						{
							"location": "loc_27",
							"probability": {
								"exp": {
									"op": "/",
									"left": 3,
									"right": 5
								}
							}
						},
						{
							"location": "loc_28",
							"probability": {
								"exp": {
									"op": "/",
									"left": 3,
									"right": 10
								}
							}
						},
						{
							"location": "loc_29",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 10
								}
							}
						}
					]
				},
				{
					"location": "loc_1",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 1
						}
					},
					"destinations": [
						{
							"location": "loc_30",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							}
						},
						{
							"location": "loc_31",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							}
						}
					]
				},
				{
					"location": "loc_1",
					"action": "finish",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 2
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 2
							},
							{
								"ref": "global_state",
								"value": 2
							}
						]
					} ]
				},
				{
					"location": "loc_1",
					"action": "close",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 3
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 3
							},
							{
								"ref": "global_state",
								"value": 3
							}
						]
					} ]
				},
				{
					"location": "loc_1",
					"action": "reset",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 3
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 0
							},
							{
								"ref": "global_state",
								"value": 0
							}
						]
					} ]
				},
				{
					"location": "loc_26",
					"action": "start",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 0
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 1
							},
							{
								"ref": "global_state",
								"value": 1
							}
						]
					} ]
				},
				{
					"location": "loc_26",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 1
						}
					},
					"destinations": [
						{
							"location": "loc_27",
							"probability": {
								"exp": {
									"op": "/",
									"left": 3,
									"right": 5
								}
							}
						},
						{
							"location": "loc_28",
							"probability": {
								"exp": {
									"op": "/",
									"left": 3,
									"right": 10
								}
							}
						},
						{
							"location": "loc_29",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 10
								}
							}
						}
					]
				},
				{
					"location": "loc_26",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 1
						}
					},
					"destinations": [
						{
							"location": "loc_30",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							}
						},
						{
							"location": "loc_31",
							"probability": {
								"exp": {
									"op": "/",
									"left": 1,
									"right": 2
								}
							}
						}
					]
				},
				{
					"location": "loc_26",
					"action": "finish",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 2
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 2
							},
							{
								"ref": "global_state",
								"value": 2
							}
						]
					} ]
				},
				{
					"location": "loc_26",
					"action": "close",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 3
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 3
							},
							{
								"ref": "global_state",
								"value": 3
							}
						]
					} ]
				},
				{
					"location": "loc_26",
					"action": "reset",
					"guard": {
						"exp": {
							"op": "=",
							"left": "state",
							"right": 3
						}
					},
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 0
							},
							{
								"ref": "global_state",
								"value": 0
							}
						]
					} ]
				},
				{
					"location": "loc_31",
					"action": "risk",
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 3
							},
							{
								"ref": "global_state",
								"value": 3
							}
						]
					} ]
				},
				{
					"location": "loc_30",
					"action": "risk",
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 2
							},
							{
								"ref": "global_state",
								"value": 2
							}
						]
					} ]
				},
				{
					"location": "loc_29",
					"action": "safe",
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 3
							},
							{
								"ref": "global_state",
								"value": 3
							}
						]
					} ]
				},
				{
					"location": "loc_28",
					"action": "safe",
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 2
							},
							{
								"ref": "global_state",
								"value": 2
							}
						]
					} ]
				},
				{
					"location": "loc_27",
					"action": "safe",
					"destinations": [ {
						"location": "loc_26",
						"assignments": [
							{
								"ref": "state",
								"value": 0
							},
							{
								"ref": "global_state",
								"value": 0
							}
						]
					} ]
				}
			]
		}
	],
	"system": {
		"elements": [ {
			"automaton": "Server"
		} ],
		"syncs": [
			{
				"synchronise": [ "start" ],
				"result": "start"
			},
			{
				"synchronise": [ "finish" ],
				"result": "finish"
			},
			{
				"synchronise": [ "close" ],
				"result": "close"
			},
			{
				"synchronise": [ "reset" ],
				"result": "reset"
			},
			{
				"synchronise": [ "risk" ],
				"result": "risk"
			},
			{
				"synchronise": [ "safe" ],
				"result": "safe"
			}
		]
	}
}

JANI File - complete list of properties I was trying to check

{ "jani-version": 1, "name": "always", "type": "mdp", "features": [ "derived-operators" ], "actions": [ { "name": "start" }, { "name": "finish" }, { "name": "close" }, { "name": "reset" }, { "name": "risk" }, { "name": "safe" } ], "variables": [ { "name": "global_state", "type": "int", "initial-value": 0 } ], "properties": [ { "name": "p_eventually_true", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": true } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_true", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": true }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_eventually_false", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": false } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_false", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": false }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_ap_eq", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 1 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_ap_var", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": false } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_not", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "≠", "left": "global_state", "right": 1 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 1 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min_bounded", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 1 }, "step-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min_s", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "<", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 2 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min_se", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≤", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min_l", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": ">", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 4 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min_le", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_min_e", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "=", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_max_s", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "<", "left": { "op": "Pmax", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_max_se", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≤", "left": { "op": "Pmax", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_max_l", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": ">", "left": { "op": "Pmax", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_max_le", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmax", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_max_e", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "=", "left": { "op": "Pmax", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_AF", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "∀", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } } } }, "states": { "op": "initial" } } }, { "name": "p_AG", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "∀", "exp": { "op": "G", "exp": { "op": "=", "left": "global_state", "right": 3 } } } } }, "states": { "op": "initial" } } }, { "name": "p_EF", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "∃", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 3 } } } } }, "states": { "op": "initial" } } }, { "name": "p_EG", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "∃", "exp": { "op": "G", "exp": { "op": "=", "left": "global_state", "right": 3 } } } } }, "states": { "op": "initial" } } }, { "name": "p_bounded_until_S", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": true, "right": false, "step-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_bounded_until_T", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": true, "right": false, "time-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_bounded_until_X", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": true, "right": false, "step-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_unbounded_until_left_variable_and_true", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": { "op": "=", "left": "global_state", "right": 3 }, "right": true } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_unbounded_until_left_variable_and_false", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": { "op": "=", "left": "global_state", "right": 3 }, "right": false } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_unbounded_until_left_true", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": true, "right": false } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_unbounded_until_left_false", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "U", "left": false, "right": false } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_bounded_finally_S", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 1 }, "step-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_bounded_finally_T", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 1 }, "time-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } }, { "name": "p_bounded_finally_X", "expression": { "op": "filter", "fun": "min", "values": { "op": "Pmin", "exp": { "op": "G", "exp": { "op": "≥", "left": { "op": "Pmin", "exp": { "op": "F", "exp": { "op": "=", "left": "global_state", "right": 1 }, "step-bounds": { "upper": 5 } } }, "right": { "op": "/", "left": 1, "right": 2 } } } }, "states": { "op": "initial" } } } ], "automata": [ { "name": "Server", "locations": [ { "name": "loc_1" }, { "name": "loc_26" }, { "name": "loc_31" }, { "name": "loc_30" }, { "name": "loc_29" }, { "name": "loc_28" }, { "name": "loc_27" } ], "initial-locations": [ "loc_1" ], "variables": [ { "name": "state", "type": "int", "initial-value": 0 } ], "edges": [ { "location": "loc_1", "action": "start", "guard": { "exp": { "op": "=", "left": "state", "right": 0 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 1 }, { "ref": "global_state", "value": 1 } ] } ] }, { "location": "loc_1", "guard": { "exp": { "op": "=", "left": "state", "right": 1 } }, "destinations": [ { "location": "loc_27", "probability": { "exp": { "op": "/", "left": 3, "right": 5 } } }, { "location": "loc_28", "probability": { "exp": { "op": "/", "left": 3, "right": 10 } } }, { "location": "loc_29", "probability": { "exp": { "op": "/", "left": 1, "right": 10 } } } ] }, { "location": "loc_1", "guard": { "exp": { "op": "=", "left": "state", "right": 1 } }, "destinations": [ { "location": "loc_30", "probability": { "exp": { "op": "/", "left": 1, "right": 2 } } }, { "location": "loc_31", "probability": { "exp": { "op": "/", "left": 1, "right": 2 } } } ] }, { "location": "loc_1", "action": "finish", "guard": { "exp": { "op": "=", "left": "state", "right": 2 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 2 }, { "ref": "global_state", "value": 2 } ] } ] }, { "location": "loc_1", "action": "close", "guard": { "exp": { "op": "=", "left": "state", "right": 3 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 3 }, { "ref": "global_state", "value": 3 } ] } ] }, { "location": "loc_1", "action": "reset", "guard": { "exp": { "op": "=", "left": "state", "right": 3 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 0 }, { "ref": "global_state", "value": 0 } ] } ] }, { "location": "loc_26", "action": "start", "guard": { "exp": { "op": "=", "left": "state", "right": 0 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 1 }, { "ref": "global_state", "value": 1 } ] } ] }, { "location": "loc_26", "guard": { "exp": { "op": "=", "left": "state", "right": 1 } }, "destinations": [ { "location": "loc_27", "probability": { "exp": { "op": "/", "left": 3, "right": 5 } } }, { "location": "loc_28", "probability": { "exp": { "op": "/", "left": 3, "right": 10 } } }, { "location": "loc_29", "probability": { "exp": { "op": "/", "left": 1, "right": 10 } } } ] }, { "location": "loc_26", "guard": { "exp": { "op": "=", "left": "state", "right": 1 } }, "destinations": [ { "location": "loc_30", "probability": { "exp": { "op": "/", "left": 1, "right": 2 } } }, { "location": "loc_31", "probability": { "exp": { "op": "/", "left": 1, "right": 2 } } } ] }, { "location": "loc_26", "action": "finish", "guard": { "exp": { "op": "=", "left": "state", "right": 2 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 2 }, { "ref": "global_state", "value": 2 } ] } ] }, { "location": "loc_26", "action": "close", "guard": { "exp": { "op": "=", "left": "state", "right": 3 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 3 }, { "ref": "global_state", "value": 3 } ] } ] }, { "location": "loc_26", "action": "reset", "guard": { "exp": { "op": "=", "left": "state", "right": 3 } }, "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 0 }, { "ref": "global_state", "value": 0 } ] } ] }, { "location": "loc_31", "action": "risk", "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 3 }, { "ref": "global_state", "value": 3 } ] } ] }, { "location": "loc_30", "action": "risk", "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 2 }, { "ref": "global_state", "value": 2 } ] } ] }, { "location": "loc_29", "action": "safe", "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 3 }, { "ref": "global_state", "value": 3 } ] } ] }, { "location": "loc_28", "action": "safe", "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 2 }, { "ref": "global_state", "value": 2 } ] } ] }, { "location": "loc_27", "action": "safe", "destinations": [ { "location": "loc_26", "assignments": [ { "ref": "state", "value": 0 }, { "ref": "global_state", "value": 0 } ] } ] } ] } ], "system": { "elements": [ { "automaton": "Server" } ], "syncs": [ { "synchronise": [ "start" ], "result": "start" }, { "synchronise": [ "finish" ], "result": "finish" }, { "synchronise": [ "close" ], "result": "close" }, { "synchronise": [ "reset" ], "result": "reset" }, { "synchronise": [ "risk" ], "result": "risk" }, { "synchronise": [ "safe" ], "result": "safe" } ] } }

Infinite loop in checkIfECWithChoiceExists?

When running

bin/storm --prism simple4.nm --prop 'multi(R{"R1"}min=? [ C ], R{"R2"}>=0 [ C ])'

for multi-general/simple4.nm from the PRISM test suite, it looks like the preprocessing, in particular the loop at

storm/src/storm/utility/graph.cpp

Line 170 in beb80cc

while (!candidateStates.empty()) {

in graph::checkIfECWithChoiceExists gets stuck in an infinite loop.

Failed test when installing stormpy in Mac OS X

Hi, I got the following error message when running the test step after installing stormpy. I suspect that the error may have something to do the python version. My system is Mac OS X 10.13.4, which has a default Python version 2.7.14 and cannot be removed (as required by the system). But I have installed Python 3.6 separately. When I install strompy, I used "python3" command. However, the test session is using python 2.7.14. Is there a way to config stormpy and let python3 be the default version?

$ py.test tests/
============================= test session starts ==============================
platform darwin -- Python 2.7.14, pytest-3.5.0, py-1.5.3, pluggy-0.6.0
rootdir: /Users/lf291/workspace/stormpy, inifile: setup.cfg
collected 0 items / 1 errors

==================================== ERRORS ====================================
______________________________ ERROR collecting _______________________________
/usr/local/lib/python2.7/site-packages/py/_path/common.py:377: in visit
for x in Visitor(fil, rec, ignore, bf, sort).gen(self):
/usr/local/lib/python2.7/site-packages/py/_path/common.py:419: in gen
if p.check(dir=1) and (rec is None or rec(p))])
/usr/local/lib/python2.7/site-packages/_pytest/main.py:434: in _recurse
ihook = self.gethookproxy(path)
/usr/local/lib/python2.7/site-packages/_pytest/main.py:338: in gethookproxy
my_conftestmodules = pm._getconftestmodules(fspath)
/usr/local/lib/python2.7/site-packages/_pytest/config.py:348: in _getconftestmodules
mod = self._importconftest(conftestpath)
/usr/local/lib/python2.7/site-packages/_pytest/config.py:376: in _importconftest
raise ConftestImportFailure(conftestpath, sys.exc_info())
E ConftestImportFailure: ImportError('No module named stormpy._config',)
E File "/usr/local/lib/python2.7/site-packages/pytest/assertion/rewrite.py", line 213, in load_module
E py.builtin.exec(co, mod.dict)
E File "/usr/local/lib/python2.7/site-packages/py/builtin.py", line 221, in exec
E exec2(obj, globals, locals)
E File "", line 7, in exec2
E File "/Users/lf291/workspace/stormpy/tests/dft/conftest.py", line 1, in
E from configurations import has_dft
E File "/Users/lf291/workspace/stormpy/tests/configurations.py", line 3, in
E import stormpy._config as config
!!!!!!!!!!!!!!!!!!! Interrupted: 1 errors during collection !!!!!!!!!!!!!!!!!!!!
=========================== 1 error in 0.19 seconds ============================

Constants defined in a properties file can not be parsed

When defining a constant in a properties file, this can not be parsed. For example, when calling
storm --prism ./model.prism --prop ./props.prop
on the model

dtmc
const double p = 0.4;
const int N = 5;

module one
x: bool init true;
num_rounds : [0..N] init 0;

[a] x & (num_rounds<N) -> p  : (num_rounds' = num_rounds+1) 
                     + (1-p) : (x' = false) & (num_rounds' = num_rounds+1);
[a] x & (num_rounds=N) -> p  : true 
                     + (1-p) : (x' = false);
endmodule

and the properties file

const int k=3;
P=? [F num_rounds = k];

the error message "ERROR (FormulaParser.cpp:101): Could not parse formula." arises, but it works fine, when the properties file is given as

const int k;
P=? [F num_rounds = k];

and the constant k is specified via command line.

storm 1.0.1 / stable macOS build error

$ ninja
[95/1187] Performing download step (git clone) for 'l3pp_ext'
Cloning into 'l3pp'...
Note: checking out 'e4f8d7fe6c328849aff34d2dfd6fd592c14070d5'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by performing another checkout.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -b with the checkout command again. Example:

  git checkout -b <new-branch-name>

HEAD is now at e4f8d7f... Fix some references to log4carl
[263/1187] Performing configure step for 'sylvan'
-- sylvan configure command succeeded.  See also /Users/macbook/Code/i2/storm/build/sylvan/src/sylvan-stamp/sylvan-configure-*.log
[383/1187] Performing configure step for 'googletest'
-- googletest configure command succeeded.  See also /Users/macbook/Code/i2/storm/build/googletest-prefix/src/googletest-stamp/googletest-configure-*.log
[591/1187] Performing build step for 'googletest'
-- googletest build command succeeded.  See also /Users/macbook/Code/i2/storm/build/googletest-prefix/src/googletest-stamp/googletest-build-*.log
[595/1187] Performing build step for 'sylvan'
-- sylvan build command succeeded.  See also /Users/macbook/Code/i2/storm/build/sylvan/src/sylvan-stamp/sylvan-build-*.log
[598/1187] Performing configure step for 'cudd3'
-- cudd3 configure command succeeded.  See also /Users/macbook/Code/i2/storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-configure-*.log
[599/1187] Performing build step for 'cudd3'
-- cudd3 build command succeeded.  See also /Users/macbook/Code/i2/storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-build-*.log
[600/1187] Performing install step for 'cudd3'
-- cudd3 install command succeeded.  See also /Users/macbook/Code/i2/storm/build/resources/3rdparty/cudd-3.0.0/src/cudd3-stamp/cudd3-install-*.log
[641/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/builder/JaniProgramGraphBuilder.cpp.o
In file included from ../src/storm-pgcl/builder/JaniProgramGraphBuilder.cpp:1:
In file included from ../src/storm-pgcl/builder/JaniProgramGraphBuilder.h:11:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[642/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/builder/ProgramGraphBuilder.cpp.o
In file included from ../src/storm-pgcl/builder/ProgramGraphBuilder.cpp:1:
In file included from ../src/storm-pgcl/builder/ProgramGraphBuilder.h:4:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[656/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/storage/ppg/ProgramAction.cpp.o
In file included from ../src/storm-pgcl/storage/ppg/ProgramAction.cpp:2:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[657/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/storage/ppg/ProgramEdge.cpp.o
In file included from ../src/storm-pgcl/storage/ppg/ProgramEdge.cpp:2:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[659/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/storage/ppg/ProgramEdgeGroup.cpp.o
In file included from ../src/storm-pgcl/storage/ppg/ProgramEdgeGroup.cpp:2:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[660/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/storage/ppg/ProgramGraph.cpp.o
In file included from ../src/storm-pgcl/storage/ppg/ProgramGraph.cpp:2:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[661/1187] Building CXX object src/storm-pgcl/CMakeFiles/storm-pgcl.dir/storage/ppg/ProgramLocation.cpp.o
In file included from ../src/storm-pgcl/storage/ppg/ProgramLocation.cpp:3:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[673/1187] Building CXX object src/storm-pgcl-cli/CMakeFiles/storm-pgcl-cli.dir/storm-pgcl.cpp.o
In file included from ../src/storm-pgcl-cli/storm-pgcl.cpp:10:
In file included from ../src/storm-pgcl/builder/ProgramGraphBuilder.h:4:
../src/storm-pgcl/storage/ppg/ProgramGraph.h:158:13: warning: control may reach end of non-void function [-Wreturn-type]
            }
            ^
1 warning generated.
[886/1187] Building CXX object src/storm/CMakeFiles/storm.dir/storage/expressions/ToRationalNumberVisitor.cpp.o
FAILED: src/storm/CMakeFiles/storm.dir/storage/expressions/ToRationalNumberVisitor.cpp.o
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++  -DBOOST_OPTIONAL_CONFIG_USE_OLD_IMPLEMENTATION_OF_OPTIONAL -DBOOST_RESULT_OF_USE_DECLTYPE -I../src -I../src/storm -I../resources/3rdparty/sparsepp -isystem /usr/local/include -Iinclude -isystem ../resources/3rdparty/l3pp -isystem ../resources/3rdparty/gmm-5.0/include -isystem ../resources/3rdparty/eigen-3.3-beta1 -isystem ../resources/3rdparty/exprtk -isystem ../resources/3rdparty/modernjson/src -isystem resources/3rdparty/cudd-3.0.0/include -isystem ../resources/3rdparty/sylvan/src -isystem ../resources/3rdparty/cpptemplate -isystem /Users/macbook/Code/i2/carl/src -isystem /usr/local/include/eigen3 -isystem /usr/local/include/ginac -mpopcnt -std=c++14 -stdlib=libc++ -ftemplate-depth=1024 -O3 -DNDEBUG -ffast-math -fno-finite-math-only -flto -march=native -fomit-frame-pointer -fPIC -MD -MT src/storm/CMakeFiles/storm.dir/storage/expressions/ToRationalNumberVisitor.cpp.o -MF src/storm/CMakeFiles/storm.dir/storage/expressions/ToRationalNumberVisitor.cpp.o.d -o src/storm/CMakeFiles/storm.dir/storage/expressions/ToRationalNumberVisitor.cpp.o -c ../src/storm/storage/expressions/ToRationalNumberVisitor.cpp
../src/storm/storage/expressions/ToRationalNumberVisitor.cpp:133:39: error: call to 'rationalize' is ambiguous
            return RationalNumberType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
                                      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Users/macbook/Code/i2/carl/src/carl/numbers/adaption_gmpxx/operations.h:225:18: note: candidate function [with T = __gmp_expr<mpq_t, mpq_t>]
inline mpq_class rationalize<mpq_class>(float n) {
                 ^
/Users/macbook/Code/i2/carl/src/carl/numbers/adaption_gmpxx/operations.h:231:18: note: candidate function [with T = __gmp_expr<mpq_t, mpq_t>]
inline mpq_class rationalize<mpq_class>(double n) {
                 ^
/Users/macbook/Code/i2/carl/src/carl/numbers/adaption_gmpxx/operations.h:237:18: note: candidate function [with T = __gmp_expr<mpq_t, mpq_t>]
inline mpq_class rationalize<mpq_class>(int n) {
                 ^
/Users/macbook/Code/i2/carl/src/carl/numbers/adaption_gmpxx/operations.h:242:18: note: candidate function [with T = __gmp_expr<mpq_t, mpq_t>]
inline mpq_class rationalize<mpq_class>(uint n) {
                 ^
/Users/macbook/Code/i2/carl/src/carl/numbers/adaption_gmpxx/operations.h:247:18: note: candidate function [with T = __gmp_expr<mpq_t, mpq_t>]
inline mpq_class rationalize<mpq_class>(sint n) {
                 ^
1 error generated.
[891/1187] Building CXX object src/storm/CMakeFiles/storm.dir/storage/expressions/ExprtkExpressionEvaluator.cpp.o
ninja: build stopped: subcommand failed.

Note that CLN & Ginac were installed with Homebrew, not sure if that’s relevant (libstd and so on?).

Building with system carl fails

OS: Linux 5.2.9-arch1-1-ARCH #1 SMP PREEMPT Fri Aug 16 11:29:43 UTC 2019 x86_64 GNU/Linux
The CARL library comes in a broken AUR package: you get to choose between carl and git-carl, both equally old (2017), both equally broken.
Downloaded carl from the git repo, version 19.06. Built ok, installed in default path (/usr/local/lib64)
Compiling storm fails with the error:

CMake Error at resources/3rdparty/CMakeLists.txt:237 (if):
  if given arguments:
    "STREQUAL" "carlLOCATION-NOTFOUND"
  Unknown arguments specified

Fix: in resources/3rdparty/CMakeLists.txt change line 237 from:
if(${carlLOCATION} STREQUAL "carlLOCATION-NOTFOUND")
to:
if("${carlLOCATION}" STREQUAL "carlLOCATION-NOTFOUND")
i.e. wrap ${carlLOCATION} in double quotes.
My cmake version is 3.15.2

Cannot set dft:approximationheuristic to anything other than `depth`

It is impossible to set an approximation heuristic any other than depth for DFTs.

storm/src/storm-dft/settings/modules/FaultTreeSettings.cpp

Line 34 in 47b2cb7

    
           this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());

sets up the command line option such that in only accepts the values depth and rateratio. However, in

storm/src/storm-dft/settings/modules/FaultTreeSettings.cpp

Lines 66 to 71 in 47b2cb7

    
           if (heuristicAsString == "depth") { 
        
               return storm::builder::ApproximationHeuristic::DEPTH; 
        
           } else if (heuristicAsString == "probability") { 
        
               return storm::builder::ApproximationHeuristic::PROBABILITY; 
        
           } 
        
           STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");

only the values depth and probability are accepted. Thus only depth is accepted by both validations.

What is supposed to be the correct option here?

Build step for carl fails

When following the Building Storm from Source tutorial, I get the following error at the make step. I got no error during the cmake step. All the dependencies are installed.

Trying to build carl manually gives the following error:

Commands I tried to build carl manually

$ git clone -b master14 https://github.com/smtrat/carl.git
$ cd carl
Prepare the build:

$ mkdir build && cd build
$ cmake .. -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON
Build lib_carl:

$ make lib_carl

Inspired by : https://moves-rwth.github.io/prophesy/installation.html

Missing check for eigen3

The check for eigen3 is missing or incomplete.

The build fails unexpectedly if eigen3 is not available on the build system.

Doxygen/Problem with older version of CMAKE

I recently got the following error message (on a machine which I can no longer access).

CMake Error at resources/doxygen/CMakeLists.txt:25 (doxygen_add_docs):
Unknown CMake command "doxygen_add_docs".

The same issue as: epfl-ecps/channelflow#13

Thus, we should add a check that the cmake version is up-to-date, or block the functionality in that file.

Missing bounded type support for constants in Jani parser

I realized that I cannot run Storm with a Jani model with a bounded type constant in it, it supports only basic types. It would be useful if it would be possible.

Wrong result for maximal end component computation (sparse)

Hi,

consider the following model (a PRISM LTL testcase):

// LTL bug(s) fixed in trunk rev 2201

mdp

module test

	x : [0..2];
	
	[] x=0 -> true;
	[] x=0 -> 0.5 : (x'=1) + 0.5: (x'=2);
	[] x=1 -> (x'=0);
	[] x=2 -> true;
	
endmodule

When computing the MEC decomposition using Storm's sparse engine, the decomposition looks like this:

MECs (model):
{{2, {3, }}}
{{1, {2, }}{0, {0, }}}

i..e, it claims that there is one MEC consisting of state 2 and one MEC consisting of state 0 and 1 (state indizes correspond to the x variable values).

But actually the second MEC should only contain the 0-state, as the second choice leaves the initial {0,1} SCC with probability 1/2. It looks like the logic here is broken. Additionally, during the SccDecomposition, I think one has to take into account which of the choices are still "fine" and are part of the underlying graph, i.e, where all successors lead back into the current MEC candidate.

MEC computation and output via the following code snippet

std::cout << "MECs (model):" << std::endl;
storm::storage::MaximalEndComponentDecomposition<ValueType> mecs(mdp.getTransitionMatrix(), mdp.getBackwardTransitions());
for (const auto& mec : mecs) {
   std::cout << mec << std::endl;
}

undefined constants that are declared in a properties file are assumed to be 0

When declaring a constant in a properties file, but not defining it (neither in the file nor via command line) storm assumes the constant to be 0. For example, when calling
storm --prism ./model.prism --prop ./props.prop
on the model

dtmc
const double p = 0.4;
const int N = 5;

module one
x: bool init true;
num_rounds : [0..N] init 0;

[a] x & (num_rounds<N) -> p  : (num_rounds' = num_rounds+1) 
                     + (1-p) : (x' = false) & (num_rounds' = num_rounds+1);
[a] x & (num_rounds=N) -> p  : true 
                     + (1-p) : (x' = false);
endmodule

and the properties file

const int k;
P=? [F num_rounds = k];

the result 1 is returned although k is not specified.

	if (heuristicAsString == "depth") {
	return storm::builder::ApproximationHeuristic::DEPTH;
	} else if (heuristicAsString == "probability") {
	return storm::builder::ApproximationHeuristic::PROBABILITY;
	}
	STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");

moves-rwth / storm Goto Github PK

storm's Introduction

Storm - A Modern Probabilistic Model Checker

Usage

Examples

Developers

Authors

Principal developers

Developers (lexicographical order)

Contributors (lexicographical order)

Citing Storm

storm's People

Contributors

Stargazers

Watchers

Forkers

storm's Issues

Recommend Projects

Recommend Topics

Recommend Org