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 |
dehnert
|
984abfd22b
|
proper renaming of files
Former-commit-id: 5594ddec38
|
9 years ago |
dehnert
|
58857d62ed
|
renamed double literal to rational literal
Former-commit-id: 7bafe79eed
|
9 years ago |
dehnert
|
7b2a667a9d
|
double literal now stores rational internally
Former-commit-id: c0f089b8ba
|
9 years ago |
dehnert
|
569b27e110
|
work towards having rational numbers instead of doubles as literals in expressions
Former-commit-id: c62f8af061
|
9 years ago |
dehnert
|
241f23f730
|
fixed bug in abstraction information object
Former-commit-id: 1338ecfa47
|
9 years ago |
PBerger
|
be7353358f
|
Added Test for constants in Cudd/Sylvan.
Added functionality for existsAbstractRepresentative in Sylvan. Still very broken!
Former-commit-id: df2b36a8d8
|
9 years ago |
dehnert
|
f7f14f13fc
|
minor fix before bedtime
Former-commit-id: c558c23122
|
9 years ago |
dehnert
|
9e64e998f3
|
fixed tests wrt. proper bottom state computation
Former-commit-id: 223795c955
|
9 years ago |
dehnert
|
e2ba3f3725
|
bottom states appear to be working, tests not yet adapted
Former-commit-id: 801d99c128
|
9 years ago |
dehnert
|
3bc0b4eacc
|
more work on proper bottom state computation
Former-commit-id: 38718e1c5c
|
9 years ago |
dehnert
|
7ab88457a7
|
corrected reference to wrong settings module
Former-commit-id: 2f35b2dc82
|
9 years ago |
dehnert
|
e43dfc2784
|
removed unused setting
Former-commit-id: 18a91c2acb
|
9 years ago |
sjunges
|
fa9e33da59
|
option for print timings
Former-commit-id: 845ce83bda
|
9 years ago |
sjunges
|
e1a8d61190
|
fix in assignment parsing, better error messages
Former-commit-id: 25b7ec8144 [formerly c291504459 ]
Former-commit-id: 1534008ff0
|
9 years ago |
sjunges
|
c812d950a5
|
restrict-initial support & error message for invariants
Former-commit-id: 2940a8c675 [formerly f9fc0f967d ]
Former-commit-id: 63a5c9e844
|
9 years ago |
dehnert
|
4f54759f38
|
intermediate commit [fixing bottom states/transitions]
Former-commit-id: d457ce2fb4
|
9 years ago |
sjunges
|
6966f2fffe
|
fix sign to be as in jani, add truncate
Former-commit-id: 9bdfa8f9fa [formerly 48e15d5070 ]
Former-commit-id: 298d46b5cc
|
9 years ago |
sjunges
|
b464ac5ecb
|
sign operator is now supported by storm::expressions
Former-commit-id: 16abfce08d [formerly a07fb24acb ]
Former-commit-id: d0f0be7df6
|
9 years ago |
sjunges
|
035a50fce9
|
support for transient assignments in locations, changed assignment to jani::variable, notice that (already broken) prism-to-jani is disabled as long as we reshape jani code
Former-commit-id: 9bf2f68c7c [formerly 2a1181a603 ]
Former-commit-id: d487b0fc74
|
9 years ago |
dehnert
|
1280c88b4f
|
renamed prob branching variables to aux variables in preparation for proper bottom state creation in game abstraction
Former-commit-id: e855b14b46
|
9 years ago |
sjunges
|
20cd2d24ca
|
dedicated error messages for clock and continuous variables
Former-commit-id: 901a6b20ef [formerly 45bc2fb66b ]
Former-commit-id: cf40a01a53
|
9 years ago |
sjunges
|
13d45118af
|
initial value support unbounded integers, some extra error messages)
Former-commit-id: 72a35269f3 [formerly 243d50b5af ]
Former-commit-id: 9c7e2bd9eb
|
9 years ago |