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

Commit Graph

  • 905f6fc970 Create lattice from model and formulas Jip Spel 2018-08-22 09:17:31 +0200
  • 128d428fcc Add .dot representation for mc Jip Spel 2018-08-21 16:16:23 +0200
  • c124ebcc93 Fixed a Jani-related issue when adding assignments to OrderedAssignments TimQu 2018-08-21 15:44:54 +0200
  • da691c8102 Add .dot representation for lattice Jip Spel 2018-08-21 14:23:46 +0200
  • 5f201da6da correctly parse templates, weights, priorities TimQu 2018-08-21 13:44:01 +0200
  • 92bd07c9c5 Allow monotonicity analysis on both Until and Eventually formulas Jip Spel 2018-08-21 13:21:21 +0200
  • 1aa8f409cb Change error messages + add new ones Jip Spel 2018-08-21 11:32:08 +0200
  • 1f40a56ed8 updated changelog TimQu 2018-08-21 10:41:35 +0200
  • a44eed65e8 allowing constant definitions for gspns via cli TimQu 2018-08-21 10:39:49 +0200
  • 3215af6fc0 Implemented single- infinite- and k- server semantics for timed gspn transitions TimQu 2018-08-21 10:39:11 +0200
  • 383814681d One map with pair of bool instead of two maps for monotonicity Jip Spel 2018-08-21 09:20:28 +0200
  • e83dad0963 Add check on amount of formulas, fix typo Jip Spel 2018-08-20 17:15:46 +0200
  • 49930ebc9e fixed help text TimQu 2018-08-20 14:33:06 +0200
  • 7f601058a1 flatten option should not require module prefix TimQu 2018-08-20 14:19:18 +0200
  • 6ac0782a18 Remove need for bisimulation Jip Spel 2018-08-20 11:43:56 +0200
  • 1af5670750 Throw error when bisimulation not set, change output monotonicity Jip Spel 2018-08-20 11:12:03 +0200
  • 0116837956 Check dtmc or mdp for simplification Jip Spel 2018-08-20 10:57:14 +0200
  • f9f6b90cc2 updated changelog TimQu 2018-08-20 09:52:05 +0200
  • 4b3e7849ed jani parser parses array variables TimQu 2018-08-17 17:18:08 +0200
  • 8202f77943 array expressions TimQu 2018-08-17 17:17:43 +0200
  • 39b8ac6c18 Analyse monotonicity for each variable Jip Spel 2018-08-17 14:01:24 +0200
  • 1536aeab47 Add keep track of time Jip Spel 2018-08-17 12:01:19 +0200
  • c6e6331db2 Move creation of Lattice to Lattice class Jip Spel 2018-08-17 11:47:52 +0200
  • 5f6a894a32 Clean up Jip Spel 2018-08-17 10:57:03 +0200
  • 8c3fb65ef9 Simplify before preprocessing Jip Spel 2018-08-17 10:48:01 +0200
  • 9bc402a20b Remove states with transition with probability 1 from model Jip Spel 2018-08-17 10:04:37 +0200
  • 8da922e4d5 started to include array support TimQu 2018-08-17 08:31:26 +0200
  • 5b78393425 Fixed issues related to allowing local variables when converting from prism to jani TimQu 2018-08-16 18:37:32 +0200
  • 817c5a218b making the time bound for generated gspn properties real valued TimQu 2018-08-16 18:35:33 +0200
  • bd475e99eb fixed flattening models with constants TimQu 2018-08-16 17:37:16 +0200
  • 394ef9f5b3 writing the correct model name into the jani file TimQu 2018-08-16 17:36:41 +0200
  • 17371e756c generate standard gspn properties automatically TimQu 2018-08-16 16:42:33 +0200
  • 299f3f5c05 disallowing capacity 0 TimQu 2018-08-16 16:41:03 +0200
  • aa630ce62b Monotone increasing in all parameters implemented Jip Spel 2018-08-16 14:25:38 +0200
  • b782d80a26 Changed nodes implementation in Lattice Jip Spel 2018-08-16 11:04:01 +0200
  • 6a11927b55 parsing pnpro files with constant definitions TimQu 2018-08-16 10:17:24 +0200
  • 629c305456 Added option to specify one global capacity for all places of a gspn TimQu 2018-08-16 10:16:09 +0200
  • d23746d7b6 Fixed computation of extended priorities for SPAREs leading to non-determinism when DC and Failed are merged Alexander Bork 2018-08-15 17:19:27 +0200
  • 1364ec8729 Clean up Jip Spel 2018-08-15 17:03:26 +0200
  • f638142ad9 Travis: Use Ubuntu 18.04 after support for 17.10 ended Matthias Volk 2018-08-15 10:02:28 +0200
  • 2c4d5c0d3f Delete Transfomer class Jip Spel 2018-08-14 10:21:14 +0200
  • 5d90eb013b Merge branch 'master' into janiTests TimQu 2018-08-14 09:37:03 +0200
  • c1758b8ea1 Remove duplicate code Jip Spel 2018-08-14 09:06:34 +0200
  • 9f8aa986ce Refactor creating State vector Jip Spel 2018-08-13 13:44:54 +0200
  • 116dbc8bba Refactor constructor Lattice Jip Spel 2018-08-13 11:34:08 +0200
  • baf5cbb074 Remove superfluous methods Jip Spel 2018-08-13 11:14:00 +0200
  • fc453143c2 missing includes.. TimQu 2018-08-11 11:28:11 +0300
  • 467abd72e9 Made model checker tests also build the model via conversion to Jani and with the Jit Builder. TimQu 2018-08-10 07:59:26 +0300
  • 19c6472843 separating declaration/implementation for storm-conv api TimQu 2018-08-09 08:14:20 +0200
  • d35bd548a8 Fixed SEQ DC computation Alexander Bork 2018-08-09 17:36:33 +0200
  • 3e8959c866 DFT: fixed stringstream clearing Matthias Volk 2018-08-08 15:07:28 +0200
  • 020c480e9c DFT: export gate dependent information to json Matthias Volk 2018-08-08 14:55:26 +0200
  • d4efcd49e3 DFT: no error for optional json arguments Matthias Volk 2018-08-08 14:55:04 +0200
  • 1990b0a1c9 DFT: updated json export Matthias Volk 2018-08-08 14:29:00 +0200
  • 48efde755b DFT: export to JSON as string Matthias Volk 2018-08-08 13:22:54 +0200
  • 369d106f99 DFT: load json from string Matthias Volk 2018-08-08 13:16:42 +0200
  • 856d62513b DFT: parse number from JSON Matthias Volk 2018-08-08 12:27:07 +0200
  • cbd709f0cd Fixed assertion Matthias Volk 2018-08-08 12:26:10 +0200
  • a34ca5c9ac dont go on as soon as trivial command set is necessary Sebastian Junges 2018-08-07 21:08:01 -0700
  • 73900f1bbe advanced stopping criteria for multi-counterexamples, additional measurements for cuts, an option to properly disable backward implications, and some cleaning Sebastian Junges 2018-08-07 21:07:15 -0700
  • ac9d9d6778 fix in counterexamples for lower bounds that was recently introduced Sebastian Junges 2018-08-07 20:56:30 -0700
  • 919dfeebae "number of edges" and "number of commands" in jani model / prism programs Sebastian Junges 2018-08-07 20:53:12 -0700
  • a21c6f7244 fixed wrong state action rewards in JaniNextStateGenerator. TimQu 2018-08-07 16:29:19 +0200
  • d8bc689259 Throw an exception instead of assertion when 'wrong' jani was detected TimQu 2018-08-07 16:27:25 +0200
  • 0332935451 Supporting TimeOperatorFormulas for MDPs and DTMCs in Sparse, Hybrid, and Dd engine TimQu 2018-08-06 13:40:31 +0200
  • d0e2d099bf AbstractModelChecker: In error messages, include class name of the actual model checker Joachim Klein 2018-08-04 15:01:55 +0200
  • da4dfc35a8 AbstractModelChecker: add getClassName() Joachim Klein 2018-08-04 15:00:04 +0200
  • ed2de09ce3 added function that reduces the nesting of expressions (e.g. when considering a big sum with many summands. This fixes stack overflows when translating expressions TimQu 2018-08-03 17:57:22 +0200
  • 2827da84ee Add TODOs Jip Spel 2018-08-03 13:12:38 +0200
  • dc88830acd First try Jip Spel 2018-08-03 12:45:27 +0200
  • 6449dee626 fixed typo TimQu 2018-08-02 16:14:52 +0200
  • e7eb80184e fixed wrong include.. TimQu 2018-08-02 16:14:43 +0200
  • c9cea88047 Export Storm-gspn headers as well Matthias Volk 2018-08-02 10:16:21 +0200
  • 910b6e6b22 fixed wrong include TimQu 2018-08-01 11:38:39 +0200
  • b3be56588f fixing time operator formulas TimQu 2018-07-31 22:27:02 +0200
  • 066facf3f1 fixed respecting the --globalvars option correctly... TimQu 2018-07-31 17:51:32 +0200
  • 611428c01f allowing constants in property bounds TimQu 2018-07-31 17:28:19 +0200
  • 9487223dc1 --globalvars option no longer requires a module prefix TimQu 2018-07-31 17:19:01 +0200
  • b4a1244d01 correct parsing of bounded until formulas with multiple bounds TimQu 2018-07-31 17:18:41 +0200
  • 56a5dcf7cb added setting in storm-conv to make variables global TimQu 2018-07-31 16:43:41 +0200
  • 5937131ff2 fixed and extended parsing of jani formulas with Emin or Emax operator TimQu 2018-07-31 16:43:04 +0200
  • fe71dfdf9b added export of reward-bounded until formulas TimQu 2018-07-31 16:42:01 +0200
  • 01549dfdea fixed segfaults when lifting transient destination assignments to the edge TimQu 2018-07-31 16:41:23 +0200
  • 8f179217d0 fixes for storm-dft and storm-gspn TimQu 2018-07-30 20:48:53 +0200
  • 52fc8c8e35 removed unused setting TimQu 2018-07-30 20:48:09 +0200
  • 41645c3f9a including the correct .h file in storm-parsers api TimQu 2018-07-30 20:47:47 +0200
  • 9563cb44cb made storm-pgcl use storm-conv TimQu 2018-07-30 20:47:17 +0200
  • d9ec0f8fcf removed include of old janiexportsettings TimQu 2018-07-30 20:46:46 +0200
  • f0d11afdb8 fixed compilation of tests TimQu 2018-07-30 20:46:19 +0200
  • 4a7a82627f storm-gspn and storm-dft now use functionalities of storm-conv TimQu 2018-07-30 14:16:18 +0200
  • c268926568 storm-pars no longer uses export settings TimQu 2018-07-30 14:15:42 +0200
  • 30d30a063c setting jani conversion options from settings TimQu 2018-07-30 14:15:00 +0200
  • 51c5c42319 Fixed export of expected time properties to jani TimQu 2018-07-30 10:23:05 +0200
  • 0fa361c393 displaying property name together with the property TimQu 2018-07-30 10:22:36 +0200
  • d343943cbd storm-conv should not fail if no input arguments were given TimQu 2018-07-30 10:15:28 +0200
  • 636d92894c Fixed an issue with time bounded properties specified in jani TimQu 2018-07-24 18:12:47 +0200
  • 31efde52c2 fixed case where no location variables were provided TimQu 2018-07-24 18:11:25 +0200
  • 35aa166f5b added possibility to check all available jani properties TimQu 2018-07-24 18:10:28 +0200
  • a4864f3c3d Using JaniExportSettings in storm-conv TimQu 2018-07-24 15:40:27 +0200
  • fbb734fbe2 Fixed using settings without the 'general' module TimQu 2018-07-24 15:39:07 +0200