Tim Quatmann
Tim Quatmann
When computing `Pmin=? [F x=2 || x=1]` for the following PRISM Program, with Storm we get `0`, although `0.3` should be correct. ``` mdp module main x : [0..2]; []...
As reported by @culechetoo [here](https://github.com/moves-rwth/storm/pull/349) (thanks), there is a potential issue with the test case `SparseMaPcaaMultiObjectiveModelCheckerTest.serverRationalNumbers`. See PR #349 for their `cmake` and `lldb` output. ~I haven't been able to...
My `stormConfig.cmake` file contained ``` set_target_properties(libsoplex-pic PROPERTIES IMPORTED_LOCATION "LOCATION-NOTFOUND") ``` which means that e.g. stormpy does not compile because it somehow can not link with a library named `LOCATION-NOTFOUND` We...
Added option `--build:state limit ` which, if set, stops expanding new states once the given `` of states has been found. This is useful for, e.g., debugging models that normally...
We currently require that the row grouping of the transition **probability** matrix is also present in the transition **reward** matrices. Specifically, we [assert](https://github.com/moves-rwth/storm/blob/58e174b11158ece3bb6b05339ba4759e32d475a2/src/storm/models/sparse/Model.cpp#L76) that `rewardMatrix.isSubmatrixOf(transitionMatrix)` is true when constructing a...
* Added options to tweak the LP encoding * Use RawMode instead of storm::expressions * Add ViToLp Method to warm-start the procedure * Topological solvers can now (optionally, if enabled)...