Commit Graph

  • 9b754177c0 Merge branch 'future' into TimParamSysAndSMT TimQu 2016-03-12 21:16:23 +0100
  • 9ae9700d5c modularisation on and and or sjunges 2016-03-12 20:43:37 +0100
  • db3c40e6d7 Fixed bugs Mavo 2016-03-12 18:46:01 +0100
  • 6ca6ab27e8 Activate failed representatives Mavo 2016-03-12 18:02:30 +0100
  • 5a066b9ae0 Used duplicate variable name Mavo 2016-03-12 15:32:48 +0100
  • 150f177bcd Symred on mcs seems to work now Mavo 2016-03-12 15:13:36 +0100
  • a21715cbc3 Nested symmetries seem to work for at least binary symmetries Mavo 2016-03-12 00:15:47 +0100
  • bb7d8ca3c5 added learning as new engine selection in options dehnert 2016-03-11 19:05:19 +0100
  • adb42b3ac0 fixed minor things related to merge dehnert 2016-03-11 16:37:59 +0100
  • e23a7f854a Merge branch 'future' into next_state_generators dehnert 2016-03-11 16:14:37 +0100
  • 4a19d81133 fixed a few bugs dehnert 2016-03-11 16:13:40 +0100
  • 306eb8a9cc Construct state from bit vector Mavo 2016-03-11 15:13:24 +0100
  • 6a99ab9ef9 expectation/variance now handled in formula parser dehnert 2016-03-11 14:56:02 +0100
  • 51402ec853 removed measure type and only added measure type to reward/time operators dehnert 2016-03-11 14:30:29 +0100
  • 652aeb7562 Fixed compile error with CarlRationalNumber instead of RationalNumber Mavo 2016-03-11 14:01:59 +0100
  • f394808e4a Merge from future with compile errors Mavo 2016-03-11 13:27:25 +0100
  • f86bfdd46f Merge branch 'future' into variance_properties dehnert 2016-03-11 12:03:26 +0100
  • 7e8b790451 Preparation for pseudo state generation from bit vector Mavo 2016-03-11 11:49:53 +0100
  • 39acf24448 fix for weak bisimulation on CTMCs dehnert 2016-03-11 11:46:21 +0100
  • a2a3a734a6 First version of symmetry for shared spares. Still some problems in contrast to Dortmund which had absolutely no problems with Tottenham. Mavo 2016-03-11 00:04:19 +0100
  • 016ab53f42 making the logic formulas better dehnert 2016-03-10 16:59:38 +0100
  • 4284c633f4 StateGenerationInfo does not use DFS for symmetries Mavo 2016-03-10 16:56:28 +0100
  • 5e1e5b55a1 renamed expected time formulas to time formulas dehnert 2016-03-10 13:06:50 +0100
  • 9cda76c675 Merge branch 'future' into variance_properties dehnert 2016-03-10 11:37:25 +0100
  • 6e8602413e ModelInstantiator + test TimQu 2016-03-09 13:29:42 +0100
  • 69c5ba604e Helper functions for parametric stuff TimQu 2016-03-09 13:29:26 +0100
  • a3aededd3a public access to model ingredients: RewardModel and exitRates TimQu 2016-03-09 13:28:50 +0100
  • 45e59848a9 first steps dehnert 2016-03-08 17:01:17 +0100
  • 811d04c2a7 Fixed bug in BitVector Mavo 2016-03-08 13:29:31 +0100
  • f54c2fb8e7 tests passing again dehnert 2016-03-08 10:00:17 +0100
  • a40d12f915 made getRowGroup more consistent and fixed some introduced bugs dehnert 2016-03-08 08:48:41 +0100
  • 0b98412bb4 further work on making row-grouping optional dehnert 2016-03-07 22:45:42 +0100
  • f285858e28 added required includes TimQu 2016-03-07 20:30:12 +0100
  • 83b6496fd2 Fixed bugs in BitVector Mavo 2016-03-07 17:25:20 +0100
  • f81ce1cac1 started making row grouping optional dehnert 2016-03-07 16:07:40 +0100
  • ccec8b8f7a Renaming Mavo 2016-03-07 13:45:53 +0100
  • 1f5439e270 added state labeling generator interface dehnert 2016-03-06 20:08:53 +0100
  • 796d7652df Fixed problem with bounds in MA model checker Mavo 2016-03-03 18:49:00 +0100
  • 3f41aa55f8 Cleaned up debug output Mavo 2016-03-03 14:57:51 +0100
  • 1dd2a5c808 Merge branch 'future' into next_state_generators dehnert 2016-03-03 11:35:31 +0100
  • 28a49659db Small fixes Mavo 2016-03-02 17:36:56 +0100
  • 43579babd6 Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft sjunges 2016-03-02 17:14:55 +0100
  • f12e02f8ff dont modularise modules sjunges 2016-03-02 17:14:50 +0100
  • 8e0e838435 Merging the rewriting Mavo 2016-03-02 16:28:02 +0100
  • 52573c90ca Copy DFT Mavo 2016-03-02 16:10:47 +0100
  • a6f8ba3716 seq examples sjunges 2016-03-02 15:30:22 +0100
  • e322c56820 findModularisationRewrite sjunges 2016-03-02 15:30:00 +0100
  • 1e79e5b2a4 Only print debug matrix for small state sizes Mavo 2016-03-02 15:24:29 +0100
  • 174058bb5e Do not destroy the universe by dividing by 0 Mavo 2016-03-02 11:53:41 +0100
  • b8c7f063c1 Maybe fix try to fix bisimulation instead of deactivating Mavo 2016-03-02 00:36:15 +0100
  • c45812c66a made bfs the default exploration order again dehnert 2016-03-01 19:22:08 +0100
  • b75b5f1928 No bisimulation for parametric case Mavo 2016-03-01 17:31:52 +0100
  • 7b7b999548 Bisimulation for small models as well Mavo 2016-03-01 16:44:34 +0100
  • cc2eb383c9 Merge Mavo 2016-03-01 13:29:51 +0100
  • c05e671111 Handling of min and max for non-determinism Mavo 2016-03-01 13:28:38 +0100
  • 4c2b1d7c22 Model info for benchmarking scripts Mavo 2016-03-01 13:22:43 +0100
  • 37a86d8190 Compile fixes for gcc Mavo 2016-03-01 13:22:14 +0100
  • e4c2702889 Fixed problem in MaximalEndComponents Mavo 2016-03-01 12:18:01 +0100
  • f8b9ece2fd Added mini test for BitVector Mavo 2016-03-01 10:21:55 +0100
  • 7f4fa27008 Initialize closed for MA Mavo 2016-03-01 10:21:21 +0100
  • ffe63ea95d made dfs as exploration order available dehnert 2016-02-29 22:10:30 +0100
  • 9b8dd018cf Fixed problem with gate as trigger events for dependencies Mavo 2016-02-29 19:08:32 +0100
  • ba26f983a9 Merge from future Mavo 2016-02-29 18:57:18 +0100
  • 55fd1b66c3 introducing exploration orders to explicit builder dehnert 2016-02-29 16:06:01 +0100
  • f935f502dd Activate pCTMCs for storm Mavo 2016-02-29 15:49:33 +0100
  • 9d97750ca5 Improved compareAndSwap on BitVector Mavo 2016-02-29 10:59:16 +0100
  • b74cd564e4 some further changes sjunges 2016-02-29 10:38:08 +0100
  • 0dfdfe7db8 using flat_map in model building instead of unordered_map dehnert 2016-02-27 16:25:19 +0100
  • fff7b2d5db fixed an allocation issue, performance is now roughly the same as before but memory consumption is reduced dehnert 2016-02-26 19:51:41 +0100
  • 63d2faf1ed DFTIsomorphism now runs in the presence of SEQs sjunges 2016-02-26 18:54:48 +0100
  • f562a84316 getRestriction added to DFT interface sjunges 2016-02-26 18:54:20 +0100
  • a6c087f461 Dont Care Propagation and SEQ are now sound (but more DCs can be propagated with some care) sjunges 2016-02-26 17:50:51 +0100
  • fad28df7d6 first working version of next-state generator for PRISM models dehnert 2016-02-26 17:34:38 +0100
  • c6098e6a6a post and pre SEQ elements for state space generation sjunges 2016-02-26 16:49:44 +0100
  • ed65140911 add missing file sjunges 2016-02-26 16:49:18 +0100
  • a204ac3a66 added a comment sjunges 2016-02-26 16:31:00 +0100
  • 6e777e88d1 fixed warning for restriction sjunges 2016-02-26 14:51:03 +0100
  • 2a41579476 refactored source file for elements sjunges 2016-02-26 14:50:46 +0100
  • 11b29cfd87 splitted elements into single headers sjunges 2016-02-26 14:33:23 +0100
  • 9802fac0ed merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft sjunges 2016-02-26 13:37:32 +0100
  • 73c88a4faf update on restrictions sjunges 2016-02-26 13:37:27 +0100
  • e9b4f06972 Better assertions in BitVector Mavo 2016-02-26 13:05:16 +0100
  • f6374c60f8 Bitte ein Bit Mavo 2016-02-26 11:25:50 +0100
  • 27b57f055e Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft sjunges 2016-02-26 10:59:47 +0100
  • 4a1f7468f5 param result file now has a semicolon between parameters sjunges 2016-02-25 18:55:48 +0100
  • 9eec5b140c refactoring of model builder dehnert 2016-02-25 18:27:23 +0100
  • edded0f8b7 Merge from future Mavo 2016-02-25 16:53:07 +0100
  • da0dafe5be ModelInstantiator!!!!11 Also: some refactoring TimQu 2016-02-25 16:29:02 +0100
  • c007c8e699 add sylvan to the resources target sjunges 2016-02-25 15:40:29 +0100
  • 9506f4f420 Merge branch 'future' into next_state_generators dehnert 2016-02-25 15:24:21 +0100
  • fde7b71933 Nice printing when no logging framework is enabled sjunges 2016-02-25 15:20:06 +0100
  • 9c30394b33 Finalize sparse for failed, failsafe, dontcare Mavo 2016-02-25 14:59:27 +0100
  • 8c2cb4887f Cmake option to disable debug and trace outputs sjunges 2016-02-25 13:49:36 +0100
  • 6818c6dc0d Fixed tests when no log4plus is available. sjunges 2016-02-25 13:44:58 +0100
  • fcd98793ee fixed supp for log4cplus sjunges 2016-02-25 11:44:02 +0100
  • cf986311ad loglevel can be set now and all logging macros support streaming sjunges 2016-02-24 22:53:13 +0100
  • abac11ab50 sylvan build stuff in 3rd party folder now sjunges 2016-02-24 22:52:36 +0100
  • e0379b9c50 Log CUDD build process sjunges 2016-02-24 22:25:15 +0100
  • e0980de0ba first version of storm without log4cplus as a dependency sjunges 2016-02-24 19:14:33 +0100
  • a75e0f5323 more work wrt cleaner model exploration dehnert 2016-02-24 18:58:25 +0100