TimQu
|
19f353591f
|
Added an option to transform CTMCs to MAs and DTMCs to MDPs.
|
8 years ago |
|
TimQu
|
6e3639c8f1
|
Added new minmax method: Vi-to-Pi, which first performs value iteration with doubles, to find a good initial policy for (potentially exact) policy iteration.
|
8 years ago |
|
TimQu
|
e6fc962e5e
|
In exact mode, use LP as LRA Method for nondeterministic models.
|
8 years ago |
|
TimQu
|
5ab404a9d3
|
added support for unbounded integer variables in explicit jani builder such that it is treated as a bounded variable (with a given number of bits) and an exception is thrown in case of an underflow or overflow
|
8 years ago |
dehnert
|
2ff18771eb
|
adding a corrected valid-block-mode for game-based abstraction
|
8 years ago |
|
dehnert
|
6ab7859c84
|
fixing more of Lindas issues
|
8 years ago |
|
dehnert
|
943de2e17c
|
changing abstraction options slightly
|
8 years ago |
|
dehnert
|
5706831ad6
|
fixing settings/tests
|
8 years ago |
|
TimQu
|
35aa166f5b
|
added possibility to check all available jani properties
|
8 years ago |
|
TimQu
|
fbb734fbe2
|
Fixed using settings without the 'general' module
|
8 years ago |
|
TimQu
|
e5e6e1bd79
|
worked on prism to jani converter
|
8 years ago |
|
TimQu
|
274d51795c
|
removed default value for maximal iteration count
|
8 years ago |
Sebastian Junges
|
e64e293d59
|
jani transformer which changes a variable into a location
|
8 years ago |
|
Sebastian Junges
|
33c189bd32
|
export setting for flattening
|
8 years ago |
|
dehnert
|
e609a240a9
|
selecting minmax topological by default
|
8 years ago |
|
dehnert
|
a7caf709ae
|
default to topological equation solver
|
8 years ago |
|
dehnert
|
c4bed85dc4
|
switching to native linear equation solver by default and power iteration
|
8 years ago |
sjunges
|
6dfce6a405
|
extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times
|
8 years ago |
|
dehnert
|
4a0134797c
|
option to add initial predicates
|
8 years ago |
|
dehnert
|
e216d55320
|
extended strategy redirection, better statistics
|
8 years ago |
|
dehnert
|
769fd4332c
|
further debugging of game-based abstraction
|
8 years ago |
|
dehnert
|
8c96548566
|
more work on game-based abstraction
|
8 years ago |
|
dehnert
|
1a46300f61
|
adding relative precision to comparator and game-based abstraction
|
8 years ago |
|
dehnert
|
77179c02ac
|
added option to feed additional constraints to abstraction
|
8 years ago |
|
Sebastian Junges
|
e7926b10c2
|
allow counterexamples for true jani models
|
8 years ago |
|
Sebastian Junges
|
61925d1c98
|
add option for sparse model builder to add a state encoding out-of-bounds state valuations to enable analysis of buggy models
|
8 years ago |
|
TimQu
|
f5511f4213
|
removed obsolete 'inplace' setting for multiplier
|
8 years ago |
|
dehnert
|
461668bc84
|
change default value of an option for abstraction
|
8 years ago |
|
dehnert
|
21c970f8f7
|
added dd-to-sparse engine that builds the model as a DD and then transforms the whole model to a sparse representation
|
8 years ago |
|
dehnert
|
3ad85ba0e6
|
fixes and improvements for game-based abstraction
|
8 years ago |
|
dehnert
|
5159afc348
|
further work towards proper scheduler extraction for games
|
8 years ago |
|
dehnert
|
9665f4fa30
|
sparse qualitative solving of menu games
|
8 years ago |
|
dehnert
|
edbe3b1952
|
more work on explicit game solving
|
8 years ago |
|
dehnert
|
733bec60bd
|
started on hybrid solution of abstraction
|
8 years ago |
|
dehnert
|
efbd899e46
|
update to game-based abstraction refinement
|
8 years ago |
|
dehnert
|
31fa43ab27
|
some fixes to interpolation in game-based abstraction refinement
|
8 years ago |
|
TimQu
|
efcb718851
|
removed the --forcebounds setting
|
8 years ago |
|
TimQu
|
be6d4f9854
|
renamed 'sound power' to 'sound value iteration'
|
8 years ago |
|
dehnert
|
b3c2d8bbd8
|
added option to not include dynamic constraints in maxsat counterexample generation
|
8 years ago |
|
dehnert
|
de2e94cac7
|
polished unifplus code a bit and made it the default MA (bounded reachability) solution method
|
8 years ago |
|
dehnert
|
139752eb66
|
added option to perform dd-bisimulation using exact arithmetic
|
8 years ago |
|
dehnert
|
34b6593ed8
|
overhauled output of dd-based bisimulation for benchmarking
|
8 years ago |
|
TimQu
|
ff18956fbb
|
reverted back to old native multiplier
|
8 years ago |
|
TimQu
|
4eb187ba4f
|
Added a new native multiplier
|
8 years ago |
|
TimQu
|
65676235bb
|
fixed selection options for native equation solver method
|
8 years ago |
|
dehnert
|
10f8ddc343
|
started on quotient extraction using the original variables, debugging CUDD...
|
8 years ago |
|
TimQu
|
e5e2a2465b
|
removed obsolete option
|
8 years ago |
|
TimQu
|
7e639b4328
|
multiplier settings and environment
|
8 years ago |
|
TimQu
|
a6c6118733
|
Renamed 'sound power' to interval iteration and 'quick sound power' to 'sound power'
|
9 years ago |
|
TimQu
|
ea25c8fd2e
|
renamed 'sound value iteration' to 'interval iteration' and 'quick sound value iteration' to 'sound value iteration'
|
9 years ago |
