dehnert
|
7750480714
|
JANI model builder for DTMCs working
Former-commit-id: 25f12f3e05
|
9 years ago |
dehnert
|
310db8a234
|
started to include reachability in JANI model generation
Former-commit-id: d54f35b999
|
9 years ago |
dehnert
|
6313e4c31b
|
fixed a bug in symbolic model generator
Former-commit-id: de49f7b812
|
9 years ago |
dehnert
|
adf8232896
|
more work and fixes for symbolic JANI builder
Former-commit-id: 5ca11938c1
|
9 years ago |
dehnert
|
c4327e91a9
|
more work on symbolic JANI model builder
Former-commit-id: 4fe002c4f8
|
9 years ago |
dehnert
|
9c75e9dbd7
|
more work on JANI model generation
Former-commit-id: c5a5df87ee
|
9 years ago |
dehnert
|
ecc1a80358
|
added conversion from PRISM to JANI. Added simplistic tests for that.
Former-commit-id: 5b31fa589c
|
9 years ago |
sjunges
|
3b5c27acba
|
more test-files included, two small fixes in parser
Former-commit-id: 0e9000c988
|
9 years ago |
sjunges
|
b64dc408ac
|
test case for die.jani parsing
Former-commit-id: b58a9102a6
|
9 years ago |
dehnert
|
d38e7d5eb9
|
started working on jani data structures
Former-commit-id: 30deb6d38d
|
9 years ago |
dehnert
|
7d03f0e4d0
|
improved error checking for custom parallel composition. added small tests.
Former-commit-id: 8f6b6913d6
|
9 years ago |
dehnert
|
bf65ef726c
|
system composition in PRISM appears to be working
Former-commit-id: e7f0dd84e8
|
9 years ago |
dehnert
|
9db10e7849
|
added all composition operators of PRISM
Former-commit-id: f9a25fbcb1
|
9 years ago |
Mavo
|
a0d659f2da
|
always use shared_ptr<Formula const>
Former-commit-id: 63a447e887
|
9 years ago |
dehnert
|
5934a42898
|
Squashed 'resources/3rdparty/sylvan/' content from commit d91f6ac
git-subtree-dir: resources/3rdparty/sylvan
git-subtree-split: d91f6acb55
|
9 years ago |
dehnert
|
3476df75e8
|
finally removed log4cplus and affected code parts
Former-commit-id: 2beea8195e
|
9 years ago |
hbruintjes
|
1bb2be74d4
|
Update CMake files
Former-commit-id: 9752e504e9
|
9 years ago |
dehnert
|
37220cae57
|
removed two assertions in tests because they no longer apply
Former-commit-id: fcf132e685
|
9 years ago |
dehnert
|
60bbce0ba1
|
added two tests for exploration engine
Former-commit-id: 960393b229
|
9 years ago |
TimQu
|
d2d1ebdb1a
|
test didn't compile due to recent changes in carl::rationalize
Former-commit-id: 81af3a0f52
|
9 years ago |
Mavo
|
7688d7ef42
|
Fixed test
Former-commit-id: 9e1094a5a0
|
9 years ago |
Mavo
|
c9f04ecc0b
|
Added IOSettings
Former-commit-id: 95946a7666
|
9 years ago |
Mavo
|
effadc5cca
|
Split into general settings and markov chain settings
Former-commit-id: 619a2e3622
|
9 years ago |
dehnert
|
e6ec8d5b60
|
fixed formula building in some performance tests
Former-commit-id: 1f6c5f67db
|
9 years ago |
Mavo
|
f48d8bc6b1
|
Initialize all modules in tests and normal storm
Former-commit-id: 249a702d66
|
9 years ago |
Mavo
|
67d77608bd
|
Refactoring of settings
Former-commit-id: ea4350fc1c
|
9 years ago |
TimQu
|
4bb4e29e43
|
Added a test case where model checking expected rewards on MDPs currently fails
Former-commit-id: 35dbe908c8
|
9 years ago |
dehnert
|
adb42b3ac0
|
fixed minor things related to merge
Former-commit-id: f428c2808b
|
9 years ago |
Mavo
|
652aeb7562
|
Fixed compile error with CarlRationalNumber instead of RationalNumber
Former-commit-id: 0fbb4ad1c1
|
9 years ago |
TimQu
|
6e8602413e
|
ModelInstantiator + test
Former-commit-id: f3c9980067
|
9 years ago |
dehnert
|
0b98412bb4
|
further work on making row-grouping optional
Former-commit-id: bae568660f
|
9 years ago |
Mavo
|
f8b9ece2fd
|
Added mini test for BitVector
Former-commit-id: 8ec7395c0d
|
9 years ago |
dehnert
|
fad28df7d6
|
first working version of next-state generator for PRISM models
Former-commit-id: 548a725e25
|
9 years ago |
sjunges
|
6818c6dc0d
|
Fixed tests when no log4plus is available.
Former-commit-id: f1ae81376c
|
9 years ago |
dehnert
|
08bed36579
|
fixed an issue in performance tests and renamed all remaining LOG4CPLUS macro invocations to that of storm
Former-commit-id: 8536943978
|
9 years ago |
dehnert
|
5ce72a85ce
|
added small test for conditional probability and conditional rewards
Former-commit-id: 891d99eea6
|
9 years ago |
dehnert
|
e40cc65117
|
added tests for fragment checker
Former-commit-id: 2de76ee5a5
|
9 years ago |
dehnert
|
dc8a5b11e0
|
more refactoring regarding fragment checking
Former-commit-id: fd335f6f8e
|
9 years ago |
dehnert
|
3727018ef4
|
added functionality to sparse MDP helper to compute until probabilities just for maybe states (and produce the corresponding scheduler)
Former-commit-id: 79aae02a13
|
9 years ago |
sjunges
|
471ae19438
|
refactored further parts of the external library building
Former-commit-id: 81ab395bb1
|
9 years ago |
dehnert
|
8f087597cc
|
more work towards proper scheduler generation
Former-commit-id: ee6237ef49
|
9 years ago |
dehnert
|
5a1039838f
|
made everything compile again and all tests passing
Former-commit-id: 65c66fb58f
|
9 years ago |
dehnert
|
52f071c74a
|
fixed minor bug (apparently because of new boost version) in spirit error handling
Former-commit-id: 23ac194fc3
|
9 years ago |
dehnert
|
4367bdb378
|
properly introduced CheckTask in all model checkers and made it compile again (+ functional tests working)
Former-commit-id: d44db3c342
|
9 years ago |
sjunges
|
d8191d8c6a
|
const formulae
Former-commit-id: 910d7ca539
|
9 years ago |
sjunges
|
ad01dfa611
|
refactored bisimulation a bit (mainly the entry point as well as hidden some options)
Former-commit-id: 5405a14930
|
9 years ago |
PBerger
|
f0f3e8cbb3
|
Fixed test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp when MathSAT support is unavailable.
Former-commit-id: c4b91a2ac5
|
9 years ago |
dehnert
|
0f6e6e4da1
|
added feature to compute step-bounded until probabilities in parametric models
Former-commit-id: 172e87cb55
|
9 years ago |
sjunges
|
1e1400d68d
|
merge
Former-commit-id: eb9efc4bb2
|
9 years ago |
dehnert
|
0d912ee59d
|
finalized sylvan tests
Former-commit-id: e20160ce2c
|
9 years ago |