5084 Commits (8da6a6e30e5fb80e899803e58cb7119f64bd7f2a)
 

Author SHA1 Message Date
TimQu caf1683f39 fixed checking whether a sink state is required in GoalStateMerger 8 years ago
Matthias Volk 36854d4636 Framework for DRN parser 8 years ago
Matthias Volk 97d09408d1 Export generated model from DFT 8 years ago
Tom Janson a22ec04f10 fix old KSP test include 8 years ago
TimQu 7a7ad8a34a Instantiation model checker for MDPs. 8 years ago
TimQu 49e6df5860 resultHint for sparse mdp model checker 8 years ago
Matthias Volk d85a949985 Parse voting gate in JSON 8 years ago
Matthias Volk 1c2426b0f4 Print model information 8 years ago
TimQu 4640e47e12 started with instantiation model checker 8 years ago
TimQu 59a72b4037 parametric simplifier for mdps 8 years ago
TimQu a4e4aba487 fixed selection of states to eliminate, added support for model simplification for step bounded properties 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
TimQu 732bbc85d2 worked on parametric model simplifier 8 years ago
Matthias Volk 21e16a9222 Assert that dependent events are BEs 8 years ago
Sebastian Junges 35178e84ba Merge branch 'master' into simplified_levels 8 years ago
TimQu fc70945aba started on refactoring of code for parametric model simplifications 8 years ago
Matthias Volk 7e933ae545 Merge from master 8 years ago
Matthias Volk 3c9363a323 Fixed compile issue 8 years ago
Matthias Volk 40212bb7e6 Added possibility to avoid non-determinism by only taking the first dependency 8 years ago
Matthias Volk 831d86a2e0 Updated parser to read new JSON format 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 8bdf6fe6b3 Merge branch 'master' into simplified_levels 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