TimQu
f3f3a31e1e
Optimization for policy recycling
Former-commit-id: b66a74b746
9 years ago
TimQu
9c645ba24b
Work on policy recycling
Former-commit-id: b8e94254ce
9 years ago
TimQu
dae0faa2a0
refactored the quick implementation of the recent bugfix
Former-commit-id: 5c0d1fa3b9
9 years ago
TimQu
4a874a5a29
Added some benchmark models from param website
Fixed two bugs considering nonatomic subformulae and constant results
Qualitative modelchecking needs to be done when applying a policy!
Former-commit-id: bd88228214
9 years ago
TimQu
87c8241ec7
policies for games
Former-commit-id: 8bfb325b60
9 years ago
TimQu
bf450688b4
The variable pool of carl needs to be cleared after executing a test.
Sampling for mdps now uses the policy of the previous iteration as initial guess
Former-commit-id: 3b8b25f30f
9 years ago
dehnert
b88165f27c
fixed the warnings related to our macros
Former-commit-id: 526b6ea956
9 years ago
dehnert
8d98403748
small fix for use of carl
Former-commit-id: 63a0e38cf5
9 years ago
TimQu
b792438d88
Added missing include
Former-commit-id: a073cf157d
9 years ago
TimQu
0089212b7e
adaptation to recent changes in carl
Former-commit-id: 90535a0d66
9 years ago
TimQu
0863d0e51a
don't store ALL the occurring policies...
Former-commit-id: f442b97b8b
9 years ago
dehnert
1d49bc6dd0
extracting the bisimulation quotient for MDPs; tests for MDP bisimulation
Former-commit-id: 5613c653ba
9 years ago
dehnert
b31d98909b
Explicit MDP bisim working but unfortunately slow :(
Former-commit-id: 6714bdbd61
9 years ago
dehnert
7156a63b0f
tried different approach for bisim for MDPs
Former-commit-id: 92d56a4620
9 years ago
dehnert
c2a0bd5ab0
initial outline of strong MDP bisimulation
Former-commit-id: 06452543ea
9 years ago
dehnert
9bac056354
enabled preconditioning for value iteration in gmm++-based MinMax equation solver
Former-commit-id: 39c4efdb52
9 years ago
TimQu
ca917a651c
MinMaxLinearEqSolvers can now use some initial policy as a first guess.
First steps to use this for region approximation
Former-commit-id: 9a8151607f
9 years ago
TimQu
a723cfca14
Made sampling for MDPs correct again
Former-commit-id: 7917200f4e
9 years ago
dehnert
9b7d4ec57b
made rational functions use cln again
Former-commit-id: a4b14f9271
9 years ago
dehnert
51bd689c96
fixed a bug in the reward model
Former-commit-id: 5302a85d6f
9 years ago
dehnert
9475d29164
fixed weak bisim for dtmc
Former-commit-id: 05462b99ec
9 years ago
dehnert
29597e014f
more work on reimplementation of weak bisim
Former-commit-id: 5bdd8ea139
9 years ago
TimQu
e80a1081bb
First steps to identify the parameters for which the optimal policy always choses the same boundary
Former-commit-id: c2561730f6
9 years ago
TimQu
b182e3fdcf
Small fix for policy extraction
Former-commit-id: fa37a1ceb2
9 years ago
dehnert
91bfdba528
Scan for equal ranges of probabilities now uses std::equal_range and reduces the number of comparisons
Former-commit-id: 3154d77a3f
9 years ago
dehnert
46fee522ff
made strong bisim for DTMCs work again
Former-commit-id: e42bafef4d
9 years ago
TimQu
6ddddd8cfa
Implemented policy extraction for value iteration
Former-commit-id: 604b4667b8
9 years ago
dehnert
1f5110b90c
work on making bisimulation fast again :(
Former-commit-id: bb89091b2d
9 years ago
dehnert
2484a515a0
some more work on bisim
Former-commit-id: aaa8088b00
9 years ago
dehnert
40a75baee7
using some template magic to make it compile again
Former-commit-id: 69888cac45
9 years ago
dehnert
11b04c7940
more work towards making the new bisim class available from the cl
Former-commit-id: b177287e00
9 years ago
dehnert
1428f1647b
commented in some more tests, however the main entry points need to be fixed because of the new templating of the bisimulation class
Former-commit-id: 7133025049
9 years ago
dehnert
11c21eb338
on my way of making (the refactored version) bisimulation work again for deterministic models
Former-commit-id: 79c089a693
9 years ago
dehnert
96954ddd15
refactoring of bisimulation class in the prospect of extending it to (CT)MDPs, not yet done
Former-commit-id: 09f47ad977
9 years ago
TimQu
b09d123779
...
Former-commit-id: 47c139f3bf
9 years ago
TimQu
1860502a3a
Deterministic states with only constant outgoing transitions are now eliminated
Former-commit-id: be5bf4f7cc
9 years ago
dehnert
97e302a78c
guarded timeouts in z3 by ifdef-guards
Former-commit-id: 1bf463686a
9 years ago
dehnert
6cfa6ac9c7
added timeout to smt solver interface
Former-commit-id: 0003c2c9cc
9 years ago
TimQu
77c2f397a9
fix for approximation model, additional test for mdps, minor changes
Former-commit-id: cc837ddf3e
10 years ago
sjunges
703013b97c
program, vector, gurobi
Former-commit-id: 6cfaf78d59
10 years ago
TimQu
c53b79b9b7
approximation model, again
Former-commit-id: a7da8e4298
10 years ago
dehnert
b3ce727f6c
fixed minor bug, tests for smt-based permissive schedulers (for upper-bounded properties) now passing
Former-commit-id: bf0261e981
10 years ago
dehnert
59501dd347
removed some object files of xerces. started working on smt-based permissive schedulers
Former-commit-id: de95333225
10 years ago
TimQu
67ff27954e
refactored approximation model (almost done)
Former-commit-id: c7f285906b
10 years ago
TimQu
046afd3804
Refactored SamplingModel
Former-commit-id: b51ed752b4
10 years ago
sjunges
ee0e34146f
build command index to action name mapping
Former-commit-id: a9b6c19e68
10 years ago
sjunges
66736c3626
More to string methods for simplevaluation
Former-commit-id: 487ed4a8d6
10 years ago
sjunges
f914c8a103
Filter std::vector by bitvector, could not find such a method before :/
Former-commit-id: b401646d07
10 years ago
sjunges
ecb214bc10
StateInfo is a StateAnnotation now
Former-commit-id: d65584b97d
10 years ago
sjunges
eacdec3939
State Annotation and subMDP also restrichts choicelabelling now
Former-commit-id: 0df7a93f3b
10 years ago