4697 Commits (fd74476340172601e5a4d335559f9ccb79a63c79)
 

Author SHA1 Message Date
dehnert fd74476340 forgot to commit header file 8 years ago
dehnert fd31e23306 allow arbitrary-layer meta variables in DdManager; make DdManager available as non-const from a DD; started on symbolic state elimination linear equation solver 8 years ago
dehnert ad1fdd41ea fixed some wrong capitalizations 8 years ago
dehnert 44dc3e7d8d fixed version output in cmake 8 years ago
dehnert 97b33cf8b1 changed version output slightly 8 years ago
dehnert 98d956275a reworked version detection via git/defaults if not available 8 years ago
dehnert a323d21751 fixed some wrong capitalization 8 years ago
dehnert 3f0afe9526 allowing underscore and dots as identifier symbols in exprtk 8 years ago
dehnert b3a02b6e8a fix in sparse ctmc model checker: bounded until returned empty result in case there are no non-prob0-states 8 years ago
dehnert 0b6c481cf2 fix for sparse mdp model checker: computing cumulative rewards did one step too much 8 years ago
Matthias Volk e5404a27e9 Implemented parsing for UnaryNumericalFunctionExpression 8 years ago
dehnert 1c32273708 made storm_developer not override build_type if one was explicitly set 8 years ago
Tom Janson a22ec04f10 fix old KSP test include 8 years ago
TimQu fd24a2586c added implementation for Z3LpSolver::getValue() when z3_optimize is not available 8 years ago
TimQu adaa55a616 Fixed the printing of two warnings 8 years ago
Matthias Volk 3c9363a323 Fixed compile issue 8 years ago
TimQu 9d70b9d768 fixed typo in an #include statement. 8 years ago
TimQu e2606e7b8c only do z3 optimizer tests if z3::optimize is available 8 years ago
TimQu 4081e4bfbe removed debug output and fixed a test 8 years ago
TimQu 1d2e7b2450 compilation fixes 8 years ago
TimQu 67d5df5bd4 fixed capitalization 8 years ago
TimQu 1e9c49f311 Merge branch 'nativepolytopes' 8 years ago
TimQu 1f4552c046 Fixed check results of hybrid multi objective model checking 8 years ago
TimQu 53402293d6 no maximal end component decomposition for multi-obj model checking when it is not necessary. 8 years ago
TimQu ec9486e8cf fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before. 8 years ago
TimQu 01d3e1f5c7 replaced EIGEN by STORMEIGEN and moved files from Eigen/ to StormEigen/ 8 years ago
TimQu 98fff70cb1 some eigen adaptions 8 years ago
dehnert dd137d6479 added test for using actions multiple times in different synch vectors in JANI model (DD builder) 8 years ago
TimQu 9fa8161110 Merge branch 'master' into nativepolytopes 8 years ago
TimQu 5181c00149 fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before. 8 years ago
TimQu cab08525f8 fix in SymbolicToSparseTransformer 8 years ago
TimQu d7ad282e8f Merge branch 'master' into nativepolytopes 8 years ago
TimQu a8b8ef27a3 fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before. 8 years ago
TimQu 715d589880 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm 8 years ago
TimQu 2567d07037 hybrid multi-objective model checking. 8 years ago
TimQu f01e48644e fixes for nativepolytopes 8 years ago
dehnert e6bf0339d3 overhaul of JANI model building to allow using actions of automata in several synchronization vectors 8 years ago
Sebastian Junges ce9ee672b5 ExportExplicitToDot now added, thanks to Joachim Klein for pointing this out. 8 years ago
Sebastian Junges e5b526b7ae SymbolicToSparseModel: MDPs 8 years ago
Sebastian Junges 598dd85972 SymbolicModel: getDeadlockStates 8 years ago
Sebastian Junges 0ead111dea SymbolicModel: getLabels 8 years ago
Sebastian Junges e847d71e13 SymbolicModel: getRewardModels. 8 years ago
TimQu 4642ed23be enable pcaa tests when hypro is not available 8 years ago
TimQu b5e68b9914 fixes for z3LP solver and nativePolytopes 8 years ago
Matthias Volk 5d79eff2cd Wrapper for file opening 8 years ago
TimQu dfb6ded682 Merge branch 'master' into nativepolytopes 8 years ago
TimQu 7dfc43c828 implemented more functionality for NativePolytopes, added functions to consider exact numbers in z3LPsolver 8 years ago
dehnert 75130ab727 added patch by Joachim Klein that forwards the boost version storm found to carl 8 years ago
dehnert 9c581bd635 fixed two issues: missing include in ToRationalNumberVisitor and missing check for whether actions are reused in a JANI parallel composition 8 years ago
JK d602d2660d utility/constants.cpp: switch to carl::parse from carl::rationalize 8 years ago