From 8dc46968cbe7edbd3f8ef144affef8064a832318 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Thu, 19 Nov 2020 18:11:20 +0100 Subject: [PATCH] added rPATL to FragmentSpecifitcations --- src/storm/logic/FragmentSpecification.cpp | 34 ++++++++++--- src/storm/logic/FragmentSpecification.h | 60 +++++++++++++---------- 2 files changed, 60 insertions(+), 34 deletions(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 9405a3841..898b9f626 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -41,21 +41,30 @@ namespace storm { pctl.setBoundedUntilFormulasAllowed(true); pctl.setStepBoundedUntilFormulasAllowed(true); pctl.setTimeBoundedUntilFormulasAllowed(true); - + return pctl; } - + FragmentSpecification flatPctl() { FragmentSpecification flatPctl = pctl(); - + flatPctl.setNestedOperatorsAllowed(false); - + return flatPctl; } - + + FragmentSpecification rpatl() { + FragmentSpecification rpatl = pctl(); + + // TODO disallow operator we currently do not support + rpatl.setCoalitionOperatorsAllowed(true); + + return rpatl; + } + FragmentSpecification prctl() { FragmentSpecification prctl = pctl(); - + prctl.setRewardOperatorsAllowed(true); prctl.setCumulativeRewardFormulasAllowed(true); prctl.setInstantaneousFormulasAllowed(true); @@ -614,12 +623,21 @@ namespace storm { bool FragmentSpecification::isRewardAccumulationAllowed() const { return rewardAccumulation; } - + FragmentSpecification& FragmentSpecification::setRewardAccumulationAllowed(bool newValue) { rewardAccumulation = newValue; return *this; } - + bool FragmentSpecification::areCoalitionOperatorsAllowed() const { + return coalitionOperator; + } + + FragmentSpecification& FragmentSpecification::setCoalitionOperatorsAllowed(bool newValue) { + coalitionOperator = newValue; + return *this; + } + + } } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index aa48c0738..830c2a9a0 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -93,105 +93,110 @@ namespace storm { bool areNestedOperatorsAllowed() const; FragmentSpecification& setNestedOperatorsAllowed(bool newValue); - + bool areNestedPathFormulasAllowed() const; FragmentSpecification& setNestedPathFormulasAllowed(bool newValue); - + bool areNestedMultiObjectiveFormulasAllowed() const; FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue); - + bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const; FragmentSpecification& setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue); - + bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const; FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue); bool areStepBoundedUntilFormulasAllowed() const; FragmentSpecification& setStepBoundedUntilFormulasAllowed(bool newValue); - + bool areTimeBoundedUntilFormulasAllowed() const; FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue); bool areRewardBoundedUntilFormulasAllowed() const; FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue); - + bool areMultiDimensionalBoundedUntilFormulasAllowed() const; FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue); - + bool areStepBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setStepBoundedCumulativeRewardFormulasAllowed(bool newValue); - + bool areTimeBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue); bool areRewardBoundedCumulativeRewardFormulasAllowed() const; FragmentSpecification& setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue); - + bool areMultiDimensionalCumulativeRewardFormulasAllowed() const; FragmentSpecification& setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue); - + bool isVarianceMeasureTypeAllowed() const; FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue); - + bool areQuantitativeOperatorResultsAllowed() const; FragmentSpecification& setQuantitativeOperatorResultsAllowed(bool newValue); bool areQualitativeOperatorResultsAllowed() const; FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue); - + bool isOperatorAtTopLevelRequired() const; FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue); - + bool isMultiObjectiveFormulaAtTopLevelRequired() const; FragmentSpecification& setMultiObjectiveFormulaAtTopLevelRequired(bool newValue); - + bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const; FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue); - + bool isQuantileFormulaAtTopLevelRequired() const; FragmentSpecification& setQuantileFormulaAtTopLevelRequired(bool newValue); - + bool isRewardAccumulationAllowed() const; FragmentSpecification& setRewardAccumulationAllowed(bool newValue); - + bool areCoalitionOperatorsAllowed() const; + FragmentSpecification& setCoalitionOperatorsAllowed(bool newValue); + + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); - + private: // Flags that indicate whether it is legal to see such a formula. bool probabilityOperator; bool rewardOperator; bool expectedTimeOperator; bool longRunAverageOperator; - + bool multiObjectiveFormula; bool quantileFormula; - + bool globallyFormula; bool reachabilityProbabilityFormula; bool nextFormula; bool untilFormula; bool boundedUntilFormula; - + bool atomicExpressionFormula; bool atomicLabelFormula; bool booleanLiteralFormula; bool unaryBooleanStateFormula; bool binaryBooleanStateFormula; - + bool cumulativeRewardFormula; bool instantaneousRewardFormula; bool reachabilityRewardFormula; bool longRunAverageRewardFormula; bool totalRewardFormula; - + bool conditionalProbabilityFormula; bool conditionalRewardFormula; - + bool reachabilityTimeFormula; - + + bool coalitionOperator; + // Members that indicate certain restrictions. bool nestedOperators; bool nestedPathFormulas; @@ -228,7 +233,10 @@ namespace storm { // Flat PCTL. FragmentSpecification flatPctl(); - + + // rPATL for SMGs + FragmentSpecification rpatl(); + // PCTL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification prctl();