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
|
d0cc24ae51
|
Updated Changelog.
|
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
|
b6fc409dd8
|
Merge branch 'modelchecker-helper-refactor'
|
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
|
84a5faef62
|
Merge branch 'ovi-implementation'
|
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
|
321bb9121f
|
Merge branch 'master' into modelchecker-helper-refactor
|
4 years ago |
|
Tim Quatmann
|
7e18fbf3c2
|
Fixed weird error when invoking Storm with portfolio engine and no input model.
|
4 years ago |
|
Tim Quatmann
|
7e6b0c27c3
|
Merge remote-tracking branch 'refs/remotes/origin/master' into modelchecker-helper-refactor
|
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 |
|
Tim Quatmann
|
19f6552b05
|
Fixed insufficient precision in CTMC LRA test
|
4 years ago |
|
Tim Quatmann
|
959e035153
|
Use the new infinite horizon helper for sparse ctmc and dtmc.
|
4 years ago |
|
Tim Quatmann
|
462ce5dce3
|
Ctmc: added a method that returns the probabilistic transition matrix.
|
4 years ago |
|
Tim Quatmann
|
d92905a7c3
|
LraVi: Fixed uninitialized bool member.
|
4 years ago |
|
Tim Quatmann
|
ef2448410b
|
Fixed selecting wrong reward kind
|
4 years ago |
|
Tim Quatmann
|
c674de5893
|
Deterministic infinite horizon: Added gain-bias and lra-distribution based solution methods
|
4 years ago |
Matthias Volk
|
72813a9774
|
Revelant DFT events are not part of symmetries
|
4 years ago |
|
Matthias Volk
|
693237a304
|
Improved hashing for BEColourClass
|
4 years ago |
|
Matthias Volk
|
f7930d22b0
|
Fixed typo which lead to wrong symmetries for voting gates
|
4 years ago |
|
Matthias Volk
|
e933df1fc1
|
Fixed parsing of ' in GalileoParser
|
4 years ago |
|
Tim Quatmann
|
0cc2b1c749
|
First version of sparse infinite horizon helpers for deterministic and nondeterministic models.
|
4 years ago |
|
Tim Quatmann
|
6ecbf113b3
|
Adding template instantiation for deterministic LRA VI
|
4 years ago |
|
Tim Quatmann
|
f145aa2c94
|
Adding includes for component utility. Making functions inline.
|
4 years ago |
|
Tim Quatmann
|
572e7ace9d
|
Moving some includes to the header file
|
4 years ago |
|
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 |
