From 63da45018e3e32a1b5b202c4bba4402252ca569b Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 23 May 2016 15:22:26 +0200 Subject: [PATCH 001/109] Added support for multi objective formulas Former-commit-id: 3d98b7104971e161244c86b7defdc698c4249981 --- src/logic/CloneVisitor.cpp | 8 ++ src/logic/CloneVisitor.h | 1 + src/logic/Formula.cpp | 12 +++ src/logic/Formula.h | 5 ++ src/logic/FormulaInformationVisitor.cpp | 8 ++ src/logic/FormulaInformationVisitor.h | 1 + src/logic/FormulaVisitor.h | 1 + src/logic/Formulas.h | 1 + src/logic/FormulasForwardDeclarations.h | 1 + src/logic/FragmentChecker.cpp | 15 ++++ src/logic/FragmentChecker.h | 1 + src/logic/FragmentSpecification.cpp | 38 ++++++++++ src/logic/FragmentSpecification.h | 14 +++- src/logic/MultiObjectiveFormula.cpp | 78 ++++++++++++++++++++ src/logic/MultiObjectiveFormula.h | 35 +++++++++ src/logic/ToExpressionVisitor.cpp | 4 + src/logic/ToExpressionVisitor.h | 1 + src/parser/FormulaParser.cpp | 17 ++++- test/functional/parser/FormulaParserTest.cpp | 31 ++++++++ 19 files changed, 269 insertions(+), 3 deletions(-) create mode 100644 src/logic/MultiObjectiveFormula.cpp create mode 100644 src/logic/MultiObjectiveFormula.h diff --git a/src/logic/CloneVisitor.cpp b/src/logic/CloneVisitor.cpp index fe7182bf7..3ed09346c 100644 --- a/src/logic/CloneVisitor.cpp +++ b/src/logic/CloneVisitor.cpp @@ -76,6 +76,14 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f)); } + 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))); + } + return std::static_pointer_cast(std::make_shared(subformulas)); + } + boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula)); diff --git a/src/logic/CloneVisitor.h b/src/logic/CloneVisitor.h index 23fc3ffdc..55c0d89c4 100644 --- a/src/logic/CloneVisitor.h +++ b/src/logic/CloneVisitor.h @@ -25,6 +25,7 @@ namespace storm { virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index de915eaa1..cdd259063 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -17,6 +17,10 @@ namespace storm { return false; } + bool Formula::isMultiObjectiveFormula() const { + return false; + } + bool Formula::isBinaryStateFormula() const { return false; } @@ -183,6 +187,14 @@ namespace storm { return dynamic_cast(*this); } + MultiObjectiveFormula& Formula::asMultiObjectiveFormula() { + return dynamic_cast(*this); + } + + MultiObjectiveFormula const& Formula::asMultiObjectiveFormula() const { + return dynamic_cast(*this); + } + BinaryStateFormula& Formula::asBinaryStateFormula() { return dynamic_cast(*this); } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index d5625a296..c2d763f46 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -46,6 +46,8 @@ namespace storm { virtual bool isBinaryBooleanStateFormula() const; virtual bool isUnaryBooleanStateFormula() const; + + virtual bool isMultiObjectiveFormula() const; // Operator formulas. virtual bool isOperatorFormula() const; @@ -101,6 +103,9 @@ namespace storm { StateFormula& asStateFormula(); StateFormula const& asStateFormula() const; + MultiObjectiveFormula& asMultiObjectiveFormula(); + MultiObjectiveFormula const& asMultiObjectiveFormula() const; + BinaryStateFormula& asBinaryStateFormula(); BinaryStateFormula const& asBinaryStateFormula() const; diff --git a/src/logic/FormulaInformationVisitor.cpp b/src/logic/FormulaInformationVisitor.cpp index b44045766..f7371abb7 100644 --- a/src/logic/FormulaInformationVisitor.cpp +++ b/src/logic/FormulaInformationVisitor.cpp @@ -61,6 +61,14 @@ namespace storm { return FormulaInformation(); } + 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))); + } + return result; + } + boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const { return boost::any_cast(f.getSubformula().accept(*this)).setContainsNextFormula(); } diff --git a/src/logic/FormulaInformationVisitor.h b/src/logic/FormulaInformationVisitor.h index 8e706cabf..444b34b1f 100644 --- a/src/logic/FormulaInformationVisitor.h +++ b/src/logic/FormulaInformationVisitor.h @@ -24,6 +24,7 @@ namespace storm { virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; diff --git a/src/logic/FormulaVisitor.h b/src/logic/FormulaVisitor.h index 1208b63a6..b0b920e53 100644 --- a/src/logic/FormulaVisitor.h +++ b/src/logic/FormulaVisitor.h @@ -23,6 +23,7 @@ namespace storm { virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(NextFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0; diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index 7183dcb01..50b51ebb2 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -18,6 +18,7 @@ #include "src/logic/RewardOperatorFormula.h" #include "src/logic/StateFormula.h" #include "src/logic/LongRunAverageOperatorFormula.h" +#include "src/logic/MultiObjectiveFormula.h" #include "src/logic/TimeOperatorFormula.h" #include "src/logic/UnaryBooleanStateFormula.h" #include "src/logic/UnaryPathFormula.h" diff --git a/src/logic/FormulasForwardDeclarations.h b/src/logic/FormulasForwardDeclarations.h index 43fcf0ab9..d8da094eb 100644 --- a/src/logic/FormulasForwardDeclarations.h +++ b/src/logic/FormulasForwardDeclarations.h @@ -20,6 +20,7 @@ namespace storm { class InstantaneousRewardFormula; class LongRunAverageOperatorFormula; class LongRunAverageRewardFormula; + class MultiObjectiveFormula; class NextFormula; class OperatorFormula; class PathFormula; diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index b86a96693..26a787455 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -159,6 +159,21 @@ namespace storm { return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed(); } + boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + + FragmentSpecification subFormulaFragment(inherited.getSpecification()); + if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){ + subFormulaFragment.setMultiObjectiveFormulasAllowed(false); + } + + bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed(); + for(uint_fast64_t index = 0; index(f.getSubformula(index).accept(*this, InheritedInformation(subFormulaFragment))); + } + return result; + } + boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areNextFormulasAllowed(); diff --git a/src/logic/FragmentChecker.h b/src/logic/FragmentChecker.h index 9b0377aba..41846c37f 100644 --- a/src/logic/FragmentChecker.h +++ b/src/logic/FragmentChecker.h @@ -25,6 +25,7 @@ namespace storm { virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index 3dd2bf12b..9014873c0 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -83,12 +83,31 @@ namespace storm { return csrl; } + FragmentSpecification multiObjective() { + FragmentSpecification multiObjective = propositional(); + + multiObjective.setMultiObjectiveFormulasAllowed(true); + multiObjective.setProbabilityOperatorsAllowed(true); + multiObjective.setUntilFormulasAllowed(true); + multiObjective.setReachabilityProbabilityFormulasAllowed(true); + multiObjective.setRewardOperatorsAllowed(true); + multiObjective.setReachabilityRewardFormulasAllowed(true); + multiObjective.setBoundedUntilFormulasAllowed(true); + multiObjective.setStepBoundedUntilFormulasAllowed(true); + // multiObjective.setTimeBoundedUntilFormulasAllowed(true); //probably better to activate this only when an MA is given... + multiObjective.setNestedOperatorsAllowed(false); + + return multiObjective; + } + FragmentSpecification::FragmentSpecification() { probabilityOperator = false; rewardOperator = false; expectedTimeOperator = false; longRunAverageOperator = false; + multiObjectiveFormula = false; + globallyFormula = false; reachabilityProbabilityFormula = false; nextFormula = false; @@ -113,6 +132,7 @@ namespace storm { nestedOperators = true; nestedPathFormulas = false; + setNestedMultiObjectiveFormulasAllowed(false); onlyEventuallyFormuluasInConditionalFormulas = true; stepBoundedUntilFormulas = false; timeBoundedUntilFormulas = false; @@ -164,6 +184,15 @@ namespace storm { return *this; } + bool FragmentSpecification::areMultiObjectiveFormulasAllowed() const { + return multiObjectiveFormula; + } + + FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulasAllowed( bool newValue) { + this->multiObjectiveFormula = newValue; + return *this; + } + bool FragmentSpecification::areGloballyFormulasAllowed() const { return globallyFormula; } @@ -334,6 +363,15 @@ namespace storm { this->nestedPathFormulas = newValue; return *this; } + + bool FragmentSpecification::areNestedMultiObjectiveFormulasAllowed() const { + return this->nestedMultiObjectiveFormulas; + } + + FragmentSpecification& FragmentSpecification::setNestedMultiObjectiveFormulasAllowed(bool newValue) { + this->nestedMultiObjectiveFormulas = newValue; + return *this; + } bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const { return this->onlyEventuallyFormuluasInConditionalFormulas; diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index 6637d0750..c53b287d0 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -24,6 +24,9 @@ namespace storm { bool areLongRunAverageOperatorsAllowed() const; FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue); + + bool areMultiObjectiveFormulasAllowed() const; + FragmentSpecification& setMultiObjectiveFormulasAllowed( bool newValue); bool areGloballyFormulasAllowed() const; FragmentSpecification& setGloballyFormulasAllowed(bool newValue); @@ -78,10 +81,13 @@ namespace storm { bool areNestedOperatorsAllowed() const; FragmentSpecification& setNestedOperatorsAllowed(bool newValue); - + bool areNestedPathFormulasAllowed() const; FragmentSpecification& setNestedPathFormulasAllowed(bool newValue); + bool areNestedMultiObjectiveFormulasAllowed() const; + FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue); + bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const; FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue); @@ -114,6 +120,8 @@ namespace storm { bool expectedTimeOperator; bool longRunAverageOperator; + bool multiObjectiveFormula; + bool globallyFormula; bool reachabilityProbabilityFormula; bool nextFormula; @@ -139,6 +147,7 @@ namespace storm { // Members that indicate certain restrictions. bool nestedOperators; bool nestedPathFormulas; + bool nestedMultiObjectiveFormulas; bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; @@ -168,6 +177,9 @@ namespace storm { // CSL + cumulative, instantaneous, reachability and long-run rewards. FragmentSpecification csrl(); + + // Multi-Objective formulas. + FragmentSpecification multiObjective(); } } diff --git a/src/logic/MultiObjectiveFormula.cpp b/src/logic/MultiObjectiveFormula.cpp new file mode 100644 index 000000000..22d02b40d --- /dev/null +++ b/src/logic/MultiObjectiveFormula.cpp @@ -0,0 +1,78 @@ +#include "src/logic/MultiObjectiveFormula.h" + +#include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace logic { + + MultiObjectiveFormula::MultiObjectiveFormula(std::vector> const& subformulas) : subformulas(subformulas) { + //Intentionally left empty + } + + MultiObjectiveFormula::~MultiObjectiveFormula() { + //Intentionally left empty + } + + bool MultiObjectiveFormula::isMultiObjectiveFormula() const { + return true; + } + + bool MultiObjectiveFormula::hasQualitativeResult() const { + for(auto const& subformula : this->subformulas){ + if(subformula->hasQuantitativeResult()){ + return false; + } + } + return true; + } + + bool MultiObjectiveFormula::hasQuantitativeResult() const { + return !hasQualitativeResult(); + }; + + Formula const& MultiObjectiveFormula::getSubformula(uint_fast64_t index) const { + STORM_LOG_THROW(index < getNumberOfSubformulas(), storm::exceptions::InvalidArgumentException, "Tried to access subformula with index " << index << " but there are only " << this->getNumberOfSubformulas() << " subformulas."); + return *this->subformulas[index]; + } + + uint_fast64_t MultiObjectiveFormula::getNumberOfSubformulas() const { + return this->subformulas.size(); + } + + boost::any MultiObjectiveFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + void MultiObjectiveFormula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { + for(auto const& subformula : this->subformulas){ + subformula->gatherAtomicExpressionFormulas(atomicExpressionFormulas); + } + } + + void MultiObjectiveFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { + for(auto const& subformula : this->subformulas){ + subformula->gatherAtomicLabelFormulas(atomicLabelFormulas); + } + } + + void MultiObjectiveFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + for(auto const& subformula : this->subformulas){ + subformula->gatherReferencedRewardModels(referencedRewardModels); + } + } + + std::ostream& MultiObjectiveFormula::writeToStream(std::ostream &out) const { + out << "multi("; + for(uint_fast64_t index = 0; index < this->getNumberOfSubformulas(); ++index){ + if(index>0){ + out << ", "; + } + this->getSubformula(index).writeToStream(out); + } + out << ")"; + return out; + } + } +} \ No newline at end of file diff --git a/src/logic/MultiObjectiveFormula.h b/src/logic/MultiObjectiveFormula.h new file mode 100644 index 000000000..7647300ac --- /dev/null +++ b/src/logic/MultiObjectiveFormula.h @@ -0,0 +1,35 @@ +#ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ +#define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ + +#include "src/logic/Formula.h" + +namespace storm { + namespace logic { + class MultiObjectiveFormula : public Formula { + public: + MultiObjectiveFormula(std::vector> const& subformulas); + + virtual ~MultiObjectiveFormula(); + + virtual bool isMultiObjectiveFormula() const override; + + virtual bool hasQualitativeResult() const override; + virtual bool hasQuantitativeResult() const override; + + Formula const& getSubformula(uint_fast64_t index) const; + uint_fast64_t getNumberOfSubformulas() const; + + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; + virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + private: + std::vector> subformulas; + }; + } +} + +#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */ \ No newline at end of file diff --git a/src/logic/ToExpressionVisitor.cpp b/src/logic/ToExpressionVisitor.cpp index 53dfedeca..534cc008b 100644 --- a/src/logic/ToExpressionVisitor.cpp +++ b/src/logic/ToExpressionVisitor.cpp @@ -82,6 +82,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } + boost::any ToExpressionVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(NextFormula const& f, boost::any const& data) const { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } diff --git a/src/logic/ToExpressionVisitor.h b/src/logic/ToExpressionVisitor.h index ee4a81d8f..ed325d38f 100644 --- a/src/logic/ToExpressionVisitor.h +++ b/src/logic/ToExpressionVisitor.h @@ -25,6 +25,7 @@ namespace storm { virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override; + virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override; virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index db6e8a1ea..206d08b13 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -36,7 +36,8 @@ namespace storm { ("max", 4) ("F", 5) ("G", 6) - ("X", 7); + ("X", 7) + ("multi", 8); } }; @@ -144,6 +145,8 @@ namespace storm { qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> longRunAverageRewardFormula; + qi::rule(), Skipper> multiObjectiveFormula; + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; @@ -166,6 +169,7 @@ namespace storm { std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + std::shared_ptr createMultiObjectiveFormula(std::vector> const& subformulas); // An error handler function. phoenix::function handler; @@ -340,7 +344,10 @@ namespace storm { orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; orStateFormula.name("or state formula"); - stateFormula = (orStateFormula); + multiObjectiveFormula = (qi::lit("multi") > qi::lit("(") >> (stateFormula % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiObjectiveFormula, phoenix::ref(*this), qi::_1)]; + multiObjectiveFormula.name("Multi-objective formula"); + + stateFormula = (orStateFormula | multiObjectiveFormula); stateFormula.name("state formula"); start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; @@ -369,6 +376,7 @@ namespace storm { debug(rewardPathFormula); debug(cumulativeRewardFormula); debug(instantaneousRewardFormula); + debug(multiObjectiveFormula); */ // Enable error reporting. @@ -395,6 +403,7 @@ namespace storm { qi::on_error(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { @@ -519,6 +528,10 @@ namespace storm { return subformula; } } + + std::shared_ptr FormulaParserGrammar::createMultiObjectiveFormula(std::vector> const& subformulas) { + return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); + } } // namespace parser } // namespace storm diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp index 1435806eb..da7d02804 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/test/functional/parser/FormulaParserTest.cpp @@ -148,3 +148,34 @@ TEST(FormulaParserTest, WrongFormatTest) { input = "P>0.5 [F y!=0)]"; EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); } + +TEST(FormulaParserTest, MultiObjectiveFormulaTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])"; + std::vector> formulas; + ASSERT_NO_THROW(formulas = formulaParser.parseFromString(input)); + ASSERT_EQ(1, formulas.size()); + ASSERT_TRUE(formulas[0]->isMultiObjectiveFormula()); + storm::logic::MultiObjectiveFormula mof = formulas[0]->asMultiObjectiveFormula(); + ASSERT_EQ(3, mof.getNumberOfSubformulas()); + + ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula()); + ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); + ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().hasBound()); + ASSERT_EQ(0.9, mof.getSubformula(0).asProbabilityOperatorFormula().getBound().threshold); + + ASSERT_TRUE(mof.getSubformula(1).isRewardOperatorFormula()); + ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); + ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().hasBound()); + ASSERT_EQ(42, mof.getSubformula(1).asRewardOperatorFormula().getBound().threshold); + + ASSERT_TRUE(mof.getSubformula(2).isProbabilityOperatorFormula()); + ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); + ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); + ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().hasOptimalityType()); + ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asProbabilityOperatorFormula().getOptimalityType())); + +} From 670ab6e241c2a035c2dce6c49331ab1971a249d1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 23 May 2016 16:00:54 +0200 Subject: [PATCH 002/109] added a simple example Former-commit-id: 1af510712a473f94610401a5fc0a0050573565dd --- examples/multi-objective/mdp/simple/simple.nm | 26 +++++++++++++++++++ .../multi-objective/mdp/simple/simple.pctl | 3 +++ 2 files changed, 29 insertions(+) create mode 100644 examples/multi-objective/mdp/simple/simple.nm create mode 100644 examples/multi-objective/mdp/simple/simple.pctl diff --git a/examples/multi-objective/mdp/simple/simple.nm b/examples/multi-objective/mdp/simple/simple.nm new file mode 100644 index 000000000..50c4fe344 --- /dev/null +++ b/examples/multi-objective/mdp/simple/simple.nm @@ -0,0 +1,26 @@ +// sum of two dice as the asynchronous parallel composition of +// two copies of Knuth's model of a fair die using only fair coins + +mdp + +module simple + + // local state + s : [0..2] init 0; + + [A] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0); + [B] s=0 -> 1 : (s'=2); + [] s>0 -> 1 : (s'=s); +endmodule + +rewards "actA" + [A] true : 1; +endrewards + +rewards "actB" + [B] true : 2; +endrewards + + +label "a" = s=1; +label "b" = s=2; \ No newline at end of file diff --git a/examples/multi-objective/mdp/simple/simple.pctl b/examples/multi-objective/mdp/simple/simple.pctl new file mode 100644 index 000000000..1300542f9 --- /dev/null +++ b/examples/multi-objective/mdp/simple/simple.pctl @@ -0,0 +1,3 @@ +Pmax=? [ F "a" ] ; +Pmax=? [ F "b" ] ; +multi(P>0.4 [ F "a"], P>0.3 [ F "b"] ) \ No newline at end of file From fc24c5596074807d1587108196f193742ebd84f6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 26 May 2016 21:40:04 +0200 Subject: [PATCH 003/109] some preprocessing for multi-objective formulas Former-commit-id: 3a909154f77c6b7f699833bc8b3752674b67d9b6 --- src/CMakeLists.txt | 5 +- src/logic/FragmentChecker.cpp | 3 + src/logic/FragmentSpecification.cpp | 18 +- src/logic/FragmentSpecification.h | 4 + src/logic/MultiObjectiveFormula.cpp | 25 +- src/logic/MultiObjectiveFormula.h | 10 +- src/modelchecker/AbstractModelChecker.cpp | 7 + src/modelchecker/AbstractModelChecker.h | 6 +- .../SparseMdpMultiObjectiveModelChecker.cpp | 46 ++++ .../SparseMdpMultiObjectiveModelChecker.h | 27 ++ ...seMdpMultiObjectivePreprocessingHelper.cpp | 254 ++++++++++++++++++ ...arseMdpMultiObjectivePreprocessingHelper.h | 62 +++++ ...rseMultiObjectiveModelCheckerInformation.h | 83 ++++++ src/utility/storm.h | 17 +- test/functional/logic/FragmentCheckerTest.cpp | 40 +++ 15 files changed, 590 insertions(+), 17 deletions(-) create mode 100644 src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp create mode 100644 src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h create mode 100644 src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp create mode 100644 src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h create mode 100644 src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 34b3cf77b..35d2e1d92 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,6 +24,8 @@ file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/ file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_EXPLORATION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp) +file(GLOB STORM_MODELCHECKER_MULTIOBJECTIVE_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/*.cpp) +file(GLOB_RECURSE STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/helper/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp) file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/permissivesched/*.h ${PROJECT_SOURCE_DIR}/src/permissivesched/*.cpp) @@ -78,6 +80,8 @@ source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FIL source_group(modelchecker\\exploration FILES ${STORM_MODELCHECKER_EXPLORATION_FILES}) source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES}) source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES}) +source_group(modelchecker\\multiobjective FILES ${STORM_MODELCHECKER_MULTIOBJECTIVE_FILES}) +source_group(modelchecker\\multiobjective\\helper FILES ${STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_FILES}) source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES}) source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES}) @@ -133,7 +137,6 @@ set_target_properties(storm-dft-main PROPERTIES OUTPUT_NAME "storm-dft") target_link_libraries(storm ${STORM_LINK_LIBRARIES}) - INSTALL(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 26a787455..b4bda1f8f 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -166,6 +166,9 @@ namespace storm { if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){ subFormulaFragment.setMultiObjectiveFormulasAllowed(false); } + if(!inherited.getSpecification().areNestedOperatorsInsideMultiObjectiveFormulasAllowed()){ + subFormulaFragment.setNestedOperatorsAllowed(false); + } bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed(); for(uint_fast64_t index = 0; indexnestedMultiObjectiveFormulas = 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; } diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index c53b287d0..88910988d 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -88,6 +88,9 @@ namespace storm { bool areNestedMultiObjectiveFormulasAllowed() const; FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue); + bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const; + FragmentSpecification& setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue); + bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const; FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue); @@ -148,6 +151,7 @@ namespace storm { bool nestedOperators; bool nestedPathFormulas; bool nestedMultiObjectiveFormulas; + bool nestedOperatorsInsideMultiObjectiveFormulas; bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; diff --git a/src/logic/MultiObjectiveFormula.cpp b/src/logic/MultiObjectiveFormula.cpp index 22d02b40d..4717fd1e4 100644 --- a/src/logic/MultiObjectiveFormula.cpp +++ b/src/logic/MultiObjectiveFormula.cpp @@ -30,7 +30,24 @@ namespace storm { bool MultiObjectiveFormula::hasQuantitativeResult() const { return !hasQualitativeResult(); - }; + } + + bool MultiObjectiveFormula::hasNumericalResult() const { + bool hasExactlyOneQualitativeSubformula = false; + for(auto const& subformula : this->subformulas){ + if(subformula->hasQualitativeResult()){ + if(hasExactlyOneQualitativeSubformula){ + return false; + } + hasExactlyOneQualitativeSubformula=true; + } + } + return hasExactlyOneQualitativeSubformula; + } + + bool MultiObjectiveFormula::hasParetoCurveResult() const { + return hasQuantitativeResult() && !hasNumericalResult(); + } Formula const& MultiObjectiveFormula::getSubformula(uint_fast64_t index) const { STORM_LOG_THROW(index < getNumberOfSubformulas(), storm::exceptions::InvalidArgumentException, "Tried to access subformula with index " << index << " but there are only " << this->getNumberOfSubformulas() << " subformulas."); @@ -41,6 +58,10 @@ namespace storm { return this->subformulas.size(); } + std::vector> const& MultiObjectiveFormula::getSubFormulas() const { + return this->subformulas; + } + boost::any MultiObjectiveFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } @@ -75,4 +96,4 @@ namespace storm { return out; } } -} \ No newline at end of file +} diff --git a/src/logic/MultiObjectiveFormula.h b/src/logic/MultiObjectiveFormula.h index 7647300ac..0e597d89f 100644 --- a/src/logic/MultiObjectiveFormula.h +++ b/src/logic/MultiObjectiveFormula.h @@ -13,12 +13,14 @@ namespace storm { virtual bool isMultiObjectiveFormula() const override; - virtual bool hasQualitativeResult() const override; - virtual bool hasQuantitativeResult() const override; + virtual bool hasQualitativeResult() const override; // Result is true or false + virtual bool hasQuantitativeResult() const override; // Result is numerical or a pareto curve + virtual bool hasNumericalResult() const; // Result is numerical + virtual bool hasParetoCurveResult() const; // Result is a pareto curve Formula const& getSubformula(uint_fast64_t index) const; uint_fast64_t getNumberOfSubformulas() 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; @@ -32,4 +34,4 @@ namespace storm { } } -#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */ diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 4fd86a13e..2e9ac6e43 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -14,6 +14,9 @@ namespace storm { std::unique_ptr AbstractModelChecker::check(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); + if (formula.isMultiObjectiveFormula()){ + return this->checkMultiObjectiveFormula(checkTask.substituteFormula(formula.asMultiObjectiveFormula())); + } if (formula.isStateFormula()) { return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula())); } @@ -240,5 +243,9 @@ namespace storm { } return subResult; } + + std::unique_ptr AbstractModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); + } } } diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index b6f009197..da69db224 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -69,8 +69,12 @@ namespace storm { virtual std::unique_ptr checkTimeOperatorFormula(CheckTask const& checkTask); virtual std::unique_ptr checkLongRunAverageOperatorFormula(CheckTask const& checkTask); virtual std::unique_ptr checkUnaryBooleanStateFormula(CheckTask const& checkTask); + + // The methods to check multi-objective formulas. + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask); + }; } } -#endif /* STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp new file mode 100644 index 000000000..7d94481f8 --- /dev/null +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -0,0 +1,46 @@ +#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" + +#include "src/utility/macros.h" +#include "src/logic/Formulas.h" +#include "src/logic/FragmentSpecification.h" + +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" + +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + template + SparseMdpMultiObjectiveModelChecker::SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model) : SparseMdpPrctlModelChecker(model) { + // Intentionally left empty. + } + + template + bool SparseMdpMultiObjectiveModelChecker::canHandle(CheckTask const& checkTask) const { + // A formula without multi objective (sub)formulas can be handled by the base class + if(SparseMdpPrctlModelChecker::canHandle(checkTask)) return true; + //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this. + if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + return checkTask.getFormula().isInFragment(storm::logic::multiObjective()); + } + + template + std::unique_ptr SparseMdpMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + + helper::SparseMultiObjectiveModelCheckerInformation info = helper::SparseMdpMultiObjectivePreprocessingHelper::preprocess(checkTask.getFormula(), this->getModel()); + + return std::unique_ptr(new ExplicitQualitativeCheckResult()); + } + + + + template class SparseMdpMultiObjectiveModelChecker>; + } +} diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h new file mode 100644 index 000000000..f6e1efdf9 --- /dev/null +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h @@ -0,0 +1,27 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ + +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" + +namespace storm { + namespace modelchecker { + template + class SparseMdpMultiObjectiveModelChecker : public SparseMdpPrctlModelChecker { + public: + typedef typename SparseMdpModelType::ValueType ValueType; + typedef typename SparseMdpModelType::RewardModelType RewardModelType; + + explicit SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model); + + virtual bool canHandle(CheckTask const& checkTask) const override; + + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; + + private: + + + }; + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp new file mode 100644 index 000000000..4366fc1a8 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp @@ -0,0 +1,254 @@ + #include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h" + +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "src/storage/BitVector.h" + +#include "src/utility/macros.h" +#include "src/utility/vector.h" +#include "src/utility/graph.h" + +#include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseMultiObjectiveModelCheckerInformation SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseMdpModelType originalModel) { + Information info(std::move(originalModel)); + + //Initialize the state mapping. + info.getNewToOldStateMapping().reserve(info.getModel().getNumberOfStates()); + for(uint_fast64_t state = 0; state < info.getModel().getNumberOfStates(); ++state){ + info.getNewToOldStateMapping().push_back(state); + } + + //Gather information regarding the individual objectives + if(!gatherObjectiveInformation(originalFormula, info)){ + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not gather information for objectives " << originalFormula << "."); + } + + // Find out whether negative rewards should be considered. + if(!setWhetherNegativeRewardsAreConsidered(info)){ + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not find out whether to consider negative rewards " << originalFormula << "."); + } + + //Invoke preprocessing on objectives + bool success = false; + for (auto& obj : info.getObjectives()){ + STORM_LOG_DEBUG("Preprocessing objective " << *obj.originalFormula << "."); + if(obj.originalFormula->isProbabilityOperatorFormula()){ + success = preprocess(obj.originalFormula->asProbabilityOperatorFormula(), info, obj); + } else if(obj.originalFormula->isRewardOperatorFormula()){ + success = preprocess(obj.originalFormula->asRewardOperatorFormula(), info, obj); + } + } + STORM_LOG_THROW(success, storm::exceptions::InvalidPropertyException, "Could not preprocess for the formula " << originalFormula << "."); + return info; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::gatherObjectiveInformation(storm::logic::MultiObjectiveFormula const& formula, Information& info) { + for(auto const& subF : formula.getSubFormulas()){ + if(!subF->isOperatorFormula()){ + STORM_LOG_ERROR("Expected an OperatorFormula as subformula of " << formula << " but got " << *subF); + return false; + } + storm::logic::OperatorFormula const& f = subF->asOperatorFormula(); + typename Information::ObjectiveInformation objective; + + objective.originalFormula = subF; + + if(f.hasBound()){ + objective.threshold = f.getBound().threshold; + // Note that we minimize if the comparison type is an upper bound since we are interested in the EXISTENCE of a scheduler... + objective.originalFormulaMinimizes = !storm::logic::isLowerBound(f.getBound().comparisonType); + } else if (f.hasOptimalityType()){ + objective.originalFormulaMinimizes = storm::solver::minimize(f.getOptimalityType()); + } else { + STORM_LOG_ERROR("Current objective" << f << "does not specify whether to minimize or maximize"); + } + + objective.rewardModelName = "objective" + std::to_string(info.getObjectives().size()); + // Make sure the new reward model gets a unique name + while(info.getModel().hasRewardModel(objective.rewardModelName)){ + objective.rewardModelName = "_" + objective.rewardModelName; + } + + if(!setStepBoundOfObjective(objective)) { + return false; + } + + info.getObjectives().push_back(std::move(objective)); + } + return true; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::setStepBoundOfObjective(typename Information::ObjectiveInformation& objective){ + if(objective.originalFormula->isProbabilityOperatorFormula()){ + storm::logic::Formula const& f = objective.originalFormula->asProbabilityOperatorFormula().getSubformula(); + if(f.isBoundedUntilFormula()){ + if(f.asBoundedUntilFormula().hasDiscreteTimeBound()){ + objective.stepBound = f.asBoundedUntilFormula().getDiscreteTimeBound(); + } else { + STORM_LOG_ERROR("Expected a discrete time bound at boundedUntilFormula but got" << f << "."); + return false; + } + } + } else if(objective.originalFormula->isRewardOperatorFormula()){ + storm::logic::Formula const& f = objective.originalFormula->asRewardOperatorFormula(); + if(f.isCumulativeRewardFormula()){ + if(f.asCumulativeRewardFormula().hasDiscreteTimeBound()){ + objective.stepBound = f.asCumulativeRewardFormula().getDiscreteTimeBound(); + } else { + STORM_LOG_ERROR("Expected a discrete time bound at cumulativeRewardFormula but got" << f << "."); + return false; + } + } + } else { + STORM_LOG_ERROR("Expected a Probability or Reward OperatorFormula but got " << *objective.originalFormula << "."); + return false; + } + return true; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::setWhetherNegativeRewardsAreConsidered(Information& info) { + // Negative Rewards are considered whenever there is an unbounded reward objective that requires to minimize. + // If there is no unbounded reward objective, we make a majority vote. + uint_fast64_t numOfMinimizingObjectives = 0; + for(auto const& obj : info.getObjectives()){ + if(obj.originalFormula->isRewardOperatorFormula() && !obj.stepBound){ + info.setNegativeRewardsConsidered(obj.originalFormulaMinimizes); + return true; + } + numOfMinimizingObjectives += obj.originalFormulaMinimizes ? 1 : 0; + } + // Reaching this point means that we make a majority vote + info.setNegativeRewardsConsidered(numOfMinimizingObjectives*2 > info.getObjectives().size()); + return true; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::ProbabilityOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + // Check if we need to complement the property, e.g., P<0.3 [ F "a" ] ---> P >=0.7 [ G !"a" ] + // This is the case if the formula requires to minimize and positive rewards are considered or vice versa + if(info.areNegativeRewardsConsidered() != currentObjective.originalFormulaMinimizes){ + STORM_LOG_ERROR("Inverting of properties not yet supported"); + //TODO + return false; + } + + bool success = false; + // Invoke preprocessing for subformula + if(formula.getSubformula().isUntilFormula()){ + success = preprocess(formula.getSubformula().asUntilFormula(), info, currentObjective); + } else if(formula.getSubformula().isBoundedUntilFormula()){ + success = preprocess(formula.getSubformula().asBoundedUntilFormula(), info, currentObjective); + } else if(formula.getSubformula().isGloballyFormula()){ + success = preprocess(formula.getSubformula().asGloballyFormula(), info, currentObjective); + } else if(formula.getSubformula().isEventuallyFormula()){ + success = preprocess(formula.getSubformula().asEventuallyFormula(), info, currentObjective); + } + STORM_LOG_ERROR_COND(success, "No implementation for the subformula of " << formula << "."); + + return success; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::RewardOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + // Make sure that our decision for negative rewards is consistent with the formula + if(info.areNegativeRewardsConsidered() != currentObjective.originalFormulaMinimizes){ + STORM_LOG_ERROR("Decided to consider " << (info.areNegativeRewardsConsidered() ? "negative" : "non-negative") << "rewards, but the formula " << formula << (currentObjective.originalFormulaMinimizes ? " minimizes" : "maximizes") << ". Reward objectives should either all minimize or all maximize."); + return false; + } + + // Check if the reward model is uniquely specified + if((formula.hasRewardModelName() && info.getModel().hasRewardModel(formula.getRewardModelName())) + || info.getModel().hasUniqueRewardModel()){ + STORM_LOG_ERROR("The reward model is not unique and the formula " << formula << " does not specify a reward model."); + return false; + } + + bool success = false; + // Invoke preprocessing for subformula + if(formula.getSubformula().isEventuallyFormula()){ + success = preprocess(formula.getSubformula().asEventuallyFormula(), info, currentObjective, formula.getOptionalRewardModelName()); + } else if(formula.getSubformula().isCumulativeRewardFormula()) { + success = preprocess(formula.getSubformula().asCumulativeRewardFormula(), info, currentObjective, formula.getOptionalRewardModelName()); + } + STORM_LOG_ERROR_COND(success, "No implementation for the subformula of " << formula << "."); + + return success; + + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::UntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + bool success = false; + CheckTask phiTask(formula.getLeftSubformula()); + CheckTask psiTask(formula.getRightSubformula()); + storm::modelchecker::SparsePropositionalModelChecker mc(info.getModel()); + success = mc.canHandle(phiTask) && mc.canHandle(psiTask); + STORM_LOG_ERROR_COND(success, "The subformulas of " << formula << " should be propositional."); + storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + // modelUnfolder(info.model, (~phiStates) | psiStates) + // info.model = modelUnfolder.info() + // build info.stateMapping from modelUnfolder.stateMapping + // build stateaction reward vector + // insert it in the model information + + // TODO + + return success; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::BoundedUntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + return preprocess(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), info, currentObjective); + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::GloballyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + //TODO + STORM_LOG_ERROR("Globally not yet implemented"); + return false; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::EventuallyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { + if(formula.isReachabilityProbabilityFormula()){ + return preprocess(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), info, currentObjective); + } + if (!formula.isReachabilityRewardFormula()){ + STORM_LOG_ERROR("The formula " << formula << " neither considers reachability Probabilities nor reachability rewards"); + return false; + } + //TODO + STORM_LOG_ERROR("Rewards not yet implemented"); + return false; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::CumulativeRewardFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { + //TODO + STORM_LOG_ERROR("Rewards not yet implemented"); + return false; + } + + + template class SparseMdpMultiObjectivePreprocessingHelper>; + + + } + } +} diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h new file mode 100644 index 000000000..a09939ee6 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h @@ -0,0 +1,62 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ + +#include "src/logic/Formulas.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" +#include "src/storage/BitVector.h" + +namespace storm { + namespace modelchecker { + + + namespace helper { + + /* + * Helper Class to invoke the necessary preprocessing for multi objective model checking + */ + template + class SparseMdpMultiObjectivePreprocessingHelper { + public: + typedef typename SparseMdpModelType::ValueType ValueType; + typedef typename SparseMdpModelType::RewardModelType RewardModelType; + typedef SparseMultiObjectiveModelCheckerInformation Information; + + /*! + * Preprocesses the given model w.r.t. the given formulas. + * @param originalModel The considered model + * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. + */ + static Information preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseMdpModelType originalModel); + + private: + + static bool gatherObjectiveInformation(storm::logic::MultiObjectiveFormula const& formula, Information& info); + static bool setStepBoundOfObjective(typename Information::ObjectiveInformation& currentObjective); + static bool setWhetherNegativeRewardsAreConsidered(Information& info); + + /*! + * Apply the neccessary preprocessing for the given formula. + * @param formula the current (sub)formula + * @param info the current state of the preprocessing. + * @return true iff there was no error + */ + // State formulas (will transform the formula and the reward model) + static bool preprocess(storm::logic::ProbabilityOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::RewardOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + + // Path formulas (will transform the model) + static bool preprocess(storm::logic::UntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::BoundedUntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::GloballyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::EventuallyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + static bool preprocess(storm::logic::CumulativeRewardFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + + static storm::storage::BitVector checkPropositionalFormula(storm::logic::Formula propFormula, SparseMdpModelType const& model); + + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h new file mode 100644 index 000000000..41e1840c4 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h @@ -0,0 +1,83 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ + +#include +#include + +#include "src/logic/Formulas.h" + +namespace storm { + namespace modelchecker { + + + namespace helper { + + template + class SparseMultiObjectiveModelCheckerInformation { + public : + + typedef typename SparseModelType::ValueType ValueType; + typedef typename SparseModelType::RewardModelType RewardModelType; + + struct ObjectiveInformation { + std::shared_ptr originalFormula; + bool originalFormulaMinimizes; + boost::optional threshold; + std::string rewardModelName; + boost::optional stepBound; + }; + + + SparseMultiObjectiveModelCheckerInformation(SparseModelType const& model) : model(model) { + //Intentionally left empty + } + + SparseMultiObjectiveModelCheckerInformation(SparseModelType && model) : model(model) { + //Intentionally left empty + } + + SparseModelType& getModel(){ + return model; + } + SparseModelType const& getModel() const { + return model; + } + + std::vector& getNewToOldStateMapping(){ + return newToOldStateMapping; + } + std::vectorconst& getNewToOldStateMapping() const{ + return newToOldStateMapping; + } + + bool areNegativeRewardsConsidered() { + return negativeRewardsConsidered; + } + + void setNegativeRewardsConsidered(bool value){ + negativeRewardsConsidered = value; + } + + std::vector& getObjectives() { + return objectives; + } + std::vectorconst& getObjectives() const { + return objectives; + } + + + private: + SparseModelType model; + std::vector newToOldStateMapping; + bool negativeRewardsConsidered; + + std::vector objectives; + + + + }; + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ */ diff --git a/src/utility/storm.h b/src/utility/storm.h index ce213cf08..a11fe2191 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -66,6 +66,7 @@ #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -301,13 +302,19 @@ namespace storm { if (storm::settings::getModule().isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(task); - } else { - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + } else { +#endif + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + if(modelchecker.canHandle(task)){ result = modelchecker.check(task); + } else { + storm::modelchecker::SparseMdpMultiObjectiveModelChecker> modelchecker2(*mdp); + if(modelchecker2.canHandle(task)){ + result = modelchecker2.check(task); + } } -#else - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(task); +#ifdef STORM_HAVE_CUDA + } #endif } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr> ctmc = model->template as>(); diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp index 0280844d3..246db82c9 100644 --- a/test/functional/logic/FragmentCheckerTest.cpp +++ b/test/functional/logic/FragmentCheckerTest.cpp @@ -130,3 +130,43 @@ TEST(FragmentCheckerTest, Csrl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); } + +TEST(FragmentCheckerTest, MultiObjective) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective().setNestedOperatorsInsideMultiObjectiveFormulasAllowed(true); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, 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]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,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(P=? [F P<0.5 [F \"label\"]], \"label\" )")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], multi(\"label\", \"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\" )")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + +} From 768cdfb77b5ce139344602af15f09cedde35553a Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 27 May 2016 23:19:15 +0200 Subject: [PATCH 004/109] state duplicator Former-commit-id: 6763b637baa3b8c05439e37f798fc8a694c0da40 --- src/CMakeLists.txt | 2 + src/modeltransformers/StateDuplicator.h | 204 ++++++++++++++++++++++++ 2 files changed, 206 insertions(+) create mode 100644 src/modeltransformers/StateDuplicator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 35d2e1d92..5fcf85253 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -32,6 +32,7 @@ file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/perm file(GLOB STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB_RECURSE STORM_MODELS_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/models/sparse/*.h ${PROJECT_SOURCE_DIR}/src/models/sparse/*.cpp) file(GLOB_RECURSE STORM_MODELS_SYMBOLIC_FILES ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.h ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.cpp) +file(GLOB_RECURSE STORM_MODELTRANSFORMER_FILES ${PROJECT_SOURCE_DIR}/src/modeltransformer/*.h ${PROJECT_SOURCE_DIR}/src/modeltransformer/*.cpp) file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) @@ -88,6 +89,7 @@ source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(models\\sparse FILES ${STORM_MODELS_SPARSE_FILES}) source_group(models\\symbolic FILES ${STORM_MODELS_SYMBOLIC_FILES}) +source_group(modeltransformer FILES ${STORM_MODELTRANSFORMER_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) diff --git a/src/modeltransformers/StateDuplicator.h b/src/modeltransformers/StateDuplicator.h new file mode 100644 index 000000000..f96e0f9c6 --- /dev/null +++ b/src/modeltransformers/StateDuplicator.h @@ -0,0 +1,204 @@ +#ifndef STORM_MDPTRIVIALSTATEELIMINATOR_H +#define STORM_MDPTRIVIALSTATEELIMINATOR_H + +#include "../utility/macros.h" + +#include +#include +#include + +#include "src/adapters/CarlAdapter.h" +#include "src/logic/Formulas.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/region/RegionCheckResult.h" +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/RegionSettings.h" +#include "src/solver/OptimizationDirection.h" +#include "src/storage/sparse/StateType.h" +#include "src/storage/FlexibleSparseMatrix.h" +#include "src/utility/constants.h" +#include "src/utility/graph.h" +#include "src/utility/macros.h" +#include "src/utility/vector.h" + +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/InvalidSettingsException.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/NotSupportedException.h" +#include "src/logic/FragmentSpecification.h" + +namespace storm { + namespace transformer { + + /* + * Duplicates the state space of the given model and redirects the incoming transitions of gateStates of the first copy to the gateStates of the second copy. + * Only states reachable from the initial states are kept. + */ +