Joachim Klein
40a982430c
cmake for carl: handle situation where carl version information is missing
Older carl versions don't provide detailed version information, so we
provide an informative error message instead of cmake syntax errors during
the comparison.
7 years ago
dehnert
ad456916e9
first working version of sparse reward model quotienting
7 years ago
dehnert
334ed077fd
lifted quotient extractor from ADDs to BDDs
7 years ago
dehnert
f55fab0924
lifted representative generation from ADDs to BDDs
7 years ago
dehnert
722cb3109c
dd quotient extraction of reward models in dd bisimulation
7 years ago
dehnert
34e23f94fc
started on reward model preservation in DD bisimulation
7 years ago
dehnert
b31fb7ab5e
first working version of sparse MDP quotient extraction of dd bisimulation
7 years ago
dehnert
c5da67d6cf
refined warning for automatic switch to policy iteration in exact mode
7 years ago
dehnert
8cdbf281fa
make minmax solvers use policy iteration when --exact is set and no other method was explicitly set
7 years ago
dehnert
f96403de9e
added reduction to state-based rewards to symbolic (reward) models
7 years ago
dehnert
eaee50f077
fixed bug, implemented new sparse quotient extraction for sylvan
7 years ago
TimQu
27ac2798c4
allowing multi(...) path formulas in multiobjective model checking
7 years ago
TimQu
5dd4bdbfc6
fixed ambiguous memory labeling
7 years ago
TimQu
a16eee4982
made multi(..) path formulas pass the fragment check
7 years ago
TimQu
0e8049d4df
removed lots of debug output
7 years ago
TimQu
354b3103f0
improved multi-dimensional reward unfolding
7 years ago
TimQu
857bc63145
fix for model-memory-product where the mapping between (modelstate, memorystate) and productState did not work as soon as the memory structure ran out of scope
7 years ago
TimQu
1f2ab1a672
added function BitVector::fill() which sets all bits to true
7 years ago
dehnert
b7be027f7a
switching workplace
7 years ago
dehnert
5e2ccaeeb5
started moving towards simpler sparse quotient extraction
7 years ago
Matthias Volk
f254a05f4e
Update mtime_cache files for travis caching
7 years ago
TimQu
2eb13cdc10
fixed exploration of reachable epochs
7 years ago
dehnert
2f97684d6d
fixed bug in recent optimization (only CUDD-based implementation was faulty)
7 years ago
TimQu
b3507b8f96
fixed 'toIntegralVector' method
7 years ago
TimQu
df6ba12c74
enabled handling of reward bounded formulas within multi-objective formulas
7 years ago
Matthias Volk
39d789f042
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
7 years ago
Matthias Volk
c09f6c1924
Update mtime_cache files for travis caching
7 years ago
dehnert
d23547d99f
started optimizing some DdManager methods
7 years ago
Sebastian Junges
8cacede55f
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
7 years ago
TimQu
9e2f8fb1a8
first version of weight-vector based apporach with reward bounded objectives
7 years ago
TimQu
cf4ee1eb5f
also store the initial states within an epoch model
7 years ago
TimQu
6334168fbe
also store the reward choices in the epoch model
7 years ago
sjunges
5624818caf
Updated Changelog
7 years ago
sjunges
66cf4f1d28
Command line access to onlyconstraints for any model type
7 years ago
sjunges
2b01e2fa61
GraphConditions for any model type
7 years ago
TimQu
3c5a270482
Further improvements for the multi dimensional reward unfolding
7 years ago
dehnert
93f385a399
remove debug output
7 years ago
dehnert
7e723b2b8f
faster block encoding for CUDD; optimizations in sparse quotient extraction
7 years ago
TimQu
5025b33aac
Merge branch 'master' into reward-bounded-multi-objective
7 years ago
TimQu
22e375bd79
Implemented more functionality of the reward unfolding
7 years ago
TimQu
938a488eb1
Get a Memory structure builder from an existing memory structure
7 years ago
TimQu
50e1fe0c15
increment() function for BitVector
7 years ago
sjunges
a27e7bdc82
no longer use arithconstraint
7 years ago
sjunges
a994b80931
getting rid of outdated carl simple constraint usage
7 years ago
Sebastian Junges
04e542059d
Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm
7 years ago
Sebastian Junges
9e9060ecd7
fix in changelog
7 years ago
sjunges
b4a8833e3f
towards getting rid of code duplication in storm-pars-cli
7 years ago
sjunges
e718acffba
move cli stuff from storm lib to an own small lib
7 years ago
sjunges
2c2dc5acd8
Changed API such that the command line settings do not occur in the settings anymore. Moreover, to prevent having 15 Boolean arguments, the build options are now part of the API.
7 years ago
sjunges
98d124bd06
As the builder options now occur in the API, we should improve their documentation.
7 years ago