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

Commit Graph

  • 9593ba5a7f better output in perm schedulers sjunges 2015-10-02 10:37:01 +0200
  • b06562ec31 fix in getSubmatrix sjunges 2015-10-02 10:36:17 +0200
  • 4b4c11048f fixed bug in prob1E. added functions to retrieve schedulers for prob0E, probGreater0E and prob1E states of MDPs dehnert 2015-10-01 17:29:12 +0200
  • 7884fc37ed explicit model builder supports non-default reward models sjunges 2015-10-01 15:14:24 +0200
  • ed94184ec8 initialize logger with loglevel as an argument sjunges 2015-10-01 14:16:56 +0200
  • 14639525b6 Revert "xerces on gitignore fix" sjunges 2015-10-01 13:51:49 +0200
  • d06c92c10a Revert "Revert "added flag that indicates which interval bound is to be taken. added xerces to the gitignore"" sjunges 2015-10-01 13:51:20 +0200
  • dfd2cda380 Revert "added flag that indicates which interval bound is to be taken. added xerces to the gitignore" sjunges 2015-10-01 13:50:07 +0200
  • 82f2927500 xerces on gitignore fix dehnert 2015-10-01 12:39:02 +0200
  • 16ea224b6a added flag that indicates which interval bound is to be taken. added xerces to the gitignore dehnert 2015-10-01 12:37:46 +0200
  • 57dffbcd4f further operators on models and reward models sjunges 2015-10-01 10:08:15 +0200
  • a28ebac022 outcommented code for maximals sjunges 2015-09-29 17:40:54 +0200
  • a07c2cacc4 missed files sjunges 2015-09-29 16:07:59 +0200
  • 7e7e025900 modifying reward models sjunges 2015-09-29 16:07:33 +0200
  • cf10fe206a modifiers for standard rew model, fix with non-const overload in model sjunges 2015-09-29 16:07:08 +0200
  • 9e24144c27 getRewardModel, private, added sjunges 2015-09-29 14:23:34 +0200
  • bd7fc0b341 operator< for stateaction pairs sjunges 2015-09-29 14:20:00 +0200
  • 0cdca6a5fc BitVector iterator += sjunges 2015-09-29 14:19:40 +0200
  • 896d2bcaef propositional model checking for further interval reward model types sjunges 2015-09-28 16:55:00 +0200
  • e4aab761d2 updates to perm schedulers sjunges 2015-09-28 16:54:30 +0200
  • 98162d1d7e interface for rew. model extended for reinforcement learning sjunges 2015-09-28 16:53:55 +0200
  • 765748c7cf graph stuff for other reward models.. sjunges 2015-09-28 16:53:06 +0200
  • e8799963fe compiles again sjunges 2015-09-27 21:28:58 +0200
  • b8343255be fixed headers, allow changes in rew. model again sjunges 2015-09-27 17:51:12 +0200
  • 53dc99deb0 prob01A for non.detmodels added (convenience function) sjunges 2015-09-27 17:50:00 +0200
  • 31be908c5a mathsat does not like boolean arguments to ite-expressions, so we encode it ourselves now dehnert 2015-09-25 18:40:52 +0200
  • 7ecd9958e8 more work on game-stuff dehnert 2015-09-25 16:57:27 +0200
  • 131ab5b674 Updates on perm. schedulers sjunges 2015-09-25 14:16:58 +0200
  • edbd7e827b MDPs, restrict choices, get choiceindex sjunges 2015-09-25 14:16:35 +0200
  • beee4a9e82 fixed a bug in the tests that caused a segfault dehnert 2015-09-24 19:00:08 +0200
  • 2376905810 more work dehnert 2015-09-24 17:44:26 +0200
  • 381fe6d9a8 more work on translating BDDs to expressions dehnert 2015-09-23 21:01:42 +0200
  • 4b24be7204 commit to switch workplace dehnert 2015-09-23 19:27:32 +0200
  • 2f49418e63 Add dependency on xercesc sjunges 2015-09-23 17:42:04 +0200
  • 21b0829b69 ... sjunges 2015-09-23 17:41:30 +0200
  • e9b4aa5de4 xerces 2nd part sjunges 2015-09-23 17:38:50 +0200
  • 73073d2fff Added Xerces sjunges 2015-09-23 17:36:57 +0200
  • 288f34b083 Added Xerces sjunges 2015-09-23 17:36:57 +0200
  • 8574d474a4 added support for computation of bottom states. not yet done dehnert 2015-09-23 17:11:43 +0200
  • 781610b05d extended tests for validity of returned strategies dehnert 2015-09-23 11:23:02 +0200
  • c624b19427 added no-cuts option. prob1 tests for game now passing. dehnert 2015-09-22 19:02:05 +0200
  • e8b7928831 fixed minor bug dehnert 2015-09-22 17:53:27 +0200
  • 1c42ed792b fixed some bugs, added some test, added some prob1 algorithm, and did some stuff, you know? dehnert 2015-09-22 16:58:56 +0200
  • 972795912a added some convenience accessor methods in symbolic model/games. added return type for prob01 for games that can also store strategies. added tests for prob0 for games dehnert 2015-09-21 21:43:04 +0200
  • 6c804732e1 introduced (probably buggy) versions of existsAbstractRepresentative on BDDs and prob0 for games dehnert 2015-09-21 16:32:31 +0200
  • 0cfc4dfd4d (re)introduced min/maxAbstractRepresentative for ADDs dehnert 2015-09-21 09:53:50 +0200
  • 0bd0b963d7 introduced new menu game class dehnert 2015-09-19 19:38:36 +0200
  • 7cd1e6324f the abstraction now properly builds an instance of the game class dehnert 2015-09-19 16:41:06 +0200
  • 1199ab95e3 fixed bug in expressions. all tests now passing dehnert 2015-09-19 13:29:41 +0200
  • 0cd148c600 fixed more bugs. however, a test still fails, because the abstraction is wrong dehnert 2015-09-18 21:19:49 +0200
  • e8794dee22 added more tests, not working yet, however dehnert 2015-09-18 16:58:09 +0200
  • 5934d67514 DD meta variables can now be inserted at particular locations. added some tests for game abstraction dehnert 2015-09-18 16:06:52 +0200
  • 8911d2ba63 added debug output and fixed some bugs dehnert 2015-09-17 23:46:45 +0200
  • 88bcd7d74c deadlock states now get fixed in abstract game dehnert 2015-09-17 19:11:36 +0200
  • 7f767993c6 Merge branch 'future' into menu_games dehnert 2015-09-17 10:39:04 +0200
  • a8f89c3875 fixed cmake file dehnert 2015-09-17 10:38:55 +0200
  • f1d9e65db7 Merge branch 'future' into menu_games dehnert 2015-09-16 20:59:32 +0200
  • 15b97057dd silenced some warnings within boost (new clang version) and fixed an unused variable issue dehnert 2015-09-16 20:59:19 +0200
  • 75632f932d added state-set abstractor as a means to, e.g., derive the initial states BDD dehnert 2015-09-16 15:16:36 +0200
  • 97c90d5437 added correct insertion of probabilities into BDD and reachability analysis dehnert 2015-09-15 22:25:38 +0200
  • c6f1cb40d3 more work on games dehnert 2015-09-15 18:00:08 +0200
  • 3059711619 Merge branch 'master' into TimParamSysAndSMT and minor stuff TimQu 2015-09-15 15:48:47 +0200
  • 3bc629561e Merge branch 'future' into menu_games dehnert 2015-09-15 14:22:25 +0200
  • 50296571f5 Merge branch 'master' into future dehnert 2015-09-15 14:21:45 +0200
  • deec423f27 fixed infinite recursion in constants comparator dehnert 2015-09-15 14:21:34 +0200
  • 1198951c3e more work on game abstraction of PRISM programs dehnert 2015-09-15 14:10:23 +0200
  • d26f38b9a2 minor stuff, some more pmdp examples and an mdp test case TimQu 2015-09-13 19:24:52 +0200
  • 4bbccd1ec6 Merge branch 'master' into TimParamSysAndSMT TimQu 2015-09-13 16:32:03 +0200
  • adc5c8d1c1 Fixed another memory leak: CheckResults have not been destructed properly. TimQu 2015-09-13 16:31:38 +0200
  • 77e086f446 small fix regarding the return type of computeValue TimQu 2015-09-13 16:12:54 +0200
  • f013ddfb4c The determined relevant predicates are now added to the SMT solver of an abstract command. Also, variable bounds are enforced. dehnert 2015-09-13 00:20:20 +0200
  • f72c30cdff First version of approximation model (with mdp intead of s2pg) TimQu 2015-09-12 14:48:41 +0200
  • c94e9c25a6 Added Mdp Region checking in storm.h, Some STORM_LOG_DEBUGs, fixes for sampling to work on Mdps TimQu 2015-09-12 12:53:28 +0200
  • 78bd4a041a Added Mdp class, sampling might work already (untested) TimQu 2015-09-11 20:54:54 +0200
  • b28f36bb34 work on game-based abstraction dehnert 2015-09-11 18:54:02 +0200
  • 36e8359efa added some useful functions to variable partition dehnert 2015-09-10 22:50:38 +0200
  • fd5e908481 more work on variable partition dehnert 2015-09-10 19:19:05 +0200
  • d4ed882795 more work on menu-game abstraction PRISM programs dehnert 2015-09-10 16:36:18 +0200
  • 312aa0bd8e Merge branch 'master' into future dehnert 2015-09-10 09:22:42 +0200
  • 70dd76c08b Splitted region modelchecker in abstract class and dtmc class (to easily add an mdp class soon) TimQu 2015-09-09 21:11:35 +0200
  • e51a3cfa85 refined cut-off of builders a little. Now, based on the property, more of the states are treated as terminal states of the model dehnert 2015-09-09 18:28:59 +0200
  • e8e77f0dd3 fixed problem with prefix of fresh variables dehnert 2015-09-09 16:56:47 +0200
  • 01f3e0a2cc Merge branch 'future' into python_api sjunges 2015-09-09 15:55:53 +0200
  • e8408cdc7b gurobi 6.05 for mac os support - second try sjunges 2015-09-09 15:41:17 +0200
  • 4425368e0c gurobi 6.05 for mac os support sjunges 2015-09-09 15:40:08 +0200
  • 7db785633b Merge branch 'future' into python_api sjunges 2015-09-09 14:39:37 +0200
  • 3a17477713 change engine in options...(preliminary) sjunges 2015-09-09 14:22:38 +0200
  • c3e390c59a extended api with an option to verify model according to given engine sjunges 2015-09-09 14:20:23 +0200
  • c7f8a653d4 CCache fixed name of option, write info about that in storm-version sjunges 2015-09-09 14:19:49 +0200
  • 559cb67813 updates to the stormpy core sjunges 2015-09-09 13:22:02 +0200
  • dfa201553f Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future sjunges 2015-09-09 13:18:46 +0200
  • 73bfdda6ed missing file sjunges 2015-09-09 13:18:42 +0200
  • ebdd979d2c settings: checks after config file, added finalize sjunges 2015-09-09 12:08:42 +0200
  • 93a0f7f8bb settings: checks after config file, added finalize sjunges 2015-09-09 12:08:42 +0200
  • 0043d3ebf5 changed template argument, used unordered_map TimQu 2015-09-08 17:45:30 +0200
  • ccad5741a7 added test case for game solver dehnert 2015-09-08 17:15:52 +0200
  • e9b5ed52a6 Merge branch 'future' into gamesolver dehnert 2015-09-08 15:36:21 +0200
  • 6a80348150 fixed issue related to row groups in sparse matrix and adapted the affected calling sites dehnert 2015-09-08 15:35:19 +0200
  • cf999006de Merge branch 'future' into python_api sjunges 2015-09-08 14:56:24 +0200
  • 649c928828 further refactored api / shifted some highlevel functionality to cli sjunges 2015-09-08 14:51:37 +0200