ac6694f103
Improved sparse mdp model checking: Now allows hints for expected rewards
10 years ago
92beab426f
created a modelCheckerHint class that allows to store all kinds of hints that a model checker might make use of
10 years ago
59a72b4037
parametric simplifier for mdps
10 years ago
732bbc85d2
worked on parametric model simplifier
10 years ago
3c9363a323
Fixed compile issue
10 years ago
9d70b9d768
fixed typo in an #include statement.
10 years ago
1d2e7b2450
compilation fixes
10 years ago
ec9486e8cf
fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before.
10 years ago
5181c00149
fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before.
10 years ago
a8b8ef27a3
fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before.
10 years ago
f01e48644e
fixes for nativepolytopes
10 years ago
e6bf0339d3
overhaul of JANI model building to allow using actions of automata in several synchronization vectors
10 years ago
b5e68b9914
fixes for z3LP solver and nativePolytopes
10 years ago
5d79eff2cd
Wrapper for file opening
10 years ago
7dfc43c828
implemented more functionality for NativePolytopes, added functions to consider exact numbers in z3LPsolver
10 years ago
9c581bd635
fixed two issues: missing include in ToRationalNumberVisitor and missing check for whether actions are reused in a JANI parallel composition
10 years ago
5cae7fca20
started on native polytopes
10 years ago
eebfa07618
expressions: do simplification involving rationals exactly
10 years ago
edee041b16
BaseExpression: evaluateAsRational
10 years ago
e37d0bd552
ToRationalNumberVisitor: make evaluator optional
10 years ago
eee1a84562
fix, BinaryNumericalFunctionExpression: simplify for pow(a,b) in double context should not cast result to integer [with Linda Leuschner]
Small test case:
dtmc
const double x = 1E-2;
const double y = pow(1-x, 10);
module M1
s: [0..2] init 0;
[] s = 0 -> y:(s'=1) + (1-y):(s'=2);
endmodule
should satisfy Pmax>0 [F (s = 1)].
10 years ago
0c2d906b09
A more accurate version of having multiple levels; seems to fix at least one open issue.
10 years ago
7bc6ce99fa
JANI Export now preserves variable names correctly
10 years ago
dfe0a445a1
JANI: Compacter export; Do not export optional values if they contain the default
10 years ago
5cd0a103b6
Eliminating superfluous assignments
10 years ago
5894f7c706
some forward declarations and header updates to battle recompilation times
10 years ago
8e32d3fa8f
Simplifying index levels
10 years ago
071d1222a1
Convenience operation hasVariable for varset
10 years ago
fcdce6dc4e
fix (set level should not be const)
10 years ago
2fd915f74c
forward declarations, reduce compilation overhead
10 years ago
f16f18bbf6
fix in Matrix-vector multiplication
10 years ago
a03a7a4ea8
towards simplifying levels by preliminary support in ordered assignments
10 years ago
6f40f24b74
JANI operator to set level in assignment
10 years ago
4ad2ac26d1
Equality Comparisons for JaniVars, just to make life easier :-)
10 years ago
0f8e00a80e
action reusal in syncvectors is not invalid jani, but not properly supported. Changed error message accordingly, allows for changes in model generators
10 years ago
b83f57ebf3
JANI assignment levels: we support index/levels other than zero (although most builders wont support them)
10 years ago
a21a0556ed
suppress warning during compilation
10 years ago
267eeca2e1
Jani: better error message in ordered assignments
10 years ago
a85f4fdc89
replaced some StoRMs and Storms by storm, reworked version output a bit
10 years ago
95bd4b7883
Add check that undefined constants / parameters do not appear in the 'if' part of IfThenElseExpressions
10 years ago
ac1ca72094
Add support for ITE expression in the likelihood part of commands (exact, parametric engine)
Support the conversion to rational numbers / rational functions for ITE expressions. Example:
... -> (s<4 ? p : q):(s'=...)
where s is a state variable and p, q are constants or parameters.
10 years ago
5b4db6f002
fixed issue in JANI abstraction
10 years ago
6b931497a2
added filters to parsers
10 years ago
a7e9c5819f
removed 'size-in-memory' output as it was outdated and unreliable. added timing measurements for model construction and model checking
10 years ago
aac7433f39
expression manager now caches types, expression evaluator avoid creating unnecessary expressions and traversals
10 years ago
d676f768dc
added floor/ceil to jit builder (rational numbers)
10 years ago
15e81f1f16
update sparsepp and fix emission of rational literal in to-cpp conversion
10 years ago
43354d0c20
bunch of fixes (prominently in prism -> jani conversion)
10 years ago
ad18fee1dc
commit to switch workplace
10 years ago
d76d34e3f9
optimized ADD::toMatrix to avoid a duplicate operation
10 years ago
TimQu
Matthias Volk
TimQu
dehnert
JK
sjunges
Sebastian Junges