Commit Graph

  • bb3e008611 added missing include dehnert 2016-04-18 20:52:28 +0200
  • d5e4eae7cb Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future dehnert 2016-04-18 20:28:49 +0200
  • fa1ac86ff2 fixed evaluation of floor/ceil in expressions dehnert 2016-04-18 20:28:44 +0200
  • 1c907566a4 Merge branch 'future' into menu_games dehnert 2016-04-18 18:48:45 +0200
  • ed92837f2d Merge branch 'cmake' into future dehnert 2016-04-18 18:46:56 +0200
  • 3476df75e8 finally removed log4cplus and affected code parts dehnert 2016-04-18 18:46:47 +0200
  • 5d9f225f9f fixed serious bug in model generation from PRISM code; can't believe that didn't cause wrong models until now dehnert 2016-04-16 17:00:11 +0200
  • 7507175795 Fix some problems with REQUIRED hbruintjes 2016-04-15 19:16:41 +0200
  • 1bb2be74d4 Update CMake files hbruintjes 2016-04-15 18:57:12 +0200
  • e9835a4772 corrected some options dehnert 2016-04-15 16:09:29 +0200
  • b8f08c41c7 adapted the custom dd operations to work again dehnert 2016-04-15 15:20:20 +0200
  • cef8a242ba started to make game-based abstraction work again dehnert 2016-04-15 14:41:12 +0200
  • 06a8e845fb Merge branch 'menu_games' of https://sselab.de/lab9/private/git/storm into menu_games dehnert 2016-04-15 14:34:23 +0200
  • 4f5dfecf36 re-add custom operations to cudd (new version) dehnert 2016-04-15 14:34:17 +0200
  • d1f477c9ba Merge branch 'future' into menu_games dehnert 2016-04-15 14:24:48 +0200
  • 37220cae57 removed two assertions in tests because they no longer apply dehnert 2016-04-15 14:10:52 +0200
  • 60bbce0ba1 added two tests for exploration engine dehnert 2016-04-15 13:56:06 +0200
  • d2b3f90a76 Merge branch 'future' into learning_engine dehnert 2016-04-15 13:30:38 +0200
  • 313edf44e1 added new uniform heuristic and changed probdiff to be the sum instead of product dehnert 2016-04-14 10:58:34 +0200
  • db3d1df863 added a sh*t ton of debug output, didn't help dehnert 2016-04-13 22:53:00 +0200
  • f9193325d4 further refactoring of exploration (better name than 'learning') based engine dehnert 2016-04-13 18:12:52 +0200
  • 6e59988a78 Merge branch 'future' into TimParamSysAndSMT TimQu 2016-04-13 16:26:31 +0200
  • d2d1ebdb1a test didn't compile due to recent changes in carl::rationalize TimQu 2016-04-13 15:59:25 +0200
  • 1424d536ca renamed learning to exploration engine and started on a minor refactoring dehnert 2016-04-12 18:15:30 +0200
  • b657866b12 Merge branch 'future' into menu_games dehnert 2016-04-12 10:49:37 +0200
  • 40b8892f7f removed debug output dehnert 2016-04-11 15:38:41 +0200
  • 03266f563c Merge branch 'future' into learning_engine dehnert 2016-04-11 15:36:35 +0200
  • 07e97e1977 added some statistics and options dehnert 2016-04-11 14:37:46 +0200
  • cffb887c4f add state labeling ThomasH 2016-04-10 01:37:22 +0200
  • 6d421a6fbe learning seems to work find on first larger example dehnert 2016-04-09 17:18:08 +0200
  • f1105aac2a EC-detection appears to work now dehnert 2016-04-08 16:15:05 +0200
  • 19a1c99fd3 Sort failable BEs according to active failure rate Mavo 2016-04-07 17:47:38 +0200
  • a41e5df39f Changed BFS to DFS in Exploration Mavo 2016-04-07 17:06:13 +0200
  • ce91fa7d5b started to work on local EC-detection dehnert 2016-04-07 16:58:48 +0200
  • 10e94d7104 Typo Mavo 2016-04-07 12:58:39 +0200
  • 599a3e99c7 minimal probabilities now working (for some test cases) dehnert 2016-04-07 11:59:34 +0200
  • 8ea869ef14 changed detection of terminal states a bit dehnert 2016-04-06 21:56:25 +0200
  • c2b287a1e1 more work on learning approach dehnert 2016-04-06 16:05:54 +0200
  • 1405cdfc46 debugged the refactoring a bit dehnert 2016-04-05 21:17:18 +0200
  • 5092435329 started refactoring learning model checker dehnert 2016-04-05 18:25:47 +0200
  • 3f06a51869 Added test setting for quick activation/deactivation of test feature Mavo 2016-04-05 16:31:57 +0200
  • 380d3f1897 CTMC constructor with exitRates Mavo 2016-04-05 16:31:12 +0200
  • 7688d7ef42 Fixed test Mavo 2016-04-05 11:39:30 +0200
  • d70317fdb5 Merge from future Mavo 2016-04-05 11:02:47 +0200
  • 62db38813b started to refactor learning engine a bit dehnert 2016-04-04 17:54:45 +0200
  • 2f5f439f26 re-added (naive) splitter selection heuristic dehnert 2016-04-04 17:31:22 +0200
  • ee7ef1deaa Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future sjunges 2016-04-04 15:43:48 +0200
  • c8d9ec5535 update sparse matrix with duplicate row detection within rowgroups sjunges 2016-04-04 15:43:43 +0200
  • e84c2692a5 Merge branch 'future' into learning_engine dehnert 2016-04-04 10:07:46 +0200
  • 38ea181e3d added tons of debug output. all small test models now show sane results dehnert 2016-04-03 20:45:31 +0200
  • c8e39c9797 add gspn model, parser and builder ThomasH 2016-04-03 18:01:56 +0200
  • 8bfb5d9694 add examples ThomasH 2016-04-03 17:58:42 +0200
  • e4a5c1d0d6 more work on EC detection (again0 more work on EC detection (again) dehnert 2016-04-01 16:01:01 +0200
  • 1136ff0d37 fixed a failing test (uninitialized data issue) dehnert 2016-04-01 14:36:00 +0200
  • b06419afe0 working towards EC detection dehnert 2016-03-31 18:28:30 +0200
  • afa72917a6 Merge branch 'future' into TimParamSysAndSMT TimQu 2016-03-31 17:09:03 +0200
  • 67cc067f35 fixed computeSchedulerProbGreater0E. Previously, it did not enforce that psiStates are actually reached. For instance, it was ok to chose a probability 1 selfloop. TimQu 2016-03-31 17:07:52 +0200
  • 5b9491448a removed debug output TimQu 2016-03-31 16:58:13 +0200
  • 9f52d9fa97 first working version (for DTMCs only) dehnert 2016-03-30 21:30:02 +0200
  • 034cf626a0 more work on learning-based engin dehnert 2016-03-30 18:28:49 +0200
  • d802f0d9c6 worked a bit on the learning-based verification of MDPs dehnert 2016-03-29 20:26:37 +0200
  • a63d004fb8 storm-dft is using settings now Mavo 2016-03-23 17:57:50 +0100
  • c9f04ecc0b Added IOSettings Mavo 2016-03-23 15:42:22 +0100
  • effadc5cca Split into general settings and markov chain settings Mavo 2016-03-22 13:31:09 +0100
  • e6ec8d5b60 fixed formula building in some performance tests dehnert 2016-03-21 17:03:55 +0100
  • f48d8bc6b1 Initialize all modules in tests and normal storm Mavo 2016-03-21 15:12:34 +0100
  • 8241df3b0b First step towards settings for multiple binaries Mavo 2016-03-21 14:48:59 +0100
  • 67d77608bd Refactoring of settings Mavo 2016-03-21 14:39:54 +0100
  • fd615289e0 outline of learning algorithm dehnert 2016-03-18 17:28:11 +0100
  • 4bb4e29e43 Added a test case where model checking expected rewards on MDPs currently fails TimQu 2016-03-18 16:47:06 +0100
  • f529a1315f Settings module do not need settings manager Mavo 2016-03-18 15:37:48 +0100
  • 2e9089eca6 Small changes Mavo 2016-03-17 18:12:04 +0100
  • c23eb73129 Cleaned examples Mavo 2016-03-17 17:31:45 +0100
  • 869b0f95d1 Support for pdeps with more than one child Mavo 2016-03-17 17:03:46 +0100
  • 8ed46ce1b8 started on learning-based verification dehnert 2016-03-17 16:57:48 +0100
  • 1fb943b658 moved some internal structs from model builder to their own files to make them reusable dehnert 2016-03-17 16:31:37 +0100
  • ca354cffe4 moved preprocessing of PRISM program to utility to make it accessible from learning-based model checker dehnert 2016-03-17 13:12:24 +0100
  • 2c172cd082 Refactoring Mavo 2016-03-17 11:55:40 +0100
  • 5796da9a5c Refactoring Mavo 2016-03-17 11:28:14 +0100
  • fe7037e7fd Support for POR (priority or) Mavo 2016-03-17 10:47:50 +0100
  • 2df485a144 Merge branch 'future' into learning_engine dehnert 2016-03-16 20:03:58 +0100
  • 7c60e4275d Some more parametric DFT examples Mavo 2016-03-16 18:18:53 +0100
  • bdad8aedd7 Set dependencies to dont care after dependent event has failed Mavo 2016-03-16 16:59:30 +0100
  • dae55eeb29 fixed some bugs and enabled markov automaton model checking from cli dehnert 2016-03-16 16:12:22 +0100
  • ebbc4ce7b4 Fixed compile issues introduced in merge Mavo 2016-03-15 18:09:24 +0100
  • 2be3f17b91 Merge from future (not yet compiling) Mavo 2016-03-15 18:05:59 +0100
  • aac9ba469b Merge branch 'future' into learning_engine dehnert 2016-03-15 16:21:07 +0100
  • 4db05a7c20 Fixed bug with wrong dormancyFactor when copying elements Mavo 2016-03-15 15:50:46 +0100
  • 6b24589966 Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update Mavo 2016-03-15 00:53:15 +0100
  • 472116a374 Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update sjunges 2016-03-15 00:21:15 +0100
  • d688296022 even more modularisation oppurtunaties are now taken sjunges 2016-03-15 00:21:10 +0100
  • 25e2a9c070 Removed assertion Mavo 2016-03-14 23:52:26 +0100
  • 9f3d160677 Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update Mavo 2016-03-14 23:15:31 +0100
  • 2c15c89751 No DC propagation for failed toplevel Mavo 2016-03-14 23:15:07 +0100
  • eeb289bdb8 Merge branch 'monolithic-dft-update' of https://sselab.de/lab9/private/git/storm into monolithic-dft-update sjunges 2016-03-14 20:47:19 +0100
  • e390e1c39d several updates for better modularisation and support for VOT-modularisation sjunges 2016-03-14 20:47:14 +0100
  • e5fd604498 Flag for disabling DC propagation Mavo 2016-03-14 16:42:53 +0100
  • 7dee6d3da2 started on learning-based MDP model checking dehnert 2016-03-14 16:04:07 +0100
  • 6a5f64c9fd resultHint for dtmc model checker TimQu 2016-03-13 18:24:26 +0100
  • ae36933d53 Merge branch 'future' into TimParamSysAndSMT TimQu 2016-03-12 22:03:18 +0100