added rPATL to FragmentSpecifitcations

5 years ago · 8dc46968cb
2 changed files with 60 additions and 34 deletions
--- 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;
+        }
+
+
    }
 }
--- 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();