Commit Graph

  • e4817759df policy iteration based weight vector checker TimQu 2018-06-22 15:04:33 +0200
  • aece3020f6 improved functionality of the scheduler evaluator TimQu 2018-06-22 15:04:07 +0200
  • dfc0141894 minor fix to Z3 API modification dehnert 2018-06-22 13:25:21 +0200
  • cdfa328464 first attempt at adapting to Z3 interface change dehnert 2018-06-22 10:57:52 +0200
  • bf973187c4 use deterministicParetoExplorer in case there is a scheduler restriction. TimQu 2018-06-21 17:32:20 +0200
  • a638104adb using new post processing class for the 'old' implementation. TimQu 2018-06-21 17:30:34 +0200
  • 80a66603fb added possibility to compute the 'downward closure' of a polytope only with respect to a set of dimensions TimQu 2018-06-21 17:29:19 +0200
  • 136084af75 started implementing deterministic scheduler finding approach for multi-objective model checking TimQu 2018-06-21 17:28:40 +0200
  • 1f221db280 Disable transformation of DFT properties to JANI Matthias Volk 2018-06-21 13:39:36 +0200
  • eea940b625 Refactoring for transformation DFT->GSPN->JANI Matthias Volk 2018-06-21 13:36:08 +0200
  • 4134630fa6 adding gap output dehnert 2018-06-20 15:40:05 +0200
  • 758382e020 Merge remote-tracking branch 'origin/dft_gspn' into dft_gspn Alexander Bork 2018-06-14 18:44:22 +0200
  • a49f88b7f5 Fixed computation of priorities to correctly represent the semantics Alexander Bork 2018-06-14 18:44:01 +0200
  • 4f4d1f4423 do not scale precision dehnert 2018-06-14 14:19:13 +0200
  • a6e6d5993f Travis: set unlimited clone depth to allow versioning with git describe Matthias Volk 2018-06-13 16:37:45 +0200
  • 0d4cf67f2e Set mergeDC from setting Matthias Volk 2018-06-12 16:57:47 +0200
  • cf316df35e Added settings for DFT-GSPN transformation Matthias Volk 2018-06-12 16:56:27 +0200
  • afb0be1245 Fixed missing dependencies to storm-parsers Matthias Volk 2018-06-12 15:08:14 +0200
  • 9e398ffaab Minor improvements for some CMake output Matthias Volk 2018-06-12 15:07:42 +0200
  • 386f0b2e47 fixing bug in scheduler improvement step of policy iteration for games dehnert 2018-06-12 12:08:41 +0200
  • 369cea775d Swapped order in PriorityQueue to propagate failures in correct order Matthias Volk 2018-06-11 22:12:49 +0200
  • 8478352030 dynamic constraints and minimality labels sjunges 2018-06-10 23:00:12 +0200
  • 2aff2e9382 adding some more timing output dehnert 2018-06-10 22:00:22 +0200
  • 53238f43f7 fixed some missing includes due to updated API sjunges 2018-06-10 21:01:38 +0200
  • 39698d6ecb fix install of storm-counterexamples sjunges 2018-06-10 21:01:14 +0200
  • 79bb6734ed compile and link parsers in seperate binary sjunges 2018-06-10 20:20:39 +0200
  • 3a704ae532 fix storm-dft missing includes sjunges 2018-06-10 18:51:25 +0200
  • 6dfce6a405 extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times sjunges 2018-06-10 18:50:56 +0200
  • b0047a5a96 improving choices in game policy iteration depending on precision of underlying solver dehnert 2018-06-10 14:06:58 +0200
  • 6fcc91b9d0 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm sjunges 2018-06-10 12:24:17 +0200
  • d1ab260068 remove outdated parts in highlevel counterexamplse Sebastian Junges 2018-06-10 12:22:34 +0200
  • e29e6c7cd2 high level counterexamples extended with more options, and improved performance when minimizing over a subset Sebastian Junges 2018-06-10 12:20:40 +0200
  • ade4b5bf72 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm sjunges 2018-06-09 22:57:03 +0200
  • 48f5608157 making policy iteration available for game-based abstraction (prototypical for now) dehnert 2018-06-09 21:59:06 +0200
  • b6d67e7995 properties.cpp: Output warning if we filter away all properties Joachim Klein 2018-06-08 16:59:03 +0200
  • 2948611f3f cli.cpp: Quote arguments in "Command line arguments" status line Joachim Klein 2018-06-08 16:54:20 +0200
  • 04a1bbedfc properties.cpp: Log filename of properties file in --verbose mode Joachim Klein 2018-06-08 12:34:43 +0200
  • 30a95ef9d6 Simplify check whether argument of --prop is a file/property Joachim Klein 2018-06-08 11:28:38 +0200
  • 9b80c65d72 more and more debugging dehnert 2018-06-08 16:38:38 +0200
  • fa43e515ee Changed DFT element transformation so priorities are used Alexander Bork 2018-06-07 23:21:45 +0200
  • 135c38777f game-based abstraction working with rational numbers dehnert 2018-06-07 22:53:41 +0200
  • 14724b529f further debugging dehnert 2018-06-07 16:45:15 +0200
  • 9f72f67d9f adding precision to less/greater in vector reduction, adding export to json dehnert 2018-06-06 22:44:23 +0200
  • 480b1fb8e5 Added priorities to GSPN transformation Matthias Volk 2018-06-06 18:02:17 +0200
  • a2c990ea58 Travis: changed mail address for notifications Matthias Volk 2018-06-06 16:50:44 +0200
  • 09876f6808 lots of debug output dehnert 2018-06-06 16:46:01 +0200
  • 1461ba9073 Fixed SMT encoding of voting gate Matthias Volk 2018-06-05 22:49:58 +0200
  • 5c7e63ee9a Merge branch 'master' into gamebased dehnert 2018-06-05 22:34:49 +0200
  • 6f320090eb fixing bug where illegal choices were copied over dehnert 2018-06-05 11:36:23 +0200
  • a2d8faece0 Fixed layout for PDEP GSPN template and added Don't Care support for SPARE elements Alexander Bork 2018-06-04 22:28:22 +0200
  • 1318bea87a adding support for manually injecting groups of refinement predicates dehnert 2018-06-01 23:03:34 +0200
  • 2c82f6554c fixing statistics dehnert 2018-06-01 22:05:14 +0200
  • c6e28a3bc7 adding setup timer dehnert 2018-06-01 20:29:18 +0200
  • 918dc349fb Multi-objective tests now set the method via the environment TimQu 2018-06-01 13:56:14 +0200
  • 7cee81a223 adapt multi-objective model checking components to new preprocessing TimQu 2018-06-01 13:55:40 +0200
  • 4c0bda2664 better modularity for multi-objective preprocessing TimQu 2018-06-01 13:54:29 +0200
  • 41b494edd3 fixing bug due to too few variables being reserved dehnert 2018-06-01 08:57:11 +0200
  • fa14b993e4 fixing valid block abstractor dehnert 2018-06-01 08:37:12 +0200
  • eaf01ab443 bugfix dehnert 2018-05-31 22:18:54 +0200
  • ba3ec0da27 lifted all new stuff to JANI menu game abstractor dehnert 2018-05-31 20:39:15 +0200
  • 4a0134797c option to add initial predicates dehnert 2018-05-31 17:08:40 +0200
  • e216d55320 extended strategy redirection, better statistics dehnert 2018-05-31 16:47:45 +0200
  • 8f4f5c555e explicit Dijkstra search for pivot state now follows the strategies separately dehnert 2018-05-31 12:26:51 +0200
  • 09797dae5a SMT encoding for SEQ gate Matthias Volk 2018-05-30 17:17:31 +0200
  • bcd3d68c61 further debugging dehnert 2018-05-30 16:32:39 +0200
  • c5e356bc40 Proper installation of Storm Matthias Volk 2018-05-29 16:50:30 +0200
  • 99e5619952 Export storm targets Matthias Volk 2018-05-28 17:33:05 +0200
  • 1e4b81812c Environment does no longer require that unused setting modules still have to be registered. TimQu 2018-05-29 16:47:39 +0200
  • ed56a77d79 started on fixing strategies dehnert 2018-05-29 16:43:22 +0200
  • 769fd4332c further debugging of game-based abstraction dehnert 2018-05-29 15:17:30 +0200
  • e4561a70e5 added scheduler restriction setting TimQu 2018-05-29 12:49:26 +0200
  • 8a6bd4d72f Added dependency don't care support Alexander Bork 2018-05-28 23:07:05 +0200
  • 57ad89adea Added dependency don't care support Alexander Bork 2018-05-28 23:06:14 +0200
  • e780572560 changing command decomposition of game-based abstraction and further debugging dehnert 2018-05-28 21:38:17 +0200
  • fa8e8749e6 scheduler restriction in multiobjective model checking environment TimQu 2018-05-28 16:53:03 +0200
  • 5750584042 schedulerClass compiles now... TimQu 2018-05-28 16:52:43 +0200
  • 7ef779a8a6 fixing one bug in abstraction using decomposition, started tracking down more dehnert 2018-05-28 16:38:59 +0200
  • b363a09025 Revert "added schedulerrestriction in checktask" TimQu 2018-05-28 15:53:57 +0200
  • a91449f5c6 Merge branch 'master' into deterministicScheds TimQu 2018-05-28 15:50:23 +0200
  • 5c38a4ef89 implemented environment for multiobjective settings TimQu 2018-05-28 15:42:59 +0200
  • 159ec044f6 added schedulerrestriction in checktask TimQu 2018-05-28 11:21:13 +0200
  • f98bd69120 schedulerClass class TimQu 2018-05-28 11:20:52 +0200
  • 8c96548566 more work on game-based abstraction dehnert 2018-05-27 22:54:54 +0200
  • cfb1bc36ce treating bounded JANI variables with single bound dehnert 2018-05-25 12:19:04 +0200
  • 07fe1a240e fixing superfluous reverse dehnert 2018-05-25 10:52:55 +0200
  • 8503dfff87 fixing issue related to unary minus in JANI dehnert 2018-05-24 14:52:31 +0200
  • e9a815666f printing new predicates in verbose mode dehnert 2018-05-24 14:10:09 +0200
  • 138c61c9e5 some more output dehnert 2018-05-24 14:09:18 +0200
  • 1a46300f61 adding relative precision to comparator and game-based abstraction dehnert 2018-05-24 12:55:41 +0200
  • e1bb35ca0f fix for the generator matrix fix dehnert 2018-05-23 15:29:37 +0200
  • 62e493d978 fix computation of generator matrix, pointed out by jklein dehnert 2018-05-23 15:27:26 +0200
  • ca651ec61c fixes github issue #24 related to MEC decomposition dehnert 2018-05-23 13:03:14 +0200
  • 03707f0234 first step for fixing MEC decomposition: making SCC decomposition accept a bit vector of subsystem choices dehnert 2018-05-22 21:49:39 +0200
  • 94a5a3da7c remove ffast-math dehnert 2018-05-22 21:00:00 +0200
  • 9e0d88e212 overhauled output slightly dehnert 2018-05-20 21:52:44 +0200
  • f9d23873f1 fixed minor bug in game-based abstraction dehnert 2018-05-20 20:52:51 +0200
  • 7d8e9aa5d4 adding more output infos for game-based dehnert 2018-05-19 08:30:25 +0200
  • 08dd8f7b7c some fixes to make gcc happy dehnert 2018-05-18 16:33:28 +0200
  • f1c2cf985a turned some debug output in game-based model checker to regular (verbose) output dehnert 2018-05-18 16:32:12 +0200
  • 77179c02ac added option to feed additional constraints to abstraction dehnert 2018-05-18 15:01:29 +0200