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

Commit Graph

  • ced0d3fbb9 Assertion requiring equal bitsizes of BitVectorHashMap and key Matthias Volk 2018-09-13 16:08:42 +0200
  • 92193cfb08 WIP: Check assumptions on samples Jip Spel 2018-09-13 14:54:06 +0200
  • ee87c50313 fixed some issues related to jani parsing TimQu 2018-09-13 13:33:31 +0200
  • 5d21109624 Removed redundant method findBucketToInsert() Matthias Volk 2018-09-13 12:58:53 +0200
  • 46e39e6a6e Removed statistics in BitVectorHashmap which were only used for debugging purposes Matthias Volk 2018-09-13 11:40:56 +0200
  • d0461f168b support for negative assignment levels TimQu 2018-09-13 10:01:54 +0200
  • 70b79caf41 Travis: Use carl tag 18.08 to avoid problems with C++17 Matthias Volk 2018-09-12 18:18:21 +0200
  • 0e0a3dd9af Fixed problem with BitVector size mismatch for DFT states Matthias Volk 2018-09-12 18:17:39 +0200
  • 3fd9522770 Replaced permutation assertion by exception to give better warning Matthias Volk 2018-09-12 18:12:59 +0200
  • 7ee196bdbb jani2jani conversions in storm-conv TimQu 2018-09-12 16:19:41 +0200
  • 7c61a16d91 fixes for array expressions, support to translate properties that consider array expressions, translating array models in cli TimQu 2018-09-12 16:16:33 +0200
  • 274bfef652 started to extend storm-conv for array elimination TimQu 2018-09-12 14:29:48 +0200
  • 69cbc28547 fixes for arrays TimQu 2018-09-12 12:51:47 +0200
  • a178f4563f slight polishing of valid-block-mode treatment, also for JANI dehnert 2018-09-11 21:06:14 +0200
  • 2ff18771eb adding a corrected valid-block-mode for game-based abstraction dehnert 2018-09-11 19:51:35 +0200
  • ba68562740 moved array variable replacement information into VariableInformation TimQu 2018-09-11 18:38:32 +0200
  • ed45fa80e6 debugging array elimination TimQu 2018-09-11 18:00:51 +0200
  • fdd3334e6f properly implemented model features TimQu 2018-09-11 17:19:21 +0200
  • 62893e01cf changing debug output slightly dehnert 2018-09-11 15:41:56 +0200
  • a7bb70f698 exporting array expressions TimQu 2018-09-11 15:29:08 +0200
  • 6ab7859c84 fixing more of Lindas issues dehnert 2018-09-11 14:10:51 +0200
  • 581410c54b Add check acyclic Jip Spel 2018-09-11 11:16:15 +0200
  • c3d40d634b started working on the github issues by Linda dehnert 2018-09-10 22:57:06 +0200
  • c256bd1677 Fix derivative comparison MonotonicityChecker Jip Spel 2018-09-10 14:04:13 +0200
  • e2b5d6fcb1 automatically switching to Eigen as default when using exact mode dehnert 2018-09-10 14:03:46 +0200
  • 9d02519b01 Allow more than 2 outgoing transitions Jip Spel 2018-09-10 13:41:49 +0200
  • 21aabc5b05 fixing treatment of zero-states in game solver causing problems in policy iteration and non-unique solutions dehnert 2018-09-10 12:44:56 +0200
  • 7c19299488 Handle cycles in pMCs Jip Spel 2018-09-10 11:20:20 +0200
  • 90c325a38f Make nodes variable before using it Jip Spel 2018-09-10 10:10:33 +0200
  • 51be532695 pulled out parsing from abstraction-refinement classes dehnert 2018-09-07 22:22:26 +0200
  • 6aaafea554 added possibility to lift transient edge destination assignments to the edge by scaling with the probability (only if this preserves the considered properties). TimQu 2018-09-07 16:36:05 +0200
  • e2cb68b31f Enable array elimination in jit builder TimQu 2018-09-07 13:59:49 +0200
  • c5a0a057c8 array elimination and assignment levels in janiNextStateGenerator TimQu 2018-09-07 13:59:29 +0200
  • dc52e9b056 Create copy of lattice and assumptionslist at earlier point Jip Spel 2018-09-07 12:57:56 +0200
  • 728dc9e8a4 Fix TODO Jip Spel 2018-09-07 09:29:47 +0200
  • 2c9cefe7cc Use predefined constants Jip Spel 2018-09-07 09:23:33 +0200
  • 83797afc5b Remove TODO AssumptionMaker (clean up) Jip Spel 2018-09-06 15:06:07 +0200
  • bb1f1a3701 Change deepCopy into constructor Jip Spel 2018-09-06 14:34:48 +0200
  • 19475b30b9 Fix issue with deepCopy not containing all transitions Jip Spel 2018-09-06 14:11:52 +0200
  • 2e4991a75e TODO added create deep copy not yet working correctly Jip Spel 2018-09-06 13:46:57 +0200
  • 28b77e6a7d Create MonotonicityChecker and fix some bugs in AssumptionMaker Jip Spel 2018-09-06 13:08:01 +0200
  • 4aff82c649 array eliminator replaces lvalues and variables TimQu 2018-09-05 18:54:20 +0200
  • 32180591c0 extended jani datastructures TimQu 2018-09-05 18:53:58 +0200
  • dadf571934 const and non-const jani traverser TimQu 2018-09-05 18:52:12 +0200
  • 2a93b89c22 Create AssumptionMaker Jip Spel 2018-09-05 15:53:21 +0200
  • 6564abd434 jani expression substitution now also works for array expressions TimQu 2018-09-03 13:06:50 +0200
  • ea6b211703 fixed storing the wrong pointers to Variables in LValues TimQu 2018-09-03 09:15:27 +0200
  • 5e01151617 jani-array fixes TimQu 2018-09-02 12:09:51 +0200
  • 234671fdca fixes to include paths dehnert 2018-08-31 19:09:38 +0200
  • dac431b263 parsing of jani-arrays TimQu 2018-08-31 17:28:36 +0200
  • 0a9b99ef2c Merge branch 'master' into gamebased dehnert 2018-08-31 12:56:45 +0200
  • 43eebf8e05 Return tuple and add assumptions Jip Spel 2018-08-31 12:35:14 +0200
  • 34c87453fb Implement extension of lattice with assumptions Jip Spel 2018-08-31 11:24:45 +0200
  • 59a81831f3 fixing bug in relevant states computation of menu-game-based abstraction dehnert 2018-08-31 10:21:47 +0200
  • 785dbbdcdb CMake version parsing of z3 without z3 binary Matthias Volk 2018-08-30 18:30:23 +0200
  • 943de2e17c changing abstraction options slightly dehnert 2018-08-30 15:07:01 +0200
  • 5706831ad6 fixing settings/tests dehnert 2018-08-30 14:28:31 +0200
  • 53e9179722 CMake more stable in case z3 version is not obtained Sebastian Junges 2018-08-30 14:06:40 +0200
  • 8ab3ea991d fix in drn parser Sebastian Junges 2018-08-30 14:05:57 +0200
  • b6e48b35cc Implement first version of LatticeExtender Jip Spel 2018-08-29 12:35:19 +0200
  • 66a956e121 Fixed return Matthias Volk 2018-08-29 11:25:15 +0200
  • 1279e9714e Merge branch 'master' into dft_gspn_new Matthias Volk 2018-08-29 11:05:47 +0200
  • a9274d841c Merge branch 'master' into jani-arrays TimQu 2018-08-29 10:17:07 +0200
  • 617f3798c3 Merge branch 'master' into janiTests TimQu 2018-08-29 09:12:38 +0200
  • 539b3230eb when exporting jani, eliminate reward accumulation kinds whenever they do not have any effect TimQu 2018-08-29 08:56:57 +0200
  • 8050f8fc67 eliminate reward accumulations on jani level TimQu 2018-08-29 08:54:28 +0200
  • 6cc0369a1c added JaniTraverser to conveniently traverse all components of a jani model. TimQu 2018-08-29 08:53:37 +0200
  • 1714126a6f traverser for jani models TimQu 2018-08-28 16:43:16 +0200
  • 9e8d910a49 WIP Add LatticeExtender Jip Spel 2018-08-28 16:25:03 +0200
  • a739ce38f1 export of reward accumulations TimQu 2018-08-28 15:18:03 +0200
  • 831f07e867 eliminate reward accumulations whenever possible TimQu 2018-08-28 15:03:45 +0200
  • 701f3832b1 parsing reward accumulations TimQu 2018-08-28 10:19:58 +0200
  • b0b0623fcf Add matrix declaration Jip Spel 2018-08-28 12:52:30 +0200
  • 5aec480a1e Clean up Jip Spel 2018-08-28 12:35:34 +0200
  • ee1dcbd483 fragment checker checks reward accumulations TimQu 2018-08-27 18:42:28 +0200
  • 4302aa0be0 added missing include TimQu 2018-08-27 18:41:43 +0200
  • 76b2eb2ee9 added reward accumulation to formulas TimQu 2018-08-27 16:36:54 +0200
  • 1c20abc1b5 Fixed return Matthias Volk 2018-08-27 16:48:22 +0200
  • 454f9350d7 Export proprties in DFT->GSPN->Jani file Matthias Volk 2018-08-27 16:48:07 +0200
  • 8c2a44494b More general method for building GSPN-Jani properties Matthias Volk 2018-08-27 16:29:20 +0200
  • 234ddb7cff fixed compilation of JaniParser TimQu 2018-08-27 14:17:07 +0200
  • e7dc7acf8e Cleanup Jip Spel 2018-08-27 14:13:10 +0200
  • a012539323 cleared some TODOs in the Jani Parser TimQu 2018-08-27 12:06:19 +0200
  • ee8971c608 Clean up Jip Spel 2018-08-27 10:22:22 +0200
  • d2e754c302 Replace transformation to State Vector with transformation in map Jip Spel 2018-08-27 09:58:26 +0200
  • cbd3880d87 General method for adding transient variables in GSPN->Jani conversion Matthias Volk 2018-08-24 15:10:34 +0200
  • 953d570ff0 fix in syntacticalEquality checker TimQu 2018-08-24 11:00:17 +0200
  • 80cf0982a9 WIP: parameter lifting Jip Spel 2018-08-24 09:39:07 +0200
  • ce3b63da12 Fixed json export settings Matthias Volk 2018-08-23 17:41:58 +0200
  • a7ffafb7d7 Merge from master Matthias Volk 2018-08-23 17:39:05 +0200
  • c136b9c628 Removed old jani file settings Matthias Volk 2018-08-23 17:15:16 +0200
  • 6f8787b6f0 Add one possible solution for critical states Jip Spel 2018-08-23 14:02:01 +0200
  • ad88992ba2 export gspns to ctmcs/mdps if no intermediate/timed transitions occur. TimQu 2018-08-23 13:44:09 +0200
  • 251c9e2141 added option to make the json export more compact TimQu 2018-08-23 09:25:18 +0200
  • 915a8b24ec Remove superfluous vars Jip Spel 2018-08-23 10:11:59 +0200
  • 8bbf4b4543 Change vector to set, add error message if more than two successors for one state, add documentation Jip Spel 2018-08-23 10:11:30 +0200
  • e038fb64be Jani: export the correct accumulation parameters for expected reward properties TimQu 2018-08-22 18:31:52 +0200
  • 0f97eb89db binary storm-gspn now exits with 0 if no gspnfile is given TimQu 2018-08-22 14:16:44 +0200
  • 4861b8d4b4 More robust parsing of capacities and allowing constants in GSPN properties TimQu 2018-08-22 12:56:08 +0200
  • 1bce5935fa Update documentation Jip Spel 2018-08-22 09:38:26 +0200