82 Commits (ebee22d5462db3db117649cbd08c7ea1ea8b4619)

Author SHA1 Message Date
dehnert 83c4b1647c solvers now can allocated auxiliary memory 9 years ago
dehnert 95b95d9c64 fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact 9 years ago
dehnert 9ab33528b4 started to fill value iteration implementation in new general min-max solver 9 years ago
dehnert b4e0cabef6 started working on general min-max solver that uses an underlying linear equation solver. provided necessary factories. adapted code and removed old min-max solvers 9 years ago
dehnert 8153306ced fixed wrong call to Eigen's iterative solvers 9 years ago
dehnert 07c787b49d added unsupported solvers of eigen 9 years ago
dehnert 69da4ff147 fixed some more problems with Eigen solver 9 years ago
dehnert 00d331ebb4 moved linear equation solver factories to the respective solver files (and away from utility). restructured settings in factories and the way they are forwarded to the linear equation solvers. fixed all resulting errors 9 years ago
PBerger b99a063cce Replaced calls to std::abs with calls to std::fabs and included cmath. 9 years ago
dehnert 3ba5902821 removed debug output and fixed small bug in adaptation of Eigen 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 9 years ago
dehnert 023325b53d added tests for Eigen solver 9 years ago
Mavo 67d77608bd Refactoring of settings 9 years ago
dehnert 5a1039838f made everything compile again and all tests passing 9 years ago
sjunges 1e1400d68d merge 9 years ago
dehnert 7f75db2790 ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working. 9 years ago
dehnert 19029cd905 functional tests compile and run again, yay! 9 years ago
dehnert 4e86ef2e47 moved CUDD-based DD implementation to own folder 9 years ago
dehnert 15b97057dd silenced some warnings within boost (new clang version) and fixed an unused variable issue 9 years ago
dehnert ccad5741a7 added test case for game solver 9 years ago
dehnert e659dd8c4a some work on sparse game solver 9 years ago
sjunges 73310b9881 fixed tests: glpk had wrong minimize, solver.cpp tested in wrong direction on policy iteration in case we use top. value iteration 9 years ago
sjunges 8568ee3986 only one optimization direction enum -- towards integration of termination criterions on the model checker 9 years ago
sjunges 1086ffc1cc Added allow early termination for min/max solvers 9 years ago
sjunges faf31156e0 fix for last changes + is probabilistic 9 years ago
sjunges 97c24fe229 solver settings now within solver, minmax refactored to share common variables 9 years ago
sjunges 5e428a795a And more includes on the right spot. 9 years ago
sjunges 3c2040f4b7 Removed many superfluous includes, added some source files -- towards faster compilation 9 years ago
sjunges a129983ae9 cleaning includes for better compilation times 9 years ago
dehnert e338cbe069 fixed a lot of warnings in the tests 9 years ago
dehnert 9d5c3e7e2f added functionality to flatten the modules of a PRISM program into one module 9 years ago
dehnert 81c627b9b7 First version of fully symbolic game solver. 10 years ago
PBerger 287393abc4 Added Policy Iteration to the NativeMinMaxLinearEquationSolver. 10 years ago
PBerger f63e5fc873 Implemented Policy Iteration inside the GmmxxMinMaxLinearEquationSolver. 10 years ago
dehnert eb5d4100a6 Renamed Nondeterminstic equation solver as this name is more than misleading. 10 years ago
dehnert d545fac471 Restructured solvers a bit: they now get the matrix upon construction and the model checkers use factories to retrieve solvers. 10 years ago
dehnert 8e71081f1e Functional tests now work again. 10 years ago
dehnert d6a299e799 MathSAT tests now running fine again. 10 years ago
dehnert 99d9a9710d Further steps to make everything work again. 10 years ago
dehnert 809217c359 Refactored some parts of expressions. In particular, visitors now can return anything they want by using boost::any. 10 years ago
dehnert b5d55335a6 All tests passing again. 10 years ago
dehnert ba14ba3613 Further work on MathSAT solver. 10 years ago
dehnert 7ff3dcecfb Added test for interpolation to MathSat tests. 10 years ago
dehnert 6eb415f87f Tests for MathSAT now run through on Mac OS. 10 years ago
dehnert d8be64f0d7 Started on making MathSatSmtSolver work properly. 10 years ago
dehnert 5ecc96fa3a Fixed some more places in the code to use the new option system. 10 years ago
dehnert a995d7dd4a The tests now run fine with the new option system. 10 years ago
dehnert 266d660d89 Added functions responsible for printing the help. Started adapting the tests to the new option system. 10 years ago
dehnert 9ad12616e2 Renamed files in settings module a bit. Started on the pseudo-modular module-settings. 10 years ago
dehnert 96e1f8faf9 Renamed Settings class to SettingsManager. 10 years ago