sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
8097 Commits
1 Branch
0 Tags
187 MiB
Tree: 121b082139
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '121b082139'
${ noResults }
Commit Graph

8097 Commits (121b082139d67cf336fea0e621f7592158e9a9f5)
 

Author SHA1 Message Date
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)."
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"
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
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
Tim Quatmann 04c2938057 Introduced hybrid engine for Markov automata (only reach. rewards for now)
5 years ago