TimQu
|
dcd9319ba4
|
fixed a convertNumber instantiation
|
8 years ago |
dehnert
|
ea02ea0838
|
started overhaul of cli/api
|
8 years ago |
dehnert
|
4e1855a440
|
use of intermediate value to make conversion work with gmp
|
9 years ago |
TimQu
|
cf340bed52
|
cleaned up some utility functions
|
9 years ago |
TimQu
|
d5d0a5f44a
|
fixed a few issues related to having CLN numbers as storm::RationalNumber
|
9 years ago |
dehnert
|
853b035473
|
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
|
9 years ago |
dehnert
|
952776a057
|
hybrid engine working for rational numbers
|
9 years ago |
dehnert
|
ee90c51b2a
|
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
|
9 years ago |
dehnert
|
aaa6f13cf4
|
separated rational numbers and rational functions and added support for rational numbers to sylvan
|
9 years ago |
TimQu
|
7f74f19342
|
exact pla
|
9 years ago |
dehnert
|
2e8ff870ff
|
completed interface of (sylvan) ADDs for storing rational functions
|
9 years ago |
TimQu
|
a1ad5377e8
|
implemented parameter lifting model checker for DTMCs (as a replacement of the old ApproximationModel).
|
9 years ago |
JK
|
d602d2660d
|
utility/constants.cpp: switch to carl::parse from carl::rationalize
carl::parse supports more syntax variants for specifying rational numbers, e.g., 1.23e-10 (scientific notation), 1/24 (fractions), ...
|
9 years ago |
JK
|
b623b4184e
|
constants.cpp: convertNumber(int_fast64_t) to RationalFunction, fix signed/unsigned cast
|
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
|
aac7433f39
|
expression manager now caches types, expression evaluator avoid creating unnecessary expressions and traversals
|
9 years ago |
dehnert
|
43354d0c20
|
bunch of fixes (prominently in prism -> jani conversion)
|
9 years ago |
dehnert
|
6dce56d0bb
|
improved printing of result to command line
|
9 years ago |
dehnert
|
56d1928b9b
|
resolved some issues (ambiguity for call to carl::rationalize and several warnings because of signed/unsigned comparison)
|
9 years ago |
TimQu
|
83a77e77ba
|
fixed use of gmp numbers
|
9 years ago |
dehnert
|
5b09b91ae1
|
fixed more warnings
|
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
|
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 |
Mavo
|
6faa7f0429
|
Abort when getting infinity in approximation
Former-commit-id: 8bfda3656a
|
9 years ago |
sjunges
|
236a2be0d3
|
pretty printing of rational functions, rewards in the drn format, option for full build
Former-commit-id: 39676106c2 [formerly b80f259a87 ]
Former-commit-id: e6f493d6f9
|
9 years ago |
dehnert
|
f342ce3287
|
translation from expressions involving the power operator to rational functions/rational numbers is now possible
Former-commit-id: e0ce43ab35
|
9 years ago |
dehnert
|
569b27e110
|
work towards having rational numbers instead of doubles as literals in expressions
Former-commit-id: c62f8af061
|
9 years ago |
sjunges
|
051ad702a7
|
solvers updated, constants updated
Former-commit-id: 011251c695
|
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 |
Mavo
|
5530f908ca
|
Fixed compile issues under Linux
Former-commit-id: 61a69f9fc7
|
9 years ago |
Mavo
|
566cef0f91
|
Started on compiling without Carl
Former-commit-id: 5e0895d7c5
|
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 |
TimQu
|
7bab48b59b
|
bounded reachability for MAs
Former-commit-id: 982277d9ab
|
9 years ago |
TimQu
|
4496b53002
|
merge fixes
Former-commit-id: ff5de6fc69
|
9 years ago |
dehnert
|
b1f2c26df0
|
made all instantiations to call MDP model checking with rational numbers
Former-commit-id: d3f8df7804
|
9 years ago |
dehnert
|
13f8f21a70
|
upgrade to eigen 3.3 and made modifications for different value types via template specializations
Former-commit-id: 8ea9d1e0c4
|
9 years ago |
dehnert
|
f3fa90cc37
|
more work towards exact solving
Former-commit-id: 38edbcf2ca
|
9 years ago |
dehnert
|
4e14ecb869
|
made elimination-based linear solver work in an alpha version. changed minor things in Eigen's SparseLU implementation to make it work with rational numbers and rational functions
Former-commit-id: e5622bd981
|
9 years ago |
TimQu
|
a6359335cf
|
Fixed compiling when hypro is not available
Former-commit-id: 402899c393
|
9 years ago |
Mavo
|
652aeb7562
|
Fixed compile error with CarlRationalNumber instead of RationalNumber
Former-commit-id: 0fbb4ad1c1
|
10 years ago |
TimQu
|
69c5ba604e
|
Helper functions for parametric stuff
Former-commit-id: 288e4de3da
|
10 years ago |
dehnert
|
55fd1b66c3
|
introducing exploration orders to explicit builder
Former-commit-id: a56620eac2
|
10 years ago |
sjunges
|
266d417168
|
constants.h/cpp extended to treat carl rational numbers
Former-commit-id: 12f0dfbc2c
|
10 years ago |
dehnert
|
8ed4a5f849
|
some refactoring in elimination-based model checker
Former-commit-id: 1fb6741479
|
10 years ago |
dehnert
|
6a80348150
|
fixed issue related to row groups in sparse matrix and adapted the affected calling sites
Former-commit-id: 96c6fd7e59
|
10 years ago |
TimQu
|
5b1494b9a9
|
Made use of this new cool rewardModel thing
Former-commit-id: d670d09278
|
10 years ago |