sjunges
|
31228486d3
|
towards merging, including a extension on the pstateeliminator, come back after generalizing the lra eliminator
Former-commit-id: 8ce98b8287
|
9 years ago |
sjunges
|
444318e624
|
refactoring up to tests done
Former-commit-id: 943a396fab
|
9 years ago |
sjunges
|
f7a3e02fb6
|
refactored model checkers st all are templated in the model, have to handle rational function bounds next
Former-commit-id: b665709a52
|
9 years ago |
dehnert
|
1944b947d3
|
modified formula parser to parse expressions as operator bounds and then convert them to rationals
Former-commit-id: ebf441c406
|
9 years ago |
sjunges
|
cf583ec9dd
|
formulae with rational number bounds
Former-commit-id: 17755ccf84
|
9 years ago |
sjunges
|
e4b3f4eeb9
|
intermediate commit, come back after refactoring formulae
Former-commit-id: 147133876f
|
9 years ago |
sjunges
|
8b5a2d4354
|
intermediate commit, come back after refactoring model checkers
Former-commit-id: 8cfb79b2d5
|
9 years ago |
sjunges
|
4b20a724dc
|
weight zero is no weight is now more explicit
Former-commit-id: e7494eb7bd
|
9 years ago |
sjunges
|
437e883bcf
|
first fixes after merge
Former-commit-id: f19347885d
|
9 years ago |
Mavo
|
5530f908ca
|
Fixed compile issues under Linux
Former-commit-id: 61a69f9fc7
|
9 years ago |
dehnert
|
510e525274
|
removed unnecessary define for boost::variant problem
Former-commit-id: 9c64abbbda
|
9 years ago |
dehnert
|
cc958bedf0
|
fixed wrong usage of boost::variant in NextStateGenerator
Former-commit-id: 0ba0e8d565
|
9 years ago |
TimQu
|
0760e2a7f9
|
tiny MA example, small fix and test cases for MAs
Former-commit-id: 9fe2b7cc76
|
9 years ago |
sjunges
|
16c1dab062
|
sylvan dependency duplicate removed
Former-commit-id: 39b9cc5e6e
|
9 years ago |
sjunges
|
7938ce448e
|
trying to fix boost variant by adding a define
Former-commit-id: 91c98c91a0
|
9 years ago |
sjunges
|
dc5d9637f5
|
storm-gspn added as target
Former-commit-id: 0ace6ec9a9
|
9 years ago |
Mavo
|
566cef0f91
|
Started on compiling without Carl
Former-commit-id: 5e0895d7c5
|
9 years ago |
sjunges
|
cfd6926add
|
a bit of progress
Former-commit-id: bbbb7ff21b
|
9 years ago |
sjunges
|
85f29ee744
|
Typo in diagnostic ignored fixed
Former-commit-id: 51559c8982
|
9 years ago |
sjunges
|
c9593b9e98
|
trying to fix the boost variant stuff differently
Former-commit-id: a1fb8efece
|
9 years ago |
sjunges
|
9398cfa54a
|
gcc pendantic warning switched off
Former-commit-id: c5b389f737
|
9 years ago |
sjunges
|
e0e5cd9f0e
|
progress on support for gmp, with cln everything should be fine
Former-commit-id: c91b5a7cef
|
9 years ago |
sjunges
|
5faebdff86
|
constants in header
Former-commit-id: 281e490873
|
9 years ago |
Mavo
|
12f7c08bac
|
New class for DftStateGenerator
Former-commit-id: 5d7f798de1
|
9 years ago |
Mavo
|
662bbd73d7
|
CompressedStateType as template argument for NextStateGenerator
Former-commit-id: 145182a918
|
9 years ago |
sjunges
|
7bb65dbb22
|
fix a problem with cln used/unused
Former-commit-id: 2c6a2447a9
|
9 years ago |
sjunges
|
efaab9abe1
|
potential fix for missing cln
Former-commit-id: 9ce9f1af0a
|
9 years ago |
Mavo
|
560b42a94a
|
Some interval functions not implemented
Former-commit-id: c88dca9d96
|
9 years ago |
ThomasH
|
84284555b2
|
add include
Former-commit-id: bf65a256dc
|
9 years ago |
ThomasH
|
b799963016
|
add const
Former-commit-id: e8c2cc6f29
|
9 years ago |
TimQu
|
bf7a86b650
|
fixed lower time bounds for MAs
Former-commit-id: 98ca60c52c
|
9 years ago |
TimQu
|
33e99b7b93
|
needed to add some utility::vector::toString(...)s
Former-commit-id: f61d69ff9c
|
9 years ago |
TimQu
|
c672f7aea2
|
fix in bounded reachability computation with Markov automata
Former-commit-id: fe2b399778
|
9 years ago |
TimQu
|
3784d59a85
|
bugfix
Former-commit-id: 3841028452
|
9 years ago |
TimQu
|
1525ea6702
|
better time bounds
Former-commit-id: 57140de514
|
9 years ago |
TimQu
|
b267394a2c
|
fixed the case where an objective is satisfied at the initial state.
correctly added support for lower time bounds
Former-commit-id: 4d13d5de1b
|
9 years ago |
TimQu
|
7bab48b59b
|
bounded reachability for MAs
Former-commit-id: 982277d9ab
|
9 years ago |
TimQu
|
252c2308fe
|
Renamed NeutralEcRemover -> EndComponentEliminator
Former-commit-id: 3a5546d1c4
|
9 years ago |
sjunges
|
380bed563c
|
updated the jani parser to actually buidl models
Former-commit-id: d0189e33e5 [formerly 4910b31ca3]
Former-commit-id: cd7f6ca5cb
|
9 years ago |
TimQu
|
90ae65ffa9
|
computation of digitization constant
Former-commit-id: cd75d84566
|
9 years ago |
hbruintjes
|
8ef899ef1c
|
Fix log file name argument
Former-commit-id: c13b4ca3ad
|
9 years ago |
hbruintjes
|
efae19b092
|
Use toString() for exit rates, ADL not working for some reason
Former-commit-id: cbc9eaf722
|
9 years ago |
hbruintjes
|
4e4bc255b5
|
Fix some typos in l3pp usage
Former-commit-id: c9da06a596
|
9 years ago |
hbruintjes
|
d9cb1a79f8
|
Replace cout macros with l3pp
Former-commit-id: 0cde42558d
|
9 years ago |
sjunges
|
88af02e723
|
towards new jani version
Former-commit-id: 0c5e6825ca [formerly b98985e8eb]
Former-commit-id: 9f5ef53aec
|
9 years ago |
TimQu
|
75dd78ebec
|
towards bounded reachability: added the ability to have a lower/upper bound for the weightVectorChecker result
Former-commit-id: 413c2dee0a
|
9 years ago |
sjunges
|
4f1b8f12f0
|
Extra method
Former-commit-id: 44b165558d
|
9 years ago |
sjunges
|
eff2acdbc6
|
parser update
Former-commit-id: 9a21a09597
|
9 years ago |
TimQu
|
d02c918f6a
|
forgot a little something...
Former-commit-id: dc5b68bdb6
|
9 years ago |
hbruintjes
|
ebe6775b27
|
Fix missing ValueType template arguments (which defaulted to double)
Former-commit-id: a97910eaf9
|
9 years ago |