TimQu
|
bb63ac6089
|
Linear equation solver + game solvers now respect the environment as well
|
8 years ago |
Joachim Klein
|
f56076aacf
|
Add virtual destructors to classes having virtual functions.
(Silences warnings from -Wdelete-non-virtual-dtor -Wnon-virtual-dtor)
|
8 years ago |
dehnert
|
eaee9bb2c2
|
removed parallel flag for bisimulation as this is now governed by sylvan:threads already, fixed bug in DD traversal
|
8 years ago |
|
dehnert
|
d2d129a836
|
toward multi-threaded dd bisimulation
|
8 years ago |
|
dehnert
|
6501fffac3
|
several optimizations related to explicit model building
|
8 years ago |
sjunges
|
12dda40919
|
split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs
|
8 years ago |
|
TimQu
|
17d6835477
|
removed acyclic minmax method as it is not much better then gauss-seidel style multiplications
|
8 years ago |
|
dehnert
|
5fd7878791
|
added option to refine over states whose signatures changed in dd-based bisimulation
|
8 years ago |
|
dehnert
|
c85e30dfd0
|
added distance-aware initial partition to dd-based bisimulation
|
8 years ago |
|
dehnert
|
669940ccd3
|
only supporting reuse of nothing or of block numbers
|
8 years ago |
|
dehnert
|
a19c2fe59b
|
work on variations which data is reused in dd-based bisimulation
|
8 years ago |
|
dehnert
|
b415c12c25
|
further preparation of partial bisimulation model checker
|
8 years ago |
|
dehnert
|
9c685f3bdb
|
started on partial bisimulation model checker
|
8 years ago |
|
dehnert
|
8204c03c0b
|
fixed a ton of warnings
|
8 years ago |
|
dehnert
|
bf727a28fd
|
remove debug output and choose sylvan automatically in exact mode
|
8 years ago |
Sebastian Junges
|
94a7cd1048
|
with some disabled setting-modules, do no longer crash in help
|
8 years ago |
|
dehnert
|
e557a8e069
|
started on EC elimination for hybrid engine
|
8 years ago |
|
TimQu
|
64a804137e
|
export of cdf's
|
8 years ago |
|
TimQu
|
96f45fe77a
|
fixed missing return statements
|
8 years ago |
|
dehnert
|
df05711f3e
|
finished rational search for MinMax solver, preparing rational search for NativeLinearEquationSolver
|
8 years ago |
|
TimQu
|
4afaca7f84
|
fixed missing return statements
|
8 years ago |
|
dehnert
|
b3f0aa511e
|
started on Kwek-Mehlhorn-based exact value computation
|
8 years ago |
|
dehnert
|
2d41de479e
|
added progress outputs to iterative solvers
|
8 years ago |
|
TimQu
|
fcd277c42a
|
added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format
|
8 years ago |
|
dehnert
|
d25cc4b05f
|
first version of sound value iteration
|
8 years ago |
|
dehnert
|
ec61e110f2
|
introducing solver formats to enable linear equation solvers to take the fixed point rather than the equation system formulation
|
8 years ago |
|
dehnert
|
8e8fc34c30
|
fixed some TBB-related issues and added power method for linear equation systems
|
8 years ago |
|
dehnert
|
c5134c364f
|
Extraction and update of TBB-parallelized stuff
|
8 years ago |
|
dehnert
|
5440d164b2
|
started on Walker-Chae algorithm
|
8 years ago |
|
dehnert
|
d27954622a
|
slightly changed handling of gauss-seidel invocations in linear equation solver
|
8 years ago |
|
dehnert
|
00f88ed452
|
gauss-seidel-style value iteration
|
8 years ago |
|
dehnert
|
4c5cdfeafc
|
Sparse MDP helper now also respects solver requirements for reachability rewards
|
8 years ago |
|
Sebastian Junges
|
d271824461
|
prepare to initialize but not make settings known, not yet fully functioning
|
8 years ago |
|
dehnert
|
8cdbf281fa
|
make minmax solvers use policy iteration when --exact is set and no other method was explicitly set
|
8 years ago |
|
dehnert
|
653e5fc184
|
setting default native technique to jacobi again
|
9 years ago |
|
dehnert
|
b25ef3f09c
|
introduced symbolic bisimulation modes lazy and eager, fixed bug in sparse quotient extraction
|
9 years ago |
|
TimQu
|
25843ee53b
|
added setting 'lramethod'
|
9 years ago |
|
TimQu
|
77c0cdc0e3
|
added minmax method 'linearprogramming'
|
9 years ago |
|
dehnert
|
f1ca2853f7
|
fixed some typo and added some documentation
|
9 years ago |
|
dehnert
|
f5ba5204c9
|
adding some debug functionality to DdManager to corner dynamic reordering issue with CUDD
|
9 years ago |
|
dehnert
|
bda9a797e8
|
fixed some issues in CUDD (fixes provided by Fabio Somenzi)
|
9 years ago |
|
dehnert
|
29855e2853
|
added option to display information about exploration progress to both jit and explicit builder
|
9 years ago |
|
TimQu
|
6621cb814c
|
new argument validator: doubleRangeValidatorIncluding
|
9 years ago |
|
dehnert
|
3bcdc1b579
|
allowing to read transient variables in guards of edges in JIT-based JANI model builder and making the optimization level an option
|
9 years ago |
|
TimQu
|
07259e8f0d
|
added parser for IMCAs explicit Markov automaton format
|
9 years ago |
|
TimQu
|
49713eea72
|
Added new MinMaxMethod: 'acyclic' which potentially increases performance on acyclic mdps
|
9 years ago |
|
TimQu
|
c7b83ffb5f
|
moved parameter lifting related code out of the main library/executable
|
9 years ago |
|
dehnert
|
ea02ea0838
|
started overhaul of cli/api
|
9 years ago |
|
dehnert
|
f0f4cd7390
|
first version of sparse quotient extraction for dd bisimulation
|
9 years ago |
|
dehnert
|
7f346d2f0b
|
more work on quotient extraction
|
9 years ago |
