dehnert
|
deec423f27
|
fixed infinite recursion in constants comparator
Former-commit-id: b36b352d36
|
9 years ago |
dehnert
|
1198951c3e
|
more work on game abstraction of PRISM programs
Former-commit-id: b5bec829e2
|
9 years ago |
TimQu
|
adc5c8d1c1
|
Fixed another memory leak: CheckResults have not been destructed properly.
Former-commit-id: 5631c101bb
|
9 years ago |
dehnert
|
f013ddfb4c
|
The determined relevant predicates are now added to the SMT solver of an abstract command. Also, variable bounds are enforced.
Former-commit-id: 703b49e732
|
9 years ago |
dehnert
|
b28f36bb34
|
work on game-based abstraction
Former-commit-id: 4635199f84
|
9 years ago |
dehnert
|
36e8359efa
|
added some useful functions to variable partition
Former-commit-id: b290129abb
|
9 years ago |
dehnert
|
fd5e908481
|
more work on variable partition
Former-commit-id: ce50d448a4
|
9 years ago |
dehnert
|
d4ed882795
|
more work on menu-game abstraction PRISM programs
Former-commit-id: acc54b7f15
|
9 years ago |
dehnert
|
e51a3cfa85
|
refined cut-off of builders a little. Now, based on the property, more of the states are treated as terminal states of the model
Former-commit-id: 4b68d6f1e8
|
9 years ago |
dehnert
|
e8e77f0dd3
|
fixed problem with prefix of fresh variables
Former-commit-id: 1a7a87cfeb
|
9 years ago |
sjunges
|
3a17477713
|
change engine in options...(preliminary)
Former-commit-id: 56e05ef08c
|
9 years ago |
sjunges
|
c3e390c59a
|
extended api with an option to verify model according to given engine
Former-commit-id: b2163590a5
|
9 years ago |
sjunges
|
73bfdda6ed
|
missing file
Former-commit-id: 3778460bdf
|
9 years ago |
sjunges
|
ebdd979d2c
|
settings: checks after config file, added finalize
Former-commit-id: a383159a02
|
9 years ago |
dehnert
|
6a80348150
|
fixed issue related to row groups in sparse matrix and adapted the affected calling sites
Former-commit-id: 96c6fd7e59
|
9 years ago |
sjunges
|
649c928828
|
further refactored api / shifted some highlevel functionality to cli
Former-commit-id: 0fc2dac6a7
|
9 years ago |
sjunges
|
c281efcde3
|
refactored parts of the api
Former-commit-id: 3457c238bb
|
9 years ago |
dehnert
|
fd86d430ae
|
minor fix
Former-commit-id: f5e5f0fde5
|
9 years ago |
dehnert
|
5521172ed1
|
more work on sparse game solver
Former-commit-id: df95038635
|
9 years ago |
dehnert
|
e659dd8c4a
|
some work on sparse game solver
Former-commit-id: 74450365b3
|
9 years ago |
sjunges
|
8fd0ee2ecd
|
Formula to string added
Former-commit-id: 53eb9bb5b4
|
9 years ago |
dehnert
|
b2d8cae9ce
|
instantiated (and fixed occurring problems) explicit parsers with intervals as the reward model value type
Former-commit-id: bf452cd751
|
9 years ago |
sjunges
|
01a3748e87
|
Refactored part of the API / more functions
Former-commit-id: eb8deb537c
|
9 years ago |
dehnert
|
bc3f6b8d80
|
fixes for parts that were affected by recent parser templating
Former-commit-id: f71de5cff4
|
9 years ago |
dehnert
|
27e06940a9
|
templated all explicit parsers so that they may now be modified to produce non-double models
Former-commit-id: dd7f8767f8
|
9 years ago |
dehnert
|
22f1d99a15
|
missing files finally added
Former-commit-id: 3ab8472b25
|
9 years ago |
sjunges
|
7fd28d4564
|
refactored cmakelists
Former-commit-id: 34e4e217a6
|
9 years ago |
chris
|
a216b5a9d9
|
added support for parsing choice labels for explicit MDPs
Former-commit-id: 89bb1817b4
|
9 years ago |
sjunges
|
dbe997a433
|
resolved linker error - sorry
Former-commit-id: 6fcb8fa245
|
9 years ago |
sjunges
|
46d8accf6e
|
logic::comparisontype operations
Former-commit-id: fdcb275bc8
|
9 years ago |
sjunges
|
ebab145180
|
use default bitvector move, which is fine
Former-commit-id: e646a13fb5
|
9 years ago |
sjunges
|
6503d929de
|
includes the headers for the number types supported by the carl-configuration used on the system
Former-commit-id: 18f80e9157
|
9 years ago |
sjunges
|
be0eee21db
|
Dont build so many models with float/rational functions
Former-commit-id: 692ab47afa
|
9 years ago |
sjunges
|
2213b01ece
|
changes in milp permissive scheduler
Former-commit-id: 6b11d01b88
|
9 years ago |
sjunges
|
b007d45543
|
Extended lp solver factory interface
Former-commit-id: 437e62619d
|
9 years ago |
dehnert
|
7946483f09
|
added function to modify state-action rewards in nondeterministic model
Former-commit-id: d3a4c38707
|
9 years ago |
sjunges
|
e7d82fbaf5
|
Fix
Former-commit-id: edd0ad8b36
|
9 years ago |
sjunges
|
6d10ba0ad0
|
compiles again
Former-commit-id: 1c09323cd1
|
9 years ago |
sjunges
|
f08f66e900
|
added an option for polic extraction to the helper, some includes
Former-commit-id: 44b6a5d03f
|
9 years ago |
sjunges
|
2dc9eb9b83
|
Currently exclude smtrat- does not compile with current version.
Former-commit-id: cbafb48242
|
9 years ago |
sjunges
|
72ef715d68
|
Return type to also include partial schedulers
Former-commit-id: 65bee19f6a
|
9 years ago |
dehnert
|
8d2bd4fd9d
|
fixed two warnings
Former-commit-id: a845b90c07
|
9 years ago |
dehnert
|
7cafd61c38
|
switched gcc to use c++14 as well
Former-commit-id: 32d9c46192
|
9 years ago |
dehnert
|
e364d3be53
|
added missing header
Former-commit-id: 9f3072ffc9
|
9 years ago |
sjunges
|
2f5df9d72f
|
use the configured factory in the sparse mdp helper
Former-commit-id: 8d3faf1c6b
|
9 years ago |
sjunges
|
73310b9881
|
fixed tests: glpk had wrong minimize, solver.cpp tested in wrong direction on policy iteration in case we use top. value iteration
Former-commit-id: 71215b8e46
|
9 years ago |
sjunges
|
8568ee3986
|
only one optimization direction enum -- towards integration of termination criterions on the model checker
Former-commit-id: 648855264e
|
9 years ago |
dehnert
|
57338640be
|
added missing include
Former-commit-id: c67bb4a99e
|
9 years ago |
dehnert
|
f4211637db
|
fixed warning and missing include
Former-commit-id: 09ad5ffb73
|
9 years ago |
dehnert
|
56eae69703
|
added more missing headers
Former-commit-id: 11be18e0d9
|
9 years ago |