sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Commit Graph

  • 4758ef73ec Fixed an issue that gcc has problems with. dehnert 2015-01-15 14:39:08 +0100
  • 5e37c09fc0 Fixed some bugs. dehnert 2015-01-15 14:29:52 +0100
  • 231d2223a9 Model building works again (more or less) dehnert 2015-01-14 21:15:39 +0100
  • 8ec362bb7d Started debugging new model generation. dehnert 2015-01-14 18:12:33 +0100
  • 6f2916d557 Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet. dehnert 2015-01-14 18:06:47 +0100
  • 26e9eac934 Added another convenience operation to bit vector class. dehnert 2015-01-14 13:57:42 +0100
  • 827839e7fd Changed internal representation of bit vector slightly, adjusted all operations. New bit vector operation runs fine now. dehnert 2015-01-14 12:09:40 +0100
  • 43d77e0adc Wrote tests for the new necessary bit vector operations (they fail, because the bit vector is organized in a weird way and needs to be restructured.) dehnert 2015-01-13 23:24:41 +0100
  • 30f78b0a99 Intermediate commit. Started improving explicit model adapter performance. dehnert 2015-01-13 20:15:57 +0100
  • aaefe7dfa5 Fixed some tests/parser. dehnert 2015-01-11 18:33:43 +0100
  • 53196f5610 Created bit vector hash map and some necessary bit vector methods. dehnert 2015-01-11 17:09:45 +0100
  • f5f2a2dd4c Added expression evaluation (header-only) library exprtk and a corresponding evaluator class. dehnert 2015-01-09 22:43:56 +0100
  • ab0caf79e8 Replaced action names by indices in PRISM programs. dehnert 2015-01-09 19:33:17 +0100
  • 3260a6203c Started improving performance of explicit model generation. dehnert 2015-01-09 17:55:35 +0100
  • b77772b242 Fixed some minor issues. dehnert 2015-01-09 15:13:05 +0100
  • 6142c6c3b7 Fixed more missing ifdefs. dehnert 2015-01-09 15:09:11 +0100
  • 994250a697 Fixed missing ifdefs. dehnert 2015-01-09 15:05:09 +0100
  • 780ddd9694 Improved simplify a bit. dehnert 2015-01-08 21:47:42 +0100
  • 650770148d Main now compiles again, yay. dehnert 2015-01-08 20:31:39 +0100
  • b37e009168 Further steps to new expressions. dehnert 2015-01-08 18:19:29 +0100
  • 43c63f1cb6 Fixed typo from aa025df9 svkurowski 2015-01-08 15:06:22 +0100
  • 25db3f9d0f Fixed error that prevents compilation if Z3 is not present. dehnert 2015-01-08 11:48:48 +0100
  • ee9533e586 Started working on making the main executable build again. dehnert 2015-01-07 20:20:19 +0100
  • 8e71081f1e Functional tests now work again. dehnert 2015-01-07 19:55:13 +0100
  • 2eeaa06d76 Z3 runs fine again. dehnert 2015-01-07 12:46:38 +0100
  • d6a299e799 MathSAT tests now running fine again. dehnert 2015-01-07 09:19:18 +0100
  • ed74392f0d Another intermediate commit. dehnert 2015-01-06 23:54:39 +0100
  • 99d9a9710d Further steps to make everything work again. dehnert 2015-01-06 17:56:07 +0100
  • 7ec3e8b214 Further fixes for new variable handling. libstorm now compiles again, yay. dehnert 2015-01-05 23:44:26 +0100
  • f76d0f93eb Adapted LP solver interface to new variable handling. dehnert 2015-01-05 21:46:46 +0100
  • 7ea6ec3644 Further refactoring. dehnert 2015-01-05 18:33:04 +0100
  • bdfbc50dab Removed some superfluous stuff. dehnert 2015-01-04 19:51:54 +0100
  • 92d550be12 More and more refactoring. dehnert 2015-01-04 19:18:00 +0100
  • 398f6c4e86 Partly adapted code to new 'type system'. dehnert 2015-01-02 20:05:10 +0100
  • 983a7d78c2 Further work on expressions. dehnert 2015-01-02 17:34:44 +0100
  • fff18f2789 Intermediate commit (refactoring expressions). dehnert 2015-01-01 22:56:21 +0100
  • 809217c359 Refactored some parts of expressions. In particular, visitors now can return anything they want by using boost::any. dehnert 2014-12-29 14:39:22 +0100
  • 0f4b19ffc9 Merge branch 'master' into SmtSolvers dehnert 2014-12-23 22:39:30 +0100
  • 85a4376e39 Now StoRM can be properly compiled without support for MathSAT if needed. dehnert 2014-12-23 22:39:07 +0100
  • 7b8c382303 Added tests for Mathsat expression adapter. dehnert 2014-12-22 23:41:10 +0100
  • f54b5671ea Done refactoring MathSAT expression adapter. dehnert 2014-12-22 15:45:08 +0100
  • a061cdbed8 Started refactoring MathSAT adapter. dehnert 2014-12-22 12:32:38 +0100
  • 84bfd58884 Minor refactoring of Z3 expression adapter. dehnert 2014-12-22 12:02:29 +0100
  • c859029094 Added some checks for illegal return values. dehnert 2014-12-19 13:32:19 +0100
  • 5e9e7b875b Proper output of MathSAT version on command line. dehnert 2014-12-19 13:18:01 +0100
  • b5d55335a6 All tests passing again. dehnert 2014-12-19 13:15:28 +0100
  • ba14ba3613 Further work on MathSAT solver. dehnert 2014-12-18 19:31:51 +0100
  • 06dfecda55 Merge branch 'philippTopologicalRevival' into cuda_integration David_Korzeniewski 2014-12-18 18:49:11 +0100
  • 81571878f7 Further refactoring of MathSAT solver. dehnert 2014-12-18 17:32:32 +0100
  • c474920fa4 Started refactoring SMT solvers. Now displaying MathSAT version in CLI. dehnert 2014-12-18 16:47:13 +0100
  • 7ff3dcecfb Added test for interpolation to MathSat tests. dehnert 2014-12-18 11:19:31 +0100
  • 6eb415f87f Tests for MathSAT now run through on Mac OS. dehnert 2014-12-17 20:43:50 +0100
  • d8be64f0d7 Started on making MathSatSmtSolver work properly. dehnert 2014-12-17 17:11:57 +0100
  • b787d6420a Using correct carl::pow now. dehnert 2014-12-17 10:05:12 +0100
  • 90b0f20167 Reachability Rewards can now be computed in parametric DTMCs (modulo bugs) dehnert 2014-12-16 13:53:32 +0100
  • 409fa6b340 Merge branch 'master' into parametricSystems dehnert 2014-12-16 09:59:52 +0100
  • 554287e082 Fixed minor issue that caused problems with the measure-driven initial partition and rewards. dehnert 2014-12-16 09:59:20 +0100
  • 6db0522c69 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2014-12-16 09:55:58 +0100
  • b7492d543a Further work regarding rewards in parameterized models. Note: this includes some debug output. dehnert 2014-12-15 17:32:09 +0100
  • 3a18d60925 Working towards reachability reward properties for parametric DTMCs. dehnert 2014-12-14 22:30:29 +0100
  • edfbfaa924 Merge branch 'master' into parametricSystems dehnert 2014-12-13 17:19:56 +0100
  • 7d0ae06f9f Fixed creation of empty blocks under certain circumstances in bisimulation. dehnert 2014-12-13 17:19:13 +0100
  • 3231ea6c06 Moved to new macros. dehnert 2014-12-13 17:08:59 +0100
  • 2912ec23fe Merge branch 'master' into SmtSolvers dehnert 2014-12-12 17:04:57 +0100
  • 91084a5da4 APs true/false can now be queried for a state. dehnert 2014-11-28 11:14:55 +0100
  • cd9488e56b Merge branch 'master' into parametricSystems dehnert 2014-12-05 13:56:11 +0100
  • cca4ba4ecf Removed debug time measurements. dehnert 2014-12-05 13:45:35 +0100
  • 0bc685969d Moved from call to list::size to counting member in bisimulation partition to avoid gcc's O(n) list::size. dehnert 2014-12-05 13:38:05 +0100
  • 5299ed5172 Adapted FindCusp to fail silently if cusp is not found. Now configuring fails with a meaningful error message instead of syntax errors. David_Korzeniewski 2014-12-04 19:21:23 +0100
  • 0ad4c5f867 More debug times. dehnert 2014-12-04 13:45:04 +0100
  • 9b91d388b7 Even morer debug times. dehnert 2014-12-04 13:35:02 +0100
  • f476caf62e More debug timings. dehnert 2014-12-04 13:20:27 +0100
  • 0af2b8d148 More debug stats. dehnert 2014-12-04 12:19:28 +0100
  • 8c403628f2 Added some debug statistics to bisim. dehnert 2014-12-04 12:03:36 +0100
  • 4b8f2e7a0b Next splitter is now chosen more deterministically. dehnert 2014-12-04 11:53:42 +0100
  • 524b6a3394 Merge branch 'master' into parametricSystems dehnert 2014-12-03 23:41:29 +0100
  • 894c3bb497 Added missing header. dehnert 2014-12-03 23:41:20 +0100
  • 262bb90188 Merge branch 'master' into parametricSystems dehnert 2014-12-03 23:07:48 +0100
  • 39fb2650cd Included missing header. dehnert 2014-12-03 23:07:35 +0100
  • c060377de5 Ignore rewards for bisimulation quotienting (of parametric models) if the property to check is not related to rewards. dehnert 2014-12-03 22:31:25 +0100
  • 05cf9f5d84 Fixed recently introduced bug in cli for parametric systems. dehnert 2014-12-03 21:41:37 +0100
  • d1fd3e5b38 Started working on parametric reward properties. dehnert 2014-12-03 18:35:49 +0100
  • 16366e941d Fixed wrong call to bisimulation computation. dehnert 2014-12-03 16:37:59 +0100
  • 4ea0e32793 Merge branch 'master' into parametricSystems dehnert 2014-12-03 14:20:39 +0100
  • 0c47d932a7 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2014-12-03 14:20:15 +0100
  • b305a3b498 Switched to FactorizedPolynomial as the basis for rational functions and added missing reward construct for one NAND model. dehnert 2014-12-03 14:19:46 +0100
  • 7014d289e8 Fixed some issues related to bisimulation in the presence of state rewards. dehnert 2014-12-03 14:16:16 +0100
  • b8a74c61c0 Set cuda_root variable in cmakelists to make it show up in the gui when configuring. David_Korzeniewski 2014-12-01 16:29:40 +0100
  • 287281d053 Enable checking MDP models from the CLI svkurowski 2014-11-28 13:54:36 +0100
  • 61e78f8d12 Adapted parameterized NAND example to use state rewards instead of transition rewards. Also, the unfactorized polynomials are now used to build and compute everything. We should detect cyclic models and use the factorized polynomials for them. dehnert 2014-11-28 14:20:20 +0100
  • 30b9811512 Enable checking MDP models from the CLI svkurowski 2014-11-28 13:54:36 +0100
  • c5f3555932 Move CUDA code into namespace svkurowski 2014-11-28 11:36:23 +0100
  • 356a690374 Merge work from master svkurowski 2014-11-28 11:32:41 +0100
  • 67bcd5038f Add general setting to enable CUDA on runtime svkurowski 2014-11-27 10:15:30 +0100
  • da3542dcec Integrate CUDA into buildsystem and add example function svkurowski 2014-11-27 10:15:20 +0100
  • aebb1e65e0 Merge branch 'master' into parametricSystems dehnert 2014-11-28 11:15:06 +0100
  • 5676d990c4 APs true/false can now be queried for a state. dehnert 2014-11-28 11:14:55 +0100
  • 980b7790a7 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2014-11-28 00:03:10 +0100
  • 609a948495 Put noexcept in Macro and use deprecated throw() for MSVC to make it happy. dehnert 2014-11-28 00:02:48 +0100
  • 27b630bccc Removed debug output. dehnert 2014-11-27 23:50:09 +0100