Commit Graph

  • c281efcde3 refactored parts of the api sjunges 2015-09-08 11:28:44 +0200
  • fd86d430ae minor fix dehnert 2015-09-07 21:56:52 +0200
  • 5b1494b9a9 Made use of this new cool rewardModel thing TimQu 2015-09-07 20:28:20 +0200
  • 5521172ed1 more work on sparse game solver dehnert 2015-09-07 19:35:37 +0200
  • e659dd8c4a some work on sparse game solver dehnert 2015-09-07 18:44:29 +0200
  • 8fd0ee2ecd Formula to string added sjunges 2015-09-07 18:27:19 +0200
  • 8a48f80a99 use ccache as an option sjunges 2015-09-07 18:26:46 +0200
  • 1766018cf7 Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future sjunges 2015-09-07 18:09:00 +0200
  • 3e9f095cd4 new version of storm-core python api sjunges 2015-09-07 18:08:13 +0200
  • df850fe085 Merge branch 'master' into TimParamSysAndSMT TimQu 2015-09-07 16:32:01 +0200
  • ebdf44485c Merge branch 'master' into TimParamSysAndSMT TimQu 2015-09-07 16:31:16 +0200
  • 0c5c782c7e Merge branch 'future' into menu_games dehnert 2015-09-07 14:35:28 +0200
  • c5c3f7ef07 Merge branch 'master' into future dehnert 2015-09-07 14:10:35 +0200
  • 7ac6dd94ab Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-09-07 14:00:51 +0200
  • b2d8cae9ce instantiated (and fixed occurring problems) explicit parsers with intervals as the reward model value type dehnert 2015-09-07 14:00:35 +0200
  • 358e6cea9d Merge branch 'future' into python_api sjunges 2015-09-07 11:59:54 +0200
  • e38bd26241 Merge branch 'master' into future sjunges 2015-09-07 11:46:34 +0200
  • 1250b842b1 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-09-07 11:44:10 +0200
  • 01a3748e87 Refactored part of the API / more functions sjunges 2015-09-07 11:35:59 +0200
  • d377e6b289 Minor improvements everywhere. Also implemented some tests TimQu 2015-09-06 21:29:22 +0200
  • c4444567e7 further optimization on approximation model initialization. Also better code structure of preprocessing steps TimQu 2015-09-05 19:15:18 +0200
  • bc3f6b8d80 fixes for parts that were affected by recent parser templating dehnert 2015-09-04 12:52:52 +0200
  • 27e06940a9 templated all explicit parsers so that they may now be modified to produce non-double models dehnert 2015-09-04 12:45:22 +0200
  • 98e3226fd1 first version of stormpy (we can parse a prism program) sjunges 2015-09-04 10:54:23 +0200
  • 22f1d99a15 missing files finally added dehnert 2015-09-04 10:15:32 +0200
  • af505c7e89 Faster and more structured initialization of approx and sampling model TimQu 2015-09-03 20:10:42 +0200
  • 2991cd0a79 Merge branch 'future' into python_api updated cmake lists accordingly sjunges 2015-09-03 18:59:29 +0200
  • 7fd28d4564 refactored cmakelists sjunges 2015-09-03 18:33:06 +0200
  • a216b5a9d9 added support for parsing choice labels for explicit MDPs chris 2015-09-03 17:53:19 +0200
  • 8ae403a769 Merge branch 'future' into python_api sjunges 2015-09-03 17:30:01 +0200
  • 70a7b5ffbd Merge branch 'master' into future sjunges 2015-09-03 17:29:35 +0200
  • d214e8783e first version for python support sjunges 2015-09-03 17:27:56 +0200
  • dbe997a433 resolved linker error - sorry sjunges 2015-09-03 14:30:51 +0200
  • bdb105ce85 cmake: marked several variables as advanced sjunges 2015-09-03 14:17:47 +0200
  • 46d8accf6e logic::comparisontype operations sjunges 2015-09-02 19:44:10 +0200
  • ebab145180 use default bitvector move, which is fine sjunges 2015-09-02 19:43:45 +0200
  • 6503d929de includes the headers for the number types supported by the carl-configuration used on the system sjunges 2015-09-02 19:16:32 +0200
  • be0eee21db Dont build so many models with float/rational functions sjunges 2015-09-02 12:44:10 +0200
  • 2213b01ece changes in milp permissive scheduler sjunges 2015-09-02 19:11:26 +0200
  • f65efdb4bb disable smtrat for now sjunges 2015-09-02 16:31:32 +0200
  • 0311e85f62 Merge branch 'master' into future sjunges 2015-09-02 12:54:51 +0200
  • 85e15c035f Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-09-02 12:44:10 +0200
  • b007d45543 Extended lp solver factory interface sjunges 2015-09-02 12:43:43 +0200
  • dbe4380b09 Option to force color output for clang/ninja. sjunges 2015-09-02 10:50:01 +0200
  • 9254e6650c Option to force color output for clang/ninja. sjunges 2015-09-02 10:50:01 +0200
  • d57551c1ec Fix for solver TimQu 2015-09-01 22:27:44 +0200
  • 7946483f09 added function to modify state-action rewards in nondeterministic model dehnert 2015-09-01 21:53:27 +0200
  • 37a7b392f6 First version of approximation for rewards TimQu 2015-09-01 19:36:18 +0200
  • e7d82fbaf5 Fix sjunges 2015-09-01 18:23:59 +0200
  • 6d10ba0ad0 compiles again sjunges 2015-09-01 18:22:16 +0200
  • c41c5150f1 Merge branch 'master' into future sjunges 2015-09-01 17:36:43 +0200
  • f08f66e900 added an option for polic extraction to the helper, some includes sjunges 2015-09-01 17:35:59 +0200
  • 2dc9eb9b83 Currently exclude smtrat- does not compile with current version. sjunges 2015-09-01 17:31:35 +0200
  • 72ef715d68 Return type to also include partial schedulers sjunges 2015-09-01 17:00:12 +0200
  • bed31b463f Added generated sources sjunges 2015-09-01 14:55:42 +0200
  • 8d2bd4fd9d fixed two warnings dehnert 2015-08-31 19:24:37 +0200
  • 7cafd61c38 switched gcc to use c++14 as well dehnert 2015-08-31 19:11:49 +0200
  • e364d3be53 added missing header dehnert 2015-08-31 18:47:11 +0200
  • 5de90c27e5 Preprocessing, sampling and state elimination now also work with rewards TimQu 2015-08-31 18:33:24 +0200
  • 2f5df9d72f use the configured factory in the sparse mdp helper sjunges 2015-08-31 17:55:45 +0200
  • 73310b9881 fixed tests: glpk had wrong minimize, solver.cpp tested in wrong direction on policy iteration in case we use top. value iteration sjunges 2015-08-31 17:54:44 +0200
  • 86b2f8d13e Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-31 14:26:01 +0200
  • 8568ee3986 only one optimization direction enum -- towards integration of termination criterions on the model checker sjunges 2015-08-31 14:22:24 +0200
  • 08bc810b2c added missing include dehnert 2015-08-31 12:41:20 +0200
  • 57338640be added missing include dehnert 2015-08-31 12:00:20 +0200
  • f4211637db fixed warning and missing include dehnert 2015-08-31 11:37:35 +0200
  • 56eae69703 added more missing headers dehnert 2015-08-31 11:31:40 +0200
  • b418782bcd added missing header dehnert 2015-08-31 11:23:04 +0200
  • 3ea084b777 included missing header dehnert 2015-08-31 11:15:49 +0200
  • ad660f0f98 more ifdefs for everyone dehnert 2015-08-31 11:09:13 +0200
  • ee6d71d3d4 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-31 11:06:49 +0200
  • 3657b13aa9 another missing ifdef dehnert 2015-08-31 11:04:42 +0200
  • 1d5faef301 cmake use carl flag sjunges 2015-08-31 11:03:42 +0200
  • 16d672a5cb put carl reference in ifdef dehnert 2015-08-31 11:03:30 +0200
  • e67e057e98 Merge branch 'master' into menu_games dehnert 2015-08-31 10:33:14 +0200
  • 032e141254 small fix to the way interval reward models are reduced to a scalar vector dehnert 2015-08-31 10:30:24 +0200
  • f409087f47 first version of interval reward model support for MDPs. also fixed a missing include that prevented compilation of the main executable dehnert 2015-08-31 10:17:47 +0200
  • f51e8eeaea moved reward model template parameter from helper classes to the affected functions. this sadly excludes the SparseDtmcPrctlHelper for which clang then produces a segfault (bug report pending) dehnert 2015-08-30 22:19:20 +0200
  • d0f7e5f6da First steps towards working with rewards TimQu 2015-08-30 17:32:37 +0200
  • 21d9e91586 work towards interval reward model dehnert 2015-08-28 23:13:24 +0200
  • 36b67a3a38 refined output of deadlock states a bit dehnert 2015-08-27 09:34:18 +0200
  • d4d49e49ce Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-26 22:48:13 +0200
  • 1713e10efc added output of first 3 deadlock states in symbolic model builder dehnert 2015-08-26 22:48:06 +0200
  • 35a154f67f Splitted graph in h and cpp` sjunges 2015-08-26 21:20:00 +0200
  • 3ae5ea7000 Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-26 19:40:12 +0200
  • e3122e5ede Faster compilation and topological failing test failed sjunges 2015-08-26 19:39:38 +0200
  • d4cd58e9c6 upon preserving a new formula, the builders now do not apply terminal states dehnert 2015-08-26 18:36:42 +0200
  • ffc9eda1c2 enabled terminal states for explicit model builder dehnert 2015-08-26 18:24:22 +0200
  • 8489328e25 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-26 16:52:52 +0200
  • 31ed578e2c Xcode generation fix. sjunges 2015-08-26 16:53:41 +0200
  • 4e8538e282 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-26 16:44:22 +0200
  • ce8819b44d Merge branch 'master' of https://sselab.de/lab9/private/git/storm sjunges 2015-08-26 16:44:28 +0200
  • 3849c59d6b formula parser now correctly accepts variables of a loaded model dehnert 2015-08-26 16:44:21 +0200
  • f219437acf Faster compilation times! sjunges 2015-08-26 16:44:00 +0200
  • 1086ffc1cc Added allow early termination for min/max solvers sjunges 2015-08-26 14:57:42 +0200
  • 080b50a890 fixed bug in symbolic model generation dehnert 2015-08-26 13:45:34 +0200
  • a027645371 Merge branch 'master' into menu_games dehnert 2015-08-26 10:48:49 +0200
  • 53524c3c6e Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2015-08-25 19:07:31 +0200
  • 9f70e7cb3b adapted DD-based model exploration to the new policy regarding writing to global variables dehnert 2015-08-25 19:07:27 +0200
  • f006d54995 vector min_if, max_if sjunges 2015-08-25 17:09:29 +0200