updated fragment checking for multi objective formulas

Former-commit-id: 8538e97e00

examples/multiobjective/ma/stream/stream.ma

@@ -0,0 +1,50 @@
+
+ma
+
+const int N; // num packages
+
+const double inRate = 4;
+const double processingRate = 5;
+
+module streamingclient
+	
+	s : [0..3]; // current state:
+	// 0: decide whether to start	
+	// 1: buffering
+	// 2: running
+	// 3: done
+	
+	n : [0..N]; // number of received packages
+	k : [0..N]; // number of processed packages 	
+	
+	[buffer]  s=0 & n<N -> 1 : (s'=1);
+	[start] s=0 & k<n -> 1 : (s'=2) & (k'=k+1);
+	
+	<> s=1 -> inRate : (n'=n+1) & (s'=0);
+	
+	<> s=2 & n<N & k<n -> inRate : (n'=n+1) + processingRate : (k'=k+1);
+	<> s=2 & n<N & k=n -> inRate : (n'=n+1) + processingRate : (s'=0); 
+	<> s=2 & n=N & k<n -> processingRate : (k'=k+1);
+	<> s=2 & n=N & k=N -> processingRate : (s'=3);
+	
+	<> s=3 -> 1 : true;
+endmodule
+
+// All packages received and buffer empty
+label "done" = (s=3);
+
+rewards "buffering"
+	s=1 : 1;
+endrewards
+
+rewards "initialbuffering"
+	s=1 & k = 0: 1;
+endrewards
+
+rewards "intermediatebuffering"
+	s=1 & k > 0: 1;
+endrewards
+
+rewards "numRestarts"
+	[start] k > 0 : 1;
+endrewards

src/logic/CloneVisitor.cpp

@@ -78,8 +78,8 @@ namespace storm {
         
         boost::any CloneVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
             std::vector<std::shared_ptr<Formula const>> subformulas;
-            for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){
-                subformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula(index).accept(*this, data)));
+            for(auto const& subF : f.getSubformulas()){
+                subformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(subF->accept(*this, data)));
             }
             return std::static_pointer_cast<Formula>(std::make_shared<MultiObjectiveFormula>(subformulas));
         }

src/logic/FormulaInformationVisitor.cpp

@@ -63,8 +63,8 @@ namespace storm {
         
         boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
             FormulaInformation result;
-            for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){
-                result.join(boost::any_cast<FormulaInformation>(f.getSubformula(index).accept(*this)));
+            for(auto const& subF : f.getSubformulas()){
+                result.join(boost::any_cast<FormulaInformation>(subF->accept(*this)));
             }
             return result;
         }

src/logic/FragmentChecker.cpp

@@ -171,8 +171,11 @@ namespace storm {
             }
             
             bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed();
-            for(uint_fast64_t index = 0; index<f.getNumberOfSubformulas(); ++index){
-                result = result && boost::any_cast<bool>(f.getSubformula(index).accept(*this, InheritedInformation(subFormulaFragment)));
+            for(auto const& subF : f.getSubformulas()){
+                if(inherited.getSpecification().areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()){
+                    result = result && subF->isOperatorFormula();
+                }
+                result = result && boost::any_cast<bool>(subF->accept(*this, InheritedInformation(subFormulaFragment)));
             }
             return result;
         }

src/logic/FragmentSpecification.cpp

@@ -87,6 +87,7 @@ namespace storm {
             FragmentSpecification multiObjective = propositional();
             
             multiObjective.setMultiObjectiveFormulasAllowed(true);
+            multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true);
             multiObjective.setProbabilityOperatorsAllowed(true);
             multiObjective.setUntilFormulasAllowed(true);
             multiObjective.setGloballyFormulasAllowed(true);
@@ -144,6 +145,7 @@ namespace storm {
             quantitativeOperatorResults = true;
             
             operatorAtTopLevelRequired = false;
+            operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
         }
         
         FragmentSpecification FragmentSpecification::copy() const {
@@ -476,5 +478,14 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const {
+            return operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue) {
+            operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue;
+            return *this;
+        }
+        
     }
 }

src/logic/FragmentSpecification.h

@@ -115,6 +115,9 @@ namespace storm {
             bool isOperatorAtTopLevelRequired() const;
             FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue);
             
+            bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
+            FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
+            
             FragmentSpecification& setOperatorsAllowed(bool newValue);
             FragmentSpecification& setTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
@@ -163,6 +166,7 @@ namespace storm {
             bool quantitativeOperatorResults;
             bool qualitativeOperatorResults;
             bool operatorAtTopLevelRequired;
+            bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
         };
         
         // Propositional.

src/logic/MultiObjectiveFormula.cpp

@@ -58,7 +58,7 @@ namespace storm {
             return this->subformulas.size();
         }
         
-        std::vector<std::shared_ptr<Formula const>> const& MultiObjectiveFormula::getSubFormulas() const {
+        std::vector<std::shared_ptr<Formula const>> const& MultiObjectiveFormula::getSubformulas() const {
             return this->subformulas;
         }
         

src/logic/MultiObjectiveFormula.h

@@ -20,7 +20,7 @@ namespace storm {
             
             Formula const& getSubformula(uint_fast64_t index) const;
             uint_fast64_t getNumberOfSubformulas() const;
-            std::vector<std::shared_ptr<Formula const>> const& getSubFormulas() const;
+            std::vector<std::shared_ptr<Formula const>> const& getSubformulas() const;
             
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp

@@ -26,7 +26,7 @@ namespace storm {
                 PreprocessorData data(originalFormula, originalModel, SparseModelType(originalModel), storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()));
                 
                 //Invoke preprocessing on the individual objectives
-                for(auto const& subFormula : originalFormula.getSubFormulas()){
+                for(auto const& subFormula : originalFormula.getSubformulas()){
                     STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< ".");
                     data.objectives.emplace_back();
                     ObjectiveInformation& currentObjective = data.objectives.back();

test/functional/logic/FragmentCheckerTest.cpp

@@ -133,7 +133,7 @@ TEST(FragmentCheckerTest, Csrl) {
 
 TEST(FragmentCheckerTest, MultiObjective) {
     storm::logic::FragmentChecker checker;
-    storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective().setNestedOperatorsInsideMultiObjectiveFormulasAllowed(true);
+    storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective();
     
     storm::parser::FormulaParser formulaParser;
     std::shared_ptr<storm::logic::Formula const> formula;
@@ -150,23 +150,31 @@ TEST(FragmentCheckerTest, MultiObjective) {
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
     EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
     
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C]"));
     EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
     
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0.5,1] \"label\"]"));
     EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])"));
-    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])"));
+    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
+    
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], \"label\", R<=4[F \"label\"])"));
+    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], \"label\" )"));
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
     EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
     
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], multi(\"label\", \"label\"))"));
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
+    EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
+    
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], multi(P<0.6 [F \"label\"], R<=4[F \"label\"]))"));
     EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
-    multiobjective.setNestedOperatorsInsideMultiObjectiveFormulasAllowed(false);
-    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], \"label\" )"));
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
+    
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )"));
     EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
     
 }