Commit Graph

  • 009dabf2f1 started cleanining up dehnert 2015-11-20 15:57:21 +0100
  • a258d1ab48 restructured ODD to be independent of the DD library being used dehnert 2015-11-20 14:19:23 +0100
  • 19029cd905 functional tests compile and run again, yay! dehnert 2015-11-19 18:00:51 +0100
  • 960ef4ff65 same shit, different day dehnert 2015-11-18 20:50:54 +0100
  • 231c3ec060 started lifting toVector, etc. from the internal classes to the general superclasses dehnert 2015-11-18 16:10:34 +0100
  • 9c645ba24b Work on policy recycling TimQu 2015-11-17 18:55:15 +0100
  • f7c26fd4b1 more modifications needed for refactoring of DD stuff dehnert 2015-11-17 17:09:11 +0100
  • dae0faa2a0 refactored the quick implementation of the recent bugfix TimQu 2015-11-16 20:36:23 +0100
  • 4a874a5a29 Added some benchmark models from param website Fixed two bugs considering nonatomic subformulae and constant results Qualitative modelchecking needs to be done when applying a policy! TimQu 2015-11-15 22:38:01 +0100
  • 8bf0f3c87e apparently, changing the DD interface implies some other changes as well... dehnert 2015-11-13 22:29:25 +0100
  • 7fa7381047 trying to get the new infrastructure of the DD abstraction layer integrated into the other parts of storm dehnert 2015-11-13 18:12:33 +0100
  • 340b39e4a7 more work on refactoring DD abstraction layer dehnert 2015-11-12 22:11:16 +0100
  • 87c8241ec7 policies for games TimQu 2015-11-12 21:00:21 +0100
  • eb1619153e same same dehnert 2015-11-12 17:01:55 +0100
  • 52062b523d more work on refactoring DD abstraction layer dehnert 2015-11-11 21:46:46 +0100
  • d683e38d4a started refactoring DD-interface a bit in an attempt to ease the integration of sylvan dehnert 2015-11-11 17:39:13 +0100
  • bf450688b4 The variable pool of carl needs to be cleared after executing a test. Sampling for mdps now uses the policy of the previous iteration as initial guess TimQu 2015-11-10 19:59:19 +0100
  • 4e86ef2e47 moved CUDD-based DD implementation to own folder dehnert 2015-11-10 19:45:49 +0100
  • 7080f954b9 Fixed sylvan cmake file to also work with xcode (stripping the build type from the directory) dehnert 2015-11-10 18:39:48 +0100
  • 226c77db77 added sylvan and started making it compile using cmake dehnert 2015-11-10 17:00:20 +0100
  • b88165f27c fixed the warnings related to our macros dehnert 2015-11-10 15:58:19 +0100
  • 4d36ee3ea1 Merge branch 'master' into future dehnert 2015-11-10 15:18:15 +0100
  • 8d98403748 small fix for use of carl dehnert 2015-11-10 15:17:58 +0100
  • 358bc14ded Merge branch 'future' into TimParamSysAndSMT TimQu 2015-11-10 14:43:32 +0100
  • e8304e7515 Merge branch 'master' into future TimQu 2015-11-10 13:09:42 +0100
  • b792438d88 Added missing include TimQu 2015-11-10 13:09:12 +0100
  • 0089212b7e adaptation to recent changes in carl TimQu 2015-11-10 13:06:35 +0100
  • 0863d0e51a don't store ALL the occurring policies... TimQu 2015-11-10 11:39:23 +0100
  • 1d49bc6dd0 extracting the bisimulation quotient for MDPs; tests for MDP bisimulation dehnert 2015-11-09 12:02:20 +0100
  • bfbe63fcb4 fix bug ThomasH 2015-11-08 23:40:10 +0100
  • dfdfef3c6e complete parser ThomasH 2015-11-08 23:20:39 +0100
  • 10e93d7cbb update parser ThomasH 2015-11-08 18:48:04 +0100
  • c5f492c9a5 add example ThomasH 2015-11-08 16:19:36 +0100
  • 3229f07d43 partial implemetation of the non-validating pnml parser ThomasH 2015-11-07 17:02:58 +0100
  • b31d98909b Explicit MDP bisim working but unfortunately slow :( dehnert 2015-11-07 11:40:38 +0100
  • 7156a63b0f tried different approach for bisim for MDPs dehnert 2015-11-06 18:58:26 +0100
  • c2a0bd5ab0 initial outline of strong MDP bisimulation dehnert 2015-11-05 17:22:41 +0100
  • 288f0418c2 Merge branch 'future' into mdpbisim dehnert 2015-11-05 13:35:02 +0100
  • 9bac056354 enabled preconditioning for value iteration in gmm++-based MinMax equation solver dehnert 2015-11-05 13:32:39 +0100
  • ca917a651c MinMaxLinearEqSolvers can now use some initial policy as a first guess. First steps to use this for region approximation TimQu 2015-11-04 19:35:19 +0100
  • a723cfca14 Made sampling for MDPs correct again TimQu 2015-11-04 11:17:59 +0100
  • 7833025829 reenabled all bisimulation tests dehnert 2015-11-03 20:11:23 +0100
  • 3054aa9866 Merge branch 'future' into mdpbisim dehnert 2015-11-03 19:47:29 +0100
  • 1de6d4ee07 Merge branch 'master' into future dehnert 2015-11-03 19:45:53 +0100
  • 9b7d4ec57b made rational functions use cln again dehnert 2015-11-03 19:45:41 +0100
  • 51bd689c96 fixed a bug in the reward model dehnert 2015-11-03 17:41:01 +0100
  • 9475d29164 fixed weak bisim for dtmc dehnert 2015-10-31 15:23:09 +0100
  • 29597e014f more work on reimplementation of weak bisim dehnert 2015-10-30 16:58:09 +0100
  • e80a1081bb First steps to identify the parameters for which the optimal policy always choses the same boundary TimQu 2015-10-29 18:59:22 +0100
  • b182e3fdcf Small fix for policy extraction TimQu 2015-10-29 18:56:39 +0100
  • 91bfdba528 Scan for equal ranges of probabilities now uses std::equal_range and reduces the number of comparisons dehnert 2015-10-29 18:40:51 +0100
  • 46fee522ff made strong bisim for DTMCs work again dehnert 2015-10-29 16:35:18 +0100
  • fe3c4a1aa3 add dependencies ThomasH 2015-10-29 15:29:01 +0100
  • 8e680bda96 include header ThomasH 2015-10-28 21:59:04 +0100
  • 6ddddd8cfa Implemented policy extraction for value iteration TimQu 2015-10-28 19:04:50 +0100
  • 1f5110b90c work on making bisimulation fast again :( dehnert 2015-10-28 18:06:44 +0100
  • 2484a515a0 some more work on bisim dehnert 2015-10-27 23:30:51 +0100
  • 40a75baee7 using some template magic to make it compile again dehnert 2015-10-27 22:44:41 +0100
  • 11b04c7940 more work towards making the new bisim class available from the cl dehnert 2015-10-27 17:43:54 +0100
  • 1428f1647b commented in some more tests, however the main entry points need to be fixed because of the new templating of the bisimulation class dehnert 2015-10-26 18:51:24 +0100
  • 4c8e29d620 add new class files ThomasH 2015-10-26 18:49:23 +0100
  • 904a7aecc0 resolve bug (index out of bounds exception) ThomasH 2015-10-26 18:47:25 +0100
  • 11c21eb338 on my way of making (the refactored version) bisimulation work again for deterministic models dehnert 2015-10-25 22:06:58 +0100
  • 8637ce8a6f use absolute paths ThomasH 2015-10-25 17:00:14 +0100
  • cb839bedc8 use vectors instead of sets ThomasH 2015-10-25 16:51:27 +0100
  • 96954ddd15 refactoring of bisimulation class in the prospect of extending it to (CT)MDPs, not yet done dehnert 2015-10-24 23:00:47 +0200
  • 9e574b6631 Merge branch 'future' into python_api sjunges 2015-10-22 11:25:59 +0200
  • 86155a5a87 extra option for export of a matrix sjunges 2015-10-22 11:25:46 +0200
  • eacfe7a389 Merge branch 'future' into TimParamSysAndSMT TimQu 2015-10-21 18:16:34 +0200
  • df7b29ef18 partial implementation of gspns, transitions and markings ThomasH 2015-10-20 23:08:44 +0200
  • b09d123779 ... TimQu 2015-10-19 20:04:14 +0200
  • 1860502a3a Deterministic states with only constant outgoing transitions are now eliminated TimQu 2015-10-19 19:56:28 +0200
  • c92db9ff1d fix typedef (switched typename and alias) Thomas Henn 2015-10-19 00:21:57 +0200
  • 97e302a78c guarded timeouts in z3 by ifdef-guards dehnert 2015-10-16 13:32:35 +0200
  • 6cfa6ac9c7 added timeout to smt solver interface dehnert 2015-10-16 10:55:16 +0200
  • 77c2f397a9 fix for approximation model, additional test for mdps, minor changes TimQu 2015-10-15 17:55:37 +0200
  • cb913658cc removed perm schedulers from gspn to circumvent error msg for now sjunges 2015-10-14 14:15:23 +0200
  • b9f8de2c01 ... sjunges 2015-10-14 11:16:10 +0200
  • 703013b97c program, vector, gurobi sjunges 2015-10-14 11:10:54 +0200
  • c53b79b9b7 approximation model, again TimQu 2015-10-14 01:26:23 +0200
  • b3ce727f6c fixed minor bug, tests for smt-based permissive schedulers (for upper-bounded properties) now passing dehnert 2015-10-13 18:47:54 +0200
  • 59501dd347 removed some object files of xerces. started working on smt-based permissive schedulers dehnert 2015-10-13 17:36:26 +0200
  • 67ff27954e refactored approximation model (almost done) TimQu 2015-10-13 17:27:46 +0200
  • 5db1678528 Merge branch 'future' into gspn sjunges 2015-10-13 13:22:39 +0200
  • 160f9e476f test descr for milp perm sched sjunges 2015-10-13 10:55:15 +0200
  • 046afd3804 Refactored SamplingModel TimQu 2015-10-11 21:09:42 +0200
  • f167a46f44 Merge branch 'future' into TimParamSysAndSMT TimQu 2015-10-10 18:42:36 +0200
  • a5fae4603a Merge branch 'future' into gspn sjunges 2015-10-08 18:24:23 +0200
  • ee0e34146f build command index to action name mapping sjunges 2015-10-08 14:40:37 +0200
  • 66736c3626 More to string methods for simplevaluation sjunges 2015-10-08 14:38:55 +0200
  • f914c8a103 Filter std::vector by bitvector, could not find such a method before :/ sjunges 2015-10-08 14:38:13 +0200
  • ecb214bc10 StateInfo is a StateAnnotation now sjunges 2015-10-08 14:37:26 +0200
  • eacdec3939 State Annotation and subMDP also restrichts choicelabelling now sjunges 2015-10-08 14:37:00 +0200
  • a90287ea1b some early content sjunges 2015-10-08 14:23:10 +0200
  • 9bd2fc70bd Merge branch 'future' into gspn sjunges 2015-10-08 14:19:48 +0200
  • 6896a4ca51 stubs for gspn files sjunges 2015-10-08 14:19:42 +0200
  • 6f59fd7aca fixed computation of rewards in MDPs dehnert 2015-10-07 14:54:16 +0200
  • de58c73c5a forgot to commit some files dehnert 2015-10-06 18:40:28 +0200
  • 5c838e2006 added the feature to build information about the state space that can be retrieved after building the model to the explicit model builder dehnert 2015-10-02 13:53:44 +0200
  • 44a9636f69 fixed an issue with getSubmatrix dehnert 2015-10-02 12:00:22 +0200