sjunges
|
0f6a741276
|
pgcl
Former-commit-id: 63d52fc706 [formerly 90b7939792 ]
Former-commit-id: 04e29e8c41
|
9 years ago |
dehnert
|
12ac3549da
|
adapted relevant parts to new way of specifying initial values/restrictions
Former-commit-id: a55abbe3b6 [formerly 6a9d8a6a55 ]
Former-commit-id: 47799adaf2
|
9 years ago |
dehnert
|
b405a67b54
|
removed RewardIncrement. fixed PRISM to JANI converter
Former-commit-id: c189fa8e60 [formerly 63dccbdb95 ]
Former-commit-id: 36449defd0
|
9 years ago |
dehnert
|
1b19372a14
|
changed a default argument initializer list to make compilers happier
Former-commit-id: 41dcbd2f10
|
9 years ago |
dehnert
|
059f55eefc
|
commit to switch workplace, debugging in progress
Former-commit-id: 9ab5d903e9
|
9 years ago |
dehnert
|
673c329311
|
prepared upcoming fix for refinement based on quantitative information
Former-commit-id: 35dee37951
|
9 years ago |
dehnert
|
156ab071a5
|
more work on abstraction refinement
Former-commit-id: 20dcaa7518
|
9 years ago |
PBerger
|
d76e9729da
|
Leave Replacement finally working.
Former-commit-id: 239ea6d897
|
9 years ago |
dehnert
|
bc1eff959f
|
graph algorithms for games now also compute player 2 prob0/1 states and the generated strategies are adapted accordingly
Former-commit-id: da52581328
|
9 years ago |
PBerger
|
c9f2eef826
|
Added functionality for replacing leaves in SRF MTBDDs.
Former-commit-id: d7af779036
|
9 years ago |
TimQu
|
d1ea675245
|
Added missing case for Power when converting to z3::expr
Former-commit-id: 4279fba636
|
9 years ago |
TimQu
|
e1aca37c86
|
some minor tweaks plus polling example
Former-commit-id: eebe4ca6d6
|
9 years ago |
dehnert
|
d16e47882d
|
fixed bug and added tons of debug output
Former-commit-id: 5bf2d6d82f
|
9 years ago |
TimQu
|
ee8d345667
|
csl MA model checker does not allow rational numbers
Former-commit-id: 86992a9fba
|
9 years ago |
dehnert
|
a663a37e21
|
fixed a bug that prevented correct strategy generation in iterative solver
Former-commit-id: 1df15b439d
|
9 years ago |
dehnert
|
20f07bf291
|
added incremental strategy generation to symbolic game solver and removed some debug output
Former-commit-id: 96af928d00
|
9 years ago |
dehnert
|
a0ad4b25de
|
corrected minor typo
Former-commit-id: f5db2f368f
|
9 years ago |
dehnert
|
f45b7f9171
|
fixed some bugs and started on quantitative refinement
Former-commit-id: 31259ad299
|
9 years ago |
PBerger
|
da199866e6
|
Added tests for minAbstractRepresentative.
Everything still in early alpha. Expect Debug output.
Former-commit-id: 2712fce4dd
|
9 years ago |
dehnert
|
66b0817a35
|
fixed bugs here and there
Former-commit-id: d10d85339d
|
9 years ago |
PBerger
|
68b14b3076
|
Moved BDD functionality in Sylvan to sylvan_bdd_int.h to allow reuse.
Added min/maxExistsRepresentative API to storage/dd/Add.
Former-commit-id: 45ff98b35a
|
9 years ago |
dehnert
|
56b5b98a2c
|
towards strategy generation in game solver
Former-commit-id: fb582ba531
|
9 years ago |
dehnert
|
bde84d0073
|
fixed symbolic game solver wrt. illegal masks. numerical solving step in game-based model checker working, but no refinement yet.
Former-commit-id: 6189a1e538
|
9 years ago |
dehnert
|
8b29ab079c
|
fixed some bugs in custom cudd functions
Former-commit-id: b73b894674
|
9 years ago |
dehnert
|
5fcc2e9e7e
|
created separate version of Cudd_addToBddApply to deal with negated edges in resulting BDDs
Former-commit-id: 8141cbddc2
|
9 years ago |
dehnert
|
6168af3c99
|
intermediate commit in an attempt to have proper cudd support for some operations
Former-commit-id: 0bb840ecff
|
9 years ago |
dehnert
|
24667fffc4
|
added cudd functions for equal/less/less_equal/greater/greater_equal that directly return a BDD instead of an ADD
Former-commit-id: 448b5e2f7c
|
9 years ago |
dehnert
|
cc550984b3
|
enabling qualitative answers of game-based model checker
Former-commit-id: b5eca1d671
|
9 years ago |
dehnert
|
d35d72d5f3
|
slightly reformulated check for initial maybe states
Former-commit-id: ac80e101bf
|
9 years ago |
dehnert
|
0cd03845e8
|
abstraction loop working for purely qualitative refinement
Former-commit-id: ce28ed97c2
|
9 years ago |
dehnert
|
a8383a283d
|
fixed wrong header inclusion in previous commit
Former-commit-id: f91e63cccd
|
9 years ago |
dehnert
|
96891acfe7
|
included missing (at least for some compilers) header
Former-commit-id: 4792acf519
|
9 years ago |
dehnert
|
a3f2abbd92
|
more work towards closing the refinement loop
Former-commit-id: 1579e73036
|
9 years ago |
ThomasH
|
b930ed0dde
|
use int instead of string ids
Former-commit-id: 91c6eda5c6
|
9 years ago |
dehnert
|
bcb13a4fe1
|
moved deletion of commands (if guard becomes false) from Program::substitute to Program::simplify
Former-commit-id: ec5b4d4a57
|
9 years ago |
dehnert
|
e6d9c85749
|
fixed some bugs related to simplifaction of PRISM programs
Former-commit-id: 3c81bcac8d
|
9 years ago |
dehnert
|
6d5f4dc9c9
|
fixed bug in detection whether parameters are only used in probabilities/rewards
Former-commit-id: 1929f5e079
|
9 years ago |
Mavo
|
5109c45c23
|
Fixed returning result for pCTMC
Former-commit-id: 2db7f87f65
|
9 years ago |
Mavo
|
495b42ff4c
|
Temporarily split new approximating state generation into own builder
Former-commit-id: 70be02f2ae
|
9 years ago |
dehnert
|
b550e61677
|
started working on refinement based on qualitative check
Former-commit-id: 3569a55851
|
9 years ago |
dehnert
|
2149bd2b10
|
added some assertions in game-based model checker
Former-commit-id: 6d7e8770b2
|
9 years ago |
dehnert
|
7d50a6b839
|
graph algorithms for games can now produce player strategies even if they can pick any choice (if requested)
Former-commit-id: 98119f274d
|
9 years ago |
ThomasH
|
8ba12791ff
|
add GspnBuilder class
Former-commit-id: e6e91366cc
|
9 years ago |
dehnert
|
4c9f22c7c2
|
included missing header
Former-commit-id: a1e81897dd
|
9 years ago |
dehnert
|
1bb116dd1c
|
some more work on game-based model checker
Former-commit-id: 50399c3d7c
|
9 years ago |
dehnert
|
033faa62f0
|
changed node shapes a little
Former-commit-id: 8c7fffaf65
|
9 years ago |
dehnert
|
d492d5c62f
|
fixed bug in ADD iterator and started on exporting menu games to dot file
Former-commit-id: 9467aa7094
|
9 years ago |
dehnert
|
5bf666be4c
|
fix in existsAbstractRepresentative
Former-commit-id: c884deaf11
|
9 years ago |
dehnert
|
f342ce3287
|
translation from expressions involving the power operator to rational functions/rational numbers is now possible
Former-commit-id: e0ce43ab35
|
9 years ago |
dehnert
|
9878c1bdc3
|
fixed some tests that were failing because of (now) proper bottom state computation
Former-commit-id: ecc8dfb065
|
9 years ago |