dehnert
cbb0b1e0f0
initial work on installation of storm
9 years ago
JK
95bd4b7883
Add check that undefined constants / parameters do not appear in the 'if' part of IfThenElseExpressions
9 years ago
JK
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.
9 years ago
Sebastian Junges
03b634d14a
suppress silly warning about no return after error
9 years ago
dehnert
c467fa5f38
printing -1 as infinity for rational numbers and added clipping result to valid range where appropriate
9 years ago
dehnert
5b4db6f002
fixed issue in JANI abstraction
9 years ago
dehnert
5bbf4ab319
fixed issue when parsing formula files
9 years ago
TimQu
0bb1c5855e
fixed bug when computing expected reachability rewards on MAs
9 years ago
dehnert
6b931497a2
added filters to parsers
9 years ago
Matthias Volk
ad2371fdae
Fixed typo
9 years ago
dehnert
398c317a7d
allowing constant definition string to refer to other variables on the right-hand side of assignments, added convergence statement in eigen solver
9 years ago
dehnert
c5ba425e54
enabling exact reachability rewards for CTMCs
9 years ago
dehnert
a2e29893f2
fixed a few bugs
9 years ago
dehnert
77bd6e4a44
fixed some model building issues
9 years ago
dehnert
810f423849
pumped cudd to -O3, fixed reference of linear equation solver, removed superfluous multiplications in symbolic dtmc helper
9 years ago
dehnert
b4685f36d4
reverted increasing CUDD precision by default
9 years ago
dehnert
75d513235a
polished cli output a bit
9 years ago
dehnert
2801f1604b
improved symbolic linear equation solving (via Jacobi) a bit
9 years ago
dehnert
fb0d589d43
fix typo
9 years ago
dehnert
ffedc2268b
Only label states as deadlocks when the behaviour was expanded (jit-builder)
9 years ago
dehnert
7af65ac804
slightly modified stats output and fixed memory measurement under linux
9 years ago
dehnert
a7e9c5819f
removed 'size-in-memory' output as it was outdated and unreliable. added timing measurements for model construction and model checking
9 years ago
dehnert
aac7433f39
expression manager now caches types, expression evaluator avoid creating unnecessary expressions and traversals
9 years ago
dehnert
76c99b55af
return more precise result in dd equation solver
9 years ago
dehnert
7b0b6fa333
fixed a formula parsing bug, corrected some result printing
9 years ago
dehnert
d676f768dc
added floor/ceil to jit builder (rational numbers)
9 years ago
dehnert
15e81f1f16
update sparsepp and fix emission of rational literal in to-cpp conversion
9 years ago
dehnert
43354d0c20
bunch of fixes (prominently in prism -> jani conversion)
9 years ago
TimQu
fb0222cf62
fixed new interface of stopwatch
9 years ago
dehnert
ad18fee1dc
commit to switch workplace
9 years ago
TimQu
f02ffd9d5b
fixed pcaa tests
9 years ago
TimQu
3e1532760e
replaced EIGEN with STORMEIGEN and Eigen/ with StormEigen/
9 years ago
dehnert
d76d34e3f9
optimized ADD::toMatrix to avoid a duplicate operation
9 years ago
dehnert
33cdee94dc
let's fill them hashtables (I mean there were there anyway, so we could as well use 'em)
9 years ago
TimQu
6eeae9ed9b
fixed pcaa tests
9 years ago
dehnert
9e8d6eee90
fixed a bug when reducing state-action rewards to state rewards for CTMCs
9 years ago
TimQu
92e837f83c
fixed closing of MAs: Previously, stateActionRewardVectors have not been handled properly.
10 years ago
dehnert
09f90dbc9f
enabled long-run average rewards for dtmc/ctmcs (sparse/hybrid engines)
10 years ago
TimQu
362b3bf6c6
removed eigen usages
10 years ago
TimQu
0b555d5d59
fixed closing of MAs: Previously, stateActionRewardVectors have not been handled properly.
10 years ago
Matthias Volk
d2e7de7067
Use Stopwatch for measuring total time
10 years ago
dehnert
64ddf12558
fixed two issues in jit builder: a) respect environment variable (instead of c++); b) casting integer variables to doubles when evaluating label expressions to avoid integer division
10 years ago
dehnert
6dce56d0bb
improved printing of result to command line
10 years ago
dehnert
603bf3562a
add trailing semicolon after property a la PRISM
10 years ago
dehnert
16a06d9f03
formula parser now directly emits properties with names; name filtering of properties from cli
10 years ago
dehnert
0a3ff157f7
constants defaulting to type int and allowing model type everywhere (on top level) of PRISM program
10 years ago
dehnert
b4381a7c48
Constants in formulas appear to be working
10 years ago
dehnert
cb8b537baa
made storm compile again with expressions in time-bounds of until formula
10 years ago
dehnert
8d3f633cbc
started working on allowing expressions in time-bounds of formulas
10 years ago
Matthias Volk
7b253ba30a
Fixed compile issue
10 years ago