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 |
|
Tim Quatmann
|
502b637df4
|
Ovi: Use an additional auxiliary row group vector (to allow caching).
|
5 years ago |
|
Tim Quatmann
|
ee82f30550
|
Removed Debug output
|
5 years ago |
|
Tim Quatmann
|
0ba0d94b84
|
Small update for the default settings.
|
5 years ago |
|
Tim Quatmann
|
c33d570610
|
Merge branch 'qcomp2020' into ovi-implementation
|
5 years ago |
|
Tim Quatmann
|
33975c181e
|
Fixes and improvements in the new unif+ implementation.
|
5 years ago |
|
Tim Quatmann
|
52857d2701
|
FoxGlyn: Print an error message instead of throwing an exception in cases where an underflow is possible.
|
5 years ago |
|
Tim Quatmann
|
4a34fb1a7c
|
MaTest: Making sure that the 'inner' MinMax solver for unif+ is allowed to switch the solution method.
|
5 years ago |
|
Tim Quatmann
|
e54a035ab9
|
SolverEnvironment: Added the switch `forceExact` to switch to exact solving methods more conveniently.
|
5 years ago |
|
TimQu
|
c3184d3afa
|
Consider relevant states in unif+
|
5 years ago |
|
TimQu
|
ca59635f8a
|
Using new time bounded environment also for IMCA method.
|
5 years ago |
|
TimQu
|
03bf55f4ab
|
Bugfix in new unif+ implementation
|
5 years ago |
|
Tim Quatmann
|
f8fbf7ace4
|
Refactored unif+ implementation (introduced relative precision criterion)
|
5 years ago |
|
Tim Quatmann
|
bb94110b74
|
MarkovAutomaton model checkers: Enable consideration of psiStates.
|
5 years ago |
|
Tim Quatmann
|
60670e1fb2
|
SparseMatrix: fixed getConstraintRowSumVector which did not allocate enough space before filling the resulting vector.
|
5 years ago |
|
Tim Quatmann
|
f0d1aff610
|
Added new settings and environment module for time-bounded settings.
|
5 years ago |
|
Matthias Volk
|
f684e48e9e
|
Support for aborting DFT state space building
|
5 years ago |
|
Matthias Volk
|
ce298fa782
|
Moved signal handling to own file to prevent problems with global static variables being non-unique
|
5 years ago |
|
Tim Quatmann
|
05471d94fd
|
Optimizations in JaniNextStateGenerator that avoid unnecessary (re-) allocations of memory. Moreover, before collecting the complete set of enabled edges for each automaton, we first check whether each automaton (that synchronizes with that action) has at least one enabled edge. This avoids checking unnecessarily many edge guards.
|
5 years ago |
|
Tim Quatmann
|
e79035c71b
|
Enabled short circuit optimization for & (and) and | (or) in ExprtkExpressionEvaluator
|
5 years ago |
|
Tim Quatmann
|
d92e6b97e5
|
updated exprtk
|
5 years ago |
|
Tim Quatmann
|
e945f28a86
|
Using raw pointers for manager in Variable.h since weak_ptr::lock() often seems to be a bottle neck during, e.g., model building.
|
5 years ago |
|
TimQu
|
b3831d0093
|
Merge branch 'master' into qcomp2020
|
5 years ago |
