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
Sebastian Junges
0f967409e6
post merge compile issues with double vs rationals in storm pomdp
5 years ago
Sebastian Junges
160043a8b8
Merge branch 'master' into prism-pomdp
5 years ago
Sebastian Junges
d26842d441
Merge branch 'master' into prism-pomdp
5 years ago
Sebastian Junges
d703516d2d
make code compile
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
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
TimQu
5d8419336f
InternalAdds: Added a comment related to GitHub issue #64
5 years ago
TimQu
36c410875c
Revert "InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order)."
This reverts commit cefe43f2bf
.
Apparently, the GameBasedMdpModelCheckerTest does not terminate when the Dd groups are retrieved in a different order. See github issue #64
5 years ago
TimQu
1f98f6c557
Reverted 'optimization' for Prob1Max (since that didn't work out).
5 years ago
TimQu
9d0d8022f9
Revert "Slight optimization in performProb1A"
This reverts commit 2df4679fbc
.
5 years ago
TimQu
d288701e9d
Graph: Changed methods for prob1 methods in performProb1Max / performProb1Min to more efficient variants that can be used as we already know the prob0 states.
5 years ago
Alexander Bork
c74a6ea201
Removal of unused extractActions function
5 years ago
Alexander Bork
e1bd87b91a
Added documentation
5 years ago
Alexander Bork
53d5e9edf5
Code Cleanup
5 years ago
Tim Quatmann
2df4679fbc
Slight optimization in performProb1A
5 years ago
Tim Quatmann
fe5cd4db86
Fixed missing ;
5 years ago