5028 Commits (9cf3c67be9cc392366fcf68adb5c4575aa2482c5)
 

Author SHA1 Message Date
ArashPartow 4c99790213 Minor updates to ExprTk 8 years ago
sjunges 977dd1ef53 Get GMP location from carl, set it as a hint for sylvan. 8 years ago
sjunges a371301312 We require gmp, so we can as well just set the corresponding flag to true. 8 years ago
sjunges 1c22fdabe1 Edit in Sylvan/cmake: Allow for hints about gmp location 8 years ago
dehnert 97a7689c67 gcc and clang working on Debian Stretch again 8 years ago
dehnert 6d9e906291 remove LTO from sylvan as it causes more problems than it solves 8 years ago
dehnert ec3468aef5 hopefully fixed the compile issue on Linux 8 years ago
dehnert 4e1855a440 use of intermediate value to make conversion work with gmp 8 years ago
dehnert bae4b421ab added missing template instantiation and print more info on LTO in cmake 8 years ago
sjunges 8bfa699519 attempt to fix link error 8 years ago
sjunges cd954aacd9 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm 8 years ago
TimQu 233c063ad8 statistics output for multi-obj model checking when -stats option is given 8 years ago
TimQu 2e01c8b137 Fixed time bounds containing constant variables for multi objective formulas. 8 years ago
TimQu 6598c2707c Merge remote-tracking branch 'origin/master' into refactor_pla 8 years ago
TimQu 9f795ffccd Merge branch 'master' into refactor_pla 8 years ago
dehnert 187e8bc52b fixed two bugs related to hybrid quantitative results 8 years ago
TimQu a896c0df28 improved exact computations 8 years ago
TimQu 09552d43a3 IsExact number trait 8 years ago
TimQu ee754c96e2 renamed ParameterLifting.h -> RegionChecker.h 8 years ago
TimQu ab7b31b08c optimized memory requirements when a large amount of regions is to be analyzed. Also: Progress bar :) 8 years ago
TimQu 2647ffa9ae added test for exact validations 8 years ago
TimQu d659d193bc Fixed game solver test and potential memory leaks 8 years ago
ArashPartow 2cdda140b8 Minor updates to ExprTk 8 years ago
TimQu de87ff1152 fixed finding of z3 library when its location is given via -DZ3_ROOT 8 years ago
TimQu f59e9a7f77 added flushing of cout in STORM_PRINT macro 8 years ago
TimQu 367b8f0a3e parameter lifting with hybrid engine 8 years ago
TimQu bb3c2bd556 Implemented policy iteration for game solver 8 years ago
Matthias Volk 0d9205c0e6 Fixed case in include path 8 years ago
Matthias Volk 00c210565b Merge from dft_case_study 8 years ago
TimQu e05672a87d Merge branch 'master' into refactor_pla 8 years ago
TimQu 936293e318 Refactored GameSolver. It is now analogous to the MinMaxLinearEquationSolver. 8 years ago
TimQu 77e71b7876 capitalization error and fix for cumulative rewards 8 years ago
sjunges c16390e7f5 Equality Comparisons for JaniVars, just to make life easier :-) 8 years ago
TimQu 3eb675f8c0 used helper methods instead of own implementations 8 years ago
TimQu 502cf4d6e0 extended model checker hint functionality to bypass the maybestates computations 8 years ago
dehnert becc43e1e1 added wokaround proposed by jklein to make the new sylvan version build on older osx 8 years ago
JK 60ab1716b1 storm: bisimulation statistics 8 years ago
JK e536851e53 Solver: provide information about solving method + number of iterations at INFO log level 8 years ago
TimQu cb0d05c947 Merge branch 'master' into refactor_pla 8 years ago
TimQu 170105c261 Fixed "division by zero" error that occurred when considering a CTMC with state rewards but without action rewards 8 years ago
TimQu 9425d3506e reworked checking whether parameter lifting is applicable 8 years ago
TimQu cf340bed52 cleaned up some utility functions 8 years ago
TimQu 575210ae69 Merge branch 'master' into refactor_pla 8 years ago
TimQu d5d0a5f44a fixed a few issues related to having CLN numbers as storm::RationalNumber 8 years ago
TimQu 9ba2f90483 started to implement a validation that checks whether parameter lifting is sound 8 years ago
TimQu 36976f0607 temporarily fixed exact validation to make things compile again 8 years ago
TimQu 0464a248a4 Merge branch 'master' into refactor_pla 8 years ago
TimQu 48d5025bd9 Fixed checking of formulas whose subformulas contain an OperatorFormula (like nested OperatorFormulas or conjunctions of Operatorformulas). 8 years ago
TimQu c5c14f3178 extended JSONExporter to properly export non-constant time/step intervals 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