Tim Quatmann
|
990d1c9759
|
OVI: seperated implementation from header file. Use a separate helper for computing the upper bounds.
|
4 years ago |
|
Tim Quatmann
|
6e2dab0e0b
|
Silenced a warning in OVI code.
|
4 years ago |
|
Tim Quatmann
|
90d5da570c
|
Renamed portfolio engine to automatic engine.
|
4 years ago |
Sebastian Junges
|
7f5f263d7b
|
observation-trace-unfolder added
|
4 years ago |
|
Sebastian Junges
|
1b73f15ff9
|
fix == operator
|
4 years ago |
|
Tim Quatmann
|
9ce9ae9eeb
|
OVI: Fixed too early termination.
|
4 years ago |
|
Sebastian Junges
|
9423d01631
|
observation valuations added
|
4 years ago |
|
Tim Quatmann
|
fb112ab191
|
Added support for modulo operators when building symbolic models in exact mode.
|
4 years ago |
|
Tim Quatmann
|
d90c14b8f5
|
Added progress information for LRA computations
|
4 years ago |
|
Tim Quatmann
|
21c07ebd42
|
DdPrismModelBuilder: Fixed a warning for zero-reward models that was triggered in some cases where the reward model is actually non-zero
|
4 years ago |
|
Tim Quatmann
|
5bcdb5f95a
|
Fixed --sound switch for LRA properties on deterministic models.
|
4 years ago |
|
Tim Quatmann
|
3919c475ad
|
Added some progress information in topological solvers.
|
4 years ago |
|
Tim Quatmann
|
3f2a5ffa62
|
Lra Tests: Added a test case for sound model checking
|
4 years ago |
|
Sebastian Junges
|
fa34f44989
|
keep state valuations in transformers on POMDPs
|
4 years ago |
|
Sebastian Junges
|
3861c502b4
|
memory unfolder can label states with the memory state
|
4 years ago |
|
Sebastian Junges
|
fd00d495f7
|
first version of the nondeterministcbelieftracker
|
4 years ago |
|
Sebastian Junges
|
5fa667b847
|
add random step functionality to simulator
|
4 years ago |
Matthias Volk
|
7963419554
|
Minor change in debug output
|
4 years ago |
|
Matthias Volk
|
c0f3e2e0ce
|
Skip long running HECS tests
|
4 years ago |
|
Matthias Volk
|
a99be1bb06
|
Revised relevant events
|
4 years ago |
|
Matthias Volk
|
4c7b069212
|
Comment explaining need for std::move
|
4 years ago |
|
Sebastian Junges
|
449e4d6f0d
|
mdp support for lower step bounds
|
4 years ago |
|
Sebastian Junges
|
843e6a9b6b
|
step bounded properties for dtmcs in a new helper, and now with support for (extra) lower bounds
|
4 years ago |
|
Sebastian Junges
|
406ffbdc7f
|
get submatrix now can set some columns to zero but retain them
|
4 years ago |
|
Sebastian Junges
|
bbafd095bf
|
no lower bound is still a zero bound :-)
|
4 years ago |
|
Sebastian Junges
|
ca591dff9f
|
better error message
|
4 years ago |
|
TimQu
|
6eeecaf7f8
|
Fixed compatibility with older boost versions.
|
4 years ago |
|
Tim Quatmann
|
3d9b53723b
|
OVI: added case where the guessed upper bound corresponds to the fixpoint.
|
4 years ago |
|
Tim Quatmann
|
2273fda7c9
|
ovi helper: Take the relative/absolute precision and the maximal iteration count as a parameter because otherwise it is not clear whether we should take this information from the NativeEnvironment or the MinMaxEnvironment.
|
4 years ago |
|
Tim Quatmann
|
5a76128e3f
|
Removed DdType::None because there is no use for this anymore.
|
4 years ago |
|
Tim Quatmann
|
f94d45483e
|
Use the new model representation enum in the model checking helpers.
|
4 years ago |
|
Tim Quatmann
|
cf20e340de
|
Added a new enum that describes the model representation (sparse, dd with sylvan, dd with cudd).
|
4 years ago |
|
Tim Quatmann
|
a6c5225f31
|
Added test case for scheduler generation for LRA Property
|
4 years ago |
|
Tim Quatmann
|
3e79e6e5ea
|
LraMdp Test: Added an additional test case.
|
4 years ago |
|
Tim Quatmann
|
fd77b71084
|
OVI helper: fixed spacing in source code, changed two while loops to for loops
|
4 years ago |
|
Tim Quatmann
|
585dd675d1
|
OviSettings: Made help message a bit shorter
|
4 years ago |
|
Tim Quatmann
|
6f6773f8ca
|
PgclParser: Do not reject variable names with a keyword as proper prefix. (fixes GitHub issue #84)
|
4 years ago |
|
Tim Quatmann
|
87ef49a2d0
|
Do not show a conversion warning if no conversion happens.
|
4 years ago |
|
Tim Quatmann
|
eb02d56b69
|
LraViHelper: Changed type of toSubModelStateMapping to std::map, which is faster in this scenario. Also fixed some awkward const&'s
|
4 years ago |
|
Tim Quatmann
|
5f119ed149
|
Fixed weird error when invoking Storm with portfolio engine and no input model.
|
4 years ago |
|
Sebastian Junges
|
923f779a09
|
explicit-state-lookup, for finding states in a model based on the variable assignment
|
4 years ago |
|
Tim Quatmann
|
7e18fbf3c2
|
Fixed weird error when invoking Storm with portfolio engine and no input model.
|
4 years ago |
|
Tim Quatmann
|
b7883a8ef1
|
Used the new SparseMatrixBuilder::addDiagonalEntry to simplify some of the LRA code.
|
4 years ago |
|
Tim Quatmann
|
6f59c4f3eb
|
SparseMatrixBuilder: Added a function to easily add diagonal entries.
|
4 years ago |
|
Tim Quatmann
|
8627cde4dc
|
Removing old LRA code in old helpers.
|
4 years ago |
|
Tim Quatmann
|
38af6357d7
|
Using the new hybrid infinite horizon helper in the model checkers
|
4 years ago |
|
Tim Quatmann
|
f8d4fd8862
|
New utility function for exchanging informations between deterministic helpers.
|
4 years ago |
|
Tim Quatmann
|
5eb2bcc71f
|
Fixing bad cast exception
|
4 years ago |
|
Tim Quatmann
|
64b9c176e7
|
symbolic Ctmc: Added method to compute the probability matrix.
|
4 years ago |
|
Tim Quatmann
|
9c82fe7b0d
|
Making hybrid infinite horizon helper ready for deterministic models.
|
4 years ago |
