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

8032 Commits (afbfd42b3a24f45bcf88844dda04ddccf4d16f7a)
 

Author SHA1 Message Date
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
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)."
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