s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity

Commit Graph

  • 57578cc560 Disable check for positive rewards (HACK) accumulation-v4.7 Sascha Wunderlich 2024-01-31 17:58:27 +0100
  • ef4610ba7c Update Dockerfile to JDK21 Sascha Wunderlich 2024-01-31 17:58:12 +0100
  • fa612cb601 Add Dockerfile Sascha Wunderlich 2023-11-12 15:03:16 +0100
  • cfb6b7c5f3 Fix missing include in sparse.cc Sascha Wunderlich 2021-06-23 21:39:13 +0200
  • ac1ea31b4f accumulation: Fix reward construction UNTESTED Joachim Klein 2021-06-21 21:51:05 +0200
  • f6417b1204 accumulation + DFA stuff (patch-based rebase) UNTESTED Joachim Klein 2021-06-21 21:37:05 +0200
  • cbfd553ddb fix DigitalClock manipulation Joachim Klein 2021-06-20 19:05:48 +0200
  • 05d615fd2c fixup DigitalClock bounds Joachim Klein 2021-06-20 17:56:06 +0200
  • f13ca25f6c fixup CounterTransformation (rewardGen) Joachim Klein 2021-06-20 17:55:42 +0200
  • c963aa67f6 imported patch ProbModel-comments-for-constructor.patch Joachim Klein 2018-10-12 14:26:44 +0200
  • 21ad6001f8 imported patch explicit-MDP-prob01ae-with-prerel-compute-strat.patch Joachim Klein 2018-10-12 14:26:43 +0200
  • 95d6d6061d imported patch explicit-mdp-prob01-rel.patch Joachim Klein 2018-10-12 14:26:42 +0200
  • d3eec878fa (TODO) IncomingChoiceRelation: calculatePreStar Joachim Klein 2018-10-12 14:26:41 +0200
  • d9633bf638 imported patch ChoicesMask.patch Joachim Klein 2018-10-12 14:26:40 +0200
  • 981d818191 imported patch BitSetTools-prelim.patch Joachim Klein 2018-10-12 14:26:39 +0200
  • a88256d555 imported patch MultiObjective-support-lowerbounds-via-LTL.patch Joachim Klein 2018-10-12 14:26:38 +0200
  • 375f4690a7 imported patch activate-ltl-step-bounds.patch Joachim Klein 2018-10-12 14:26:37 +0200
  • 94c095ffc6 imported patch ExpandStepBoundsSyntactically.patch Joachim Klein 2018-10-12 14:26:36 +0200
  • 5022be36c3 imported patch time-bounded-not-supported-message.patch Joachim Klein 2018-10-12 14:26:35 +0200
  • 709a5859c1 imported patch predecessor-LTLMC-use-backward.patch Joachim Klein 2018-10-12 14:26:34 +0200
  • d76bd5d8eb imported patch predecessor-ec-computer-use-backward.patch Joachim Klein 2018-10-12 14:26:33 +0200
  • dd9c794e34 imported patch predecessor-ECComputer.setPre.patch Joachim Klein 2018-10-12 14:26:32 +0200
  • 2800975309 imported patch predecessor-restrict-diagnostics.patch Joachim Klein 2018-10-12 14:26:31 +0200
  • 35786a8b38 imported patch NondetModelChecker-cosafety-guard-against-rewards.patch Joachim Klein 2018-10-12 14:26:30 +0200
  • b11409c674 imported patch Wrapper.patch Joachim Klein 2018-10-12 14:26:29 +0200
  • 26404d8bb3 imported patch symb-counter-transform-ProbModelChecker-protect-dtmc-trew.patch Joachim Klein 2018-10-12 14:26:28 +0200
  • 6f227818bc imported patch symb-counter-transform-ProbModelChecker-protect-negative.patch Joachim Klein 2018-10-12 14:26:27 +0200
  • 42dc01a1b5 imported patch symb-counter-transform-ProbModelChecker.patch Joachim Klein 2018-10-12 14:26:26 +0200
  • cd75a75415 imported patch symb-counter-transform-NondetModelChecker.patch Joachim Klein 2018-10-12 14:26:25 +0200
  • a362472fd8 imported patch symb-counter-transform-transformations.patch Joachim Klein 2018-10-12 14:26:24 +0200
  • c5fce8f507 imported patch symb-counter-transform-TransitionsByRewardsInfo.patch Joachim Klein 2018-10-12 14:26:23 +0200
  • 2e0d123a68 imported patch symb-MET-LTLModelChecker-rabin-no-darowcol.patch Joachim Klein 2018-10-12 14:26:22 +0200
  • 418b5e7bd6 imported patch symb-MET-LTLModelChecker-rabin-darowcol-optional.patch Joachim Klein 2018-10-12 14:26:21 +0200
  • 1043d51ccf imported patch symb-common-symbolic-streett-ecs.patch Joachim Klein 2018-10-12 14:26:20 +0200
  • 774edd1dbf imported patch min-max--multi-protect-against-explicitMinMax.patch Joachim Klein 2018-10-12 14:26:19 +0200
  • 3ebd913326 imported patch min-max-min.max.parser-refresh.patch Joachim Klein 2018-10-12 14:26:18 +0200
  • 29bf08abb3 imported patch min-max-min.max.parser.patch Joachim Klein 2018-10-12 14:26:17 +0200
  • eb2e84b40f quantile-common: Adapt OpRelBound to multi-threshold Joachim Klein 2018-10-12 14:26:16 +0200
  • 93c5049660 imported patch min-max-ExpressionProbRewardMinMaxConstructor.patch Joachim Klein 2018-10-12 14:26:15 +0200
  • 1012e1e65a imported patch min-max-min-max-2.patch Joachim Klein 2018-10-12 14:26:14 +0200
  • 57e8229ceb imported patch min-max-new-min-max-check.patch Joachim Klein 2018-10-12 14:26:13 +0200
  • 4b5675dbcb imported patch symb.ModelExpressionTransformationIdentity.patch Joachim Klein 2018-10-12 14:26:12 +0200
  • f8c7b90c69 imported patch symb-common-ModelCheckers.public.checkUntilProbs.patch Joachim Klein 2018-10-12 14:26:11 +0200
  • aff916e48a imported patch common-smmd-ExpressionIsNextMinus.patch Joachim Klein 2018-10-12 14:26:10 +0200
  • 49b38136ce imported patch common-smmd-StateValuesAndNot.patch Joachim Klein 2018-10-12 14:26:09 +0200
  • cbc53e1ff3 imported patch common-explicit.StateValues.partition.patch Joachim Klein 2018-10-12 14:26:08 +0200
  • 3dac91de49 imported patch rewardcounter-DTMC-no-negative.patch Joachim Klein 2018-10-12 14:26:07 +0200
  • 1d38f7d070 imported patch rewardcounter-CTMC-extra-check-TODO.patch Joachim Klein 2018-10-12 14:26:06 +0200
  • bf959ba54e imported patch rewardcounter-DTMC-MC-resolve-rewards.patch Joachim Klein 2018-10-12 14:26:05 +0200
  • 272967a7e1 imported patch rewardcounter-continous-time-bounds.patch Joachim Klein 2018-10-12 14:26:04 +0200
  • 9a14a28bba imported patch rewardcounter-reward-bound-checks.patch Joachim Klein 2018-10-12 14:26:03 +0200
  • 638d21fa1a imported patch rewardcounter-DTMCCounterTransformation.groupBounds.patch Joachim Klein 2018-10-12 14:26:02 +0200
  • 07eb44539e imported patch rewardcounter-CounterProduct.getStatesWithAccumulatedRewardInBoundConjunction.patch Joachim Klein 2018-10-12 14:26:01 +0200
  • ef54f16e89 imported patch rewardcounter-IntegerBounds.isInBoundForConjunction.patch Joachim Klein 2018-10-12 14:26:00 +0200
  • ea1a1ca21b imported patch rewardcounter-IntegerBounds.getMaximalInterestingValueForConjunction.patch Joachim Klein 2018-10-12 14:25:59 +0200
  • f1881a61e0 imported patch rewardcounter-TemporalBound.hasSameDomain.patch Joachim Klein 2018-10-12 14:25:58 +0200
  • 903eee7cbd imported patch rewardcounter-groupBoundsByRewardStructure.patch Joachim Klein 2018-10-12 14:25:57 +0200
  • 0506cc412c imported patch rewardcounter-TemporalBound.rewardStruct.patch Joachim Klein 2018-10-12 14:25:56 +0200
  • bab19207a4 imported patch rewardcounter-MDPModelChecker.simple-path-formulas-with-bounds.patch Joachim Klein 2018-10-12 14:25:55 +0200
  • ce1af01e42 imported patch rewardcounter-MDPCounterAndCounterTransformation.patch Joachim Klein 2018-10-12 14:25:54 +0200
  • a012138134 imported patch rewardcounter-DTMCCounterTransformation.patch Joachim Klein 2018-10-12 14:25:52 +0200
  • 0dfbc3fc12 explicit: DTMCRewardCounterProduct Joachim Klein 2018-10-12 14:25:51 +0200
  • a0fa61f265 imported patch rewardcounter-expression.getTemporalOperator.patch Joachim Klein 2018-10-12 14:25:49 +0200
  • c47e6f7494 imported patch rewardcounter-IntegerBound.fromTemporalOperatorBound.patch Joachim Klein 2018-10-12 14:25:48 +0200
  • 53c679061c imported patch rewardcounter-ReplaceBound.patch Joachim Klein 2018-10-12 14:25:47 +0200
  • d769919086 imported patch rewardcounter-TemporalOperatorBounds-use-refresh.patch Joachim Klein 2018-10-12 14:25:46 +0200
  • aeec397851 imported patch copyBoundsFrom-use-for-toUntil.patch Joachim Klein 2018-10-12 14:25:45 +0200
  • f0bacc9ccc imported patch copyBoundsFrom.patch Joachim Klein 2018-10-12 14:25:44 +0200
  • 32ada06833 imported patch FIX-temporal-bound-printing.patch Joachim Klein 2018-10-12 14:25:43 +0200
  • 6e033b5d65 imported patch rewardcounter-TemporalOperatorBounds-use.patch Joachim Klein 2018-10-12 14:25:42 +0200
  • 3fa0b761a5 imported patch rewardcounter-TemporalOperatorBounds.patch Joachim Klein 2018-10-12 14:25:41 +0200
  • 22ff99026f imported patch rewardcounter-TemporalOperatorBound-use-refresh.patch Joachim Klein 2018-10-12 14:25:40 +0200
  • fc07b9f9fb imported patch rewardcounter-TemporalOperatorBound-use.patch Joachim Klein 2018-10-12 14:25:39 +0200
  • 2c4df3a20d imported patch rewardcounter-TemporalOperatorBound.patch Joachim Klein 2018-10-12 14:25:38 +0200
  • 6cce20c5ed imported patch prod-with-productstates-rely-on-product-for-soi.patch Joachim Klein 2018-10-12 14:25:37 +0200
  • a08718e68b imported patch rewardcounter-ProductWithProductStates.patch Joachim Klein 2018-10-12 14:25:36 +0200
  • 4d4faa7236 imported patch rewardcounter-MDPProductOperator.patch Joachim Klein 2018-10-12 14:25:35 +0200
  • 346a6e053e explicit: +ProductOperator (generic) Joachim Klein 2018-10-12 14:25:34 +0200
  • ba7e1c4c14 imported patch rewardcounter-ProductState-int.patch Joachim Klein 2018-10-12 14:25:33 +0200
  • f2789fb0f5 explicit: +ProductState Joachim Klein 2018-10-12 14:25:32 +0200
  • cfede9f44e imported patch MET-ModelExpressionTransformationIdentity.patch Joachim Klein 2018-10-12 14:25:31 +0200
  • bad808fd85 ModelExpressionTransformationNested Joachim Klein 2018-10-12 14:25:30 +0200
  • bad132c250 Add ModelExpressionTransformation interface Joachim Klein 2018-10-12 14:25:29 +0200
  • 4ec20a4e34 imported patch symb-common-TemporaryJDDRefs.patch Joachim Klein 2018-10-12 14:25:28 +0200
  • 04a7e5ef56 imported patch common-REVERT-prodStatesList-explicit-LTLMC.patch Joachim Klein 2018-10-12 14:25:24 +0200
  • 5b0d6b0a6b imported patch explicit-fairness-warning.patch Joachim Klein 2018-10-12 14:25:23 +0200
  • 764c2800ef imported patch MT-states-of-interest.patch Joachim Klein 2018-10-12 14:25:22 +0200
  • a79bc54188 (HOA path) Add support in LTLModelCheckers (ex/sym) to support HOA path specifications Joachim Klein 2018-10-12 14:25:21 +0200
  • b50e56701b (HOA path) LTL2DA: readHOA and fromExpressionHOA helpers Joachim Klein 2018-10-12 14:25:20 +0200
  • bcded2e24f (HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications (parser refresh) Joachim Klein 2018-10-12 14:25:19 +0200
  • cef6f8c35d (HOA path) PrismParser: PathSpecification supports LTL and HOA-style path specifications Joachim Klein 2018-10-12 14:25:18 +0200
  • 2a2d7d64c9 (HOA path) ExpressionHOA for HOA-based path formula Joachim Klein 2018-10-12 14:25:17 +0200
  • f6851caee7 (HOA path) PrismParser: support QuotedString (parser refresh) Joachim Klein 2018-10-12 14:25:16 +0200
  • 6b83df3d32 (HOA path) PrismParser: support QuotedString Joachim Klein 2018-10-12 14:25:15 +0200
  • 186da7e071 (HOA path) AST: QuotedString element Joachim Klein 2018-10-12 14:25:14 +0200
  • badd6f924c (HOA path) PrismParser: refactor double quoted identifiers (parser refresh) Joachim Klein 2018-10-12 14:25:13 +0200
  • 16c5442ab1 (HOA path) PrismParser: refactor double quoted identifiers Joachim Klein 2018-10-12 14:25:12 +0200
  • ac02a22ae6 (HOA path) PrismPaths for resolving paths, e.g., relative to a model or properties file Joachim Klein 2018-10-12 14:25:11 +0200
  • a58de4025a (HOA path) PathUtil: Some static helper methods for dealing with paths Joachim Klein 2018-10-12 14:25:10 +0200
  • 7055482770 (HOA path) StateModelChecker (symbolic, explicit): Provide access to the ModulesFile / PropertiesFile stored in the model checker Joachim Klein 2018-10-12 14:25:09 +0200