TimQu
529526593b
improved structure in rewardunfolding
7 years ago
TimQu
2bccb7af78
modelMemoryProduct can now return the considered model and memory structure
7 years ago
TimQu
de1e9967a3
added some necessary conditions for the rewardbounded weight vector checker
7 years ago
TimQu
0cca4a51d0
added weight vector checker for reward bounded objectives
7 years ago
TimQu
721dd37a62
Moved reduction of the preprocessed model into the weightvectorchecker
7 years ago
TimQu
76c01de25c
use utility::vector::max_if to compute the maximum exit rate in an MA
7 years ago
TimQu
4d248eb0a1
fixed assertion
7 years ago
TimQu
8efccd76d2
started to make multi-objective preprocessing more flexible w.r.t. different checkers
7 years ago
TimQu
dae09653e5
Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective
7 years ago
dehnert
569b0122b8
introduced different minmax equation system types for requirement retrieval
7 years ago
dehnert
f7c803827b
remove debug output
7 years ago
dehnert
4adee85fa5
added checking requirements of MinMax solvers to model checker helpers
7 years ago
dehnert
3829b58e0d
introduced top-level solve equations function to centrally check for requirements
7 years ago
dehnert
72234e96b2
started on requirements for MinMax solvers
7 years ago
TimQu
31af523ea1
implemented caching of the EC elimination result in the standard weight vector checker
7 years ago
TimQu
9716289f6a
Added abstract superclass for WeightVectorCheckers
7 years ago
Matthias Volk
3c8f9a2ecf
Added 5th build stage
7 years ago
dehnert
e278c3ef69
moving from internal reference to pointer in StandardMinMax solver
equipped MinMax solvers with default constructors
7 years ago
TimQu
591a53582a
fixed test
7 years ago
TimQu
e0253ecba2
fixed new test
7 years ago
TimQu
acd6c5e9be
fix for toIntegralVector
7 years ago
TimQu
e1aba323bf
more tests for reward unfolding
7 years ago
dehnert
0c5aa1645d
fix reward model generation in JIT builder
7 years ago
dehnert
5bb6564078
remove debug output
7 years ago
TimQu
06ec288296
enabled pcaa test that uses rational numbers
7 years ago
TimQu
2d2cc95774
fixed issue #12 raised by Joachim Klein
7 years ago
dehnert
beb80cc5af
fixes issue #11 raised by Joachim Klein
7 years ago
dehnert
2d30108b49
fixes issue #10 raised by Joachim Klein
7 years ago
dehnert
ecade3f857
fixes issue #9 raised by Joachim Klein
7 years ago
TimQu
172b17d7ae
simple testcase for the reward unfolding
7 years ago
TimQu
3beaf6cd64
Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective
7 years ago
TimQu
e2ba3dbd06
fix for multiple subobjectives
7 years ago
sjunges
12c79ad6ea
export choice labels
7 years ago
dehnert
e2e1407f3e
not calling sylvan_var on leaf nodes of sylvan anymore
7 years ago
dehnert
5856d9fe51
removed some debug output
7 years ago
dehnert
04a24a2108
Merge remote-tracking branch 'origin/master' into symbolic_bisimulation
7 years ago
dehnert
6bebb3c9d5
fix bug in rational number/function handling with sylvan
7 years ago
dehnert
ee87067c9a
fixed type to make gcc happy
7 years ago
dehnert
d2a493a92d
fixed several crucial bugs related to dd bisimulation, tests now passing
7 years ago
dehnert
a7dcdcd84d
started on tests and added a ton of debug output
7 years ago
dehnert
11d2ee2fda
making sure to add meta variables to transition matrix DD to make sure one can abstract from them later
7 years ago
dehnert
36554b5b87
fixed some issues with reward preservation in dd-based bisimulation
7 years ago
dehnert
9a6abf7eec
fixed a bug in dd-based reward model building
7 years ago
sjunges
b120b74fa9
StateActionPair to index should be part of nondeterministicmodel
7 years ago
sjunges
6e506e5a66
moved application of permissive scheduler to an own transformer
7 years ago
Sebastian Junges
d271824461
prepare to initialize but not make settings known, not yet fully functioning
7 years ago
Sebastian Junges
d2002129b7
remove output
7 years ago
Sebastian Junges
e0452be54b
move some of the cli stuff to an own header
7 years ago
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