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

Commit Graph

  • 0a68d8afa2 fixed out-of-bounds access in symbolic to explicit conversion of game-based abstraction dehnert 2018-03-29 09:44:58 +0200
  • cbc7246885 min/max sparse game solving alpha version in game-based abstraction dehnert 2018-03-29 09:35:03 +0200
  • c3e66f2dec more work on solving the abstractions explicitly dehnert 2018-03-28 22:34:27 +0200
  • 25853f08f1 fixed newly introduced issues with more restrictive choice updates dehnert 2018-03-28 18:57:17 +0200
  • 0534216a85 preparations for scheduler extraction support Sebastian Junges 2018-03-28 17:14:36 +0200
  • 5159afc348 further work towards proper scheduler extraction for games dehnert 2018-03-28 16:45:03 +0200
  • e205b1bf6a check task API slightly extended for scheduler extraction Sebastian Junges 2018-03-28 15:36:13 +0200
  • a49b52f93e Merge remote-tracking branch 'origin' into gamebased dehnert 2018-03-28 14:03:00 +0200
  • 0725b5e590 changes to tracking values in mult-and-reduce functions of matrix dehnert 2018-03-28 14:02:49 +0200
  • 3952b47d1b fix some compile issues dehnert 2018-03-28 11:03:12 +0200
  • d557ef1075 started to make game solver flexible enough to also solve the (explicit) games of game-based abstraction dehnert 2018-03-27 22:21:02 +0200
  • d3bbe4df10 explicit interpolation and started on explicit quantitative solution dehnert 2018-03-27 16:44:19 +0200
  • c2e646b887 working towards predicate synthesis from explicit (qualitative) result for game-based abstraction dehnert 2018-03-26 22:30:36 +0200
  • c6a5d5a74d started on refining menu games based on explicit results dehnert 2018-03-26 16:42:15 +0200
  • 6fa88b1c14 Disable unnecessary output for DFT model checking Matthias Volk 2018-03-26 11:14:00 +0200
  • a03f9c80d2 Updated README Matthias Volk 2018-03-26 11:13:01 +0200
  • 3f6a8fed92 fixed some issues in qualitative sparse solution of game-based abstraction dehnert 2018-03-25 21:58:19 +0200
  • 9665f4fa30 sparse qualitative solving of menu games dehnert 2018-03-25 20:55:43 +0200
  • edbe3b1952 more work on explicit game solving dehnert 2018-03-24 22:10:38 +0100
  • 51e08bb1a5 removed old inPlaceMultiplier TimQu 2018-03-23 09:31:03 +0100
  • cedae194e3 towards labeling generation in dd to sparse conversion dehnert 2018-03-22 19:15:27 +0100
  • 733bec60bd started on hybrid solution of abstraction dehnert 2018-03-22 16:46:19 +0100
  • efbd899e46 update to game-based abstraction refinement dehnert 2018-03-22 14:29:11 +0100
  • b4d8c209cd optimizations for game-based abstraction refinement dehnert 2018-03-21 21:54:24 +0100
  • c35b446926 Updated CHANGELOG Matthias Volk 2018-03-21 17:16:01 +0100
  • b998b3abf9 Cleanup Matthias Volk 2018-03-21 17:15:05 +0100
  • cf478b2984 Updated README Matthias Volk 2018-03-21 17:11:39 +0100
  • 94ad73e510 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2018-03-21 16:51:26 +0100
  • 31fa43ab27 some fixes to interpolation in game-based abstraction refinement dehnert 2018-03-21 16:38:23 +0100
  • 4bdedfbb9a Added missing settings Matthias Volk 2018-03-21 16:06:08 +0100
  • a04ca743f7 Merge from master Matthias Volk 2018-03-21 15:59:07 +0100
  • d9db3f84b6 Fixed dft tests Matthias Volk 2018-03-21 13:43:35 +0100
  • 172c5f3657 Making things compile again... TimQu 2018-03-21 11:42:12 +0100
  • 263e6ed5f8 Removed generated files from git Matthias Volk 2018-03-21 11:23:38 +0100
  • df1571d737 Added more DFT tests Matthias Volk 2018-03-21 11:17:34 +0100
  • efcb718851 removed the --forcebounds setting TimQu 2018-03-20 18:39:02 +0100
  • 94fb16e654 svi now considers bounds by default TimQu 2018-03-20 18:38:40 +0100
  • 3310f51857 allowed for more fine grained solver requirements TimQu 2018-03-20 18:12:14 +0100
  • 415e22743d Moved same parts of the dft api into cpp file Matthias Volk 2018-03-20 18:01:35 +0100
  • 853901af45 Introduced api dir in storm-gspn Matthias Volk 2018-03-20 15:07:31 +0100
  • 48a0b88cd0 Fixed linking issues with duplicate symbols Matthias Volk 2018-03-20 15:05:45 +0100
  • ca8608db5c Use different configurations in DFT tests Matthias Volk 2018-03-20 13:54:53 +0100
  • 9559a96fd7 Travis: allow failure of LTO config Matthias Volk 2018-03-19 16:53:25 +0100
  • 752a1fff86 Use pars settings for pars tests Matthias Volk 2018-03-19 14:10:16 +0100
  • 2c9f6294a4 Started on DFT regression tests Matthias Volk 2018-03-16 18:51:24 +0100
  • 6821d3c76c Different function for exact and approximate DFT analysis Matthias Volk 2018-03-16 18:06:05 +0100
  • c8c0b73e7a Removed duplicated test Matthias Volk 2018-03-16 14:36:36 +0100
  • 95c19de197 Added missing multiplier settings to storm-pars Matthias Volk 2018-03-16 14:19:44 +0100
  • 480894f1b6 Added missing topological settings to storm-pars Matthias Volk 2018-03-16 14:14:30 +0100
  • fc43d3f506 Added a return type to some lambda expressions as this apparently caused trouble when using gmp numbers TimQu 2018-03-14 19:53:25 +0100
  • 40285bac26 handled early termination in svi more carefully TimQu 2018-03-14 17:35:06 +0100
  • 3cd1edb378 added virtual destructors to multipliers TimQu 2018-03-14 17:34:27 +0100
  • 316412c5d3 fixed a bug related to closing symbolic Markov automata dehnert 2018-03-14 10:46:06 +0100
  • 09866e4577 enabling changing value type in quotient extraction of dd-bisimulation dehnert 2018-03-13 21:44:49 +0100
  • 5f7cd17789 added printing info when value type is converted after preprocessing dehnert 2018-03-13 19:42:56 +0100
  • ded1040d04 added missing template instantiations TimQu 2018-03-13 17:08:37 +0100
  • 12f8685080 Custom Termination Conditions for sound value iteration TimQu 2018-03-13 15:55:51 +0100
  • 8b00f8441e Improved caching for svi TimQu 2018-03-13 14:10:30 +0100
  • be6d4f9854 renamed 'sound power' to 'sound value iteration' TimQu 2018-03-13 13:46:50 +0100
  • a24de86ce1 Avoided duplicated code for sound value iteration TimQu 2018-03-13 13:41:12 +0100
  • 3beff87636 Try to fix LTO issue by adding virtual destructor Matthias Volk 2018-03-12 09:14:24 +0100
  • ec5a947d56 Enable LTO for gcc >= 7.0 again Matthias Volk 2018-03-11 22:48:15 +0100
  • b3c2d8bbd8 added option to not include dynamic constraints in maxsat counterexample generation dehnert 2018-03-09 10:35:14 +0100
  • de2e94cac7 polished unifplus code a bit and made it the default MA (bounded reachability) solution method dehnert 2018-03-06 21:27:09 +0100
  • 19070a27a9 added 'fixed ring' pattern TimQu 2018-03-06 18:14:21 +0100
  • 0026c73096 Use strong bisim instead of weak bisim Sebastian Junges 2018-03-06 17:13:03 +0100
  • 3c04ed2e8d Merge branch 'master' into unifplus dehnert 2018-03-06 16:46:18 +0100
  • 7150354b9d fixing issue related to vector swapping in (explicit) value iteration and power method dehnert 2018-03-06 14:32:41 +0100
  • 51ebb47587 added timing measurements to symbolic to sparse conversion in hybrid model checkers dehnert 2018-03-05 12:08:44 +0100
  • 67519ff5f6 Merge branch 'pomdp_datastructures' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into pomdp_datastructures Sebastian Junges 2018-03-04 20:55:42 +0100
  • 139752eb66 added option to perform dd-bisimulation using exact arithmetic dehnert 2018-03-04 20:53:17 +0100
  • 2e15674580 fixed an issue in state-act reward refinement for nondet models dehnert 2018-03-04 14:55:23 +0100
  • 207b608e20 using sylvan way of computing cache/table sizes given a memory bound dehnert 2018-03-03 16:13:49 +0100
  • 77a031aaeb changed encoding of spirit parser, fixed an issue in variable information related to how many bits are necessary to store the state, changed some output formatting dehnert 2018-03-03 10:46:51 +0100
  • fdc2f2bd0c removed wrong include to make it compile again dehnert 2018-03-02 18:32:16 +0100
  • d06c2c791a introducing pomdp memory patterns TimQu 2018-03-02 16:22:29 +0100
  • acf297a811 fixing precision issue in sanity check and silencing min-max solver a bit dehnert 2018-03-02 15:12:31 +0100
  • 4ec07926d1 Merge remote-tracking branch 'origin/master' TimQu 2018-03-02 14:24:34 +0100
  • ea21aca117 second attempt at fixing issue when not reusing blocks dehnert 2018-03-02 13:34:19 +0100
  • 6638984b8e fixed an issue in sylvan refiner when not reusing block numbers dehnert 2018-03-02 12:56:13 +0100
  • f87b6875ed Merge remote-tracking branch 'origin/master' TimQu 2018-03-02 11:48:39 +0100
  • d6f2261ca9 enable representatives in quotient extraction also for MDP/MA dehnert 2018-03-02 10:26:32 +0100
  • 831686c076 Merge remote-tracking branch 'origin/master' into pomdp_datastructures TimQu 2018-03-02 09:23:51 +0100
  • 24382630dc removed output of performed iterations to cout TimQu 2018-03-02 09:19:49 +0100
  • 38959ccf0a Merge branch 'sound-vi' TimQu 2018-03-02 09:16:35 +0100
  • f6c504214a Merge remote-tracking branch 'origin/master' into sound-vi TimQu 2018-03-02 09:16:02 +0100
  • 66e08f9cd7 more time output in dd-based bisimulation dehnert 2018-03-02 09:05:01 +0100
  • 34b6593ed8 overhauled output of dd-based bisimulation for benchmarking dehnert 2018-03-01 22:09:06 +0100
  • c1ecc22303 new multiplyRow method for sound vi TimQu 2018-03-01 19:58:42 +0100
  • ff18956fbb reverted back to old native multiplier TimQu 2018-03-01 19:57:09 +0100
  • e491dc3813 fixed usage of multiplyrow TimQu 2018-03-01 17:54:00 +0100
  • 4eb187ba4f Added a new native multiplier TimQu 2018-03-01 17:53:44 +0100
  • 48945d1199 improved multiplyRow method TimQu 2018-03-01 14:29:19 +0100
  • 65676235bb fixed selection options for native equation solver method TimQu 2018-03-01 12:52:54 +0100
  • 1b6200e4eb added missing includes TimQu 2018-03-01 12:50:06 +0100
  • 51884895c8 Removed linear equation solver factories in model checkers TimQu 2018-03-01 10:28:04 +0100
  • ba96fde3c9 fixed sum that was too much nested TimQu 2018-03-01 10:27:11 +0100
  • 24cca08ccf disabling LTO for gcc >= 7 dehnert 2018-03-01 09:28:18 +0100
  • 4690ac1faf Adding MultiplierTest TimQu 2018-02-28 16:57:16 +0100
  • 69a27ddad6 fixed compiling storm-pars TimQu 2018-02-28 16:28:38 +0100