From 0d7e763b00852ea55e0bf4c04aa2bc0bf6b9faa2 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 08:03:24 +0100 Subject: [PATCH] added rPATL to FragmentSpecifitcations --- src/storm/logic/FragmentSpecification.cpp | 224 +++++++++++----------- src/storm/logic/FragmentSpecification.h | 38 ++-- 2 files changed, 131 insertions(+), 131 deletions(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 9fd7353b9..96cbaf181 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -5,34 +5,34 @@ namespace storm { namespace logic { - + FragmentSpecification propositional() { FragmentSpecification propositional; - + propositional.setBooleanLiteralFormulasAllowed(true); propositional.setBinaryBooleanStateFormulasAllowed(true); propositional.setUnaryBooleanStateFormulasAllowed(true); propositional.setAtomicExpressionFormulasAllowed(true); propositional.setAtomicLabelFormulasAllowed(true); - + return propositional; } - + FragmentSpecification reachability() { FragmentSpecification reachability = propositional(); - + reachability.setProbabilityOperatorsAllowed(true); reachability.setUntilFormulasAllowed(true); reachability.setReachabilityProbabilityFormulasAllowed(true); reachability.setOperatorAtTopLevelRequired(true); reachability.setNestedOperatorsAllowed(false); - + return reachability; } - + FragmentSpecification pctl() { FragmentSpecification pctl = propositional(); - + pctl.setProbabilityOperatorsAllowed(true); pctl.setGloballyFormulasAllowed(true); pctl.setReachabilityProbabilityFormulasAllowed(true); @@ -76,34 +76,34 @@ namespace storm { prctl.setLongRunAverageOperatorsAllowed(true); prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); - + return prctl; } - + FragmentSpecification csl() { FragmentSpecification csl = pctl(); - + csl.setTimeBoundedUntilFormulasAllowed(true); - + return csl; } - + FragmentSpecification csrl() { FragmentSpecification csrl = csl(); - + csrl.setRewardOperatorsAllowed(true); csrl.setCumulativeRewardFormulasAllowed(true); csrl.setInstantaneousFormulasAllowed(true); csrl.setReachabilityRewardFormulasAllowed(true); csrl.setLongRunAverageOperatorsAllowed(true); csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true); - + return csrl; } - + FragmentSpecification multiObjective() { FragmentSpecification multiObjective = propositional(); - + multiObjective.setMultiObjectiveFormulasAllowed(true); multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true); multiObjective.setNestedMultiObjectiveFormulasAllowed(false); @@ -125,10 +125,10 @@ namespace storm { return multiObjective; } - + FragmentSpecification quantiles() { FragmentSpecification quantiles = propositional(); - + quantiles.setQuantileFormulasAllowed(true); quantiles.setQuantileFormulaAtTopLevelRequired(true); quantiles.setProbabilityOperatorsAllowed(true); @@ -143,44 +143,44 @@ namespace storm { quantiles.setCumulativeRewardFormulasAllowed(true); quantiles.setMultiDimensionalBoundedUntilFormulasAllowed(true); quantiles.setMultiDimensionalCumulativeRewardFormulasAllowed(true); - + return quantiles; } - + FragmentSpecification::FragmentSpecification() { probabilityOperator = false; rewardOperator = false; expectedTimeOperator = false; longRunAverageOperator = false; - + multiObjectiveFormula = false; quantileFormula = false; - + globallyFormula = false; reachabilityProbabilityFormula = false; nextFormula = false; untilFormula = false; boundedUntilFormula = false; - + atomicExpressionFormula = false; atomicLabelFormula = false; booleanLiteralFormula = false; unaryBooleanStateFormula = false; binaryBooleanStateFormula = false; - + cumulativeRewardFormula = false; instantaneousRewardFormula = false; reachabilityRewardFormula = false; longRunAverageRewardFormula = false; totalRewardFormula = false; - + conditionalProbabilityFormula = false; conditionalRewardFormula = false; - + reachabilityTimeFormula = false; - + gameFormula = false; - + nestedOperators = true; nestedPathFormulas = false; nestedMultiObjectiveFormulas = false; @@ -195,296 +195,296 @@ namespace storm { rewardBoundedCumulativeRewardFormulas = false; multiDimensionalCumulativeRewardFormulas = false; varianceAsMeasureType = false; - + qualitativeOperatorResults = true; quantitativeOperatorResults = true; - + operatorAtTopLevelRequired = false; multiObjectiveFormulaAtTopLevelRequired = false; operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false; quantileFormulaAtTopLevelRequired = false; - + rewardAccumulation = false; } - + FragmentSpecification FragmentSpecification::copy() const { return FragmentSpecification(*this); } - + bool FragmentSpecification::areProbabilityOperatorsAllowed() const { return probabilityOperator; } - + FragmentSpecification& FragmentSpecification::setProbabilityOperatorsAllowed(bool newValue) { this->probabilityOperator = newValue; return *this; } - + bool FragmentSpecification::areRewardOperatorsAllowed() const { return rewardOperator; } - + FragmentSpecification& FragmentSpecification::setRewardOperatorsAllowed(bool newValue) { this->rewardOperator = newValue; return *this; } - + bool FragmentSpecification::areTimeOperatorsAllowed() const { return expectedTimeOperator; } - + FragmentSpecification& FragmentSpecification::setTimeOperatorsAllowed(bool newValue) { this->expectedTimeOperator = newValue; return *this; } - + bool FragmentSpecification::areLongRunAverageOperatorsAllowed() const { return longRunAverageOperator; } - + FragmentSpecification& FragmentSpecification::setLongRunAverageOperatorsAllowed(bool newValue) { this->longRunAverageOperator = newValue; return *this; } - + bool FragmentSpecification::areMultiObjectiveFormulasAllowed() const { return multiObjectiveFormula; } - + FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulasAllowed( bool newValue) { this->multiObjectiveFormula = newValue; return *this; } - + bool FragmentSpecification::areQuantileFormulasAllowed() const { return quantileFormula; } - + FragmentSpecification& FragmentSpecification::setQuantileFormulasAllowed( bool newValue) { this->quantileFormula = newValue; return *this; } - + bool FragmentSpecification::areGloballyFormulasAllowed() const { return globallyFormula; } - + FragmentSpecification& FragmentSpecification::setGloballyFormulasAllowed(bool newValue) { this->globallyFormula = newValue; return *this; } - + bool FragmentSpecification::areReachabilityProbabilityFormulasAllowed() const { return reachabilityProbabilityFormula; } - + FragmentSpecification& FragmentSpecification::setReachabilityProbabilityFormulasAllowed(bool newValue) { this->reachabilityProbabilityFormula = newValue; return *this; } - + bool FragmentSpecification::areNextFormulasAllowed() const { return nextFormula; } - + FragmentSpecification& FragmentSpecification::setNextFormulasAllowed(bool newValue) { this->nextFormula = newValue; return *this; } - + bool FragmentSpecification::areUntilFormulasAllowed() const { return untilFormula; } - + FragmentSpecification& FragmentSpecification::setUntilFormulasAllowed(bool newValue) { this->untilFormula = newValue; return *this; } - + bool FragmentSpecification::areBoundedUntilFormulasAllowed() const { return boundedUntilFormula; } - + FragmentSpecification& FragmentSpecification::setBoundedUntilFormulasAllowed(bool newValue) { this->boundedUntilFormula = newValue; return *this; } - + bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const { return atomicExpressionFormula; } - + FragmentSpecification& FragmentSpecification::setAtomicExpressionFormulasAllowed(bool newValue) { this->atomicExpressionFormula = newValue; return *this; } - + bool FragmentSpecification::areAtomicLabelFormulasAllowed() const { return atomicLabelFormula; } - + FragmentSpecification& FragmentSpecification::setAtomicLabelFormulasAllowed(bool newValue) { this->atomicLabelFormula = newValue; return *this; } - + bool FragmentSpecification::areBooleanLiteralFormulasAllowed() const { return booleanLiteralFormula; } - + FragmentSpecification& FragmentSpecification::setBooleanLiteralFormulasAllowed(bool newValue) { this->booleanLiteralFormula = newValue; return *this; } - + bool FragmentSpecification::areUnaryBooleanStateFormulasAllowed() const { return unaryBooleanStateFormula; } - + FragmentSpecification& FragmentSpecification::setUnaryBooleanStateFormulasAllowed(bool newValue) { this->unaryBooleanStateFormula = newValue; return *this; } - + bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const { return binaryBooleanStateFormula; } - + FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) { this->binaryBooleanStateFormula = newValue; return *this; } - + bool FragmentSpecification::areCumulativeRewardFormulasAllowed() const { return cumulativeRewardFormula; } - + FragmentSpecification& FragmentSpecification::setCumulativeRewardFormulasAllowed(bool newValue) { this->cumulativeRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areInstantaneousRewardFormulasAllowed() const { return instantaneousRewardFormula; } - + FragmentSpecification& FragmentSpecification::setInstantaneousFormulasAllowed(bool newValue) { this->instantaneousRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areReachabilityRewardFormulasAllowed() const { return reachabilityRewardFormula; } - + FragmentSpecification& FragmentSpecification::setReachabilityRewardFormulasAllowed(bool newValue) { this->reachabilityRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areLongRunAverageRewardFormulasAllowed() const { return longRunAverageRewardFormula; } - + FragmentSpecification& FragmentSpecification::setLongRunAverageRewardFormulasAllowed(bool newValue) { this->longRunAverageRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areTotalRewardFormulasAllowed() const { return totalRewardFormula; } - + FragmentSpecification& FragmentSpecification::setTotalRewardFormulasAllowed(bool newValue) { this->totalRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areConditionalProbabilityFormulasAllowed() const { return conditionalProbabilityFormula; } - + FragmentSpecification& FragmentSpecification::setConditionalProbabilityFormulasAllowed(bool newValue) { this->conditionalProbabilityFormula = newValue; return *this; } - + bool FragmentSpecification::areConditionalRewardFormulasFormulasAllowed() const { return conditionalRewardFormula; } - + FragmentSpecification& FragmentSpecification::setConditionalRewardFormulasAllowed(bool newValue) { this->conditionalRewardFormula = newValue; return *this; } - + bool FragmentSpecification::areReachbilityTimeFormulasAllowed() const { return reachabilityTimeFormula; } - + FragmentSpecification& FragmentSpecification::setReachbilityTimeFormulasAllowed(bool newValue) { this->reachabilityTimeFormula = newValue; return *this; } - + bool FragmentSpecification::areNestedOperatorsAllowed() const { return this->nestedOperators; } - + FragmentSpecification& FragmentSpecification::setNestedOperatorsAllowed(bool newValue) { this->nestedOperators = newValue; return *this; } - + bool FragmentSpecification::areNestedPathFormulasAllowed() const { return this->nestedPathFormulas; } - + FragmentSpecification& FragmentSpecification::setNestedPathFormulasAllowed(bool newValue) { this->nestedPathFormulas = newValue; return *this; } - + bool FragmentSpecification::areNestedMultiObjectiveFormulasAllowed() const { return this->nestedMultiObjectiveFormulas; } - + FragmentSpecification& FragmentSpecification::setNestedMultiObjectiveFormulasAllowed(bool newValue) { this->nestedMultiObjectiveFormulas = newValue; return *this; } - + bool FragmentSpecification::areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const { return this->nestedOperatorsInsideMultiObjectiveFormulas; } - + FragmentSpecification& FragmentSpecification::setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue) { this->nestedOperatorsInsideMultiObjectiveFormulas = newValue; return *this; } - + bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const { return this->onlyEventuallyFormuluasInConditionalFormulas; } - + FragmentSpecification& FragmentSpecification::setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue) { this->onlyEventuallyFormuluasInConditionalFormulas = newValue; return *this; } - + bool FragmentSpecification::areStepBoundedUntilFormulasAllowed() const { return this->stepBoundedUntilFormulas; } - + FragmentSpecification& FragmentSpecification::setStepBoundedUntilFormulasAllowed(bool newValue) { this->stepBoundedUntilFormulas = newValue; return *this; } - + bool FragmentSpecification::areTimeBoundedUntilFormulasAllowed() const { return this->timeBoundedUntilFormulas; } - + FragmentSpecification& FragmentSpecification::setTimeBoundedUntilFormulasAllowed(bool newValue) { this->timeBoundedUntilFormulas = newValue; return *this; @@ -498,7 +498,7 @@ namespace storm { this->rewardBoundedUntilFormulas = newValue; return *this; } - + bool FragmentSpecification::areMultiDimensionalBoundedUntilFormulasAllowed() const { return this->multiDimensionalBoundedUntilFormulas; } @@ -511,16 +511,16 @@ namespace storm { bool FragmentSpecification::areStepBoundedCumulativeRewardFormulasAllowed() const { return this->stepBoundedCumulativeRewardFormulas; } - + FragmentSpecification& FragmentSpecification::setStepBoundedCumulativeRewardFormulasAllowed(bool newValue) { this->stepBoundedCumulativeRewardFormulas = newValue; return *this; } - + bool FragmentSpecification::areTimeBoundedCumulativeRewardFormulasAllowed() const { return this->timeBoundedCumulativeRewardFormulas; } - + FragmentSpecification& FragmentSpecification::setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue) { this->timeBoundedCumulativeRewardFormulas = newValue; return *this; @@ -534,7 +534,7 @@ namespace storm { this->rewardBoundedCumulativeRewardFormulas = newValue; return *this; } - + bool FragmentSpecification::areMultiDimensionalCumulativeRewardFormulasAllowed() const { return this->multiDimensionalCumulativeRewardFormulas; } @@ -543,7 +543,7 @@ namespace storm { this->multiDimensionalCumulativeRewardFormulas = newValue; return *this; } - + FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) { this->setProbabilityOperatorsAllowed(newValue); this->setRewardOperatorsAllowed(newValue); @@ -551,40 +551,40 @@ namespace storm { this->setTimeOperatorsAllowed(newValue); return *this; } - + FragmentSpecification& FragmentSpecification::setTimeAllowed(bool newValue) { this->setTimeOperatorsAllowed(newValue); this->setReachbilityTimeFormulasAllowed(newValue); return *this; } - + FragmentSpecification& FragmentSpecification::setLongRunAverageProbabilitiesAllowed(bool newValue) { this->setLongRunAverageOperatorsAllowed(newValue); return *this; } - + bool FragmentSpecification::isVarianceMeasureTypeAllowed() const { return varianceAsMeasureType; } - + FragmentSpecification& FragmentSpecification::setVarianceMeasureTypeAllowed(bool newValue) { this->varianceAsMeasureType = newValue; return *this; } - + bool FragmentSpecification::areQuantitativeOperatorResultsAllowed() const { return this->quantitativeOperatorResults; } - + FragmentSpecification& FragmentSpecification::setQuantitativeOperatorResultsAllowed(bool newValue) { this->quantitativeOperatorResults = newValue; return *this; } - + bool FragmentSpecification::areQualitativeOperatorResultsAllowed() const { return this->qualitativeOperatorResults; } - + FragmentSpecification& FragmentSpecification::setQualitativeOperatorResultsAllowed(bool newValue) { this->qualitativeOperatorResults = newValue; return *this; @@ -593,7 +593,7 @@ namespace storm { bool FragmentSpecification::isOperatorAtTopLevelRequired() const { return operatorAtTopLevelRequired; } - + FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) { operatorAtTopLevelRequired = newValue; return *this; @@ -602,7 +602,7 @@ namespace storm { bool FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired() const { return multiObjectiveFormulaAtTopLevelRequired; } - + FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired(bool newValue) { multiObjectiveFormulaAtTopLevelRequired = newValue; return *this; @@ -611,7 +611,7 @@ namespace storm { bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const { return operatorsAtTopLevelOfMultiObjectiveFormulasRequired; } - + FragmentSpecification& FragmentSpecification::setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue) { operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue; return *this; diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 19cf232ed..8ac56b885 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -6,9 +6,9 @@ namespace storm { namespace logic { - + class RewardAccumulation; - + class FragmentSpecification { public: FragmentSpecification(); @@ -16,24 +16,24 @@ namespace storm { FragmentSpecification(FragmentSpecification&& other) = default; FragmentSpecification& operator=(FragmentSpecification const& other) = default; FragmentSpecification& operator=(FragmentSpecification&& other) = default; - + FragmentSpecification copy() const; - + bool areProbabilityOperatorsAllowed() const; FragmentSpecification& setProbabilityOperatorsAllowed(bool newValue); - + bool areRewardOperatorsAllowed() const; FragmentSpecification& setRewardOperatorsAllowed(bool newValue); - + bool areTimeOperatorsAllowed() const; FragmentSpecification& setTimeOperatorsAllowed(bool newValue); bool areLongRunAverageOperatorsAllowed() const; FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue); - + bool areMultiObjectiveFormulasAllowed() const; FragmentSpecification& setMultiObjectiveFormulasAllowed( bool newValue); - + bool areQuantileFormulasAllowed() const; FragmentSpecification& setQuantileFormulasAllowed( bool newValue); @@ -75,10 +75,10 @@ namespace storm { bool areReachabilityRewardFormulasAllowed() const; FragmentSpecification& setReachabilityRewardFormulasAllowed(bool newValue); - + bool areLongRunAverageRewardFormulasAllowed() const; FragmentSpecification& setLongRunAverageRewardFormulasAllowed(bool newValue); - + bool areTotalRewardFormulasAllowed() const; FragmentSpecification& setTotalRewardFormulasAllowed(bool newValue); @@ -156,7 +156,7 @@ namespace storm { bool areGameFormulasAllowed() const; FragmentSpecification& setGameFormulasAllowed(bool newValue); - + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -217,16 +217,16 @@ namespace storm { bool multiObjectiveFormulaAtTopLevelRequired; bool quantileFormulaAtTopLevelRequired; bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired; - + bool rewardAccumulation; }; - + // Propositional. FragmentSpecification propositional(); - + // Just reachability properties. FragmentSpecification reachability(); - + // Regular PCTL. FragmentSpecification pctl(); @@ -238,16 +238,16 @@ namespace storm { // PCTL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification prctl(); - + // Regular CSL. FragmentSpecification csl(); - + // CSL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification csrl(); - + // Multi-Objective formulas. FragmentSpecification multiObjective(); - + // Quantile formulas. FragmentSpecification quantiles();