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

Commit Graph

  • d86dbcd4e3 removed partial results for formula parsing, added fragment checks for rpatl Lukas Posch 2021-08-13 10:09:11 +0200
  • 5452240944 removed unnecessary testcases (e.g. there are no atomic label formulas in game formulas since they must have a coalition of players and an operator) Lukas Posch 2021-08-13 09:53:04 +0200
  • 567584e285 added MultiObjectiveFormulaTest to GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:33:34 +0200
  • 284a944f63 added WrongFormatTest to GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:28:17 +0200
  • 3f2e636e34 added CommentTest to GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:25:04 +0200
  • a381618403 added NestedPathFormulaTest to GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:20:16 +0200
  • 4d84b84230 added ConditionalProbabilityTest to GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:18:04 +0200
  • 90568c54a2 added RewardOperatorTest to GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:15:11 +0200
  • 442ffecd13 created NextOperatorTest in GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:04:04 +0200
  • bc6dabb088 fixed UntilOperatorTest in GameFormulaParserTest.cpp Lukas Posch 2021-08-13 09:03:37 +0200
  • 45319ca2da WIP GameFormulaParserTest.cpp Lukas Posch 2021-08-12 16:18:33 +0200
  • f1aa210b5a shielding check for FragmentCheckerTest Prctl Lukas Posch 2021-08-12 10:00:44 +0200
  • d8592bffa2 shielding check for FragmentCheckerTest Rpatl Lukas Posch 2021-08-12 09:56:33 +0200
  • 868f42b38b Bounded LTL formula check for FragmentCheckerTest Rpatl Lukas Posch 2021-08-12 09:43:22 +0200
  • e1b00dae7a small change in FragmentCheckerTest Rpatl Lukas Posch 2021-08-12 09:42:51 +0200
  • 1b81c009c1 WIP added GameFormulaParserTest.cpp Lukas Posch 2021-08-12 08:22:38 +0200
  • 04dd2b2e92 added a smg to PrismParserTest.cpp Stefan Pranger 2021-09-03 15:19:04 +0200
  • d14b04fe72 WIP DEBUG message for multiplier type Lukas Posch 2021-08-11 15:29:08 +0200
  • 3a91b266d4 WIP expanded tests, now tests run for X, U, G, F Lukas Posch 2021-08-11 15:07:32 +0200
  • b49dd59101 WIP added testcases for globally probabilities for SmgRpatlModelCheckerTest "Walker" Lukas Posch 2021-08-11 11:35:33 +0200
  • d0f85313f3 added probabalisticFormula.rpatl in testfolder for rpatl for future purposes Lukas Posch 2021-08-11 11:33:46 +0200
  • fdb84fdee5 changed the info about statesOfCoalition to STORM_LOG_INFO Lukas Posch 2021-08-11 09:50:06 +0200
  • 7565bc5d6a created SmgRpatlModelCheckerTest.cpp as test suite for rpatl smg models Lukas Posch 2021-08-10 16:10:19 +0200
  • a7919a651c added a smg example for checking test-modelchecker-rpatl-smg Lukas Posch 2021-08-10 16:09:14 +0200
  • 3d73e71162 introduced test-modelchecker-rpatl-smg Lukas Posch 2021-08-10 16:08:07 +0200
  • 8d11ed9f42 added first rpatl fragment checker tests Stefan Pranger 2021-09-03 15:16:09 +0200
  • 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