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

Commit Graph

  • fd3b8adc00 fixed bug in formula parser dehnert 2016-06-16 17:57:30 +0200
  • 3f23d7b322 add advanced state labeling (wrt a given formula) ThomasH 2016-06-16 17:54:04 +0200
  • 6810c0d50f fixed bug in computation of instantaneous rewards on DTMCs dehnert 2016-06-16 17:42:54 +0200
  • c88e540a1a fixed bug in graph preprocessing algorithms that support a maximal number of steps dehnert 2016-06-16 16:54:56 +0200
  • 2c23b1ed99 fixed bug in sparse DTMC model checker dehnert 2016-06-16 16:28:56 +0200
  • cae04c0e20 fixed bug in symbolic quantitative check result dehnert 2016-06-16 16:12:05 +0200
  • 71bfb45220 added check for multiple writes to the same global variable in explicit JANI next-state generator dehnert 2016-06-16 11:26:15 +0200
  • ad1e530756 added subsystemBuilder for preprocessing infinite rewards TimQu 2016-06-15 23:08:51 +0200
  • 7861df4f20 JANI next-state generator appears to be working (without rewards) dehnert 2016-06-15 22:43:37 +0200
  • 669e9c6352 fix regarding creation of downward closure in 3D TimQu 2016-06-15 18:42:18 +0200
  • 08112d98aa more work on JANI next state generator and the corresponding tests dehnert 2016-06-15 13:39:19 +0200
  • 4b406c5e74 bugfix TimQu 2016-06-15 13:26:52 +0200
  • 7d2db7b591 fixed zeroconf model files TimQu 2016-06-15 12:10:14 +0200
  • f442d9a434 disabled the "conservative" choice selection for value iteration because it produced wrong results (and we don't need this anymore) TimQu 2016-06-15 10:46:58 +0200
  • 05fecb03b3 started on introducing multiple initial locations in JANI models dehnert 2016-06-14 22:38:01 +0200
  • b62f8819b9 JANI next-state generator can now generate transitions from silent edges dehnert 2016-06-14 21:41:27 +0200
  • e6c89a6f45 more on total rewards TimQu 2016-06-14 19:42:36 +0200
  • 3b9740c95d fixed model files for team benchmark TimQu 2016-06-14 19:19:05 +0200
  • de35d40905 total reward formulas TimQu 2016-06-14 18:44:24 +0200
  • 000a8c2d77 more work on JANI next-state generator dehnert 2016-06-14 16:59:41 +0200
  • 0e1293cabb creation of check results for numerical and achievability queries TimQu 2016-06-14 15:44:31 +0200
  • f461c990b5 introduced post processor plus a little renaiming of things TimQu 2016-06-14 15:02:33 +0200
  • eaa50eb47e updated prism benchmark table TimQu 2016-06-14 14:30:42 +0200
  • abfa23c4de missing override TimQu 2016-06-14 14:30:18 +0200
  • 1d3539ab9a factored out some parts from the PRISM next-state generator into the superclass dehnert 2016-06-14 11:52:10 +0200
  • a9c4415466 put the prism results in a beautiful table TimQu 2016-06-14 11:50:47 +0200
  • bed5939a7b Merge branch 'future' into multi-objective TimQu 2016-06-14 11:14:52 +0200
  • 1a18ea3aec fixed the case where a maximal end componend decomposition is requested for an empty subsystem TimQu 2016-06-14 11:14:16 +0200
  • 543ecfac50 prism benchmark logs TimQu 2016-06-13 19:18:18 +0200
  • 0b6d0a7e5e improvements for preprocessor TimQu 2016-06-13 19:13:53 +0200
  • d496e71169 linear transformation for polytopes TimQu 2016-06-13 15:20:07 +0200
  • b00d3f154c further polishing code TimQu 2016-06-13 15:04:23 +0200
  • c86c6953b5 Renamed and refactored the helpers a little TimQu 2016-06-13 02:00:34 +0200
  • d5f1e6d5e7 multi objective settings TimQu 2016-06-12 19:51:05 +0200
  • ea46ef78d0 property files and a script TimQu 2016-06-12 17:08:12 +0200
  • b4ad182911 reorganized prism benchmark files a little TimQu 2016-06-12 14:30:40 +0200
  • 4e16de6ca6 modified the simple example a little TimQu 2016-06-11 13:49:51 +0200
  • a54c9f0023 Added test and fix for neutralECRemover TimQu 2016-06-11 13:43:23 +0200
  • da65ef3aa9 Renamed Effectless -> Neutral. Also removed additional (useless) sink state TimQu 2016-06-11 11:47:47 +0200
  • c401de1fb9 handling of end components in which no reward is earned TimQu 2016-06-11 00:43:03 +0200
  • 18d3c06f12 fix in state duplicator TimQu 2016-06-11 00:39:47 +0200
  • 4cc780cbc0 tests compiling and running again dehnert 2016-06-09 14:54:22 +0200
  • 4063d88913 added option to build all labels/reward models for next-state generators dehnert 2016-06-09 10:51:19 +0200
  • d35c99e844 renamed central model builder function dehnert 2016-06-09 09:57:04 +0200
  • 9f6bd1805f modified the entry point code to deal with the new generator-builder-structure dehnert 2016-06-09 09:51:46 +0200
  • 9ec10f7bcb some modifications for preprocessing TimQu 2016-06-09 00:48:58 +0200
  • 5310793653 minor fixes and debug output TimQu 2016-06-09 00:48:02 +0200
  • ddf165d4d3 more work on tearing PRISM-specific functionality out of the explicit model builder dehnert 2016-06-08 23:24:31 +0200
  • 6655ee41d8 started to restructure explicit model builder to make it fit for JANI models dehnert 2016-06-08 16:57:26 +0200
  • cda4e666d3 globally formulas TimQu 2016-06-08 14:20:17 +0200
  • d50211ac63 added examples from ATVA'12 paper TimQu 2016-06-08 14:19:32 +0200
  • 2bab103a87 numerical and pareto queries TimQu 2016-06-08 12:41:47 +0200
  • efda4e2950 changed the ordering of operations a bit to get more performance dehnert 2016-06-07 18:13:26 +0200
  • ca57e22abc started profiling dehnert 2016-06-07 16:59:41 +0200
  • c393449ca6 [fixing] a bug a day keeps insanity away dehnert 2016-06-06 21:27:51 +0200
  • fab04934bf towards numerical and pareto queries TimQu 2016-06-06 15:45:35 +0200
  • 3d4552cbf8 started working on improved JANI model building that still allows for more relaxed rules than PRISM when it comes to writing global variables dehnert 2016-06-05 23:38:51 +0200
  • fb1fa2f23c implemented the LP solving to find a separating halfspace TimQu 2016-06-05 12:24:53 +0200
  • 4ca7628319 bug fixes and improved debug output TimQu 2016-06-04 18:13:26 +0200
  • 7c4770df07 scheduler tracking for value iteration TimQu 2016-06-04 17:40:02 +0200
  • f529816df4 WeighedObjectives model checking, first version for multi-objective achievability queries TimQu 2016-06-04 15:00:38 +0200
  • 82023d280d JANI model builder for MDPs is working now, but too slow dehnert 2016-06-03 15:09:52 +0200
  • 3919f90712 started debugging JANI MDP building dehnert 2016-06-02 23:09:42 +0200
  • a6359335cf Fixed compiling when hypro is not available TimQu 2016-06-02 20:03:08 +0200
  • a4ef3cf778 added CTMC tests for JANI model builder dehnert 2016-06-02 16:55:41 +0200
  • d84ae34cc6 re-enabled omitting unused variables from PRISM models when converting to JANI dehnert 2016-06-02 15:22:54 +0200
  • 7750480714 JANI model builder for DTMCs working dehnert 2016-06-02 15:21:25 +0200
  • 310db8a234 started to include reachability in JANI model generation dehnert 2016-06-01 23:32:00 +0200
  • 32ec106588 more work on symbolic JANI model building dehnert 2016-06-01 16:57:26 +0200
  • 0fad8eb144 another fix for downward closure TimQu 2016-06-01 15:07:41 +0200
  • 6db2886624 small fix TimQu 2016-06-01 14:47:16 +0200
  • 5084372718 polytope adapter for hypro TimQu 2016-06-01 14:11:58 +0200
  • a2e9559faf some auxiliary functions for vectors TimQu 2016-06-01 14:10:51 +0200
  • 6313e4c31b fixed a bug in symbolic model generator dehnert 2016-05-31 23:45:41 +0200
  • adf8232896 more work and fixes for symbolic JANI builder dehnert 2016-05-31 16:27:17 +0200
  • c4327e91a9 more work on symbolic JANI model builder dehnert 2016-05-30 20:59:54 +0200
  • 1c01a54b53 fixed more issues with boost::transform_iterator dehnert 2016-05-30 18:10:09 +0200
  • 14208d8f58 Fix transform_iterator thingamajig hbruintjes 2016-05-30 17:58:14 +0200
  • 9c75e9dbd7 more work on JANI model generation dehnert 2016-05-30 17:20:14 +0200
  • de50d85140 more polytopes, hyproadapter TimQu 2016-05-30 14:24:15 +0200
  • a3e0a3c55b first steps for geometric representations TimQu 2016-05-30 01:26:45 +0200
  • 2624f63598 added linking with hypro TimQu 2016-05-29 21:14:48 +0200
  • 32dc38b48f some more steps towards symbolic builder for JANI models dehnert 2016-05-29 18:47:06 +0200
  • ad73e61f12 improvements for preprocessing TimQu 2016-05-29 16:06:14 +0200
  • 1892a9657f added some accessor functions and iteration capabilities. started on symbolic jani model builder dehnert 2016-05-29 15:34:21 +0200
  • ecc1a80358 added conversion from PRISM to JANI. Added simplistic tests for that. dehnert 2016-05-29 11:05:53 +0200
  • b0d2af20ae added check for existence of __builtin_popcountll (reverted from commit 30bcfcad0e [formerly 65f94a6d6e]) TimQu 2016-05-28 17:24:19 +0200
  • dbac45d9be more StateDuplicator TimQu 2016-05-28 17:32:17 +0200
  • 81662f5ab4 Fixed some comments in utility::vector TimQu 2016-05-28 17:31:57 +0200
  • 30bcfcad0e added check for existence of __builtin_popcountll TimQu 2016-05-27 23:22:16 +0200
  • 358fe02b11 fix for the case where carl is available but cln isn't TimQu 2016-05-27 23:21:06 +0200
  • 768cdfb77b state duplicator TimQu 2016-05-27 23:19:15 +0200
  • 41640bfbd4 JaniParser: several extensions to expressions, probabilities, locations in destinations of edges sjunges 2016-05-27 00:25:58 +0200
  • a6aa909a12 convenience functions for operatiosn on expressions sjunges 2016-05-27 00:25:12 +0200
  • 813515d546 JaniParser: support for local variables sjunges 2016-05-26 23:22:39 +0200
  • 48f2cc156c JaniParser: extended expression parsing sjunges 2016-05-26 21:54:53 +0200
  • fc24c55960 some preprocessing for multi-objective formulas TimQu 2016-05-26 21:40:04 +0200
  • dd22841682 JaniParser: extended edge parsing sjunges 2016-05-26 20:33:54 +0200
  • 9bf5cf15b6 JaniParser: some more expressions, better error messages and prel. stub for edge parsing sjunges 2016-05-26 20:15:59 +0200
  • 510d51e5c1 parser support for bounded ints sjunges 2016-05-24 18:24:49 +0200