diff --git a/examples/multiobjective/ma/stream/stream.ma b/examples/multiobjective/ma/stream/stream.ma new file mode 100644 index 000000000..820934a8c --- /dev/null +++ b/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 1 : (s'=1); + [start] s=0 & k 1 : (s'=2) & (k'=k+1); + + <> s=1 -> inRate : (n'=n+1) & (s'=0); + + <> s=2 & n inRate : (n'=n+1) + processingRate : (k'=k+1); + <> s=2 & n inRate : (n'=n+1) + processingRate : (s'=0); + <> s=2 & n=N & k 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 diff --git a/src/logic/CloneVisitor.cpp b/src/logic/CloneVisitor.cpp index d6161f324..89fe36cd3 100644 --- a/src/logic/CloneVisitor.cpp +++ b/src/logic/CloneVisitor.cpp @@ -78,8 +78,8 @@ namespace storm { boost::any CloneVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { std::vector> subformulas; - for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){ - subformulas.push_back(boost::any_cast>(f.getSubformula(index).accept(*this, data))); + for(auto const& subF : f.getSubformulas()){ + subformulas.push_back(boost::any_cast>(subF->accept(*this, data))); } return std::static_pointer_cast(std::make_shared(subformulas)); } diff --git a/src/logic/FormulaInformationVisitor.cpp b/src/logic/FormulaInformationVisitor.cpp index a23124031..ad588eac1 100644 --- a/src/logic/FormulaInformationVisitor.cpp +++ b/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(f.getSubformula(index).accept(*this))); + for(auto const& subF : f.getSubformulas()){ + result.join(boost::any_cast(subF->accept(*this))); } return result; } diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 1a1bc0087..8fc26c315 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -171,8 +171,11 @@ namespace storm { } bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed(); - for(uint_fast64_t index = 0; index(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(subF->accept(*this, InheritedInformation(subFormulaFragment))); } return result; } diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index 0235e5ddf..8602b10ea 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/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 { @@ -475,6 +477,15 @@ namespace storm { operatorAtTopLevelRequired = newValue; return *this; } + + bool FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const { + return operatorsAtTopLevelOfMultiObjectiveFormulasRequired; + } + + FragmentSpecification& FragmentSpecification::setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue) { + operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue; + return *this; + } } } diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index d19f7da11..587d49bf3 100644 --- a/src/logic/FragmentSpecification.h +++ b/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. diff --git a/src/logic/MultiObjectiveFormula.cpp b/src/logic/MultiObjectiveFormula.cpp index e3bfe3078..861628e69 100644 --- a/src/logic/MultiObjectiveFormula.cpp +++ b/src/logic/MultiObjectiveFormula.cpp @@ -58,7 +58,7 @@ namespace storm { return this->subformulas.size(); } - std::vector> const& MultiObjectiveFormula::getSubFormulas() const { + std::vector> const& MultiObjectiveFormula::getSubformulas() const { return this->subformulas; } diff --git a/src/logic/MultiObjectiveFormula.h b/src/logic/MultiObjectiveFormula.h index 0e597d89f..e5e1dea2a 100644 --- a/src/logic/MultiObjectiveFormula.h +++ b/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> const& getSubFormulas() const; + std::vector> const& getSubformulas() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 5d1661412..a4149ff58 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/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(); diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp index 246db82c9..3fe0c46bd 100644 --- a/test/functional/logic/FragmentCheckerTest.cpp +++ b/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 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)); }