TimQu
|
234ddb7cff
|
fixed compilation of JaniParser
|
7 years ago |
TimQu
|
a012539323
|
cleared some TODOs in the Jani Parser
|
7 years ago |
TimQu
|
e038fb64be
|
Jani: export the correct accumulation parameters for expected reward properties
|
7 years ago |
TimQu
|
d8bc689259
|
Throw an exception instead of assertion when 'wrong' jani was detected
|
7 years ago |
TimQu
|
6449dee626
|
fixed typo
|
7 years ago |
TimQu
|
611428c01f
|
allowing constants in property bounds
|
7 years ago |
TimQu
|
b4a1244d01
|
correct parsing of bounded until formulas with multiple bounds
|
7 years ago |
TimQu
|
5937131ff2
|
fixed and extended parsing of jani formulas with Emin or Emax operator
|
7 years ago |
TimQu
|
636d92894c
|
Fixed an issue with time bounded properties specified in jani
|
7 years ago |
Sebastian Junges
|
93da59fa04
|
fixed an issue with jani properties for expected time not being parsed as requested
|
7 years ago |
sjunges
|
79bb6734ed
|
compile and link parsers in seperate binary
|
7 years ago |
Sebastian Junges
|
fdcbd6369c
|
simple sanity check for bounded integers in jani
|
7 years ago |
Sebastian Junges
|
5b678f524a
|
removed old spurious output
|
7 years ago |
dehnert
|
c18340b76a
|
added mod as binary operation in expressions and slightly extended JANI support for filters
|
7 years ago |
TimQu
|
23686a0f09
|
reward bounded cumulative reward formulas + fixes for dimensions that do not need memory
|
8 years ago |
Sebastian Junges
|
324c0770dd
|
jani parser supports abscence of action declarations
|
8 years ago |
Sebastian Junges
|
241fc88077
|
multi-dimensional time bounds
|
8 years ago |
Sebastian Junges
|
3de51e28e5
|
towards reward-bounded properties
|
8 years ago |
Sebastian Junges
|
a21995052c
|
fix for probabilistic reachability formulae
|
8 years ago |
TimQu
|
f0ae3a2dfb
|
Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N
|
8 years ago |
dehnert
|
82cc586718
|
fixed some issues related to assigning an initializer list to an unordered_map which causes problems on older platforms
|
8 years ago |
dehnert
|
a323d21751
|
fixed some wrong capitalization
|
8 years ago |
Matthias Volk
|
5d79eff2cd
|
Wrapper for file opening
|
8 years ago |
sjunges
|
d8952ab5f6
|
JANI parsing formulae now with correct variable names
|
8 years ago |
sjunges
|
57fd0fa2dd
|
Fixed variable parsing in JANI, now stricter and handles a larger set of files (also detects issues in our export...).
|
8 years ago |
Sebastian Junges
|
5894f7c706
|
some forward declarations and header updates to battle recompilation times
|
8 years ago |
Sebastian Junges
|
8e32d3fa8f
|
Simplifying index levels
|
8 years ago |
Sebastian Junges
|
d3774f9958
|
JANI: parse assignment index/level
|
8 years ago |
Sebastian Junges
|
c9f1b3217d
|
Jani parsing of ITE now gets local variables
|
8 years ago |
dehnert
|
a85f4fdc89
|
replaced some StoRMs and Storms by storm, reworked version output a bit
|
8 years ago |
Sebastian Junges
|
03b634d14a
|
suppress silly warning about no return after error
|
8 years ago |
dehnert
|
b4381a7c48
|
Constants in formulas appear to be working
|
8 years ago |
dehnert
|
cb8b537baa
|
made storm compile again with expressions in time-bounds of until formula
|
8 years ago |
dehnert
|
8d3f633cbc
|
started working on allowing expressions in time-bounds of formulas
|
8 years ago |
dehnert
|
158ddc0533
|
equipped automata in JANI models with expression variable representing their location
|
8 years ago |
dehnert
|
ae93211aeb
|
template edges in JANI models
|
8 years ago |
dehnert
|
a6beda6a82
|
some more fixes to jit model builder
|
9 years ago |
Sebastian Junges
|
04003de854
|
transient unbounded variables must have iniatial value
|
9 years ago |
Sebastian Junges
|
d246517757
|
removed src prefix in all includes
|
9 years ago |
Sebastian Junges
|
e1d201c85e
|
c++ code compiles again after rename
|
9 years ago |
Sebastian Junges
|
3a7ee7867b
|
rename files (does not compile)
|
9 years ago |
sjunges
|
1fd89f3922
|
fixes in reach expression parsing for expected reward
Former-commit-id: d9f5e887d8 [formerly 02cea9bff2 ]
Former-commit-id: dd387c2595
|
9 years ago |
dehnert
|
b579978938
|
cleaned up jit model builder, added options, added doctor procedure, prepared Markov automata
Former-commit-id: bb8d1d95cc [formerly 6deb9e19a0 ]
Former-commit-id: d6b8563723
|
9 years ago |
sjunges
|
ecc74595ba
|
several jani related fixes: IsInitialRestrictionSet(), FormulaContext, minor things
Former-commit-id: f1a5b2edcf [formerly 6a9cb0a988 ]
Former-commit-id: 11bf234fcc
|
9 years ago |
sjunges
|
435b3084cb
|
Finally, Globally
Former-commit-id: fa2ff942de [formerly 105d3af631 ]
Former-commit-id: 1560f7cfce
|
9 years ago |
sjunges
|
9faa7539c5
|
parser
Former-commit-id: 6e1af26d2f [formerly 995647eeb7 ]
Former-commit-id: 0865990abf
|
9 years ago |
sjunges
|
ed970d78b1
|
property support for jani -- several changes throughout code, parser currently only supports probability properties
Former-commit-id: d5db0cda02 [formerly 66d55d7e43 ]
Former-commit-id: 1672b21b12
|
9 years ago |
sjunges
|
3626c044d3
|
several improvements towards jani-property support
Former-commit-id: 3d56f22d99 [formerly 1f527643ab ]
Former-commit-id: 75e40a9b69
|
9 years ago |
sjunges
|
744216d5d2
|
export formulae
Former-commit-id: 4932938e38 [formerly 95b3269c75 ]
Former-commit-id: 974a891cb6
|
9 years ago |
sjunges
|
12a5258a45
|
second time is a charm
Former-commit-id: 9af436c843 [formerly 0594ee49f8 ]
Former-commit-id: db0f6c4dc3
|
9 years ago |