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

Commit Graph

  • 86f0195b18 removed jani conversion in cli of main binary TimQu 2018-07-24 15:38:34 +0200
  • e5e6e1bd79 worked on prism to jani converter TimQu 2018-07-24 10:55:01 +0200
  • 2e035f3957 started working on conversion binary TimQu 2018-07-23 10:11:42 +0200
  • a8d4c45299 Reworked extended priority computation Alexander Bork 2018-07-19 21:56:38 +0200
  • db72a05358 fixed log output TimQu 2018-07-19 10:04:44 +0200
  • 6051363782 initial support for multi-reward structures in counterexample generation Sebastian Junges 2018-07-18 16:55:00 +0200
  • 6e2e3d452d minor fixes in counterexample generation Sebastian Junges 2018-07-18 16:54:34 +0200
  • 85671ef6f1 fixing segfault pointed out by Paul Gainer dehnert 2018-07-18 13:56:16 +0200
  • abe7510ae9 added clearing requirements dehnert 2018-07-17 18:58:51 +0200
  • b895911c7d New storm version containing fix for version parsing Matthias Volk 2018-07-17 16:48:13 +0200
  • e0d50d1b53 Set correct capacity for unavailable places Matthias Volk 2018-07-17 16:27:35 +0200
  • 9902bb9dff Fixed version parsing for 'commits ahead' Matthias Volk 2018-07-17 14:22:21 +0200
  • c5cfe70176 Added extended priorities inside AND/OR/VOT gates Alexander Bork 2018-07-16 21:05:49 +0200
  • 2cfdb56450 Storm version 1.2.2 Matthias Volk 2018-07-16 17:13:59 +0200
  • 41c20c7b63 updated changelog TimQu 2018-07-15 13:50:00 +0100
  • e1047e787f handled case where no threshold for the number of iterations is provided TimQu 2018-07-15 13:44:29 +0100
  • 274d51795c removed default value for maximal iteration count TimQu 2018-07-14 16:36:17 +0100
  • 6a1ab53e35 Use carl version 18.06 if building from within Storm Matthias Volk 2018-07-13 10:45:09 +0200
  • 7a5b93bdfa Updated changelog Matthias Volk 2018-07-13 10:41:54 +0200
  • f0c451aae9 fixed a case where time path propreties were not identified as such, and ensured for debugging that time operators now get a time path formula Sebastian Junges 2018-07-12 18:17:25 +0200
  • 93da59fa04 fixed an issue with jani properties for expected time not being parsed as requested Sebastian Junges 2018-07-12 18:16:26 +0200
  • 264d9158c8 bugfix for dd-based MA building from JANI dehnert 2018-07-12 15:30:19 +0200
  • cc1fc8a7be adding exact sampling for parametric systems dehnert 2018-07-12 13:35:55 +0200
  • c2870e42b0 changed help slightly dehnert 2018-07-12 12:27:20 +0200
  • add5ee533e Merge branch 'master' into parameter_sampling dehnert 2018-07-12 11:53:02 +0200
  • a08cb4ac18 making game solver respect equation solver format dehnert 2018-07-12 11:51:11 +0200
  • caf9975109 Fixed an issue with topological min max solver TimQu 2018-07-12 11:18:26 +0200
  • 10da10a7d1 started on enabling sampling of parametric models from command line dehnert 2018-07-11 22:39:53 +0200
  • 601b73608a adapting changelog dehnert 2018-07-11 21:06:52 +0200
  • 1adc1ce564 Merge branch 'master' into chris_diss dehnert 2018-07-11 20:40:09 +0200
  • cb89ab7509 clearing end-component requirement in topological solver dehnert 2018-07-11 20:39:21 +0200
  • 54c0bbb7c3 flatten of jani models before export via appropriate setting Sebastian Junges 2018-07-11 19:50:03 +0200
  • b7f88907b6 counterexamples record their timings to a structure, and support for rewards fixed Sebastian Junges 2018-07-11 19:49:35 +0200
  • f2a7621e0a updated changelog Sebastian Junges 2018-07-11 15:52:48 +0200
  • 9aaf7e0bfb Merge branch 'master' into chris_diss dehnert 2018-07-11 15:51:38 +0200
  • a616e2743d fixes to standard-compliant prism-to-jani conversion dehnert 2018-07-11 15:51:12 +0200
  • e64e293d59 jani transformer which changes a variable into a location Sebastian Junges 2018-07-11 15:50:16 +0200
  • f9e4208268 export jani with comment expressions to ease debugging jani models Sebastian Junges 2018-07-11 15:49:37 +0200
  • 6275c52779 several convenience additions to jani data structures Sebastian Junges 2018-07-11 15:48:48 +0200
  • 33c189bd32 export setting for flattening Sebastian Junges 2018-06-30 12:37:02 +0200
  • a46e6439eb enabled switching of methods if unsupported method chosen in symbolic min-max equation solver dehnert 2018-07-10 14:18:41 +0200
  • 9ed6f084e7 adding uniqueness constraint in LRA computation also for fixed-point formulation dehnert 2018-07-10 11:07:04 +0200
  • b73f0ef94e fixing issue in jani-to-prism label replacement dehnert 2018-07-09 21:49:13 +0200
  • ec3cb1a134 Added alternative method to calculate priorities for better compatibility with MC4CSLTA Alexander Bork 2018-07-07 02:40:17 +0200
  • 9d528db2fc adding translation of expressions used in formulas to symbolic-to-sparse transformers dehnert 2018-07-06 16:22:45 +0200
  • 3e7b1ffc71 Added dependency names to win and lose flip transitions for PDEPs Alexander Bork 2018-07-06 10:02:00 +0200
  • 0c0f61e27b Fix: Only access counterexample settings in model-handling, if they are available. TimQu 2018-07-06 09:28:54 +0200
  • d9d86e4f56 asserted that infinity is never obtained as a model checker result TimQu 2018-07-06 08:49:50 +0200
  • e609a240a9 selecting minmax topological by default dehnert 2018-07-05 19:56:47 +0200
  • 4500f98ae1 fixing typo dehnert 2018-07-05 14:12:36 +0200
  • a7caf709ae default to topological equation solver dehnert 2018-07-04 11:43:42 +0200
  • dff67450e0 fixed recently introduced bug in JANI export dehnert 2018-07-03 20:55:46 +0200
  • 8114437cee allowing cumulative and instantaneous reward properties to be transformed to JANI dehnert 2018-07-03 16:12:19 +0200
  • d638972bc8 enabled pushing location assignments to edges dehnert 2018-07-03 15:22:53 +0200
  • 958ad6d8d2 Merge branch 'master' into deterministicScheds TimQu 2018-07-02 10:57:23 +0200
  • 749ba87254 Made SVI log output more clear TimQu 2018-07-02 10:57:13 +0200
  • 98969e627c updated counterexamples to support statistics to be exported Sebastian Junges 2018-06-30 12:36:10 +0200
  • db6f43ed9d made LRA computation for deterministic systems able to respect that the underlying solver requires a fixed-point formulation dehnert 2018-06-30 11:04:22 +0200
  • 86069b8552 fix typo in JSON exporter dehnert 2018-06-29 21:58:30 +0200
  • 50aa6d1424 assuming the only global real transient variable is the reward when exporting JANI and no reward model is mentioned in the property (issues a warning) dehnert 2018-06-29 19:33:10 +0200
  • c4bed85dc4 switching to native linear equation solver by default and power iteration dehnert 2018-06-29 15:56:12 +0200
  • 1c0eef96df Merge branch 'master' into deterministicScheds TimQu 2018-06-28 13:05:33 +0200
  • 1f6fc7e273 Better conversion of MA to CTMC if there are only Markovian states TimQu 2018-06-27 15:55:33 +0200
  • b696d63953 checking if a facet has been analyzed sufficiently precise via smt TimQu 2018-06-28 13:02:59 +0200
  • fbce6a4795 added function to check whether a vector has a zero element TimQu 2018-06-28 13:02:29 +0200
  • d8d616abdf Merge branch 'master' into deterministicScheds TimQu 2018-06-28 10:04:58 +0200
  • 8a579f1e95 Better conversion of MA to CTMC if there are only Markovian states TimQu 2018-06-27 15:55:33 +0200
  • c50407bcc3 Merge branch 'master' into deterministicScheds TimQu 2018-06-27 15:56:08 +0200
  • d47b86d4d7 Better conversion of MA to CTMC if there are only Markovian states TimQu 2018-06-27 15:55:33 +0200
  • ac1d5df5c4 debugging and output of results for deterministic pareto explorer TimQu 2018-06-27 15:49:06 +0200
  • 571e157eef added missing return statement TimQu 2018-06-27 15:48:15 +0200
  • 5c08d85a38 Fixes for multiobjective preprocessor in cases where reduction to total rewards is not possible TimQu 2018-06-27 15:47:51 +0200
  • cd5b805a76 Under- and overapproximation for Pareto curve check result are now optional TimQu 2018-06-27 15:44:20 +0200
  • b748b27b85 fixed compilation of settings... TimQu 2018-06-27 15:42:33 +0200
  • b14c554df2 correct treatment of Markov Automata in scheduler evaluator TimQu 2018-06-27 15:38:10 +0200
  • a73574a99f added functionality to translate a polytope to an expression TimQu 2018-06-27 15:37:10 +0200
  • f1eaab5603 enabling preservation of total reward formulas in ContinuousToDiscreteTimeModelTransformer TimQu 2018-06-27 15:28:53 +0200
  • 0e70cfc617 added setting to print intermediate results during the computation TimQu 2018-06-27 09:45:53 +0200
  • 789367a28b using new memory incorporation in multi objective model checking TimQu 2018-06-27 09:45:03 +0200
  • d24d1bdcd8 added memory incorporation transformer TimQu 2018-06-27 09:44:18 +0200
  • 5163803243 added nondeterministic memory structure TimQu 2018-06-27 09:43:39 +0200
  • 51a5a82a5f more functionality for deterministic Pareto Explorer TimQu 2018-06-26 10:22:13 +0200
  • 7b43e79ff5 adding missing template instantiation TimQu 2018-06-26 10:21:48 +0200
  • 5f8af5a38a added coordinate utility file TimQu 2018-06-26 10:21:31 +0200
  • 80da98eec5 adding shift method to polytope interface TimQu 2018-06-26 10:21:06 +0200
  • b075c16ce0 Merge branch 'master' into deterministicScheds TimQu 2018-06-25 15:24:30 +0200
  • ca2295be1d updated changelog: support for expected total rewards TimQu 2018-06-25 15:24:13 +0200
  • 5a16b2befa minor fixes to let the total reward tests compile and pass TimQu 2018-06-25 15:23:25 +0200
  • 081c0a95d0 Export pnpro with single-server semantics Matthias Volk 2018-06-25 14:04:35 +0200
  • 1f4c0325be test cases for ctmcs and markov automata TimQu 2018-06-25 11:22:52 +0200
  • 8df9b461cb total reward formulas for ctmcs and markov automata TimQu 2018-06-25 11:22:31 +0200
  • b5566fa861 more on total reward formulas for mdps TimQu 2018-06-25 11:22:02 +0200
  • b3edae8707 fixed fragment specification: total reward formulas should not be supported for hybrid/dd right now TimQu 2018-06-25 11:21:31 +0200
  • 8c3bd15eae Fixed priorities for dependencies and export of PDEP probabilities into PNPRO format Alexander Bork 2018-06-24 23:45:48 +0200
  • 7dc17065c1 Updated DFT export to new JSON format Matthias Volk 2018-06-24 20:53:58 +0200
  • 0be0126095 fixed support for highlevel counterex for expected rewards in dtmcs Sebastian Junges 2018-06-24 15:07:23 +0200
  • 73a1911a53 Merge branch 'master' into counterexample_improvements Sebastian Junges 2018-06-24 12:52:18 +0200
  • 1850cf7368 Fixed trigger rates for timed transitions not being saved in .pnpro files Alexander Bork 2018-06-22 17:54:17 +0200
  • c2dd57cda5 total rewards for mdps TimQu 2018-06-22 17:28:01 +0200
  • 87e34d7b32 Added Support for Total Reward Formulas for DTMCs in the Sparse Engine TimQu 2018-06-22 15:05:36 +0200