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

Commit Graph

  • defcd7d5d7 Multi-objective model checking: adapted data structures to allow more general objectives TimQu 2017-07-19 11:42:06 +0200
  • d35a5e4bdd returning the time bound type from a timeBoundReference TimQu 2017-07-19 11:39:37 +0200
  • 9207f4fbd8 Merge branch 'memoryproductimprovements' TimQu 2017-07-18 13:07:10 +0200
  • e8e189723f fixed applying memoryless schedulers TimQu 2017-07-18 13:06:05 +0200
  • 5651b23771 fixing minor compiling issue TimQu 2017-07-18 11:58:07 +0200
  • 6af15f3a0d Memory Structure Product with custom reward model type TimQu 2017-07-18 11:29:34 +0200
  • a348f6ea8e function to apply a given scheduler to a nondeterministic model TimQu 2017-07-18 11:24:24 +0200
  • 7bd9ef798f returning the memory structure of a scheduler TimQu 2017-07-18 10:57:07 +0200
  • 4251c9f525 added function to build a trivial memory structure TimQu 2017-07-18 10:56:28 +0200
  • 4351be5512 Allowed building memory product with respect to a scheduler TimQu 2017-07-18 10:43:34 +0200
  • afd6c21c7d Replaced switch-fallthrough in travis Matthias Volk 2017-07-14 17:04:05 +0200
  • ff6037ed79 Use master branch for carl again Matthias Volk 2017-07-14 16:38:59 +0200
  • ae9641baba Install eigen3 in dockerfiles Matthias Volk 2017-07-14 16:38:34 +0200
  • cc268b3140 Fixed problem in travis Matthias Volk 2017-07-14 16:38:11 +0200
  • 556a7df213 Refactored travis build script Matthias Volk 2017-07-14 16:28:24 +0200
  • 9df6e58127 Travis dependency already part of docker Matthias Volk 2017-07-14 16:28:01 +0200
  • 6c2213b9a1 Remove build directory in first stage of travis Matthias Volk 2017-07-14 16:24:25 +0200
  • 8c29e6d04b Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-14 16:03:41 +0200
  • 5bdbc00bcd Changed carlConfig path for shipped carl Matthias Volk 2017-07-14 13:35:48 +0200
  • e4783846e0 Changed carlConfig path for shipped carl Matthias Volk 2017-07-14 10:55:23 +0200
  • 9ad4203b09 Export to cmake for shipped carl Matthias Volk 2017-07-14 10:45:15 +0200
  • 1067a94c6b Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-13 17:21:54 +0200
  • 43642fef84 Improved product of model and memory structure: We can now enforce that certain states are considered reachable. TimQu 2017-07-13 16:41:28 +0200
  • 9bccae9c5c uint_fast64_t -> uint64_t TimQu 2017-07-13 15:59:31 +0200
  • 11b9c60515 Adapted fragment checker test to new multiobjective-fragment specification TimQu 2017-07-13 12:12:41 +0200
  • 156d1055f3 Merge branch 'master' into symbolic_bisimulation dehnert 2017-07-12 21:13:46 +0200
  • 29855e2853 added option to display information about exploration progress to both jit and explicit builder dehnert 2017-07-12 19:52:39 +0200
  • 040c1f0d4c fixed ignoring the hypothesis when not doing refinement TimQu 2017-07-12 12:51:27 +0200
  • 48e029dd9d Adapted region settings and CLI to new features. TimQu 2017-07-12 10:42:34 +0200
  • 6621cb814c new argument validator: doubleRangeValidatorIncluding TimQu 2017-07-12 10:42:04 +0200
  • 56616f1e26 trying to clarify sylvan dependency on carl Sebastian Junges 2017-07-11 22:49:04 +0200
  • 53a2723e0c storm pars result moved from storm to storm pars Sebastian Junges 2017-07-11 22:48:09 +0200
  • 5a3c67c352 Use result.toString to generate easier-to-parse result files sjunges 2017-07-03 23:36:58 +0200
  • 3bcdc1b579 allowing to read transient variables in guards of edges in JIT-based JANI model builder and making the optimization level an option dehnert 2017-07-11 22:01:41 +0200
  • 6fd75ac37e fixed issue in cli related to transforming PRISM to JANI dehnert 2017-07-11 22:01:02 +0200
  • 9591157996 new features for storm-pars api: - depth limit for iterative refinement - the regions with inconclusive result are now also part of the result - when analyzing a region, a hypothesis (AllSat or AllViolated) can now be given TimQu 2017-07-11 19:04:40 +0200
  • 8aa2b57640 minor fix for multi-objective preprocessor TimQu 2017-07-11 15:57:48 +0200
  • 9bfb1fedc2 requiring that multi objective queries have a multi(..) formula at top level. TimQu 2017-07-11 14:48:54 +0200
  • 988b2a9af9 added functionality to split a rational vector into an integer vector and a rational factor TimQu 2017-07-11 10:44:20 +0200
  • 92f2f23603 initialization of some data for reward bounded objectives TimQu 2017-07-11 10:42:27 +0200
  • 275f1ff15e only filter the result if there actually is a result and a filter TimQu 2017-07-11 10:25:55 +0200
  • 0e88d711e8 Correctly handled reward bounded objectives in multi-objective preprocessing TimQu 2017-07-11 10:24:55 +0200
  • d5eb222bfa Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-09 16:38:15 +0200
  • b44870dc09 implemented SMT-Lib export SmtSolver interface TimQu 2017-07-07 18:20:28 +0200
  • d9d201f56b Fixed eigen package in docker Matthias Volk 2017-07-07 15:20:55 +0200
  • 2a32e2cd77 Install eigen package in travis Matthias Volk 2017-07-07 15:17:27 +0200
  • a860776164 Try to print error output in travis Matthias Volk 2017-07-07 14:00:49 +0200
  • d6447a56f0 minor fixes for reward bounded formulas TimQu 2017-07-06 19:07:15 +0200
  • c1b4cb848c added missing newlines in the storm-pars cli. Also do not segfault when there is no result TimQu 2017-07-06 19:06:24 +0200
  • 07259e8f0d added parser for IMCAs explicit Markov automaton format TimQu 2017-07-05 17:49:52 +0200
  • 1f71e9af79 extend debug output of gmmxx adapter TimQu 2017-07-05 14:33:50 +0200
  • 5b868081f0 Fixed MA LRA computation for the case where the whole MA is a MEC TimQu 2017-07-05 14:33:04 +0200
  • 89d8993cfb updated changelog (long-run rewards on MAs) TimQu 2017-07-05 09:05:18 +0200
  • 1eaa02fab1 Clear mtime_cache when starting Matthias Volk 2017-07-05 22:54:49 +0200
  • f2492c9e97 Small fix in travis script Matthias Volk 2017-07-05 18:21:57 +0200
  • 186894822d Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-07-05 18:21:33 +0200
  • c46ce03e60 make storm compile with latest version of carl Sebastian Junges 2017-07-05 18:08:15 +0200
  • 4a43d7ab0d towards compiling storm with the latest carl version Sebastian Junges 2017-07-05 15:29:09 +0200
  • 14c18929df Merge branch 'master' into parsing_reward_bounded Sebastian Junges 2017-07-04 23:35:15 +0200
  • 6a46d0abd5 formula parser extended with reward bounded rewards Sebastian Junges 2017-07-04 23:34:46 +0200
  • 95831c1058 make formula grammar compile again dehnert 2017-07-04 20:30:45 +0200
  • 9af46452bc first attempt for a parser Sebastian Junges 2017-07-04 16:54:26 +0200
  • 980f1864af test cases Sebastian Junges 2017-07-04 16:54:08 +0200
  • c70a815589 Refactored travis scripts Matthias Volk 2017-07-04 16:34:58 +0200
  • 79f96ad2ed Added Dockerfile for Storm Matthias Volk 2017-07-04 14:52:22 +0200
  • 33656791ba Merge branch 'master' into filter_additions dehnert 2017-07-04 11:56:30 +0200
  • 6471bfdcea made cli output respect filters dehnert 2017-07-04 11:17:01 +0200
  • d0551c1d59 getting time/step/reward bounds as rational number TimQu 2017-07-04 10:48:26 +0200
  • 322808db5b getting reward name from reward bounded until formula. TimQu 2017-07-04 10:47:44 +0200
  • 3de51e28e5 towards reward-bounded properties Sebastian Junges 2017-07-03 22:53:47 +0200
  • 1c9d888676 uint_fast64_t -> uint64_t TimQu 2017-07-03 17:10:33 +0200
  • 8da6a6e30e reduced memory consumption of VI based LRA computation TimQu 2017-07-03 17:04:35 +0200
  • 49713eea72 Added new MinMaxMethod: 'acyclic' which potentially increases performance on acyclic mdps TimQu 2017-07-03 17:03:51 +0200
  • 19925ac74d implemented value iteration based Long run average rewards for Markov automata by Butkova et al. (TACAS 2017) TimQu 2017-06-30 19:05:02 +0200
  • bff745656c Fixed some matrix builder bugs related to 0x0 matrices TimQu 2017-06-30 19:01:04 +0200
  • fb3b28e08f Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2017-06-30 18:30:54 +0200
  • 6bd8c8f9b5 Fixed some typos Matthias Volk 2017-06-30 18:27:27 +0200
  • 4cafe33415 Changed unique_ptr to shared_ptr for RegionModelCheckers Matthias Volk 2017-06-30 18:27:04 +0200
  • bec6b664d9 actually check carl version, error if outdated Sebastian Junges 2017-06-29 16:50:33 +0200
  • fb170a910a Merge from upstream Matthias Volk 2017-06-29 15:52:29 +0200
  • ae470851f4 Do not segfault when a property could not be verified TimQu 2017-06-29 13:59:43 +0200
  • 75e4c229cb minor fix for Long run average rewards for Markov automata TimQu 2017-06-29 13:54:16 +0200
  • b8844d5ad1 updated changelog TimQu 2017-06-29 11:57:22 +0200
  • 6151dc0e96 Enabled Long Run Average Rewards for MAs (LP based) TimQu 2017-06-29 11:42:49 +0200
  • d5902ac694 Started on changelog for next version Matthias Volk 2017-06-29 11:25:44 +0200
  • 28fc5b7c29 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2017-06-29 10:45:03 +0200
  • 9611a1b243 Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-06-29 10:40:28 +0200
  • fd63603b5c Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Sebastian Junges 2017-06-29 10:30:20 +0200
  • 9b90e0c784 typo Sebastian Junges 2017-06-29 10:30:17 +0200
  • 752af135cd When computing expected rewards for Markov Automata, we now invoke the MDP implementation (instead of the rather inefficient MA implementation) TimQu 2017-06-29 09:38:24 +0200
  • e2cfa54d5b Fixed an issue when computing expected rewards of Markov Automata TimQu 2017-06-28 18:37:36 +0200
  • ed53c9287f Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-06-28 17:24:18 +0200
  • b1b6b4b8cf Merge branch 'storm-pars' TimQu 2017-06-28 15:47:01 +0200
  • 68213ace06 fixed computation of player 1 matrix for parameter lifting on pMDPs with infinite reward at some states TimQu 2017-06-28 15:45:37 +0200
  • aef9a5c99e Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2017-06-28 14:36:58 +0200
  • 2231e9dfa3 Fixed stage skipping in travis Matthias Volk 2017-06-28 14:08:07 +0200
  • 08f9578b9a Merge remote-tracking branch 'origin/master' into storm-pars TimQu 2017-06-27 18:27:09 +0200
  • ed550e6255 fixed invocation of instantiation checkers TimQu 2017-06-27 18:13:05 +0200
  • 57490a7947 fixed continuous to discrete time transformation TimQu 2017-06-27 18:11:18 +0200
  • f2294fadb0 fixed compiling storm-pars cli and improved output a little TimQu 2017-06-27 16:08:02 +0200