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

Commit Graph

  • 8ba365fee9 Fixed includes after moving files Matthias Volk 2017-11-03 15:58:04 +0100
  • ac759d2671 minor performance improvements to model building dehnert 2017-11-03 14:06:39 +0100
  • 6501fffac3 several optimizations related to explicit model building dehnert 2017-11-03 11:14:05 +0100
  • 12dda40919 split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs sjunges 2017-11-03 00:20:18 +0100
  • 8116b360ba changed hash function of bit vector hash map dehnert 2017-11-02 18:30:22 +0100
  • 183eea7a89 more work on abstraction refinement framework dehnert 2017-11-02 16:35:44 +0100
  • 3a11914da0 commit to switch workplace dehnert 2017-11-02 16:32:40 +0100
  • f772af6241 fixed bug in bit vector hash map dehnert 2017-11-02 14:12:46 +0100
  • 29903bef04 more work on general abstraction refinement framework dehnert 2017-11-02 08:28:24 +0100
  • db7d058800 converted some assertions into exceptions in bit vector hash map dehnert 2017-11-01 19:22:40 +0100
  • b99bc59215 adding some primes dehnert 2017-10-31 14:05:01 +0100
  • 41bc2c0de4 explicit instantiations to make gcc hapy dehnert 2017-10-31 12:46:02 +0100
  • 374f7e1fbb kSP: disallow access to index 0 (1-based indices!) Tom Janson 2017-10-30 17:02:37 +0100
  • 2682100cfd fixed more tests TimQu 2017-10-29 20:17:50 +0100
  • 48dc03846e extended partial bisimulation model checker by games as quotients dehnert 2017-10-29 13:45:25 +0100
  • aa1d9a6f85 Revert "intermediate commit to switch workplace" dehnert 2017-10-27 19:23:50 +0200
  • 90cb987357 intermediate commit to switch workplace dehnert 2017-10-27 16:18:16 +0200
  • 419fcd1b43 Fixed test TimQu 2017-10-27 16:01:52 +0200
  • c9beea4f33 better lower/upper result bounds TimQu 2017-10-27 15:42:45 +0200
  • 746a58ff12 better statistics output TimQu 2017-10-27 14:23:40 +0200
  • 86253fe88a moved multidimensional unfolding implementation from multiobjective into helper namespace TimQu 2017-10-27 13:24:59 +0200
  • 17d6835477 removed acyclic minmax method as it is not much better then gauss-seidel style multiplications TimQu 2017-10-27 12:54:54 +0200
  • d85a845b7d Fixed cases where a solver guarantee was not established although it was needed by the termination condition TimQu 2017-10-27 12:47:28 +0200
  • 117d1b5c99 clean up single objective reward bounded case TimQu 2017-10-27 11:01:30 +0200
  • c4c6c9cbce Test compiler configurations within cmake Matthias Volk 2017-10-26 22:22:08 +0200
  • 5fd7878791 added option to refine over states whose signatures changed in dd-based bisimulation dehnert 2017-10-26 16:09:24 +0200
  • 016fedd58e Better progress info TimQu 2017-10-26 14:50:24 +0200
  • 199d12a2c2 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective TimQu 2017-10-26 11:11:00 +0200
  • f2d837dc42 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective TimQu 2017-10-26 11:10:36 +0200
  • 518773f18f commit missing version file dehnert 2017-10-26 09:53:14 +0200
  • e6f61fb441 fixed bug in hybrid engine when using interval iteration dehnert 2017-10-26 09:32:42 +0200
  • 9859f60db0 Fixed solver tests TimQu 2017-10-25 20:27:14 +0200
  • f44ce8801c "fixed" the tests that failed because of unsound value iteration TimQu 2017-10-25 20:14:06 +0200
  • 3571f0ddca Respected that the solution is unique when doing value iteration TimQu 2017-10-25 19:48:17 +0200
  • 33585c811f MinMax Solver requirements now respect whether the solution is known to be unique or not. TimQu 2017-10-25 17:51:36 +0200
  • 7dcb450aad started on computing changed states in one shot dehnert 2017-10-25 16:35:48 +0200
  • c85e30dfd0 added distance-aware initial partition to dd-based bisimulation dehnert 2017-10-25 15:35:20 +0200
  • 9498705c95 more reuse of values in bisimulation-based abstraction refinement dehnert 2017-10-24 22:13:59 +0200
  • 4fad33b5e8 started on optimizing bisimulation-based abstraction-refinement dehnert 2017-10-24 16:59:36 +0200
  • 669940ccd3 only supporting reuse of nothing or of block numbers dehnert 2017-10-23 16:21:29 +0200
  • 4e4526182f adding information about which technique is used to symbolic native linear equation solver dehnert 2017-10-23 14:21:20 +0200
  • a19c2fe59b work on variations which data is reused in dd-based bisimulation dehnert 2017-10-22 22:13:54 +0200
  • b8120ed73a Markov automaton model checker now clearing basic requirements dehnert 2017-10-20 15:46:36 +0200
  • 41828ca27d more work on bisimulation-based abstraction-refinement dehnert 2017-10-20 15:38:24 +0200
  • 9d17aa10bf Merge branch 'master' into pomdp_datastructures sjunges 2017-10-19 22:22:24 +0200
  • b415c12c25 further preparation of partial bisimulation model checker dehnert 2017-10-19 22:07:41 +0200
  • 3215f25513 upper result bounds for cumulative reward formulas to enable interval iteration TimQu 2017-10-19 21:54:43 +0200
  • d91d979d90 changed some output TimQu 2017-10-19 16:57:08 +0200
  • 9c685f3bdb started on partial bisimulation model checker dehnert 2017-10-19 16:03:26 +0200
  • ea507a0b13 added dd-based partial quotient extraction for DTMCs dehnert 2017-10-19 15:09:12 +0200
  • ab12e4ff3d started on partial quotient extraction in symbolic bisimulation dehnert 2017-10-18 22:29:48 +0200
  • d90c507431 fixed bug in sparse bisimulation quotient extraction related to rewards dehnert 2017-10-17 13:18:43 +0200
  • 70dc9ce7ac Bypassing requirements check to make value iteration without a lower result bound work TimQu 2017-10-17 13:14:13 +0200
  • 58c8531d34 Use Carl 17.10 Matthias Volk 2017-10-17 11:07:20 +0200
  • 26efa18d32 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective TimQu 2017-10-16 18:37:09 +0200
  • e3a506ecc6 Property information output TimQu 2017-10-16 18:36:59 +0200
  • 34485836b8 fixed some convertNumber applications dehnert 2017-10-16 17:24:40 +0200
  • f47e40d363 Fixed removed variable Matthias Volk 2017-10-16 14:43:37 +0200
  • 4d7770aea6 fixed issue in hybrid reachability reward computation that caused empty row groups dehnert 2017-10-16 14:16:55 +0200
  • 3185719fe5 fix for linking issue under linux, adding missing l3pp dependency l3pp_ext dehnert 2017-10-16 14:14:28 +0200
  • c0f07557ed simplified state signature computation in dd-based bisimulation dehnert 2017-10-16 11:20:55 +0200
  • c66175c5e0 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective TimQu 2017-10-15 20:48:44 +0200
  • 29b915ccbf fix out-of-index write in bisimulation quotienting dehnert 2017-10-15 20:37:23 +0200
  • 4cadc61f19 less searches for epoch solutions TimQu 2017-10-15 20:14:30 +0200
  • 0ef06fd31b re-add time output to storm output and make iterative minmax solver respect linear equation solver format for policy iteration dehnert 2017-10-15 19:37:20 +0200
  • b56cd07d0e Consider only a submap of all epochsolutions for faster search TimQu 2017-10-15 19:36:30 +0200
  • 5c1de03d14 fixed min prob computation for single objective case TimQu 2017-10-15 11:43:41 +0200
  • 8204c03c0b fixed a ton of warnings dehnert 2017-10-15 10:38:31 +0200
  • bb890cb91f Merge branch 'master' into rationalsearch dehnert 2017-10-15 10:12:25 +0200
  • 5071df5c82 made sound value iteration work and respect the correct precision TimQu 2017-10-14 22:56:01 +0200
  • 546c897947 Merge branch 'master' into pomdp_datastructures Sebastian Junges 2017-10-14 17:22:37 +0200
  • ccfb1a292c drn parser and exporter use reward names Sebastian Junges 2017-10-14 17:22:28 +0200
  • 93521fd491 Merge branch 'master' into pomdp_datastructures Sebastian Junges 2017-10-14 15:41:27 +0200
  • 2ce145745a parameters from rewards are now also collected in wellformedness analysis Sebastian Junges 2017-10-14 15:41:18 +0200
  • fc7a3a8897 Merge branch 'master' into pomdp_datastructures Sebastian Junges 2017-10-14 15:17:58 +0200
  • 6832fc805c parser improvements in changelog Sebastian Junges 2017-10-14 15:17:38 +0200
  • 378e2ee40f Better error message if expression parser fails Sebastian Junges 2017-10-14 14:13:13 +0200
  • 02c23865da reworked memory leak solution in sylvan according to Tom van Dijks hints dehnert 2017-10-14 14:24:39 +0200
  • fda3445746 options how to transform fsc Sebastian Junges 2017-10-14 14:12:51 +0200
  • 9140c1dc0e statistics and empty-epoch-matrix optimization also for single objective case TimQu 2017-10-13 21:15:44 +0200
  • 108e8e69e8 Changed statistics output a little. Optimized the case where the transition matrix of the epoch model is empty TimQu 2017-10-13 20:37:04 +0200
  • 8adb1b75bd Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm dehnert 2017-10-13 20:30:04 +0200
  • 72d58b6155 fix for sylvan workers not releasing mmap'ed memory dehnert 2017-10-13 20:28:09 +0200
  • dc78ea9c9e Merge branch 'dft-refactor' Matthias Volk 2017-10-13 18:21:01 +0200
  • 4c19c60fb5 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2017-10-13 18:19:59 +0200
  • 0913388cd3 Renamed ExplicitDFTModelBuilderApprox to ExplicitDFTModelBuilder Matthias Volk 2017-10-13 18:11:05 +0200
  • 8f95032d34 not logging exceeding precision in Kwek-Mehlhorn dehnert 2017-10-13 09:20:25 +0200
  • bf727a28fd remove debug output and choose sylvan automatically in exact mode dehnert 2017-10-13 09:18:38 +0200
  • 23686a0f09 reward bounded cumulative reward formulas + fixes for dimensions that do not need memory TimQu 2017-10-13 00:41:24 +0200
  • fb4b5b2d84 added functionality to clear specified solution bounds of equation solvers TimQu 2017-10-13 00:39:08 +0200
  • c7d9b0b61d Fixed that bisimulation did not preserve reward bounded formulas TimQu 2017-10-12 21:29:07 +0200
  • 87778a6775 Finally removed old DFTModelBuilder Matthias Volk 2017-10-12 20:33:24 +0200
  • 1f16008b75 added proper exception handling to sylvan-based sharpening dehnert 2017-10-12 19:59:34 +0200
  • 4456069e81 Fixed typo Matthias Volk 2017-10-12 18:19:52 +0200
  • 88544a9ec7 Added assertion for turnRatesToProbabilities in MA Matthias Volk 2017-10-12 18:19:36 +0200
  • 983e09fd63 Fixed possible problem with rates and exit rates in MA Matthias Volk 2017-10-12 18:18:36 +0200
  • 94a7cd1048 with some disabled setting-modules, do no longer crash in help Sebastian Junges 2017-10-12 17:07:39 +0200
  • d612337ebf added bunch of debug output for aliasing problem dehnert 2017-10-12 16:47:40 +0200
  • 305f607507 fixed another parsing issue pointed out by Assistant Professor Dr. Nils Jansen dehnert 2017-10-12 15:30:25 +0200
  • 49cc789ca2 symbolic minmax solver respecting linear equation solver problem format; fixed parsing bug pointed out by Dr. Nils Jansen dehnert 2017-10-12 15:05:49 +0200