Tim Quatmann
|
40f4141b56
|
Jani: Allowing bounded types for constants as pointed out in GitHub issue #37
|
6 years ago |
|
Tim Quatmann
|
971f4c8508
|
Quantiles: Fixed analysing epochs unnecessarily, fixed having multiple quantile formulas over the same variables.
|
6 years ago |
|
Tim Quatmann
|
8a72aee764
|
QuantileFormulas: ignore optimization direction (min/max) for quantile variables.
|
6 years ago |
|
TimQu
|
e3fbb77362
|
JaniParser::parseFormula: Boolean connections of AtomicExpressionFormulas are now parsed as a single AtomicExpressionFormula (i.e. 'a>1 & b>2' becomes a single atomic proposition instead of having two propositions 'a>1' and 'b>2'). This reduces the number of labels that need to be considered and improves partial state space exploration for formulas such as 'P=? [F a>1 & b>2]'.
|
6 years ago |
Matthias Volk
|
399c061086
|
Typos
|
6 years ago |
|
TimQu
|
9e282c8bb2
|
QuantileFormulas: A boost::spiritual abyss.
|
6 years ago |
|
TimQu
|
602d18d844
|
Fixed parsing of edge assignments.
|
6 years ago |
|
TimQu
|
bbe9253777
|
JaniParser: Actually fixed parsing of long run average reward formulas
|
6 years ago |
|
TimQu
|
082d624174
|
Jani: import/export of steady-state properties
|
6 years ago |
|
TimQu
|
d9279a72ab
|
Fixed an issue where jani formulas using conjunctions of boolean transient variables could not be parsed.
|
6 years ago |
|
TimQu
|
aba1856786
|
JaniParser: fixed an issue related to using constants in the definition of other constants.
|
6 years ago |
|
TimQu
|
2b90975525
|
parsing prism PTAs
|
6 years ago |
|
TimQu
|
4e9ae0823e
|
JaniParser: fixed parsing of integer variables without initial value
|
6 years ago |
|
TimQu
|
03c80f3ae1
|
correct treatment of non-trivial reward expressions
|
6 years ago |
Sebastian Junges
|
035bbd0952
|
removed spurious debugging output
|
6 years ago |
|
TimQu
|
bf40fb54f2
|
added api call that directly applies a given jani-property filter
|
6 years ago |
dehnert
|
3ab4a28db1
|
fixing bug triggered by one of Steffen's (TUD) input models
|
6 years ago |
|
TimQu
|
019cc8b1a0
|
preserved order of jani-properties as given in the file
|
6 years ago |
|
TimQu
|
6dec8ca659
|
Increased precision of parsing of floating point numbers
|
6 years ago |
|
TimQu
|
7cdbd257d3
|
support for parsing/storing/exporting non-trivial reward expressions
|
6 years ago |
|
TimQu
|
e7c0bd0f7d
|
array variables can now have only a lower (or upper) element type bound
|
6 years ago |
|
TimQu
|
0bacb6f5eb
|
fixed incorrect parsing of jani constants
|
6 years ago |
|
TimQu
|
bb04291860
|
fixed parsing of jani-function: two passes are required as functions can be defined before they are used
|
6 years ago |
|
TimQu
|
f50f1c2ee4
|
Fixed parsing of jani function definitions
|
6 years ago |
|
TimQu
|
c3837968dd
|
nicer output for storm-conv and fixed an issue in storm-conv related to substituting constants before translating the functions
|
6 years ago |
|
TimQu
|
4d74ec501a
|
substitute formulas in properties after parsing
|
6 years ago |
|
TimQu
|
1190f32b56
|
cleanup in jani parser
|
6 years ago |
|
TimQu
|
f89817da3b
|
eliminating reward accumulations directly at parsing time
|
6 years ago |
|
TimQu
|
101b49b898
|
detect unsupported jani-features directly upon parsing the model.
|
6 years ago |
|
TimQu
|
e85b9759e2
|
better parsing of model features
|
6 years ago |
|
TimQu
|
7bae50d0ba
|
fixed correct parsing of prism formulas
|
6 years ago |
|
TimQu
|
ea76f6d0be
|
prism parser no longer inserts formula definitions directly. Note that these have to be eliminated afterwards
|
6 years ago |
|
TimQu
|
b1272c58b6
|
Parsing and exporting of jani-functions
|
6 years ago |
|
TimQu
|
ee87c50313
|
fixed some issues related to jani parsing
|
6 years ago |
|
TimQu
|
d0461f168b
|
support for negative assignment levels
|
6 years ago |
|
TimQu
|
69cbc28547
|
fixes for arrays
|
6 years ago |
|
TimQu
|
fdd3334e6f
|
properly implemented model features
|
6 years ago |
|
dehnert
|
6ab7859c84
|
fixing more of Lindas issues
|
6 years ago |
|
dehnert
|
c3d40d634b
|
started working on the github issues by Linda
|
6 years ago |
|
TimQu
|
ea6b211703
|
fixed storing the wrong pointers to Variables in LValues
|
6 years ago |
|
TimQu
|
5e01151617
|
jani-array fixes
|
6 years ago |
|
TimQu
|
dac431b263
|
parsing of jani-arrays
|
6 years ago |
|
Sebastian Junges
|
8ab3ea991d
|
fix in drn parser
|
6 years ago |
|
TimQu
|
701f3832b1
|
parsing reward accumulations
|
6 years ago |
|
TimQu
|
234ddb7cff
|
fixed compilation of JaniParser
|
6 years ago |
|
TimQu
|
a012539323
|
cleared some TODOs in the Jani Parser
|
6 years ago |
|
TimQu
|
e038fb64be
|
Jani: export the correct accumulation parameters for expected reward properties
|
6 years ago |
|
TimQu
|
4b3e7849ed
|
jani parser parses array variables
|
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 |
