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

Commit Graph

  • c099183063 (MDP-LTL) MaximalEndComponent: containsAnyState Joachim Klein 2020-08-24 22:25:14 +0200
  • 5855a82e80 (MDP-LTL) CheckTask: negate() Joachim Klein 2020-08-24 22:25:13 +0200
  • b6b31f20af (MDP-LTL) AcceptanceCondition: extractFromDNF Joachim Klein 2020-08-24 22:25:13 +0200
  • cf6af6c456 (stateformula) Modelcheckers: support P[phi], Pmax/min[phi] where phi is a state formula Joachim Klein 2020-08-24 22:25:10 +0200
  • af10aa8b4b (stateformula) StateFormula: a StateFormula is a probabilistic path formula Joachim Klein 2020-08-24 22:25:09 +0200
  • a639836f6f (stateformula) CheckResults: provide constructor for quantitative from qualitative result Joachim Klein 2020-08-24 22:25:09 +0200
  • 27ca10a668 (stateformula) SymbolicQualitativeCheckResult: add getReachableStates() and getStates() accessors, like SymbolicQuantitativeCheckResult Joachim Klein 2020-08-24 22:25:08 +0200
  • 1243b9300c (LTL) SparseDtmcModelChecker: Implement LTL model checking Joachim Klein 2020-08-27 06:25:25 +0200
  • ab32af463b (LTL) AbstractModelChecker: detect need for LTL PMC, call (unimplemented) computeLTLProbabilities Joachim Klein 2020-08-24 22:25:05 +0200
  • 5427702376 WIP:needed? Boolean path formulas: allow storing context Joachim Klein 2020-08-24 22:25:05 +0200
  • fbe5236c4d (LTL) FragmentSpecification: add pctlstar() and prctlstar() fragments Joachim Klein 2020-08-24 22:25:04 +0200
  • 6404c526e2 WIP (LTL) LTL2DeterministicAutomaton (first hacky attempt) Joachim Klein 2020-08-24 22:25:01 +0200
  • 393dd2af87 (LTL) ExtractMaximalStateFormulasVisitor Joachim Klein 2020-08-24 22:25:03 +0200
  • b04d2723c2 (LTL) Add Formula::toPrefixString() Joachim Klein 2020-08-24 22:25:03 +0200
  • bd0a882cd5 (LTL) FormulaInformation: add containsComplexPathFormula() Joachim Klein 2020-08-24 22:25:01 +0200
  • 5482a32b8a (LTL) Refactor unary/boolean state formulas to allow path formulas as well Joachim Klein 2020-08-24 22:25:00 +0200
  • 256f9839da SparseDtmcPrctlModelChecker: computeDAProductProbabilities() Joachim Klein 2020-08-27 06:35:10 +0200
  • ad774e5138 WIP (HOA-path) FormulaParser: parse HOAPathFormula Joachim Klein 2020-08-24 22:24:56 +0200
  • ba907a1d75 WIP (HOA-path) FormulaParser: parse HOAPathFormula Joachim Klein 2020-08-24 22:24:56 +0200
  • aed8e53a29 (HOA-path) AbstractModelChecker: default handling for HOAPathFormulas (= reject) Joachim Klein 2020-08-24 22:24:56 +0200
  • 21b9d73816 WIP (HOA-path) logic: HOAPathFormula Joachim Klein 2020-08-24 22:24:55 +0200
  • 85a408dd72 (DA-product) tests: DAProductBuilderTest Joachim Klein 2020-08-24 22:24:59 +0200
  • 044074a4b1 (DA) tests: HOAParsingTest Stefan Pranger 2021-08-07 19:10:58 +0200
  • e5282708dd (DA-product) transformer: Product, DAProduct + builders Joachim Klein 2020-08-24 22:24:57 +0200
  • 3696e13736 (DA) ItemLabeling: addUniqueLabel, generateUniqueLabel Joachim Klein 2020-08-24 22:24:57 +0200
  • de0dd71679 (DA) Automata classes: DeterministicAutomaton, APSet, HOAConsumer, AcceptanceCondition Joachim Klein 2020-08-24 22:24:54 +0200
  • 8d680749cd (DA) Add cpphoafparser 0.99.2 Joachim Klein 2020-08-24 22:24:51 +0200
  • f4fb0188be Merge pull request 'Adapt Property Ctors with ShieldingExpression Parameter' (#44) from storm_prs_and_updates into main Stefan Pranger 2021-08-06 13:55:24 +0000
  • b53a255365 adapted property ctors with ShieldingExpression param Stefan Pranger 2021-08-06 15:52:25 +0200
  • d3e313dcb4 Merge pull request '[STORM PR] Summary' (#43) from storm_prs_and_updates into main Stefan Pranger 2021-08-06 13:48:25 +0000
  • 9d4e654ec2 fix for quantitative computations in computeUntilProb Lukas Posch 2021-08-06 11:26:28 +0200
  • d88feb18ea Merge remote-tracking branch 'storm_gh/master' into storm_prs_and_updates Stefan Pranger 2021-08-05 16:31:05 +0200
  • 4dfb2a959f
         Updated Author list in Readme.md Tim Quatmann 2021-08-03 16:02:36 +0200
  • e8c24ec532 Merge pull request 'Shields for MDPs' (#24) from mdp_shields into main Stefan Pranger 2021-07-29 11:01:54 +0000
  • 6a5f626259 refactored helper code Stefan Pranger 2021-07-25 17:29:45 +0200
  • b686bfebb0 remove whitespaces and debug output Stefan Pranger 2021-07-25 17:28:07 +0200
  • e6eed7cbc4 moved computation out of if/else Stefan Pranger 2021-07-25 17:27:27 +0200
  • 1599034b5c fixed shield handling Lukas Posch 2021-07-20 15:15:18 +0200
  • 7cbe2886eb fixed shield handling for MDP Next and BoundedGlobally Lukas Posch 2021-07-20 11:13:30 +0200
  • 591e63e11e fixed choiceValues for MDP shields - Until and Globally Lukas Posch 2021-07-19 16:57:18 +0200
  • 78a3b2a6a7 Nullpointer check for dirOverride Lukas Posch 2021-07-19 16:53:58 +0200
  • 444929a9a3 create MDP shields if it is a shielding task Lukas Posch 2021-07-15 11:52:47 +0200
  • 76a34bc957 expanded compute method in SparseNondeterministicStepBoundedHorizonHelper.* with resultMaybestates and choiceValues Lukas Posch 2021-07-15 11:51:12 +0200
  • def9e65525 store the choiceValues in the iterations and the maybeStates then return it to the SparseMdpPrctlModelChecker.cpp Lukas Posch 2021-07-15 11:49:33 +0200
  • 053f0a8d19 extended MDPModelCheckingHelperReturnType with maybeStates and choiceValues Lukas Posch 2021-07-15 11:46:08 +0200
  • 222a18a760 added methods reduce and repeatedMultiplyAndReduceWithChoices to Multiplier.* to store the choiceValues between multiply and reduce Lukas Posch 2021-07-15 11:45:07 +0200
  • 731c060c4e added method isShieldingTask() to SolveGoal.* Lukas Posch 2021-07-15 11:42:52 +0200
  • 79447073d0 changed shield-handling.h to ShieldHandling.cpp and ShieldHandling.h renamed createOptimalShield() to createQuantitativShield() Lukas Posch 2021-07-15 11:41:23 +0200
  • a63d8cda6b Merge pull request 'Flip Bits when Passing CoalitionStates to ShieldHandling' (#29) from fix_formula_parser_debug into main Stefan Pranger 2021-07-29 10:58:29 +0000
  • bb6cd2232f flip bits when passing coalition to shieldhandling Stefan Pranger 2021-07-06 20:33:12 +0200
  • 6f19aaea7f Merge pull request 'Introduce Shields' (#16) from safety_shields into main Stefan Pranger 2021-07-28 06:40:34 +0000
  • 4746a81b51 removed output and check in checkGameFormula Stefan Pranger 2021-07-26 18:26:08 +0200
  • 8ffcabc79d fixed error messages in shield handling Stefan Pranger 2021-07-26 18:23:41 +0200
  • 8304c897cd refactored creation of coalitionStates Stefan Pranger 2021-07-26 18:07:44 +0200
  • 6e8387235d
         Merge pull request #120 from sjunges/master Sebastian Junges 2021-07-26 09:04:12 -0700
  • 774299bdc2 removed commented code from Property Stefan Pranger 2021-07-26 17:17:11 +0200
  • b73b0b2a75 removed unused code and added method desc Stefan Pranger 2021-07-26 17:13:40 +0200
  • a8d6b5e874 removed unused code from MultiplierEnv Stefan Pranger 2021-07-26 16:53:00 +0200
  • 6bd625e4c8 removed debug output Stefan Pranger 2021-07-26 16:52:31 +0200
  • 9b6afac4d7 renamed factors for shielding to probabilities Stefan Pranger 2021-07-26 16:52:07 +0200
  • 1d5eba326d removed comment from PostScheduler Stefan Pranger 2021-07-26 16:51:48 +0200
  • 29fb202761 cleaned up GameVi and LraViHelper Stefan Pranger 2021-07-26 16:51:28 +0200
  • f77293de78 added comments for CheckTask methods Stefan Pranger 2021-07-26 16:38:26 +0200
  • dadcda9f0c Merge pull request 'Fix Formula Parser Debug Methods' (#25) from formula_parser_debug into main Stefan Pranger 2021-07-26 11:14:10 +0000
  • f9d2df0b0a move ConstantDataType and added ostream Stefan Pranger 2021-07-25 15:28:14 +0200
  • f0b58781b1 added os operator to FormulaContext Stefan Pranger 2021-07-25 10:01:24 +0200
  • d749b3c46a allow optional 'Shield' string when parsing Stefan Pranger 2021-07-26 10:08:08 +0200
  • b7daafc4c1 fix in predicate expression simplify pointed out by TQ, thanks Sebastian Junges 2021-07-25 22:25:12 -0700
  • a326f876f4 Merge branch 'master' of https://github.com/sjunges/storm Sebastian Junges 2021-07-17 14:24:21 -0700
  • 6c1caae20c simplifications in predicate expressions Sebastian Junges 2021-07-17 14:24:17 -0700
  • df1aefda71
         Update src/storm/storage/expressions/PredicateExpression.cpp Sebastian Junges 2021-07-17 14:23:54 -0700
  • 3d05cc5791
         DdJaniModelBuilder: Added proper error message in case a bounded integer variable only has an upper or a lower bound. Tim Quatmann 2021-07-15 11:58:33 +0200
  • 4d231c06b2 Merge branch 'master' of https://github.com/moves-rwth/storm Sebastian Junges 2021-07-09 17:42:57 -0700
  • a95ff3056a
         Fixed incorrect results for PcaaWeightVectorChecker. Tim Quatmann 2021-07-01 12:34:07 +0200
  • 1241829981
         Merge pull request #131 from tquatmann/update-eigen Tim Quatmann 2021-07-01 11:21:07 +0200
  • bfbc339d27
         update eigen version mentioned in comments and directory names Tim Quatmann 2021-07-01 06:52:39 +0200
  • 91382c8662
         Update Eigen to 3.3.9 Tim Quatmann 2021-06-29 11:45:07 +0200
  • 74a24c3ac9
         Merge pull request #130 from jipspel/fixes jipspel 2021-06-28 14:22:19 +0200
  • d77c285faf Fix TODOs Jip Spel 2021-06-28 12:16:19 +0200
  • 24fa7c9529 Fix warnings Jip Spel 2021-06-28 11:26:34 +0200
  • 0f0256b422 Fix warning Jip Spel 2021-06-28 11:08:07 +0200
  • 9f5128c4af Update documentation with fixed choices Jip Spel 2021-06-28 10:26:11 +0200
  • 044a900aa1
         Added new gurobi versions Tim Quatmann 2021-06-24 07:58:51 +0200
  • 62ad294e1e
         Merge pull request #129 from tquatmann/update-gtest Tim Quatmann 2021-06-18 15:05:08 +0200
  • 7bcf78650f
         Included missing header required to output boost::optionals in tests Tim Quatmann 2021-06-18 05:47:43 +0200
  • 72a387960d
         Merge pull request #123 from johannesalehmann/master Tim Quatmann 2021-06-17 13:18:45 +0200
  • 3af128184e
         Fixed usage of missing operator<< for permissive scheduler tests Tim Quatmann 2021-06-17 13:15:21 +0200
  • 32ddadea17
         Added explanations on how to update gtest in the future. Tim Quatmann 2021-06-17 11:37:10 +0200
  • 4e93e0a19d
         Renamed gtest directory to make it version independent. Tim Quatmann 2021-06-17 11:17:26 +0200
  • 9f21e0e777
         Updated to gtest 1.11 (see #128) Tim Quatmann 2021-06-17 11:10:50 +0200
  • 1cd97080d4 explicitly state that we override the functions from the expression visitor Sebastian Junges 2021-06-12 16:59:29 -0700
  • c01e0c11f5 silence warning due to time being returned as an int Sebastian Junges 2021-06-12 16:57:46 -0700
  • c6ec2355e4 avoid use of constants comparator to avoid skewing the distribution Sebastian Junges 2021-06-12 14:21:32 -0700
  • af2e8a7d03 get reward names (in order) provided by the simulator Sebastian Junges 2021-06-11 20:30:08 -0700
  • 35d136574d clear debug code from tests (feedback from TQ) Sebastian Junges 2021-06-11 17:36:35 -0700
  • da3c1a1be2 some comments and API restrictions for clearer usage Sebastian Junges 2021-06-11 17:36:08 -0700
  • 1df5296934 cleaned code, reduce number of checks by half due to symmetry Sebastian Junges 2021-06-11 13:55:06 -0700
  • 2cd25d069c To dice translation, remove hack for modulo Sebastian Junges 2021-06-11 13:54:30 -0700
  • d144a1776c prism next state generator, rename actions to reflect labeled choices vs unlabeled choices are sync vs async Sebastian Junges 2021-06-11 13:53:42 -0700
  • 3f165785d0 integrated feedback on code quality by TQ Sebastian Junges 2021-06-11 13:52:47 -0700