Commit Graph

  • 7f5e775395 adapted counterexample generation to refactoring dehnert 2015-08-25 13:53:45 +0200
  • 7b79725421 Allow hints for z3 sjunges 2015-08-25 13:27:28 +0200
  • 0a061274b6 support for downloaded version of z3 sjunges 2015-08-25 13:27:14 +0200
  • 7722165256 Support for gurobi 602 sjunges 2015-08-25 13:11:57 +0200
  • 0b6cc91808 Remove not existing variant of compute until probabilities. sjunges 2015-08-25 11:56:44 +0200
  • d7490a74cb properties can now be given as string or file. both ways accept multiple formulas dehnert 2015-08-25 11:37:21 +0200
  • f9f5a4e206 reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas dehnert 2015-08-25 10:53:08 +0200
  • 63df1f6329 includes to make clang on the build server happy dehnert 2015-08-25 00:09:44 +0200
  • 9cf488b249 moved to checking the validity of transition matrices by calling the matrix function dehnert 2015-08-24 23:21:45 +0200
  • 29716ea5f8 performance tests now compile again. also fixed some warnings dehnert 2015-08-24 22:15:50 +0200
  • 6c5f6b5d5e Merge branch 'master' into newrewardmodel dehnert 2015-08-24 21:14:16 +0200
  • b94e978843 another round of fixes dehnert 2015-08-24 19:08:34 +0200
  • 707a4f500b vector sum_if sjunges 2015-08-24 18:26:41 +0200
  • da120d9de5 Refactored some stuff in constants... sjunges 2015-08-24 18:26:23 +0200
  • d4ba7905fa Extra constructor for simple testing. sjunges 2015-08-24 18:25:47 +0200
  • faf31156e0 fix for last changes + is probabilistic sjunges 2015-08-24 16:36:30 +0200
  • 32e4a71acf Merge branch 'newrewardmodel' of https://sselab.de/lab8/private/git/storm into newrewardmodel dehnert 2015-08-24 15:01:49 +0200
  • 8d6a5a7fd5 added some missing includes dehnert 2015-08-24 15:00:36 +0200
  • 5d07a840be removed debug output dehnert 2015-08-24 14:37:38 +0200
  • 972c391eb1 fixed some more bugs/warnings dehnert 2015-08-24 14:04:13 +0200
  • dc2735b6ff moved some template parameters from class scope to function scope dehnert 2015-08-24 13:03:21 +0200
  • 45d6bc0f6f added more headers to make gcc even happier dehnert 2015-08-24 12:43:50 +0200
  • 28f5a8799a added header to make gcc happy dehnert 2015-08-24 12:38:55 +0200
  • e2b84c8155 changed some method signatures to make gcc happier dehnert 2015-08-24 11:58:46 +0200
  • 97c24fe229 solver settings now within solver, minmax refactored to share common variables sjunges 2015-08-24 11:44:11 +0200
  • a9142a752d fixed another bug dehnert 2015-08-24 11:37:49 +0200
  • 30fc452623 fixed another bug dehnert 2015-08-23 21:59:16 +0200
  • fbd05cd780 more and more bugfixes dehnert 2015-08-23 11:48:36 +0200
  • b3178e17f6 more bug fixes dehnert 2015-08-21 17:25:54 +0200
  • 7d9cc8e905 Minimal progress on perm schedulers sjunges 2015-08-21 16:59:56 +0200
  • 54e89e1519 Merge master into future sjunges 2015-08-21 16:11:40 +0200
  • 73a2491dfb more bugfixes dehnert 2015-08-20 22:45:19 +0200
  • 88631a1ded small fix for solver to work with timeout TimQu 2015-08-20 22:07:37 +0200
  • dbc7d860a4 functional tests compile again, started to debug changes dehnert 2015-08-20 19:06:00 +0200
  • 1a07b24682 added some convenience functions for reward model building dehnert 2015-08-20 16:41:25 +0200
  • 234627d18c more structured and safe access to some members TimQu 2015-08-20 13:07:19 +0200
  • 5b77d827dc fixed a bug dehnert 2015-08-19 23:58:32 +0200
  • 42754f8676 Merge branch 'master' into TimParamSysAndSMT TimQu 2015-08-19 22:18:25 +0200
  • ba95065ce3 Fixed memory leak by adding destructors for linear equation solvers. Previously, the member unique_ptr<...> gmmxxMatrix from the gmmxx subclasses was not deleted properly TimQu 2015-08-19 21:04:53 +0200
  • 511284cd5b Added a couple of settings that replace hardcoded switches TimQu 2015-08-19 20:30:35 +0200
  • 4ca64a913a main executable compiling again, started to debug dehnert 2015-08-19 16:55:32 +0200
  • 6133c3462a symbolic models can now have several reward models, adapted reward generation in model builders, probably introduced quite some bugs dehnert 2015-08-19 14:32:00 +0200
  • 3c098f085a In principal, we need a fixpoint iteration for the static simplification. For now, we just call simplify twice. sjunges 2015-08-19 10:17:49 +0200
  • 9201c6420a Removes identity assignments sjunges 2015-08-19 10:17:11 +0200
  • e631dbd1a0 more work on new reward models dehnert 2015-08-18 17:40:41 +0200
  • 5e428a795a And more includes on the right spot. sjunges 2015-08-18 13:31:13 +0200
  • 72cb30d6b0 started replacing ValueType template argument by model class in all instantiations dehnert 2015-08-18 10:35:38 +0200
  • 5beb33e3d8 merged a bit more dehnert 2015-08-17 19:58:43 +0200
  • 3ff1dce532 Merge master into newrewardmodel. dehnert 2015-08-17 19:41:32 +0200
  • dd97e3d0b6 Merge branch 'master' into newrewardmodel dehnert 2015-08-17 19:29:45 +0200
  • 61fb277024 more work on refactoring (storm stinks and should be rewritten :P) dehnert 2015-08-17 19:25:58 +0200
  • 84ecabd2c8 further fixes, for performance tests and windows sjunges 2015-08-17 18:21:20 +0200
  • 92082dc970 gurobi lp solver refactored in case gurobi is not found, and fixes for linux - sorry about earlier lack of checks on linux sjunges 2015-08-17 16:22:09 +0200
  • 8ff557cfad more work on creating helpers for model checkers dehnert 2015-08-17 15:58:21 +0200
  • 9d138d86f7 further work on creating helper classes for model checking tasks dehnert 2015-08-14 21:52:01 +0200
  • f85d28325e Further work towards faster and more modular compilation sjunges 2015-08-14 18:34:03 +0200
  • 3c2040f4b7 Removed many superfluous includes, added some source files -- towards faster compilation sjunges 2015-08-14 17:31:58 +0200
  • b56766e993 more work on reward model that turned out to be refactoring in disguise dehnert 2015-08-14 16:53:56 +0200
  • a129983ae9 cleaning includes for better compilation times sjunges 2015-08-13 19:02:47 +0200
  • 661ba7d16f Further work on new reward model dehnert 2015-08-12 22:58:35 +0200
  • 3bb84ff5b4 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-12 14:44:53 +0200
  • c7becb3c60 improved cmake for z3 and gurobi sjunges 2015-08-12 14:44:49 +0200
  • 72784d752d permissive schedulers - ongoing work sjunges 2015-08-12 12:54:33 +0200
  • 67502592d7 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-11 23:07:24 +0200
  • bb7d4c3b0e update for gmm++: 4.2 to 5.0 dehnert 2015-08-11 23:07:17 +0200
  • 6fa1078fb1 some more work on reward model dehnert 2015-08-11 22:11:45 +0200
  • 7521be7408 Fixed some problems on windows. David_Korzeniewski 2015-08-11 20:41:15 +0200
  • dcd42d5653 started reworking reward models dehnert 2015-08-11 17:47:47 +0200
  • 1a0bf89671 minor changes... TimQu 2015-08-11 13:15:05 +0200
  • 584df037f0 Merge branch 'master' into TimParamSysAndSMT TimQu 2015-08-10 23:29:15 +0200
  • 61b825e7fb Merge 'master' into 'menu_games'. dehnert 2015-08-10 23:05:57 +0200
  • efadc84593 Beautified the Code, removed unused stuff, minor improvements TimQu 2015-08-10 19:56:14 +0200
  • d7f1012509 got rid of more warnings dehnert 2015-08-10 19:37:37 +0200
  • 719ac4fb4e move perm sched to own dir sjunges 2015-08-10 19:26:48 +0200
  • 5ec1e2acbe PermissiveSchedulers are on future now sjunges 2015-08-10 19:25:03 +0200
  • 6357c4b7aa Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-10 18:58:55 +0200
  • 56b4f53ce7 got rid of more warnings dehnert 2015-08-10 18:58:49 +0200
  • 011dd82096 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-10 18:35:03 +0200
  • 90fa8f6f0d convenience methods for sparse matrix added sjunges 2015-08-10 18:34:58 +0200
  • 1e61030fa3 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-10 17:50:37 +0200
  • e338cbe069 fixed a lot of warnings in the tests dehnert 2015-08-10 17:50:25 +0200
  • eb19d7f709 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-10 16:45:42 +0200
  • 1bb4d2c0ae silenced glpk warnings for clang on OSX sjunges 2015-08-10 16:45:35 +0200
  • 5365d50811 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-10 16:17:46 +0200
  • 44e609ce86 merge fix sjunges 2015-08-10 16:19:12 +0200
  • 7f7ea57bbe merge sjunges 2015-08-10 16:17:45 +0200
  • 04f789619c some work towards eliminating compiler warnings dehnert 2015-08-10 16:17:08 +0200
  • 812b101c40 better program checks, some extensions in model and matrix sjunges 2015-08-10 16:15:09 +0200
  • 21627fbab4 Started to get rid of some warnings. In particular this means making the compiler more silent for third-party stuff. dehnert 2015-08-10 00:23:47 +0200
  • 28326b14e4 more efficient instantiation of matrices. TimQu 2015-08-09 19:10:27 +0200
  • c683934ea0 removed debug output and fixed bug dehnert 2015-08-07 19:53:58 +0200
  • 08747378d5 workplace switch dehnert 2015-08-07 15:00:01 +0200
  • 507331d8a9 more debug output dehnert 2015-08-07 14:47:56 +0200
  • b2cec6395a more debug output dehnert 2015-08-07 14:34:17 +0200
  • 8985ad77cf added first debug output to track down bug dehnert 2015-08-07 14:16:45 +0200
  • 0bd4b9b8ad fixed some guards for smtsolver sjunges 2015-08-06 10:01:42 +0200
  • 2e0c9c1244 unification of some constructs in carl propagated to storm sjunges 2015-08-05 19:27:18 +0200
  • 613724fa9f fix sjunges 2015-08-05 17:04:13 +0200
  • 05e918a484 merge sjunges 2015-08-05 10:50:34 +0200
  • 8e2de5fbb1 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-05 10:48:33 +0200