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

Commit Graph

  • 8271045b27 ToString is const Mavo 2016-01-08 18:12:37 +0100
  • 3e23a9ad40 some typos dehnert 2016-01-05 21:21:03 +0100
  • 4c09f9ce29 Minor improvements Mavo 2016-01-04 11:17:44 +0100
  • 94b817c531 removed debug output dehnert 2016-01-04 10:52:58 +0100
  • ed035440c5 Merge branch 'future' into param_elim_order dehnert 2016-01-04 10:04:59 +0100
  • 73ed137587 support for gurobi 6.5.0 on MacOS sjunges 2016-01-04 10:03:56 +0100
  • 4e16571f8a removed missing function. sjunges 2016-01-04 10:02:51 +0100
  • b1c103811b conditional probabilities in MDPs should now also work in the min-case dehnert 2015-12-29 22:00:46 +0100
  • 3e38e73efe conditional probabilities in MDPs (Baier method) available in sparse MDP model checker dehnert 2015-12-29 20:56:02 +0100
  • 756b2c5e30 added globally operator to functionality of hybrid/symbolic MDP model checkers dehnert 2015-12-29 19:22:09 +0100
  • 135dfb27b1 added globally operator to funcationlity of sparse MDP model checker dehnert 2015-12-29 19:01:40 +0100
  • d42f52d983 all DTMC model checkers now support checking globally formulas dehnert 2015-12-27 23:37:59 +0100
  • 38a2352e83 Merge remote-tracking branch 'origin/future' into TimParamSysAndSMT TimQu 2015-12-27 16:52:37 +0100
  • 6006d95193 Fixed compile errors: Added missing include and fixed call of std::max TimQu 2015-12-27 14:14:52 +0100
  • 84205a0bf6 refined computation of conditional probs a bit. Sebastian, if you're reading this: shouldn't you be working? :) dehnert 2015-12-26 22:10:47 +0100
  • 33757633c8 first version of conditional probabilities for (non-parametric) DTMCs a la Baier dehnert 2015-12-26 12:45:26 +0100
  • 0ffbda5aff initial draft of long-run rewards for parametric models dehnert 2015-12-25 17:36:37 +0100
  • 645f130a62 introduced long-run average reward formula dehnert 2015-12-24 13:01:16 +0100
  • 52dedca2a0 added tiny example for long-run properties dehnert 2015-12-24 09:31:37 +0100
  • 2a5780d5be first version of long-run-average for parametric DTMCs dehnert 2015-12-23 22:12:10 +0100
  • cd8fd76520 some refactoring in an attempt to make the state-elimination procedure flexible and readable at the same time dehnert 2015-12-23 18:02:18 +0100
  • 0f6e6e4da1 added feature to compute step-bounded until probabilities in parametric models dehnert 2015-12-22 19:33:39 +0100
  • 98d173ca3c changed elimination-based model checker to be able to compute values for all states (for reachability probs and reachability rewards) dehnert 2015-12-22 17:26:54 +0100
  • 8ed4a5f849 some refactoring in elimination-based model checker dehnert 2015-12-22 15:48:50 +0100
  • 1225b056f2 a little refactoring TimQu 2015-12-22 14:20:50 +0100
  • e3d4a3c019 Merge branch 'future' into python_api sjunges 2015-12-22 14:06:50 +0100
  • 3217a2ce18 Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future sjunges 2015-12-22 14:06:21 +0100
  • 89d6891c5d Merge branch 'future' into python_api sjunges 2015-12-22 14:04:23 +0100
  • bfd6e62c69 updated python api + setup.py sjunges 2015-12-22 14:04:18 +0100
  • 1e1400d68d merge sjunges 2015-12-22 13:59:53 +0100
  • 096778a5d0 assorted fixes (builder for no-fix-deadline, semicolon, xercesbuild) sjunges 2015-12-22 13:45:35 +0100
  • 8ab7cae974 early termination TimQu 2015-12-21 19:16:16 +0100
  • d5601bd328 bugfix dehnert 2015-12-21 16:07:02 +0100
  • f5298819d6 Merge branch 'future' into python_api sjunges 2015-12-21 15:43:09 +0100
  • fc41c3a6dd some more work on other elimination orders dehnert 2015-12-20 20:05:55 +0100
  • c0b5190022 Extended interface of linEqSolvers a little, eq solver is now called repeatedly with increased precision, until the result is good enough.. TimQu 2015-12-20 15:03:03 +0100
  • dd5af80d5a work towards easier deployment of other ordering heuristics dehnert 2015-12-18 17:01:29 +0100
  • 6e2f5602e1 Finished templating Mavo 2015-12-18 14:00:02 +0100
  • 7a0207637a Small templating Mavo 2015-12-18 10:35:15 +0100
  • 69168e9236 Use rate instead of prob Mavo 2015-12-17 13:52:34 +0100
  • 7737205149 More refactoring with templates Mavo 2015-12-17 12:16:34 +0100
  • 4343b5b980 Refactored some classes into templates Mavo 2015-12-17 11:55:29 +0100
  • d5474722c0 Label generation from FT Mavo 2015-12-17 11:35:28 +0100
  • 34ba28cfdb some minor fixes dehnert 2015-12-16 18:02:46 +0100
  • 91fe16c699 1st try on CTMC model checking Mavo 2015-12-16 17:59:55 +0100
  • 4ae86c76f9 Output uses logger now Mavo 2015-12-16 16:53:33 +0100
  • 0c37f078fb Build transition matrix for FT Mavo 2015-12-16 14:16:26 +0100
  • f72f556018 improved spirit error handling a bit dehnert 2015-12-16 13:49:16 +0100
  • 3adc6a7280 Merge branch 'future' into sylvan dehnert 2015-12-15 20:53:33 +0100
  • 0d912ee59d finalized sylvan tests dehnert 2015-12-15 20:52:57 +0100
  • d0e15d1a4f more work (and stuff, you know?) dehnert 2015-12-15 17:02:58 +0100
  • 4c1d71fc91 Fixed compile warnings Mavo 2015-12-15 12:14:12 +0100
  • 7b37023f79 Some refactoring Mavo 2015-12-15 11:48:11 +0100
  • 4bd59b8649 Small formatting changes Mavo 2015-12-14 16:44:53 +0100
  • b297cdf38f added some syntatic sugar to PRISM parser in order to enhance performance tests of symbolic model checker dehnert 2015-12-14 15:58:37 +0100
  • 329fee6b32 added performance tests for symbolic DTMC model checker dehnert 2015-12-13 21:28:35 +0100
  • 0d6612352c silenced sylvan and gmm warnings (for clang) dehnert 2015-12-11 19:52:22 +0100
  • 7643ebc70d Compile fixes Mavo 2015-12-11 19:10:55 +0100
  • 1faa2c6f9e Merge from future Mavo 2015-12-11 19:00:37 +0100
  • abacfdd28d added sylvan settings. made sylvan available from the cli dehnert 2015-12-11 17:01:07 +0100
  • 0708672a68 removed ite for ADDs as this operation should be formed with a BDD as the first argument. as a compensation, we provide a version of ite that takes a BDD and two ADDs and returns the corresponding ADD dehnert 2015-12-09 22:01:48 +0100
  • b7ea918d1b update to latest version of sylvan and accompanying changes (mostly because 0 * inf = nan in IEEE754) dehnert 2015-12-07 21:34:50 +0100
  • f8fc39870a hybrid and symbolic model checkers working with sylvan dehnert 2015-12-07 12:21:12 +0100
  • 7376eaf866 made symbolic MDP model checker tests work dehnert 2015-12-07 10:52:12 +0100
  • 7f75db2790 ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working. dehnert 2015-12-06 22:16:50 +0100
  • f2a01afbdf ODD-based stuff working for Sylvan. Almost all tests passing dehnert 2015-12-05 20:32:05 +0100
  • 36a6e9e76e more work on sylvan ODD-related stuff dehnert 2015-12-04 15:47:57 +0100
  • fd417fb6d6 started working on ODD-based functionality for sylvan dehnert 2015-12-03 23:01:37 +0100
  • 50e7bbfe35 fixed a tests, all tests running again dehnert 2015-12-03 19:10:21 +0100
  • ebe9ccbb15 some work on DD stuff dehnert 2015-12-03 17:57:55 +0100
  • 4a772fe48d fixed bug in sylvan dehnert 2015-12-02 21:56:44 +0100
  • f5b1193a56 Merge remote-tracking branch 'origin/future' into future sjunges 2015-12-02 20:06:24 +0100
  • 693dce8618 update to newest version of sylvan dehnert 2015-12-02 16:51:21 +0100
  • 8657fb0181 introduced relational product operations to prob0/1 algorithms (where possible) dehnert 2015-12-02 16:36:52 +0100
  • 494f263b71 fixed a wrong assumption for sylvan relnext dehnert 2015-12-01 20:40:44 +0100
  • 3556743d7e more work on introducing relation products dehnert 2015-12-01 19:40:37 +0100
  • e43bdfaaaa more work on the dd stuff *sigh* dehnert 2015-12-01 17:31:04 +0100
  • f98f701e05 Merge remote-tracking branch 'origin/future' into TimParamSysAndSMT TimQu 2015-12-01 09:54:32 +0100
  • fdf237ca67 added support to create measure driven initial partition for bisimulation for MDPs from formula that does not specify an optimization direction dehnert 2015-11-30 19:35:44 +0100
  • 598ed08116 worked in newest sylvan changes to api dehnert 2015-11-30 15:58:30 +0100
  • 5a0c54034e committed missing files dehnert 2015-11-30 15:40:08 +0100
  • fb4c103320 merged sylvan updates into the sylvan copy. made more tests work dehnert 2015-11-30 13:27:26 +0100
  • 91fb664910 Refactored a little and implemented functions for prophesy TimQu 2015-11-29 19:31:43 +0100
  • 3eed9dce39 Merge branch 'future' into TimParamSysAndSMT TimQu 2015-11-29 10:48:06 +0100
  • 0fee7d40a6 fixed bug in sylvan dehnert 2015-11-27 20:22:32 +0100
  • 10996b4ab5 more work on sylvan dehnert 2015-11-27 17:01:46 +0100
  • 7ea0cb19b3 added some new functions to sylvan. isolated new code to make it easier to update sylvan to newer versions later dehnert 2015-11-26 22:29:24 +0100
  • 8eb3720f91 more work on sylvan integration dehnert 2015-11-26 17:40:33 +0100
  • 6c1a21c43f added more functions in sylvan dehnert 2015-11-25 22:24:03 +0100
  • 31147a90d2 removed or and not operation on ADDs as they should conceptually be used on BDDs dehnert 2015-11-25 18:47:33 +0100
  • 2c69232560 started cleaning ADD interface dehnert 2015-11-25 16:42:09 +0100
  • 472851508c changed return type of equal, notEqual, less, lessOrEqual, greater, greaterOrEqual to BDD since returning an ADD is logically not quite correct dehnert 2015-11-24 22:06:25 +0100
  • 8194454621 more work on making sylvan mtbdds work dehnert 2015-11-24 17:55:30 +0100
  • 99f096635f started integrating sylvan dehnert 2015-11-23 15:56:09 +0100
  • f7992f5aa7 Forgot adaptation of test... TimQu 2015-11-22 21:34:23 +0100
  • b4a4a81bb1 Renamed, moved, added some benchmarks TimQu 2015-11-22 21:33:26 +0100
  • f3f3a31e1e Optimization for policy recycling TimQu 2015-11-22 21:25:09 +0100
  • cb58b79e24 moved cudd's c++ objects to a separate namespace in an attempt to make cudd and sylvan coexist without name clashes dehnert 2015-11-20 21:03:18 +0100
  • d25bd3a32f added 'empty' framework for sylvan-based implementation of DD abstraction layer dehnert 2015-11-20 20:14:41 +0100
  • c36d869b3c done cleaining up dehnert 2015-11-20 17:07:50 +0100