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
Jan Erik Karuc
99db5693ca
OVI: Implement upper bound only iterations
5 years ago
Tim Quatmann
a5d3d0e696
slight optimizations in the JaniNextStateGenerator
5 years ago
Matthias Volk
f01d8943ad
Indicate if result is not fully correct due to abort
5 years ago
Matthias Volk
3bb3ff9bc7
Support abortion in Unif+
5 years ago
Matthias Volk
45aa451be5
Signal handler supporting termination after waiting period
5 years ago
Tim Quatmann
248c0ecd35
Improved performance of SCC Decomposition by avoiding memory (re-)allocations
5 years ago
Jan Erik Karuc
f56cdb1b93
OVI: Add upper bound only iterations option
5 years ago
Jan Erik Karuc
1c65a936c3
OVI: Use correct environment variable
5 years ago
Jan Erik Karuc
c016d0716e
OVI: Fixed edge case, if x = 0 and ub = 0
5 years ago
Jan Erik Karuc
3db9112a27
OVI: Introduced OVI as a minmax solver for topological solving
5 years ago
Matthias Volk
06787ab9c2
Added calls to setUrgentOptions for binaries
5 years ago
Matthias Volk
6af34ffbe1
Removed old file
5 years ago
Jan Erik Karuc
739d6a4420
OVI: Implement the guessing scaler factor option
5 years ago
Jan Erik Karuc
6ecee7e371
OVI: Add upper bound guessing scaler factor option
5 years ago
Jan Erik Karuc
8b97895e24
OVI: More debug output & cross case assert
5 years ago
Jan Erik Karuc
50a51a70c0
OVI: Debug output for inner interval iteration
5 years ago
Tim Quatmann
b1dc6fec06
Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set.
5 years ago
Tim Quatmann
bf99724f3b
Added missing include.
5 years ago
Tim Quatmann
95b2095151
Implemented simplification of system composition (this enables compatibility for more benchmarks in the dd engine).
5 years ago
TimQu
38439fc867
jani/Automaton: Implemented possibility to clone an automaton.
5 years ago
Tim Quatmann
4e7f8af851
Merge branch 'master' into qcomp2020
5 years ago
Tim Quatmann
141316943c
DdJaniModelBuilder: Also apply max. progress if the system consists of just a single automaton.
5 years ago
Tim Quatmann
5d530bb532
Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards)
5 years ago
Tim Quatmann
eaacc6c0ac
Included the hybrid engine in the MA test.
5 years ago
Tim Quatmann
cefe43f2bf
InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order).
5 years ago
Tim Quatmann
7bf1abe136
Implemented LRA properties for the hybrid engine of MAs.
5 years ago
Tim Quatmann
e6597b35a6
OVI: Added a few settings to tweak ovi
5 years ago
Tim Quatmann
50ff86e709
Polished/ improved ovi.
5 years ago
Jan Erik Karuc
f73be674a9
Update solver status if iterations exceeded
5 years ago
Tim Quatmann
73b68836c5
Hybrid MA engine: (bounded) reachability probabilities
5 years ago
Tim Quatmann
72eb58f73d
Merge branch 'portfolio' into ma-hybrid
5 years ago
Tim Quatmann
a36e75db67
Fixed error introduced during merge
5 years ago