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

added rPATL to FragmentSpecifitcations

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
a93a8ed0b0
commit
0d7e763b00
2 changed files with 131 additions and 131 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 224
      src/storm/logic/FragmentSpecification.cpp
  2. 38
      src/storm/logic/FragmentSpecification.h

224
src/storm/logic/FragmentSpecification.cpp
View File

@ -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;

38
src/storm/logic/FragmentSpecification.h
View File

@ -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();

Write Preview
Loading…
Cancel
Save