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

Commit Graph

  • 9a0be7e9ca added first rpatl fragment checker tests Stefan Pranger 2021-09-03 15:15:25 +0200
  • fc18ea12d3 Merge pull request 'Cleanup SMG RPATL Model Checking' (#34) from smg_cleanup into main Stefan Pranger 2021-09-03 12:57:25 +0000
  • 1391b26e93 Removed unnecessary debug information Lukas Posch 2021-08-10 10:25:46 +0200
  • fb84fc6af0 Added a comment why this computeBoundedGlobally check happens. Lukas Posch 2021-08-10 10:14:12 +0200
  • 679279a339 By changing the computation we now allow lowerBounds in bounded-globally formulas Stefan Pranger 2021-09-03 14:56:30 +0200
  • 86c3b3d9c6 changed computeBoundedGloballyProbabilities computation by using computeBoundedUntilProbabilities Lukas Posch 2021-08-10 09:27:54 +0200
  • 4373c324f9 checks for bounds in SparseSmgRpatlModelChecker Lukas Posch 2021-08-09 15:42:50 +0200
  • 9fea23981a finished computeBoundedUntilProbability in SparseSmgRpatlHelper Lukas Posch 2021-08-09 15:25:47 +0200
  • 03ec53321e added updateStatesOfCoalition to GameViHelper Lukas Posch 2021-08-09 15:24:58 +0200
  • fefd6b0951 WIP helper functions in GameViHelper Lukas Posch 2021-08-06 15:49:02 +0200
  • c2d2c38c28 WIP computeBoundedUntilProbabilities in SparseSmgRpatlHelper Lukas Posch 2021-08-06 15:47:42 +0200
  • 28252a3caf added computeBoundedUntilProbabilities to SparseSmgRpatlModelChecker Lukas Posch 2021-08-06 15:45:05 +0200
  • 44d83b9fe0 added checks for bounds in computeBoundedGloballyProbabilities Lukas Posch 2021-08-06 15:44:17 +0200
  • 3f408d059c allow boundedUntilFormulas in rpatl Lukas Posch 2021-08-06 15:43:32 +0200
  • 75bacaa6b2 deleted BoundedGloballyGameViHelper Lukas Posch 2021-08-04 15:46:14 +0200
  • e5dd9ab90f small cleanup SparseSmgRpatlModelChecker Lukas Posch 2021-08-04 15:40:37 +0200
  • f4615614c1 use GameViHelper instead of BoundedGloballyGameViHelper Lukas Posch 2021-08-04 15:38:48 +0200
  • d222337715 added functionality of BoundedGloballyGameViHelper to GameViHelper Lukas Posch 2021-08-04 15:36:47 +0200
  • 6289788a68 small changes to fit to the GameViHelper.* Lukas Posch 2021-08-04 15:35:36 +0200
  • 65a5308809 small change in computation in computeNextProbabilities Lukas Posch 2021-08-04 14:35:03 +0200
  • b6ffa9a649 small change in the comments of computeGloballyProbabilities Lukas Posch 2021-08-04 14:33:17 +0200
  • 7bdb5e11a8 fixed case for empty relevantStates in computeBoundedGlobally Probabilities Lukas Posch 2021-08-04 14:31:46 +0200
  • 8301c3dc88 fixed case for empty relevantStates in computeUntilProbabilities Lukas Posch 2021-08-04 14:30:48 +0200
  • 6c6f501900 Merge pull request '[STORM PR] Fixes after LTL merge' (#47) from merge_pr_137 into main Stefan Pranger 2021-09-03 12:54:35 +0000
  • 90dba4cd5d adapted mdpprctlhelper call in MA model checker Stefan Pranger 2021-09-03 14:51:50 +0200
  • c19639d156 added missing method to visitor Stefan Pranger 2021-09-03 14:51:35 +0200
  • d53fafa078 fixed some changes which have been overwritten Stefan Pranger 2021-09-03 14:51:20 +0200
  • 85c5125610 removed duplicate code after big merge Stefan Pranger 2021-09-03 14:51:10 +0200
  • 814f7b036d Merge pull request '[STORM PR] LTL Model Checking#137' (#45) from merge_pr_137 into main Stefan Pranger 2021-09-03 12:37:24 +0000
  • 7e7d6defa0 Merge pull request #137 from tquatmann/ltl Tim Quatmann 2021-08-30 12:41:16 +0200
  • 3d96b0728d CI: Use spot in all existing configurations. Add a new configuration without Spot. Tim Quatmann 2021-08-28 13:32:23 +0200
  • e0e1b097eb Merge branch 'master' into ltl-github Tim Quatmann 2021-08-28 13:24:23 +0200
  • 1dab437496 Compare floating points upto precision instead == Daniel Basgöze 2021-08-26 12:47:15 +0200
  • 94ec1a7aeb Fix print_storm_rational_number Daniel Basgöze 2021-08-25 13:50:58 +0200
  • 78a10f201e Use memcpy instead of strcpy Daniel Basgöze 2021-08-25 13:43:29 +0200
  • 57874ff460 Remove C-style casts in storm_wrapper.cpp Daniel Basgöze 2021-08-25 13:40:27 +0200
  • 22a9703524 Remove erroneous mutex lock in sylvan_wrapper Daniel Basgöze 2021-08-25 13:09:51 +0200
  • 12111a91bd Use pass-by-value in constructor Daniel Basgöze 2021-08-24 18:09:49 +0200
  • 8de8f1517a Fix conversion ambiguity: Use convertNumber() Daniel Basgöze 2021-08-24 18:08:37 +0200
  • a34fcca339 Fix conversion ambiguity: Use 1 instead of 1.0 Daniel Basgöze 2021-08-24 18:06:26 +0200
  • ebd85a43d3 Fix conversion ambiguity: Use * instead of *= Daniel Basgöze 2021-08-24 18:04:11 +0200
  • 22388425d7 Remove unnecessary convertNumber Daniel Basgöze 2021-08-24 16:45:22 +0200
  • c6be1b6a92 Always define CLN_INCLUDE_DIR when available Daniel Basgöze 2021-08-24 15:33:38 +0200
  • 6420709a50 CI: Test GMP/CLN configurations and reduce tests Daniel Basgöze 2021-08-13 18:05:54 +0200
  • 1e60fa7914 LTLSchedulerHelper: make handling of overlapping ECs more explicit and reduced the amount of memory states. Tim Quatmann 2021-08-13 15:42:34 +0200
  • 5fe81952cb Removed an outdated TODO comment. Tim Quatmann 2021-08-13 15:33:54 +0200
  • 6af47eaadc new class for scheduler computation during LTL-MC hannah 2021-08-12 12:45:59 +0200
  • 8a26af29f9 allow HOA formulas for cslstar and pctlstar hannah 2021-08-11 21:01:29 +0200
  • 63a400ea5a added some documentation hannah 2021-08-11 20:42:44 +0200
  • 133219f3c7 using exact fractions in tests hannah 2021-08-11 18:12:03 +0200
  • 0713c5dccd skipDontCareStates-option for scheduler printing hannah 2021-08-11 17:08:05 +0200
  • e5b19643e8 dontCareStates can now be (non)deterministic and (un)defined hannah 2021-08-11 16:45:45 +0200
  • 24ba65f5e1 added documentation hannah 2021-08-11 15:44:17 +0200
  • 62cede1759 Added missing include. Tim Quatmann 2021-08-10 15:34:04 +0200
  • 6c7d6b0d2b Silenced some unused variable-warnings. Tim Quatmann 2021-08-10 14:38:01 +0200
  • 396b39a21b Fixed a typo (thanks @PrangerStefan) Tim Quatmann 2021-08-10 14:32:33 +0200
  • 4ddb9c4337 Some simplifications for memory structure. Tim Quatmann 2021-08-10 14:30:19 +0200
  • c46c711eb7 cpphoafparser: added missing include. Tim Quatmann 2021-08-10 12:53:44 +0200
  • 693d5470a3 Updated changelog a bit. Tim Quatmann 2021-08-09 18:21:44 +0200
  • dffc04a280 Cleaned up some includes for the model checkers. Tim Quatmann 2021-08-09 18:21:26 +0200
  • e92e32239b Support for globally and next formulae for Markov Automata and CTMC Tim Quatmann 2021-08-09 18:05:39 +0200
  • db16aa50e6 LTL Helper: Removed some debug output to reduce clutter Tim Quatmann 2021-08-09 17:51:43 +0200
  • a81f5e284b Further simplified LTLHelper Interface a bit. Support for LTL and HOA formulaes for *all* (sparse) model types Tim Quatmann 2021-08-09 17:12:59 +0200
  • 9cf3d6af5d Adding debug output and file I/O checks whenever parsing a HOA automaton from a file. Tim Quatmann 2021-08-09 17:10:44 +0200
  • 6310462060 Cleaned up dtmc and mdp helpers a bit. Tim Quatmann 2021-08-09 15:28:28 +0200
  • 3a12b1cc10 Model Checkers: Reduced code duplications by using a single `computeStateFormulaProbabilities` method Tim Quatmann 2021-08-09 15:22:22 +0200
  • 1207af13a2 symbolic and sparse models now have a public member `Representation` Tim Quatmann 2021-08-09 15:21:20 +0200
  • 10fc5d18c8 Clarified what a complex path formula is. Tim Quatmann 2021-08-09 13:49:05 +0200
  • b097a442ee Processed some TODOs in storm/logic Tim Quatmann 2021-08-09 13:48:51 +0200
  • cdedf4e78f Added comment for formula equality check. Strongly related to github issue #132. Tim Quatmann 2021-08-09 12:28:36 +0200
  • c8e9b43100 Changed ltl2da option to slightly more descriptive ltl2datool (this is also the name of the corresponding option in PRISM) Tim Quatmann 2021-08-09 12:21:33 +0200
  • 948e7fdaba cmake: Fixed marking non-existing option as advanced Tim Quatmann 2021-08-06 15:18:28 +0200
  • 7a851901e2 updates after cherry pick Stefan Pranger 2021-09-02 12:53:46 +0200
  • feadd3af77 Added cmake option STORM_RESOURCES_BUILD_JOBCOUNT to have better control on how many jobs we shall use to build external stuff (like spot, carl, cudd, glpk, ?) Tim Quatmann 2021-08-05 15:16:04 +0200
  • 98bb05b86f Trying to build spot with a single thread Tim Quatmann 2021-08-05 11:31:22 +0200
  • 3a3587370e Skip a test if LTL model checking is not available. Tim Quatmann 2021-08-05 11:30:41 +0200
  • efeeea0d54 Spot: re-iterated cmake interface to hopefully make it more clean. Added documentation on how to update spot Tim Quatmann 2021-08-04 16:33:07 +0200
  • e76c5ab4ba Fixed ambiguous operator overload. Tim Quatmann 2021-08-03 15:54:46 +0200
  • 5a2e489403 github buildtest workflow should test with spot. Tim Quatmann 2021-08-03 15:30:24 +0200
  • 4e6d334f9b Updated Changelog Tim Quatmann 2021-08-03 15:16:10 +0200
  • ba1d0d052d added simulator to tests Stefan Pranger 2021-08-08 12:15:06 +0200
  • 093b01f0c5 adjusted scheduler dontCare hannah 2021-08-03 13:51:41 +0200
  • adc5d9ae68 MA scheduler export hannah 2021-07-30 01:03:10 +0200
  • 1f17b31bbe arbitrary choice for dontCareStates hannah 2021-07-30 01:02:44 +0200
  • ebdfb2def8 keep the original modeltype during product construction hannah 2021-07-29 23:36:10 +0200
  • c80a62ce06 added function for computation of memory states hannah 2021-07-27 21:35:48 +0200
  • 71100e9d65 scheduler json export hannah 2021-07-27 20:42:38 +0200
  • cceb3513ce set states to dontCare during scheduler computations, adapted Tests hannah 2021-07-27 14:10:36 +0200
  • f92b2104b5 TODOs and fixed an error during scheduler creation hannah 2021-07-27 11:07:10 +0200
  • 6b0aaeadb4 ignore dontCare States while printing hannah 2021-07-27 11:05:41 +0200
  • 77ced0aefe fixed warning hannah 2021-07-21 23:59:55 +0200
  • c057e437e4 CMAKE: Do not mark STORM_USE_SPOT as advanced. Tim Quatmann 2021-07-21 12:36:51 +0200
  • 9626c3c5f1 Cmake: Fixed output when including spot. Tim Quatmann 2021-07-21 12:06:26 +0200
  • c1b06f40b7 CMAKE: Added option to include and link against Spot Tim Quatmann 2021-07-21 12:02:42 +0200
  • 412489a57f Added possibility to set (un)reachable states for scheduler hannah 2021-07-21 10:19:21 +0200
  • 214d586d10 fixed scheduler choice in EC hannah 2021-07-20 16:48:31 +0200
  • 6865ae1464 build memory structure from all states hannah 2021-07-20 16:31:49 +0200
  • 5c204182eb Added some todos Tim Quatmann 2021-07-20 14:16:16 +0200
  • b8712041bf fixed memory structure hannah 2021-07-16 16:41:42 +0200
  • 1191e3068f more ltl scheduler tests hannah 2021-07-16 16:40:41 +0200