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

Commit Graph

  • 2ba70e964c Added hasParameters() and supportsParameters() for symbolic models Matthias Volk 2018-05-18 13:45:25 +0200
  • 6b91485382 Removed redundant file Matthias Volk 2018-05-18 11:35:16 +0200
  • 057f8798a6 avoiding bottom state computation when possible dehnert 2018-05-17 21:55:45 +0200
  • 433b23d989 more fixes to (JANI) game-based abstraction dehnert 2018-05-17 16:46:23 +0200
  • 627a79fe35 fix to restriction to relevant state space in game-based abstraction dehnert 2018-05-17 09:28:09 +0200
  • f52aab0012 fixed out-of-bounds-labelling, added overlapping guards building, and some improved error messages if something goes wrong with highlevel counterex generation Sebastian Junges 2018-05-16 22:58:36 +0200
  • 91bbe85a07 builder options for labeling overlapping guards Sebastian Junges 2018-05-16 22:55:34 +0200
  • 7f8a830b5a refined detection of trivial initial states restriction of JANI models dehnert 2018-05-16 16:02:20 +0200
  • 87843e084e several fixes related to game-based abstraction dehnert 2018-05-16 15:53:35 +0200
  • fa0da0bc7f fixes to parser dehnert 2018-05-15 22:16:51 +0200
  • 5271ab558c Merge branch 'master' into gamebased dehnert 2018-05-15 15:07:10 +0200
  • ceea5198d6 fixed detection of unreachability of target state in MaxSAT-based high-level counterexample generation dehnert 2018-05-15 15:07:02 +0200
  • 01dc010c08 Reworked POR DFT element and added dontCare support Alexander Bork 2018-05-14 22:02:25 +0200
  • 4ec2bc0583 fixed bug in jani model generation dehnert 2018-05-14 16:42:27 +0200
  • d66047e3b7 few fixes to jani game-based abstraction dehnert 2018-05-14 07:59:21 +0200
  • 4642a968c7 Merge branch 'master' into gamebased dehnert 2018-05-13 20:09:32 +0200
  • dfd6c624c7 Reworked PAND DFT element to suit the new "exclusive" template and added dontCare support Alexander Nikolai Bork 2018-05-12 01:07:19 +0200
  • ce13ce40a9 Added dontCare transformation support for VOT DFT elements. Alexander Nikolai Bork 2018-05-11 13:03:41 +0200
  • e7926b10c2 allow counterexamples for true jani models Sebastian Junges 2018-05-11 11:21:45 +0200
  • c517ec14b1 support for liveness cex in jani Sebastian Junges 2018-05-11 11:20:58 +0200
  • 0726dfc7a0 bugfix only add label out of bounds is option is set and state is present Sebastian Junges 2018-05-11 11:20:22 +0200
  • 875764c472 Added dontCare transformation support for BE, AND and OR DFT elements. Alexander Nikolai Bork 2018-05-09 20:08:28 +0200
  • e069925854 Merge branch 'master' into dft_smt Matthias Volk 2018-05-09 11:52:03 +0200
  • c9b66b2492 Added comments Matthias Volk 2018-05-08 15:40:55 +0200
  • 0674f88cf5 Added option for merging DC and Failed places Matthias Volk 2018-05-08 15:22:12 +0200
  • ad8350c684 Make elements for DC propagation choosable in GSPN transformation Matthias Volk 2018-05-08 09:31:07 +0200
  • e6090d2d2c Removed unused code Matthias Volk 2018-05-08 08:57:22 +0200
  • 5b6383b5ef fix gspn export to pnml Sebastian Junges 2018-05-06 22:28:30 +0200
  • 7a2a46cae9 fix warning about non-const comparison operator in set Sebastian Junges 2018-05-06 22:18:51 +0200
  • 89f3aac33f add error messages for sparse model building when lower bounds for variables are above upper bounds Sebastian Junges 2018-05-06 22:18:15 +0200
  • 61925d1c98 add option for sparse model builder to add a state encoding out-of-bounds state valuations to enable analysis of buggy models Sebastian Junges 2018-05-06 22:17:00 +0200
  • d77f4e7564 gspn pnml export for capacities Sebastian Junges 2018-05-03 00:00:45 +0200
  • 61f31fb919 improved handling of capacities by switching to boost::optional Sebastian Junges 2018-05-03 00:00:10 +0200
  • 1c9f7b0f2f translate prism to jani with a suffix for location names etc when doing this for multiple models Sebastian Junges 2018-05-02 23:42:00 +0200
  • 33ac2e0793 make jani models copyable Sebastian Junges 2018-05-02 23:41:08 +0200
  • 56df741d32 formula parser does not depend on jani model Sebastian Junges 2018-05-02 23:38:06 +0200
  • 687bb0dd86 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Sebastian Junges 2018-05-02 23:19:52 +0200
  • fdcbd6369c simple sanity check for bounded integers in jani Sebastian Junges 2018-05-02 20:52:16 +0200
  • 5b678f524a removed old spurious output Sebastian Junges 2018-05-02 20:51:54 +0200
  • a67b1a73da Fixed issues in storm-gspn cmdline Matthias Volk 2018-05-02 15:58:36 +0200
  • bb6fb04f72 fixing volatile k-shortest path test that returns different (yet correct) results on different machines/compilers because of double imprecisions dehnert 2018-04-26 09:26:17 +0200
  • 60b1ef5a57 Travis: test against Ubuntu 18.04 Matthias Volk 2018-04-25 17:17:12 +0200
  • eaf13b1d69 Travis: use absolute path Matthias Volk 2018-04-20 17:56:30 +0200
  • df52f3fbb4 Travis: move timeout into docker container as suggested by jklein Matthias Volk 2018-04-20 11:16:02 +0200
  • 331e82da1e Travis: use movesrwth docker containers Matthias Volk 2018-04-19 16:26:23 +0200
  • b8794fd9c8 Made the default multiplier matching the selected equation solver. TimQu 2018-04-19 13:58:55 +0300
  • 300ccd731f Use to_string in DRN exporter Matthias Volk 2018-04-18 16:32:45 +0200
  • ec411ffc78 Typos Matthias Volk 2018-04-18 16:32:20 +0200
  • 2658a02604 Fixed compiler warnings for unused lambda captures Matthias Volk 2018-04-18 16:31:14 +0200
  • 4378279c64 fixes second half of github issue #18 dehnert 2018-04-17 16:28:03 +0200
  • 6d445e38af fixes github issue #18 dehnert 2018-04-17 15:04:42 +0200
  • 0f357366cb Improved variable names in findModularisationRewrite Matthias Volk 2018-04-17 14:11:17 +0200
  • 006ccaa2ee Build all labels for DFT model if export is enabled Matthias Volk 2018-04-17 13:46:42 +0200
  • 87edc3abe0 Better debug output Matthias Volk 2018-04-17 13:46:10 +0200
  • c9496a255b corrected tests (pointed out by jklein) dehnert 2018-04-13 11:25:47 +0200
  • 844608488a using max_digits10 to increase precision enough to uniquely identify double (as proposed by Joachim) dehnert 2018-04-12 14:20:46 +0200
  • 533e48bdbc increasing precision for rational to ExprTk rational literal conversion dehnert 2018-04-12 14:12:46 +0200
  • 759ea3604f fixed expression to ExprTk translation for rational literals (pointed out by Joachim Klein) dehnert 2018-04-12 14:05:58 +0200
  • 0fed84c5a9 removed superfluous return dehnert 2018-04-12 09:06:50 +0200
  • bf88eca92f Export DRN format for model composed from DFT modularisation Matthias Volk 2018-04-10 15:25:45 +0200
  • c18340b76a added mod as binary operation in expressions and slightly extended JANI support for filters dehnert 2018-04-09 22:08:04 +0200
  • 618d300914 fixed minor issue in MILP minimal label set generation dehnert 2018-04-09 18:45:47 +0200
  • cab33179e7 Typo Matthias Volk 2018-04-08 22:09:16 +0200
  • e513015b49 Compute all reachabilities probabilities in a forward manner Matthias Volk 2018-04-08 22:09:00 +0200
  • 692587495f fixed bug in quotient extraction dehnert 2018-04-07 11:22:43 +0200
  • ede791cff7 fixing bug in Z3 LP solver dehnert 2018-04-06 15:59:02 +0200
  • 93bf17f54b remove debug output dehnert 2018-04-06 15:45:16 +0200
  • 7636a0339d removed warning for missing naming capabilities in Z3 LP solver dehnert 2018-04-06 15:16:39 +0200
  • e019bf19d1 fixing Z3 hint handling dehnert 2018-04-06 14:50:46 +0200
  • 3a464d7a6b Fixed issue for clang3.8 TimQu 2018-04-06 10:53:10 +0200
  • 06e3d4a331 fixing issues in gmmxx TBB multiply-and-reduce dehnert 2018-04-05 22:56:36 +0200
  • 237d390e40 reworked version retrieval slightly dehnert 2018-04-05 14:30:09 +0200
  • 869271259e updated git version retrieval cmake plugin dehnert 2018-04-05 14:29:29 +0200
  • 32d19e6f0e debug output in git version parsing dehnert 2018-04-05 11:05:50 +0200
  • 333d1ae375 Function for computing all transient probabilities Matthias Volk 2018-04-03 23:41:29 +0200
  • 4e60f3e137 updated changelog TimQu 2018-04-03 17:22:55 +0200
  • 7002138aeb removed setPrecision in solver interface since this is now covered via storm::Environment TimQu 2018-04-03 17:01:59 +0200
  • 7cdc7bd21d progress measurement can now correctly handle the case where maxcount = 0 TimQu 2018-04-03 17:00:52 +0200
  • f5511f4213 removed obsolete 'inplace' setting for multiplier TimQu 2018-03-28 18:01:29 +0200
  • 61e94610fd Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2018-04-03 11:13:27 +0200
  • 2468de47f9 jani -- get expression manager signature now looks more like prism -- get (expression) manager Sebastian Junges 2018-04-03 11:12:27 +0200
  • 461668bc84 change default value of an option for abstraction dehnert 2018-04-02 21:54:49 +0200
  • 4d4b178853 counterexamples options: add silent and open to outside Sebastian Junges 2018-03-31 16:32:30 +0200
  • dc92696cc3 Jani: make edge-index encoding static functions Sebastian Junges 2018-03-31 16:31:54 +0200
  • 7f7778533a Typos Matthias Volk 2018-04-02 17:46:31 +0200
  • d09bcc2e3b Merge remote-tracking branch 'origin' into gamebased dehnert 2018-04-02 13:09:57 +0200
  • 64cd0ae212 optimizations to trace formula generation dehnert 2018-04-02 13:09:46 +0200
  • 21c970f8f7 added dd-to-sparse engine that builds the model as a DD and then transforms the whole model to a sparse representation dehnert 2018-04-02 13:02:17 +0200
  • 03a94016b3 workaround for bug in clang (bug report filed) dehnert 2018-04-02 13:01:44 +0200
  • 1169195be7 some fixes (in particular for warnings) dehnert 2018-03-31 17:24:45 +0200
  • 72c1e79ccd Mention -pc flag in error message Matthias Volk 2018-03-31 13:18:31 +0200
  • 3ad85ba0e6 fixes and improvements for game-based abstraction dehnert 2018-03-30 23:12:00 +0200
  • a13ed96966 first working version of sparse game-based abstraction refinement dehnert 2018-03-29 19:18:14 +0200
  • a31929c00f Travis: build portable version of Storm Matthias Volk 2018-03-29 17:05:53 +0200
  • 14bad02bc4 fixes to player 1 choice labeling dehnert 2018-03-29 15:02:00 +0200
  • ef1cbae83c Tests for DRN parser Matthias Volk 2018-03-29 14:21:05 +0200
  • db32a91c7c Changed logging level for some output Matthias Volk 2018-03-29 13:45:20 +0200
  • 3e2aba515d Added support for exit rates and Markovian/probabilistic states in DRN Format Matthias Volk 2018-03-29 13:44:23 +0200
  • 692ded94cf Typo Matthias Volk 2018-03-29 13:43:26 +0200
  • 76d5ddad30 Minor improvements in DRN parser Matthias Volk 2018-03-29 13:42:56 +0200