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

Commit Graph

  • 05e97917aa Enable travis support for stable branch Matthias Volk 2017-08-11 10:54:56 +0200
  • 8aaa205c57 Added travis build status to README Matthias Volk 2017-08-11 10:42:01 +0200
  • c639f39076 require carl version 17.08 Sebastian Junges 2017-08-10 15:10:40 +0200
  • 115f7734eb more work on dd bisim dehnert 2017-08-10 14:53:55 +0200
  • ea7843d64b Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-08-10 10:13:45 +0200
  • 9a20aed7f9 proper caching in all min/max/exists abstract representative functions dehnert 2017-08-09 20:36:58 +0200
  • 27ffeb3a45 fixed a critical bug in symbolic bisimulation and started reworking sparse quotient extraction dehnert 2017-08-09 16:58:33 +0200
  • 6edbc52171 Removed remark to non-existing make command in README Matthias Volk 2017-08-09 15:26:14 +0200
  • a1934ce8a9 Fixed minor things in README Matthias Volk 2017-08-09 13:27:10 +0200
  • 8ede347fdd Fixed warning by fixing typo Matthias Volk 2017-08-09 12:02:01 +0200
  • a71c0cb585 Made some sylvan Bdd creations explicit dehnert 2017-08-07 20:38:06 +0200
  • 51e5c11dfa using refs in sylvan signature refinement dehnert 2017-08-07 20:33:19 +0200
  • 2441d9b8d7 removed conversion operator for Bdd dehnert 2017-08-07 20:32:02 +0200
  • d0ec9a362f added time output to cli dehnert 2017-08-07 20:29:26 +0200
  • cdf76b0c15 fixed DD-based quotient extraction in bisimulation dehnert 2017-08-06 15:17:55 +0200
  • 653e5fc184 setting default native technique to jacobi again dehnert 2017-08-05 07:41:21 +0200
  • 18ba906914 re-added gmp include directory to sylvan CMakeLists.txt dehnert 2017-08-04 23:26:07 +0200
  • 6b59e1563b Merge remote-tracking branch 'origin/master' into symbolic_bisimulation dehnert 2017-08-04 23:04:16 +0200
  • d0cf2ef57b update to version 1.4.0 of sylvan dehnert 2017-08-04 23:01:17 +0200
  • 81e9d2ae50 added some sanity checks and debug output dehnert 2017-08-04 14:35:38 +0200
  • c3d07063d4 Merge from upstream/master Matthias Volk 2017-08-04 11:07:20 +0200
  • 9342cc3f6c Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-08-04 10:51:04 +0200
  • 38cc9b1265 Fixed typo in doc Matthias Volk 2017-08-04 10:27:27 +0200
  • 9373e3d763 started on MDP quotient extraction dehnert 2017-08-03 22:14:05 +0200
  • 2b0911d627 more work on MDP bisimulation dehnert 2017-08-03 18:20:30 +0200
  • 07fe0a8e3a new target: binaries, compiles all the storm binaries, but not the tests etc Sebastian Junges 2017-08-03 17:41:37 +0200
  • 324c0770dd jani parser supports abscence of action declarations Sebastian Junges 2017-08-03 17:40:51 +0200
  • 6434587774 update changelog Sebastian Junges 2017-08-03 17:17:36 +0200
  • a3337afb22 changelog updated in preparation of version 1.1.0 Sebastian Junges 2017-08-03 17:00:53 +0200
  • b24ba75909 option to only get welldefinedness constraints for a parametric model Sebastian Junges 2017-08-03 16:56:39 +0200
  • ca3b475ce5 collect variables during collection of constraints Sebastian Junges 2017-08-03 16:56:05 +0200
  • 472eaffabc more work on refiners that deal with nondeterminism variables dehnert 2017-08-03 16:57:11 +0200
  • 9ca14a54fc templated the LpSolvers TimQu 2017-08-03 16:24:26 +0200
  • f46e8bcccf fixed selecting LPMinMaxSolver in --exact mode TimQu 2017-08-03 16:22:47 +0200
  • e38ec10459 fixed permissive scheduler test (which is only compiled when gurobi is there) TimQu 2017-08-03 16:21:27 +0200
  • 8ff7cd1026 removed solver and constraint names in the LpMinMaxSolver TimQu 2017-08-03 09:36:53 +0200
  • 9341a5d386 added support for scheduler generation with the Lp based MinMaxSolver TimQu 2017-08-02 13:44:44 +0200
  • 89f1796c56 Fixed creation of LpMinMaxSolver with the generalMinMaxSolverFactory TimQu 2017-08-02 13:44:17 +0200
  • 31b5d77560 fixed expected results which have been too imprecise for the LP-based MinMaxLinearEquationSolver TimQu 2017-08-02 13:43:03 +0200
  • 6a986d2490 tests for MinMaxLinearEquationSolver TimQu 2017-08-01 15:41:54 +0200
  • 5fdb03440d First version of LpMinMaxLinearEquationSolver TimQu 2017-08-01 15:41:40 +0200
  • 499b25c3ea removed methods 'getPrecision' and 'getRelative' from the abstract MinMax solver interface. Not every solver needs these methods. TimQu 2017-08-01 15:41:12 +0200
  • 26aba5ebb2 make sure cudd makefile.in and aclocal.m4 are ignored Sebastian Junges 2017-08-03 16:37:59 +0200
  • 9ac6d40e6e Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-08-03 12:05:20 +0200
  • 369319310a Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-08-03 11:18:22 +0200
  • 3f241280ea Refactored version setting in CMake Matthias Volk 2017-08-03 11:16:48 +0200
  • 7330f1659e Set development flag for Storm version Matthias Volk 2017-08-03 10:49:26 +0200
  • 1f90b41046 Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-08-03 10:10:46 +0200
  • d0840f783a further in debugging MDP bisimulation dehnert 2017-08-02 21:58:54 +0200
  • a1db269e8f started on debugging MDP bisimulation dehnert 2017-08-02 13:55:30 +0200
  • f3ebfaa90f more work on MDP bisimulation dehnert 2017-08-01 21:23:08 +0200
  • 03920c096a missing file dehnert 2017-08-01 15:25:06 +0200
  • c586213bc6 started on factoring out preservation information dehnert 2017-08-01 13:28:54 +0200
  • 277faf6673 started on MDP partition refiner dehnert 2017-08-01 12:49:56 +0200
  • 22d5cb95cd add forgotten file dehnert 2017-08-01 12:29:38 +0200
  • 4af363811f reworked refinement a bit in an attempt to prepare for MDPs dehnert 2017-08-01 12:24:13 +0200
  • b3a2da48d9 storm wellformedness constraints fixed in case of negative coefficients Sebastian Junges 2017-07-31 16:38:51 +0200
  • d1f8712542 Check updates do not contain negative likelihoods Sebastian Junges 2017-07-31 16:38:05 +0200
  • cd8dafa6ea Check for absence of negative probabilities in matrix Sebastian Junges 2017-07-31 16:37:40 +0200
  • b25ef3f09c introduced symbolic bisimulation modes lazy and eager, fixed bug in sparse quotient extraction dehnert 2017-07-31 10:19:06 +0200
  • 31f85e4b5b Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-31 09:59:05 +0200
  • cbe906605f updated changelog TimQu 2017-07-29 22:51:07 +0200
  • e7d273354c Allowing to write 'R=? [MP]' instead of 'R=? [LRA]' TimQu 2017-07-29 22:48:23 +0200
  • 39549f6ebd Moved some functionality of StandardMinMaxSolver into a subclass TimQu 2017-07-29 21:21:20 +0200
  • 25843ee53b added setting 'lramethod' TimQu 2017-07-29 13:54:24 +0200
  • 5b10b027fc implemented VI based Long-run-average method for MDPs TimQu 2017-07-29 12:08:23 +0200
  • bae41009a2 LRA method for MAs can now be switched to LP-based method TimQu 2017-07-29 12:07:41 +0200
  • 77c0cdc0e3 added minmax method 'linearprogramming' TimQu 2017-07-29 11:49:26 +0200
  • 724e059083 Fixed parsing prism models with action rewards that refer to action labels introduced during module renaming. TimQu 2017-07-29 11:48:00 +0200
  • f1ca2853f7 fixed some typo and added some documentation dehnert 2017-07-29 11:25:05 +0200
  • 4492f428bb worked in fix to Cudd_addMinus suggested by Fabio Somenzi dehnert 2017-07-29 09:55:04 +0200
  • f5ba5204c9 adding some debug functionality to DdManager to corner dynamic reordering issue with CUDD dehnert 2017-07-28 22:28:17 +0200
  • bda9a797e8 fixed some issues in CUDD (fixes provided by Fabio Somenzi) dehnert 2017-07-28 22:04:43 +0200
  • 66e1cf8bd6 Add support for Fedora's z3 package. Enno Ruijters 2017-07-28 16:33:58 +0200
  • aebe9fa3c3 LP-based long run average rewards for MDPs TimQu 2017-07-27 16:08:31 +0200
  • 2646097d8e added virtual destructor for NextStateGenerator TimQu 2017-07-27 12:30:53 +0200
  • fb6aa69750 started building the model for a given epoch TimQu 2017-07-27 11:28:38 +0200
  • 4c65739090 Merge branch 'master' into symbolic_bisimulation dehnert 2017-07-25 17:11:48 +0200
  • 282345e49d remove debug output dehnert 2017-07-25 17:04:28 +0200
  • 3bf40471b4 small fixes in matrix builder and removal of debug output dehnert 2017-07-25 17:03:36 +0200
  • fffb9207d7 implemented basic functionality of the multi-dimensional reward unfolding TimQu 2017-07-25 15:36:17 +0200
  • 291264fff6 restricting multi-dimensional bounded until formulas to a single-dimensional one TimQu 2017-07-25 15:35:35 +0200
  • 52b07a0c2f fixed a bug in sparse matrix builder, fixed some tests dehnert 2017-07-25 12:17:53 +0200
  • 4c3a409961 readd sparsepp in new version dehnert 2017-07-24 23:02:43 +0200
  • 4b21026bd7 Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-24 09:52:35 +0200
  • 8a01765005 enabling symbolic bisimulation from cli dehnert 2017-07-23 18:43:10 +0200
  • 5e67d66a3b Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective TimQu 2017-07-23 13:56:22 +0200
  • ad9008e0c1 fixing more warnings related to struct vs. class forward declarations dehnert 2017-07-22 21:22:01 +0200
  • c03c5fceb7 fixed warnings related to the mixed use of struct/class dehnert 2017-07-22 19:48:51 +0200
  • 7c23aab43c code skeleton for multi-dimensional reward unfolding TimQu 2017-07-21 17:27:49 +0200
  • 63917eb073 Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-07-21 11:41:59 +0200
  • 1cb9c553eb Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-20 15:52:13 +0200
  • 234b590bdf Fixed #include TimQu 2017-07-20 15:51:36 +0200
  • 069a1ae85e Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-20 10:12:40 +0200
  • 5b35927ecb fix for some multi-objective queries TimQu 2017-07-19 20:20:28 +0200
  • c0d364cf1b fixed a warning TimQu 2017-07-19 19:15:41 +0200
  • 241fc88077 multi-dimensional time bounds Sebastian Junges 2017-07-19 20:23:52 +0200
  • c770649f26 Increased caching timeout in travis Matthias Volk 2017-07-19 16:47:28 +0200
  • 1bf272263f Decreased timeout for mac in travis once again Matthias Volk 2017-07-19 16:42:55 +0200
  • 3b561cece8 Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-19 13:41:14 +0200