Sebastian Junges
|
3c58b5b2f7
|
case split for MDPs actually checks for MDPs
|
5 years ago |
|
Sebastian Junges
|
08f928456c
|
fix guard for code that considers transient assignments to also consider only transient assignments
|
5 years ago |
|
Sebastian Junges
|
6b6f44100e
|
allow building parametric models of the form s --p-->, s--q-->
|
5 years ago |
|
Sebastian Junges
|
4a7ea35959
|
first version for action mask callbacks in explicit generator
|
5 years ago |
|
Sebastian Junges
|
7a38f54d01
|
extend the next state generator to support prism program simulation
|
5 years ago |
|
Sebastian Junges
|
e5ed114715
|
a first simulator of prism files
|
5 years ago |
|
Sebastian Junges
|
aa6a3d2142
|
sampling from a distribution and from a choice
|
5 years ago |
|
Sebastian Junges
|
00a85cb184
|
accessors for model
|
5 years ago |
Matthias Volk
|
e610edc197
|
Run github actions daily
|
5 years ago |
Daniel Basgöze
|
741d04c797
|
Implement manually triggered github actions CI
|
5 years ago |
Tim Quatmann
|
02695da9b7
|
Fixed several issues regarding powers with negative exponents.
|
5 years ago |
|
Tim Quatmann
|
a3ada8a0c3
|
cli: added a space that was missing in output of steady-state result
|
5 years ago |
|
Tim Quatmann
|
4dcd1cfb64
|
Fixed simplification of expressions that use the power operator with negative exponents.
|
5 years ago |
|
Tim Quatmann
|
09cb0e5a5d
|
LraCtmcTest: Renamed a testcase as its name was misleading before.
|
5 years ago |
|
Tim Quatmann
|
5245d77bfc
|
SteadyState: Issue a warning in sound mode because it is not supported.
|
5 years ago |
|
Tim Quatmann
|
818f8cb8ee
|
steadystate: Added a testcase.
|
5 years ago |
|
Tim Quatmann
|
b73e2e5d1c
|
Fixing steady state distribution computation.
|
5 years ago |
|
Tim Quatmann
|
77d2e9c98f
|
Fixed output of steady-state distr computation.
|
5 years ago |
|
Tim Quatmann
|
211a72b6d7
|
fixing compilation of storm-pars
|
5 years ago |
|
Tim Quatmann
|
19e6473806
|
making the cudd warning sound a bit less dangerous
|
5 years ago |
|
Tim Quatmann
|
2e593dc014
|
Added computation of steady state probabilities for DTMC/CTMC in the sparse engine.
|
5 years ago |
|
Tim Quatmann
|
28ab011eb8
|
Added an export of check results to json.
|
5 years ago |
|
Tim Quatmann
|
84e6984659
|
StateValuations::toJson now has a template parameter to change the exported type of rationals.
|
5 years ago |
|
Tim Quatmann
|
75b6ac27e8
|
JaniParser: Making result field optional (fixes #83)
|
5 years ago |
|
Tim Quatmann
|
3184ba1611
|
Jani: Correctly parse the input-enable field. Throw an error in the sparse model builder, as these are not supported right now.
|
5 years ago |
|
Tim Quatmann
|
41ae9d5624
|
Fixed silently truncating bits when parsing integer literal expressions (see https://github.com/moves-rwth/stormpy/issues/20)
|
5 years ago |
|
Tim Quatmann
|
51f86db9eb
|
Storm version 1.6.3
|
5 years ago |
|
Tim Quatmann
|
7002946845
|
Updated changelog.
|
5 years ago |
|
Tim Quatmann
|
251527bccf
|
storm-pars: Make a more explicit warning if a non-parametric equation solver type is selected.
|
5 years ago |
|
Tim Quatmann
|
1243feba8c
|
Substitute constants in JANI Properties (fixes #95)
|
5 years ago |
|
Tim Quatmann
|
065b366198
|
Removed superfluous '.' in output of Markov automata model data.
|
5 years ago |
|
Tim Quatmann
|
6d6e142236
|
Fixed an issue with JANI models concerning properties using transient variable expressions.
|
5 years ago |
|
Tim Quatmann
|
ee5fff680a
|
Indefinite Horizon helpers: Do not compute values of MaybeStates if they are not relevant for the property. (Fixes #87)
|
5 years ago |
|
Tim Quatmann
|
20d424e289
|
JaniTraverser: Only traverse lower/upper bound expressions of BoundedIntegerVariables, if these bounds exists.
|
5 years ago |
|
Tim Quatmann
|
ce0283d80d
|
Cmake: checked whether the stack-check issue still persists with current AppleClang v12.0.0
|
5 years ago |
|
Tim Quatmann
|
8619a4d833
|
CMake: Implemented a workaround for building CUDD on MacOS Big Sur.
|
5 years ago |
|
Tim Quatmann
|
1982dc0dba
|
SparsePcaaParetoQuery: Added a (hopefully explaining) comment
|
5 years ago |
|
Matthias Volk
|
c12c0352f7
|
Support for parsing jani model from string
|
5 years ago |
|
Matthias Volk
|
209090eb93
|
storm-dft: Ignore compound nodes in json parser
|
5 years ago |
|
Tim Quatmann
|
d0c153da8d
|
Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs)
|
5 years ago |
|
Tim Quatmann
|
9775964f43
|
Pcaa: Fixed unnecessary insertion of diagonal entries in deterministic transitions.
|
5 years ago |
|
Tim Quatmann
|
3a4af89b66
|
graph: Cycle check ignores Zero entries.
|
5 years ago |
|
Sebastian Junges
|
d53cffab08
|
avoid resize that caused unstable behavior
|
5 years ago |
|
Tim Quatmann
|
f7d75b1677
|
Merge remote-tracking branch 'refs/remotes/origin/master'
|
5 years ago |
|
Tim Quatmann
|
2cadf3a252
|
Added support for generating optimal schedulers for globally formulae
|
5 years ago |
|
Tim Quatmann
|
f5ce4860ac
|
Updated changelog.
|
5 years ago |
|
Tim Quatmann
|
4ffe13063c
|
Fixed the offline_package.md documentation to incorporate more recent changes in Storm.
|
5 years ago |
|
Tim Quatmann
|
dc8612b751
|
Fixed not always using the acyclic solver within LRA and multi-objective time-bounded reachability computations.
|
5 years ago |
|
Matthias Volk
|
8b05837e77
|
Fixed assertion for RationalFunction
|
5 years ago |
|
Sebastian Junges
|
32c88825e2
|
cleanup
|
5 years ago |
