Tim Quatmann
|
70e2263783
|
MarkovAutomatonCslModelCheckerTest: Prevent this test from failing in cases where z3 is installed without optimization support.
|
5 years ago |
|
Tim Quatmann
|
137f41abac
|
FormulaInformation: Fixed detection of property type.
|
5 years ago |
|
Tim Quatmann
|
1fd052aee4
|
InformationCollector: Use infinite precision to determine the state domain size.
|
5 years ago |
|
Tim Quatmann
|
2b89da2f4b
|
Updated decision tree used in portfolio engine.
|
5 years ago |
|
Tim Quatmann
|
5dcebdef93
|
Fixed invocation of storm without a model.
|
5 years ago |
|
Tim Quatmann
|
49e4bba7c1
|
Merge branch 'master' into qcomp2020
|
5 years ago |
|
Tim Quatmann
|
f4820628a5
|
Incorporated more features for the portfolio engine.
|
5 years ago |
|
Tim Quatmann
|
3b53e1e583
|
Implemented retrieval of jani model information with a traverser. Also determine the size of the state domain.
|
5 years ago |
|
Tim Quatmann
|
d3ece2a2e5
|
Better simplification of prism commands.
|
5 years ago |
|
Tim Quatmann
|
0e91887ebb
|
Queried the termination flag in a few more places.
|
5 years ago |
|
Tim Quatmann
|
4585f8f555
|
One more fix for AcyclicSolverHelper.
|
5 years ago |
|
Tim Quatmann
|
7766a96783
|
Fixes for Acylic equation solvers.
|
5 years ago |
|
Tim Quatmann
|
bbc6f8b786
|
Fixed invalid memory access when applying BitVector::resize on BitVectors of length 0.
|
5 years ago |
|
Tim Quatmann
|
99f2344da9
|
Use acyclic solver in various Markov automata methods.
|
5 years ago |
|
Tim Quatmann
|
c83721066c
|
Use acyclic solver in reward bounded properties.
|
5 years ago |
|
Tim Quatmann
|
53db0b1f22
|
Added AcyclicMinMaxLinearEquationSolver and AcyclicLinearEquationSolver which are optimized for many calls on an acyclic model.
|
5 years ago |
|
Tim Quatmann
|
250a4b9b9a
|
MdpModelChecheckerTest: added test cases for the different multiplication styles and multiplier types.
|
5 years ago |
|
Tim Quatmann
|
31cbe14d3c
|
Multiplier: Added a flag to specify whether gaussSeidel style multiplications should be performed forward or backwards.
|
5 years ago |
Matthias Volk
|
d88e7e9951
|
Explicit header files to include all defined environments
|
5 years ago |
|
Tim Quatmann
|
14f07a2d1a
|
Unif+: Update kappa only based on the results at the initial state
|
5 years ago |
|
Tim Quatmann
|
dd958bcedd
|
Changed default of the unifpluskappa
|
5 years ago |
|
Tim Quatmann
|
4d55dfbf07
|
Fixed doing non-exact model checking in portfolio engine, even if the --exact switch was set.
|
5 years ago |
|
Tim Quatmann
|
c399c31c52
|
Added missing include
|
5 years ago |
|
Matthias Volk
|
c17a50904d
|
Updated CHANGELOG
|
5 years ago |
|
Matthias Volk
|
6f62e8d402
|
Support abort in model building
|
5 years ago |
|
Matthias Volk
|
679327ee9d
|
Merge branch 'qcomp2020' into signals
|
5 years ago |
|
Matthias Volk
|
e65e5587f0
|
Support for abort in Gmm++ by throwing exception
|
5 years ago |
|
Matthias Volk
|
823ae23180
|
Use updateStatus in more cases
|
5 years ago |
|
Matthias Volk
|
f50a7a424b
|
General updateStatus function in AbstractEquationSolver
|
5 years ago |
|
Tim Quatmann
|
c6b984ca51
|
Do not perform the conversion from a prism program to a jani model twice.
|
5 years ago |
|
Matthias Volk
|
b745b10b77
|
Moved reportStatus() and updateStatusIfNotConverged() to AbstractEquationSolver
|
5 years ago |
|
Tim Quatmann
|
9962da7453
|
Registered missing settings modules in storm-dft and storm-pars
|
5 years ago |
|
Tim Quatmann
|
e3663ee740
|
Portfolio: print true/false instead of 1/0
|
5 years ago |
|
Tim Quatmann
|
7e9029e5bd
|
Optimization for PRISM model building: Avoid evaluating unnecessarily many guards.
|
5 years ago |
|
Tim Quatmann
|
4012094f9d
|
Use new time bounded environment also in the ctmc solver.
|
5 years ago |
|
Tim Quatmann
|
11ed073632
|
Making storm-dft compile again...
|
5 years ago |
|
Matthias Volk
|
3debbbc64d
|
Added more abortion checks
|
5 years ago |
|
Matthias Volk
|
d35d31ce94
|
Added SolverStatus::Abort for abort signal handling
|
5 years ago |
|
Matthias Volk
|
acd5a94162
|
Use general SolverStatus in StandardGameSolver
|
5 years ago |
|
Tim Quatmann
|
8168b9d125
|
Using OVI as default
|
5 years ago |
|
Tim Quatmann
|
7617d4f96f
|
Updated changelog.
|
5 years ago |
|
Tim Quatmann
|
20f5cf158b
|
storm-dft: Using symmetry reduction by default.
|
5 years ago |
|
Matthias Volk
|
0dd1c70e12
|
Set waiting time after signal with flag --signal-timeout
|
5 years ago |
|
Matthias Volk
|
f6d6d952a6
|
Fixed warnings
|
5 years ago |
|
Matthias Volk
|
5192bd1623
|
Merge from qcomp2020
|
5 years ago |
|
Tim Quatmann
|
a8c0cfbcdd
|
Enabled OVI for linear equation systems in test cases.
|
5 years ago |
|
Tim Quatmann
|
383e2172d4
|
Added OVI for linear equation systems (i.e. DTMC/CTMC)
|
5 years ago |
|
Tim Quatmann
|
7c49edb68f
|
Put most of the optimistic value iteration code into a new helper file
|
5 years ago |
|
Matthias Volk
|
6c095e757a
|
Fixed problem with Windows linebreak \r\n, because this is still a problem in 2020
|
5 years ago |
|
Tim Quatmann
|
502b637df4
|
Ovi: Use an additional auxiliary row group vector (to allow caching).
|
5 years ago |
