ca59635f8a
Using new time bounded environment also for IMCA method.
5 years ago
03bf55f4ab
Bugfix in new unif+ implementation
5 years ago
f8fbf7ace4
Refactored unif+ implementation (introduced relative precision criterion)
5 years ago
bb94110b74
MarkovAutomaton model checkers: Enable consideration of psiStates.
5 years ago
60670e1fb2
SparseMatrix: fixed getConstraintRowSumVector which did not allocate enough space before filling the resulting vector.
5 years ago
f0d1aff610
Added new settings and environment module for time-bounded settings.
5 years ago
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
e79035c71b
Enabled short circuit optimization for & (and) and | (or) in ExprtkExpressionEvaluator
5 years ago
d92e6b97e5
updated exprtk
5 years ago
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
b3831d0093
Merge branch 'master' into qcomp2020
5 years ago
5d8419336f
InternalAdds: Added a comment related to GitHub issue #64
5 years ago
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#64
5 years ago
1f98f6c557
Reverted 'optimization' for Prob1Max (since that didn't work out).
5 years ago
9d0d8022f9
Revert "Slight optimization in performProb1A"
This reverts commit 2df4679fbc
5 years ago
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
2df4679fbc
Slight optimization in performProb1A
5 years ago
fe5cd4db86
Fixed missing ;
5 years ago
a5d3d0e696
slight optimizations in the JaniNextStateGenerator
5 years ago
248c0ecd35
Improved performance of SCC Decomposition by avoiding memory (re-)allocations
5 years ago
b1dc6fec06
Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set.
5 years ago
bf99724f3b
Added missing include.
5 years ago
95b2095151
Implemented simplification of system composition (this enables compatibility for more benchmarks in the dd engine).
5 years ago
38439fc867
jani/Automaton: Implemented possibility to clone an automaton.
5 years ago
4e7f8af851
Merge branch 'master' into qcomp2020
5 years ago
141316943c
DdJaniModelBuilder: Also apply max. progress if the system consists of just a single automaton.
5 years ago
5d530bb532
Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards)
5 years ago
eaacc6c0ac
Included the hybrid engine in the MA test.
5 years ago
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
7bf1abe136
Implemented LRA properties for the hybrid engine of MAs.
5 years ago
73b68836c5
Hybrid MA engine: (bounded) reachability probabilities
5 years ago
72eb58f73d
Merge branch 'portfolio' into ma-hybrid
5 years ago
a36e75db67
Fixed error introduced during merge
5 years ago
04c2938057
Introduced hybrid engine for Markov automata (only reach. rewards for now)
5 years ago
98bd96eace
Merge branch 'master' into portfolio
5 years ago
f7e2ff0843
Apply max. Prog. assumption while building with the dd engine.
5 years ago
ba6f0c0e87
BuildSettings: Added the possiblities to build a model with choiceorigins and without max. progress assumption.
5 years ago
9e54ce4e8b
Improved detection of terminal states for Dd engine. Also reduced code duplication.
5 years ago
0060e594c0
Added Missing includes.
5 years ago
066593f4c1
Updated Changelog.
5 years ago
c66b0ea442
model-handling: Fixed compatibility checks
5 years ago
bb3f7c52fd
DdJaniModelBuilder: Fixed canHandle
5 years ago
77c3c37e3c
Implemented portfolio decisions
5 years ago
1e8a12170d
FormulaInformation: Also track whether a formula contains a long-run average formula
5 years ago
54b37d8698
Added entry points for portfolio engine
5 years ago
c6c6f45483
Fixed compilation for storm-pars and storm-pomdp
5 years ago
4da25662f8
Engine: check whether an engine can handle the query given by a model and a *list* of properties
5 years ago
8711b32c99
When using bisimulation with the dd-to-sparse engine, the quotient is automatically extracted in a sparse way.
5 years ago
1574f4444a
CLI: Introduced ModelProcessingInformation which allows to set certain settings (regardinge model building and model verification) in an on-the-fly manner.
5 years ago
a99f0905e2
dd/bisimulation: Added argument to "getQuotient" which allows to set the quotient type (dd / sparse)
5 years ago
TimQu