Tim Quatmann
|
f316bb9d38
|
Added missing include.
|
4 years ago |
|
Tim Quatmann
|
05d2af2bfd
|
Fixing destructors of model checker helpers.
|
4 years ago |
Matthias Volk
|
cec37005ae
|
Set relevant DFT elements earlier in code
|
4 years ago |
|
TimQu
|
485d75f466
|
Towards using the infinite horizon helpers also for deterministic models.
|
4 years ago |
|
TimQu
|
35c57fe980
|
LraViHelper: Put component utility functions to separate file.
|
4 years ago |
|
Tim Quatmann
|
fa6c47db64
|
Removed old LRA code for Markov automata.
|
4 years ago |
|
Tim Quatmann
|
aabe3ce776
|
Added simple infinite horizon helper for the hybrid engine.
|
4 years ago |
|
Tim Quatmann
|
7795ce5f35
|
ModelCheckerHelper: Added utility function that copies model checking information from one helper to another.
|
4 years ago |
|
Tim Quatmann
|
626b7a819a
|
InfiniteHorizon: Fixed storing backwardstransition properly. Allowed to specify a mec decomposition. Pushed _produceScheduler flag to the SingleValueModelCheckerHelper.
|
4 years ago |
|
Tim Quatmann
|
68b4d8dbd2
|
Nondet Lra: Fixed LP implementation for Markov automata.
|
4 years ago |
|
Tim Quatmann
|
9fbb587884
|
LraViHelper: Fix for NondetTsNoIs
|
4 years ago |
|
Tim Quatmann
|
f113ac7187
|
NondeterministicLraHelper: Removed old ViHelper code.
|
4 years ago |
|
Tim Quatmann
|
7e65e797fa
|
SingleValueModelCheckerHelper: Fixed signature of getOptimizationDirection so that a const& is returned.
|
4 years ago |
|
Tim Quatmann
|
6e55dba8d4
|
Moved LraViHelper to a separate file. Merged MDP and MA implementation.
|
4 years ago |
|
Tim Quatmann
|
a618147192
|
gmm Multiplier: Added support for computing y += A*x in Parallel.
|
4 years ago |
|
Tim Quatmann
|
51c8779e73
|
Added missing template instantiations.
|
4 years ago |
|
Tim Quatmann
|
5917b020fc
|
GMM Multiplier: Support for y += A*x
|
4 years ago |
|
Tim Quatmann
|
9d2e5c2193
|
Relaxed precision requirements on an MA LRA test-case to correctly represent a relative precision criterion.
|
4 years ago |
|
Tim Quatmann
|
32503594d5
|
Use new LRA helper for Markov automata.
|
4 years ago |
|
Tim Quatmann
|
b5bd7aa0c2
|
Introduced a utility function that sets information from a CheckTask to a helper.
|
4 years ago |
|
Tim Quatmann
|
092873e99a
|
LRA VI: Added helper for Markov Automata.
|
4 years ago |
|
Matthias Volk
|
ab045f2865
|
Ignore zoom attribute in pnpro files
|
4 years ago |
|
Tim Quatmann
|
fc66e01ed5
|
Nondeterministic Infinite horizon: Split value getters into StateValueGetter and ActionValueGetters. Made VI code more general, so that they may also be used for Markov Automata.
|
4 years ago |
|
Tim Quatmann
|
31dd1d8f49
|
sparse/StandardRewardModel: Added a method that only yields the action-based rewards (excl. state rewards)
|
4 years ago |
|
Tim Quatmann
|
9d3de84122
|
MaximalEndComponent: Added size() method.
|
4 years ago |
|
Matthias Volk
|
395081cdf9
|
Moved DFT preprocessing in api functions
|
4 years ago |
|
Tim Quatmann
|
d06a39eb79
|
Dropping old MDP LRA code.
|
4 years ago |
|
Tim Quatmann
|
3c84e68216
|
Using the new helper for MDP LRA properties.
|
4 years ago |
|
Tim Quatmann
|
486d62ff2c
|
First version of newly structured ModelCheckerHelpers (only MDP LRA properties, for now)
|
4 years ago |
|
Tim Quatmann
|
d49210ac2e
|
Added DdType::None to encode that an explicit representation should be used.
|
4 years ago |
|
Tim Quatmann
|
1929cfaf77
|
utility/vector: Added a few asserts in utility functions.
|
4 years ago |
Jan Erik Karuc
|
6c70b42549
|
OVI: Defaulting to M1/M2, changed CLI option for termination guarantee
Adapted CLI option description
|
4 years ago |
|
Matthias Volk
|
fe5e4c4e1d
|
Updated DFT test which is not throwing an exception anymore
|
4 years ago |
|
Matthias Volk
|
190e36605a
|
Refactored computation of relevant events
|
4 years ago |
|
Matthias Volk
|
a1c6b998ec
|
Ignore SEQ and FDEP children
|
4 years ago |
|
Matthias Volk
|
a7096f748b
|
Fix segfault for empty spare modules
|
5 years ago |
|
Matthias Volk
|
ed8a48a24c
|
Correct check if claiming labels are supported
|
5 years ago |
|
Matthias Volk
|
936985f536
|
Add labels for claiming in Markov chain with flag --labels-claiming
|
5 years ago |
|
Matthias Volk
|
2d543d1314
|
Added BE class for distribution defined by samples
|
5 years ago |
|
Matthias Volk
|
e9dfcb8e45
|
Fixed type comparision for BEs
|
5 years ago |
|
Matthias Volk
|
df28d8ef84
|
Added getUnreliability() for BEs
|
5 years ago |
|
Matthias Volk
|
641c9992a1
|
Distinguish between different BEType and use single BE type in DFTElementTypes
|
5 years ago |
Sebastian Junges
|
d6bfcb4818
|
refactoring: moving some code out of the util folder
|
4 years ago |
|
Sebastian Junges
|
5722c1258c
|
pipe all rf-variable creations through a single object file
|
4 years ago |
|
Matthias Volk
|
8d75b84ba6
|
Throw error when using ThinLTO and GCC
|
4 years ago |
|
TimQu
|
17a1d02757
|
Cmake: Detection for the old in-source "storm-version.cpp" file. The file will now be deleted (if found) to prevent build issues for people that upgraded from older storm versions.
|
4 years ago |
|
TimQu
|
c6fd7423f2
|
Disabling stack checks once again for all clang versions >= 11.0.0 because they somehow interfere with exception handling in the PrismParser. (most likely a clang bug).
|
4 years ago |
|
Sebastian Junges
|
b3e37c1eb8
|
partial (parametric) model instantiators
|
4 years ago |
|
Sebastian Junges
|
03e0b01ae2
|
Making POMDPs simple now does not introduce further initial states
|
4 years ago |
|
TimQu
|
1343ae5c19
|
Fixed 'boost/optional.hpp file not found' error in storm-version library (simply by not using boost).
|
4 years ago |
