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

Commit Graph

  • 722e67fe64 parsing choice labels for explicit models TimQu 2017-05-24 17:02:43 +0200
  • f558cb866c using exact data types for smt-based multi objective model checking tests. Also disabled a few tests that test (yet) unsupported queries or that take too long. TimQu 2017-05-24 16:10:06 +0200
  • 1d329176ba Resolved compiling issues due to recent merge TimQu 2017-05-24 16:08:40 +0200
  • 8dfa141a4a Exporting .dot for explicit input. removed duplicated code for explicit input with parametric engine TimQu 2017-05-24 16:08:15 +0200
  • 77a90184e7 building choice labeling when the corresponding option is given TimQu 2017-05-24 13:22:55 +0200
  • cd5ee63cce fixed preserving the choice labeling when an ma is closed TimQu 2017-05-24 13:21:46 +0200
  • dc079b3196 moved a function to graph.h TimQu 2017-05-24 10:26:46 +0200
  • 7c90e1e6c2 Merge remote-tracking branch 'origin/smt-based-multi-objective' TimQu 2017-05-24 10:18:10 +0200
  • 58fad65ab6 fixes for the string representations of prism choice origins TimQu 2017-05-23 19:20:08 +0200
  • b531dccad9 .dot output for deterministic models with choice labels TimQu 2017-05-23 17:55:20 +0200
  • e7bc5fdef9 fixed several minor bugs regarding the choicelabeling TimQu 2017-05-23 14:45:52 +0200
  • bf97d79573 moved building the choice origin strings into the ChoiceOrigins class TimQu 2017-05-23 13:09:57 +0200
  • 7e5bb4aa0e Merge remote-tracking branch 'origin/master' into choicelabels TimQu 2017-05-22 22:08:28 +0200
  • 0aed35f4b4 worked on human readable representations of prism command sets TimQu 2017-05-22 22:08:03 +0200
  • db31c1cb11 improved .dot export of models with choice labeling TimQu 2017-05-22 22:06:22 +0200
  • 6537fd8b72 Replaced the old choice labeling with the new one and used choice origins for the minimal command set counterexample generators TimQu 2017-05-22 15:22:40 +0200
  • a067527aa0 As pointed out by Joachim Klein, weak bisimulation does not preserve reward properties. Therefore, weak bisimulation now refines blocks with non-zero reward wrt. strong bisimulation. dehnert 2017-05-20 11:00:01 +0200
  • c5d0b281ce fixed a recently introduced bug affecting entry counts in explicit reward matrices dehnert 2017-05-20 08:27:43 +0200
  • 89454481d0 Merge pull request #4 from ArashPartow/master cdehnert 2017-05-20 07:42:38 +0200
  • dcbd8fdb12 Wrong order for timeout Matthias Volk 2017-05-19 17:32:41 +0200
  • 1afd8388d5 Small fixes Matthias Volk 2017-05-19 16:39:53 +0200
  • cb5c42feb6 Fixed typo Matthias Volk 2017-05-19 15:28:22 +0200
  • 987a53dfd1 Two tries for building libstorm Matthias Volk 2017-05-19 15:22:40 +0200
  • 5bfc0f91c1 Second build stage to make building libstorm more robust Matthias Volk 2017-05-19 14:44:07 +0200
  • 70ebe36ec6 adapted tests to recent changes wrt to 0-transition insertions in explicit parser dehnert 2017-05-19 13:53:05 +0200
  • 9bc55e3107 Merge remote-tracking branch 'origin/master' into choicelabels TimQu 2017-05-19 13:35:28 +0200
  • f762491ce4 fixed tests that used the prism model builder TimQu 2017-05-19 13:28:32 +0200
  • 759e351e95 Improved explicit model building: - There is now an option to generate a choice labeling that corresponds to the specified action names. - The old choice labeling (where each choice was labeled with an index set representing the corresponding prism commands) is renamed to choiceOrigins and has been improved towards support of other input formats (such as Jani) and other applications such as scheduler synthesis TimQu 2017-05-19 13:27:59 +0200
  • c595fee4dc removed some unnecessary transition insertions in parser dehnert 2017-05-19 13:04:16 +0200
  • 2b142c83bb Disabled verbose output Matthias Volk 2017-05-19 12:41:01 +0200
  • a2517c7a12 Set mtime for StormEigen Matthias Volk 2017-05-18 14:07:46 +0200
  • cb90600abb Silenced a warning TimQu 2017-05-18 10:54:53 +0200
  • 25074b50a9 Added function to get the next unset bit in a bitvector TimQu 2017-05-18 10:54:38 +0200
  • 4413afb542 used new helper functions at some points in the code TimQu 2017-05-18 09:49:32 +0200
  • 8a7609fb83 fixed Rmin computation with exact sparse engine when very high rewards occur TimQu 2017-05-17 09:51:24 +0200
  • 869d7e7ba7 Build sylvan beforehand Matthias Volk 2017-05-18 10:31:53 +0200
  • 7f346d2f0b more work on quotient extraction dehnert 2017-05-17 21:35:48 +0200
  • 4cf79ab8cc Try to avoid rebuilding Matthias Volk 2017-05-17 10:38:39 +0200
  • 34e48473b3 Updated changelog Sebastian Junges 2017-05-16 11:28:36 +0200
  • e3759eb326 Verbose output for make Matthias Volk 2017-05-16 08:17:52 +0200
  • f72200bd2c - removed deprecated option USE_CARL (now a variable). - changed behaviour of POPCNT: we usually rely on march=native which uses popcnt if available, and now can force its usuage in other situations sjunges 2017-05-15 23:24:29 +0200
  • 5693144f32 refactored code to prevent duplication, added support for rational functions at edges when collecting constraints sjunges 2017-05-15 23:07:35 +0200
  • 165d168cd6 fix for gcc, add state reward support for constraint collection sjunges 2017-05-15 22:29:53 +0200
  • 5c7d3db743 towards proper side constraints for parametetric systems Sebastian Junges 2017-05-15 21:42:16 +0200
  • cb5aff10ae Fix ambigious isspace that was preventing compilation, introduced by some earlier commit. Sebastian Junges 2017-05-15 21:41:06 +0200
  • 2e02e34f94 Insert jobs according to stage Matthias Volk 2017-05-15 17:15:10 +0200
  • 982538bfec Use jobs instead of matrix Matthias Volk 2017-05-15 17:11:15 +0200
  • 822d098caa Next fix Matthias Volk 2017-05-15 16:40:45 +0200
  • 120bf729d4 Fixed parsing issue Matthias Volk 2017-05-15 16:36:41 +0200
  • 7dc71ff12b Generate travis file Matthias Volk 2017-05-15 16:29:24 +0200
  • 811ca84944 Cd build Matthias Volk 2017-05-15 12:52:39 +0200
  • 8aff592e10 Try beta feature of build stages Matthias Volk 2017-05-15 12:30:20 +0200
  • 19b9ca14d0 Decreased timeout Matthias Volk 2017-05-12 14:23:11 +0200
  • 18798f7950 An existing file is also writable Sebastian Junges 2017-05-12 11:23:44 +0200
  • 87f494627c Fixes after carl update in order to get ginac from carl. Sebastian Junges 2017-05-11 22:31:13 +0200
  • d88350e556 Merge remote-tracking branch 'upstream/master' Matthias Volk 2017-05-11 15:51:38 +0200
  • d655621ea1 Fixed seg fault when building model valuations TimQu 2017-05-11 13:13:13 +0200
  • c4d6c1b787 Added tests in Release mode Matthias Volk 2017-05-11 12:03:06 +0200
  • c1d2fbf73c Output on test failure Matthias Volk 2017-05-11 10:58:58 +0200
  • ce41123049 Cache timeout and tests Matthias Volk 2017-05-11 09:47:56 +0200
  • 3557399336 Support for Debian 9 Matthias Volk 2017-05-10 18:17:00 +0200
  • 94590ff5b9 Several changes Matthias Volk 2017-05-10 17:29:40 +0200
  • d810595f11 Fixed copy in before_cache Matthias Volk 2017-05-10 17:05:01 +0200
  • 9d441d21af More debug output Matthias Volk 2017-05-10 16:41:16 +0200
  • 927a8f93cc fixed translation of rational numbers to mathsat expressions TimQu 2017-05-10 16:33:06 +0200
  • dcedea5a08 Caching from docker as well Matthias Volk 2017-05-10 15:59:01 +0200
  • 6b2db852be Ruby is needed in docker Matthias Volk 2017-05-10 14:11:23 +0200
  • 1e720a97df Next try with docker and Ubuntu Matthias Volk 2017-05-10 13:33:08 +0200
  • 25be35aa50 First test of Travis, docker and Ubuntu 16.10 Matthias Volk 2017-05-10 12:57:25 +0200
  • 453e31ef67 First try on docker for Ubuntu 16.10 Matthias Volk 2017-05-10 11:27:47 +0200
  • b7e64cb191 Increased timeout Matthias Volk 2017-05-10 10:38:09 +0200
  • c2373a7cd4 Test timeout Matthias Volk 2017-05-10 10:03:09 +0200
  • c2261d2185 Make all Matthias Volk 2017-05-09 21:43:25 +0200
  • dc3634910a Make aggain Matthias Volk 2017-05-09 19:41:28 +0200
  • 7a3d9b32ed Folding in travis Matthias Volk 2017-05-09 18:37:47 +0200
  • d8cc0428f4 Next test Matthias Volk 2017-05-09 17:37:48 +0200
  • e6af59c23f Make verbose Matthias Volk 2017-05-09 11:10:24 +0200
  • 2ff20b58ce More globs Matthias Volk 2017-05-08 17:31:38 +0200
  • 29687ca5d5 added some statistics output TimQu 2017-05-08 16:52:39 +0200
  • e49de6434b fix for multi-obj preprocessor TimQu 2017-05-08 16:50:45 +0200
  • 9f963a6ace Added mtime_cache script Matthias Volk 2017-05-08 13:01:23 +0200
  • 530802c179 Try building storm with cached resources Matthias Volk 2017-05-08 10:53:25 +0200
  • 9ebb2b9160 Try only building resources Matthias Volk 2017-05-08 10:12:56 +0200
  • 8f42bd2ec0 moved to new sparsepp version and made the appropriate changes dehnert 2017-05-06 16:12:00 +0200
  • 1eac717c47 Merge branch 'master' into smt-based-multi-objective TimQu 2017-05-05 19:36:32 +0200
  • 267768a5b6 enabled markov automata with rationals TimQu 2017-05-05 19:24:34 +0200
  • 9aa7dd6b4d Cache build directory Matthias Volk 2017-05-05 17:48:14 +0200
  • f6963f5bd1 Fixed translation of z3 expressions using the distinct operator (n-ary !=) to storm expressions TimQu 2017-05-05 15:59:26 +0200
  • 3d4d23691c fixed translation of mathsat's rational number expressions to storm's rational number expressions TimQu 2017-05-05 15:58:13 +0200
  • 748e100aad fixed/improved .dot output for MAs and Mdps. We now also display the index of each choice. TimQu 2017-05-05 15:54:04 +0200
  • 1c768c1ceb constraint based tests for multi-obj MAs TimQu 2017-05-05 15:51:01 +0200
  • 9c8531d40a constraint based achievability queries TimQu 2017-05-05 15:50:05 +0200
  • d54dd25a96 Just compile libstorm Matthias Volk 2017-05-05 15:47:46 +0200
  • 50fc3b1922 Fixed path in travis helper script Matthias Volk 2017-05-05 13:46:27 +0200
  • bb5a363689 Use scripts from https://github.com/google/fruit Matthias Volk 2017-05-05 13:37:02 +0200
  • b82e0608e5 Fix for CheckTask: now properly updating uperator information to make nested formulas work again (pointed out by Matt S Bauer) dehnert 2017-05-05 08:24:31 +0200
  • 4f1c3d5a6d Removed already installed packages Matthias Volk 2017-05-04 17:53:24 +0200
  • 9b7517d8bc Started working on travis support Matthias Volk 2017-05-04 17:14:41 +0200
  • 5c338b0092 added missing file extension TimQu 2017-05-04 09:23:21 +0200
  • b8229da6cd disabled quantitative query tests for constraint based checking TimQu 2017-05-03 19:21:30 +0200