From 2687809591bcab658079cb83ece72f69e87718ab Mon Sep 17 00:00:00 2001 From: masawei Date: Tue, 12 Aug 2014 02:07:03 +0200 Subject: [PATCH] Finished testing of Csl. Former-commit-id: 91172a1b89e1f172cb39201cb7f2e2774c00fba4 --- src/formula/AbstractFilter.h | 2 +- src/formula/csl/CslFilter.h | 51 +++-- src/formula/csl/Next.h | 4 +- src/formula/csl/ProbabilisticBoundOperator.h | 30 +-- src/modelchecker/csl/AbstractModelChecker.h | 2 +- .../SparseMarkovAutomatonCslModelChecker.h | 2 +- src/parser/CslParser.cpp | 34 +-- src/parser/PrctlParser.cpp | 4 +- test/functional/modelchecker/FilterTest.cpp | 210 +++++++++++++++++- test/functional/parser/CslParserTest.cpp | 75 ++++++- 10 files changed, 350 insertions(+), 64 deletions(-) diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h index 59bc935fa..f1e7017f7 100644 --- a/src/formula/AbstractFilter.h +++ b/src/formula/AbstractFilter.h @@ -49,7 +49,7 @@ public: if(emptyCount > 0) { // There is at least one nullptr action. // Allocate space for the non null actions. - this->actions = std::vector>>(actions.size() - emptyCount); + this->actions.reserve(actions.size() - emptyCount); // Fill the vector. Note: For most implementations of the standard there will be no reallocation in the vector while doing this. for(auto action : actions){ diff --git a/src/formula/csl/CslFilter.h b/src/formula/csl/CslFilter.h index fffd78663..d09902760 100644 --- a/src/formula/csl/CslFilter.h +++ b/src/formula/csl/CslFilter.h @@ -55,13 +55,18 @@ public: this->actions.clear(); } - void check(storm::modelchecker::prctl::AbstractModelChecker const & modelchecker) const { + void check(storm::modelchecker::csl::AbstractModelChecker const & modelchecker) const { // Write out the formula to be checked. std::cout << std::endl; LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString()); std::cout << "Model checking formula:\t" << this->toString() << std::endl; + writeOut(evaluate(modelchecker), modelchecker); + + } + + Result evaluate(storm::modelchecker::csl::AbstractModelChecker const & modelchecker) const { Result result; try { @@ -73,13 +78,9 @@ public: } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); - std::cout << std::endl << "-------------------------------------------" << std::endl; - - return; } - writeOut(result, modelchecker); - + return result; } virtual std::string toString() const override { @@ -121,10 +122,10 @@ public: for(auto action : this->actions) { desc += action->toString(); - desc += ", "; + desc += "; "; } - // Remove the last ", ". + // Remove the last "; ". desc.pop_back(); desc.pop_back(); @@ -151,10 +152,10 @@ public: for(auto action : this->actions) { desc += action->toString(); - desc += ", "; + desc += "; "; } - // Remove the last ", ". + // Remove the last "; ". desc.pop_back(); desc.pop_back(); @@ -189,15 +190,15 @@ public: private: - storm::storage::BitVector evaluate(storm::modelchecker::csl::AbstractModelChecker const & modelchecker, std::shared_ptr> const & formula) const { + Result evaluate(storm::modelchecker::csl::AbstractModelChecker const & modelchecker, std::shared_ptr> const & formula) const { // First, get the model checking result. - storm::storage::BitVector result = modelchecker.checkMinMaxOperator(*formula); + Result result; if(this->opt != UNDEFINED) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(formula, this->opt == MINIMIZE ? true : false); + result.stateResult = modelchecker.checkMinMaxOperator(*formula, this->opt == MINIMIZE ? true : false); } else { - result = formula->check(modelchecker); + result.stateResult = formula->check(modelchecker); } @@ -205,15 +206,15 @@ private: return evaluateActions(result, modelchecker); } - std::vector evaluate(storm::modelchecker::csl::AbstractModelChecker const & modelchecker, std::shared_ptr> const & formula) const { + Result evaluate(storm::modelchecker::csl::AbstractModelChecker const & modelchecker, std::shared_ptr> const & formula) const { // First, get the model checking result. - std::vector result; + Result result; if(this->opt != UNDEFINED) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(*formula, this->opt == MINIMIZE ? true : false); + result.pathResult = modelchecker.checkMinMaxOperator(*formula, this->opt == MINIMIZE ? true : false); } else { - result = formula->check(modelchecker, false); + result.pathResult = formula->check(modelchecker, false); } // Now apply all filter actions and return the result. @@ -223,8 +224,9 @@ private: Result evaluateActions(Result result, storm::modelchecker::csl::AbstractModelChecker const & modelchecker) const { // Init the state selection and state map vectors. - result.selection = storm::storage::BitVector(result.stateResult.size(), true); - result.stateMap = std::vector(result.selection.size()); + uint_fast64_t size = result.stateResult.size() == 0 ? result.pathResult.size() : result.stateResult.size(); + result.selection = storm::storage::BitVector(size, true); + result.stateMap = std::vector(size); for(uint_fast64_t i = 0; i < result.selection.size(); i++) { result.stateMap[i] = i; } @@ -236,7 +238,14 @@ private: return result; } - void writeOut(Result const & result, storm::modelchecker::prctl::AbstractModelChecker const & modelchecker) const { + void writeOut(Result const & result, storm::modelchecker::csl::AbstractModelChecker const & modelchecker) const { + + // Test if there is anything to write out. + // The selection size should only be 0 if an error occurred during the evaluation (since a model with 0 states is invalid). + if(result.selection.size() == 0) { + std::cout << std::endl << "-------------------------------------------" << std::endl; + return; + } // Test for the kind of result. Values or states. if(!result.pathResult.empty()) { diff --git a/src/formula/csl/Next.h b/src/formula/csl/Next.h index f8a8ae0f4..3148377a6 100644 --- a/src/formula/csl/Next.h +++ b/src/formula/csl/Next.h @@ -114,10 +114,8 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const override { - std::string result = "("; - result += " X "; + std::string result = "X "; result += child->toString(); - result += ")"; return result; } diff --git a/src/formula/csl/ProbabilisticBoundOperator.h b/src/formula/csl/ProbabilisticBoundOperator.h index 02986e3f8..6d0e0d6a3 100644 --- a/src/formula/csl/ProbabilisticBoundOperator.h +++ b/src/formula/csl/ProbabilisticBoundOperator.h @@ -60,7 +60,7 @@ public: /*! * Empty constructor */ - ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr) { + ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr) { // Intentionally left empty. } @@ -69,10 +69,10 @@ public: * * @param comparisonOperator The relation for the bound. * @param bound The bound for the probability - * @param pathFormula The child node + * @param child The child node */ - ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & pathFormula) - : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { + ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr> const & child) + : comparisonOperator(comparisonOperator), bound(bound), child(child) { // Intentionally left empty. } @@ -97,7 +97,7 @@ public: std::shared_ptr> result(new ProbabilisticBoundOperator()); result->setComparisonOperator(comparisonOperator); result->setBound(bound); - result->setPathFormula(pathFormula->clone()); + result->setChild(child->clone()); return result; } @@ -121,7 +121,7 @@ public: * @return true iff the subtree conforms to some logic. */ virtual bool validate(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->pathFormula); + return checker.validate(this->child); } /*! @@ -138,7 +138,7 @@ public: result += " "; result += std::to_string(bound); result += " ("; - result += pathFormula->toString(); + result += child->toString(); result += ")"; return result; } @@ -146,25 +146,25 @@ public: /*! * @returns the child node (representation of a formula) */ - std::shared_ptr> const & getPathFormula () const { - return pathFormula; + std::shared_ptr> const & getChild () const { + return child; } /*! * Sets the child node * - * @param pathFormula the path formula that becomes the new child node + * @param child the path formula that becomes the new child node */ - void setPathFormula(std::shared_ptr> const & pathFormula) { - this->pathFormula = pathFormula; + void setChild(std::shared_ptr> const & child) { + this->child = child; } /*! * * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise */ - bool pathFormulaIsSet() const { - return pathFormula.get() != nullptr; + bool childIsSet() const { + return child.get() != nullptr; } /*! @@ -207,7 +207,7 @@ public: private: storm::property::ComparisonType comparisonOperator; T bound; - std::shared_ptr> pathFormula; + std::shared_ptr> child; }; } //namespace csl diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index af7d28f86..3a9ff9285 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -174,7 +174,7 @@ public: */ virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator const& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. - std::vector quantitativeResult = formula.getPathFormula()->check(*this, false); + std::vector quantitativeResult = formula.getChild()->check(*this, false); // Create resulting bit vector that will hold the yes/no-answer for every state. storm::storage::BitVector result(quantitativeResult.size()); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 0b4c6bd43..71213f1b8 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -65,7 +65,7 @@ public: } // First, we need to compute the probability for satisfying the path formula for each state. - std::vector quantitativeResult = formula.getPathFormula()->check(*this, false); + std::vector quantitativeResult = formula.getChild()->check(*this, false); //Remove the minimizing operator entry from the stack. this->minimumOperatorStack.pop(); diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index f0a51afa6..1f2f66361 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -78,27 +78,27 @@ struct CslParser::CslGrammar : qi::grammar> stateFormula >> qi::lit(")"); + atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | (qi::lit("(") >> stateFormula >> qi::lit(")")) | (qi::lit("[") >> stateFormula >> qi::lit("]")); atomicStateFormula.name("atomic state formula"); atomicProposition = (freeIdentifierName)[qi::_val = MAKE(csl::Ap, qi::_1)]; atomicProposition.name("atomic proposition"); probabilisticBoundOperator = ( - (qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + (qi::lit("P") >> comparisonType > qi::double_ > pathFormula )[qi::_val = MAKE(csl::ProbabilisticBoundOperator , qi::_1, qi::_2, qi::_3)] ); probabilisticBoundOperator.name("probabilistic bound operator"); steadyStateBoundOperator = ( - (qi::lit("S") >> comparisonType > qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - MAKE(csl::SteadyStateBoundOperator , qi::_1, qi::_2, qi::_3)] + (qi::lit("S") >> comparisonType > qi::double_ > stateFormula )[qi::_val = + MAKE(csl::SteadyStateBoundOperator , qi::_1, qi::_2, qi::_3)] ); steadyStateBoundOperator.name("steady state bound operator"); //This block defines rules for parsing probabilistic path formulas - pathFormula = (timeBoundedEventually | eventually | globally | next | timeBoundedUntil | until); + pathFormula = (timeBoundedEventually | eventually | globally | next | timeBoundedUntil | until | (qi::lit("(") >> pathFormula >> qi::lit(")")) | (qi::lit("[") >> pathFormula >> qi::lit("]"))); pathFormula.name("path formula"); timeBoundedEventually = ( - (qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val = + (qi::lit("F") >> qi::lit("[") >> qi::double_ >> qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val = MAKE(csl::TimeBoundedEventually, qi::_1, qi::_2, qi::_3)] | (qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val = MAKE(csl::TimeBoundedEventually, 0, qi::_1, qi::_2)] | @@ -116,11 +116,11 @@ struct CslParser::CslGrammar : qi::grammar , qi::_1)]; globally.name("globally"); timeBoundedUntil = ( - (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula) + (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("[") >> qi::double_ >> qi::lit(",") >> qi::double_ >> qi::lit("]") >> stateFormula) [qi::_val = MAKE(csl::TimeBoundedUntil, qi::_2, qi::_3, qi::_a, qi::_4)] | - (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula) + (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula) [qi::_val = MAKE(csl::TimeBoundedUntil, 0, qi::_2, qi::_a, qi::_3)] | - (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula) + (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula) [qi::_val = MAKE(csl::TimeBoundedUntil, qi::_2, std::numeric_limits::infinity(), qi::_a, qi::_3)] ); timeBoundedUntil.name("time bounded until"); @@ -135,14 +135,14 @@ struct CslParser::CslGrammar : qi::grammar> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit("min") >> qi::lit("=") > qi::lit("?") >> pathFormula)[qi::_val = MAKE(csl::CslFilter, qi::_1, storm::property::MINIMIZE)] | - (qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> pathFormula)[qi::_val = MAKE(csl::CslFilter, qi::_1, storm::property::MAXIMIZE)] | - (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + (qi::lit("P") >> qi::lit("=") > qi::lit("?") >> pathFormula)[qi::_val = MAKE(csl::CslFilter, qi::_1)]; probabilisticNoBoundOperator.name("probabilistic no bound operator"); - steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> stateFormula >> qi::lit("]"))[qi::_val = + steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") > qi::lit("?") >> stateFormula )[qi::_val = MAKE(csl::CslFilter, qi::_1, storm::property::UNDEFINED, true)]; steadyStateNoBoundOperator.name("steady state no bound operator"); @@ -176,11 +176,15 @@ struct CslParser::CslGrammar : qi::grammar> (qi::lit(";") | qi::eps); + abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps); abstractAction.name("filter action"); filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = MAKE(csl::CslFilter, qi::_2, qi::_1)] | + (qi::lit("filter") >> qi::lit("[") >> qi::lit("max") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = + MAKE(csl::CslFilter, qi::_2, qi::_1, storm::property::MAXIMIZE)] | + (qi::lit("filter") >> qi::lit("[") >> qi::lit("min") > +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = + MAKE(csl::CslFilter, qi::_2, qi::_1, storm::property::MINIMIZE)] | (noBoundOperator)[qi::_val = qi::_1] | (formula)[qi::_val = @@ -188,7 +192,7 @@ struct CslParser::CslGrammar : qi::grammar (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = nullptr] ) > qi::eoi; + start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(csl::CslFilter, nullptr)] ) > qi::eoi; start.name("CSL formula filter start"); } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index b31b621bb..bd9590980 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -146,7 +146,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar, qi::_1, storm::property::MINIMIZE)] | (qi::lit("R") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val = MAKE(prctl::PrctlFilter, qi::_1, storm::property::MAXIMIZE)] | - (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> rewardPathFormula )[qi::_val = + (qi::lit("R") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val = MAKE(prctl::PrctlFilter, qi::_1)] ); @@ -183,7 +183,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar> (qi::lit(";") | qi::eps); + abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps); abstractAction.name("filter action"); filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp index 65fa50e7a..a9f3cfbe8 100644 --- a/test/functional/modelchecker/FilterTest.cpp +++ b/test/functional/modelchecker/FilterTest.cpp @@ -10,11 +10,16 @@ #include "src/models/Dtmc.h" #include "src/parser/DeterministicModelParser.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/formula/prctl/PrctlFilter.h" #include "src/formula/csl/CslFilter.h" #include "src/formula/ltl/LtlFilter.h" #include "src/parser/PrctlParser.h" +#include "src/parser/CslParser.h" +#include "src/parser/MarkovAutomatonParser.h" +#include "src/formula/actions/InvertAction.h" #include @@ -42,12 +47,12 @@ TEST(PrctlFilterTest, generalFunctionality) { formula->check(mc); - std::string output = buffer.str(); - ASSERT_NE(std::string::npos, output.find("\t6: 1")); - // Reset cout to the original buffer. std::cout.rdbuf(sbuf); + std::string output = buffer.str(); + ASSERT_NE(std::string::npos, output.find("\t6: 1")); + // The remaining queries use evaluate directly as its easier to work with in a test environment. // Get the probability to reach a b state for all states but those that cannot reach a 'b' state or are 'b' states themselves. // Sorted by value; highest first. @@ -148,9 +153,206 @@ TEST(PrctlFilterTest, Safety) { // Make a stub formula as child. auto apFormula = std::make_shared>("a"); + // Test the filter for nullptr action handling. auto formula = std::make_shared>(apFormula, nullptr); - ASSERT_NO_THROW(formula->check(mc)); + ASSERT_EQ(0, formula->getActionCount()); + ASSERT_NO_THROW(formula->evaluate(mc)); + + // Repeat with vector containing only one action but three nullptr. + std::vector>> actions(4, nullptr); + actions[1] = std::make_shared>(); + + formula = std::make_shared>(apFormula, actions); + + ASSERT_EQ(1, formula->getActionCount()); + ASSERT_NO_THROW(formula->evaluate(mc)); + + // Test the filter for nullptr child formula handling. + // It sholud not write anything to the standard out and return an empty result. + formula = std::make_shared>(); + Result result; + + // To capture the output, redirect cout and test the written buffer content. + std::stringstream buffer; + std::streambuf *sbuf = std::cout.rdbuf(); + std::cout.rdbuf(buffer.rdbuf()); + + ASSERT_NO_THROW(result = formula->evaluate(mc)); + + // Reset cout to the original buffer. + std::cout.rdbuf(sbuf); + + ASSERT_EQ(0, buffer.str().length()); + + ASSERT_EQ(0, result.pathResult.size()); + ASSERT_EQ(0, result.stateResult.size()); + ASSERT_EQ(0, result.selection.size()); + ASSERT_EQ(0, result.stateMap.size()); } +TEST(CslFilterTest, generalFunctionality) { + // Test filter queries of increasing complexity. + + // Setup model and modelchecker. + storm::models::MarkovAutomaton model = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_cslFilterTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_cslFilterTest.lab"); + storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(model, std::make_shared>()); + + // Find the best valued state to finally reach a 'r1' state. + std::string input = "filter[max; sort(value, descending); range(0,0)](F r1)"; + std::shared_ptr> formula(nullptr); + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + // Here we test if the check method gives the correct result. + // To capture the output, redirect cout and test the written buffer content. + std::stringstream buffer; + std::streambuf *sbuf = std::cout.rdbuf(); + std::cout.rdbuf(buffer.rdbuf()); + + formula->check(mc); + + // Reset cout to the original buffer. + std::cout.rdbuf(sbuf); + + std::string output = buffer.str(); + ASSERT_NE(std::string::npos, output.find("\t6: 1")); + + // The remaining queries use evaluate directly as its easier to work with in a test environment. + // Get the maximum probability to reach an 'r1' state for all states but those that cannot reach an 'r1' state or are 'r1' states themselves. + // Sorted by value; highest first. + input = "filter[max; formula(P<=0(F r1) | r1); invert; sort(value, desc)](F r1)"; + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + Result result = formula->evaluate(mc); + + // Test the selection. + ASSERT_EQ(6, result.selection.getNumberOfSetBits()); + ASSERT_TRUE(result.selection[0]); + ASSERT_TRUE(result.selection[1]); + ASSERT_TRUE(result.selection[2]); + ASSERT_TRUE(result.selection[3]); + ASSERT_TRUE(result.selection[4]); + ASSERT_TRUE(result.selection[5]); + ASSERT_FALSE(result.selection[6]); + ASSERT_FALSE(result.selection[7]); + + // Test the sorting. + ASSERT_EQ(6, result.stateMap[0]); + ASSERT_EQ(5, result.stateMap[1]); + ASSERT_EQ(2, result.stateMap[2]); + ASSERT_EQ(3, result.stateMap[3]); + ASSERT_EQ(0, result.stateMap[4]); + ASSERT_EQ(4, result.stateMap[5]); + ASSERT_EQ(1, result.stateMap[6]); + ASSERT_EQ(7, result.stateMap[7]); + + // Get the minimum probability for reaching an 'err' state only for those states that have a probability to do so of at most 0.2. + // Sorted by value; lowest first. + input = "filter[min; bound(<, 0.2); sort(value, ascending)](F err)"; + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + result = formula->evaluate(mc); + + // Test the selection. + ASSERT_EQ(5, result.selection.getNumberOfSetBits()); + ASSERT_FALSE(result.selection[0]); + ASSERT_TRUE(result.selection[1]); + ASSERT_FALSE(result.selection[2]); + ASSERT_FALSE(result.selection[3]); + ASSERT_TRUE(result.selection[4]); + ASSERT_TRUE(result.selection[5]); + ASSERT_TRUE(result.selection[6]); + ASSERT_TRUE(result.selection[7]); + + // Test the sorting. + ASSERT_EQ(6, result.stateMap[0]); + ASSERT_EQ(7, result.stateMap[1]); + ASSERT_EQ(5, result.stateMap[2]); + ASSERT_EQ(4, result.stateMap[3]); + ASSERT_EQ(1, result.stateMap[4]); + ASSERT_EQ(0, result.stateMap[5]); + ASSERT_EQ(2, result.stateMap[6]); + ASSERT_EQ(3, result.stateMap[7]); + + // Get the three highest indexed states reaching an 'r2' state with probability at most 0.3. + input = "filter[sort(value); range(5,7); sort(index, descending)](P<=0.3(F r2))"; + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + result = formula->evaluate(mc); + + // Test the selection. + ASSERT_EQ(3, result.selection.getNumberOfSetBits()); + ASSERT_FALSE(result.selection[0]); + ASSERT_FALSE(result.selection[1]); + ASSERT_FALSE(result.selection[2]); + ASSERT_TRUE(result.selection[3]); + ASSERT_FALSE(result.selection[4]); + ASSERT_TRUE(result.selection[5]); + ASSERT_TRUE(result.selection[6]); + ASSERT_FALSE(result.selection[7]); + + // Test the sorting. + ASSERT_EQ(7, result.stateMap[0]); + ASSERT_EQ(6, result.stateMap[1]); + ASSERT_EQ(5, result.stateMap[2]); + ASSERT_EQ(4, result.stateMap[3]); + ASSERT_EQ(3, result.stateMap[4]); + ASSERT_EQ(2, result.stateMap[5]); + ASSERT_EQ(1, result.stateMap[6]); + ASSERT_EQ(0, result.stateMap[7]); +} + +TEST(CslFilterTest, Safety) { + // Setup model and modelchecker. + storm::models::MarkovAutomaton model = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_cslFilterTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_cslFilterTest.lab"); + storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(model, std::make_shared>()); + + // Make a stub formula as child. + auto apFormula = std::make_shared>("r1"); + + // Test the filter for nullptr action handling. + auto formula = std::make_shared>(apFormula, nullptr, storm::property::MAXIMIZE); + + ASSERT_NO_THROW(formula->evaluate(mc)); + ASSERT_EQ(0, formula->getActionCount()); + + // Repeat with vector containing only one action but three nullptr. + std::vector>> actions(4, nullptr); + actions[1] = std::make_shared>(); + + formula = std::make_shared>(apFormula, actions, storm::property::MAXIMIZE); + + ASSERT_EQ(1, formula->getActionCount()); + ASSERT_NO_THROW(formula->evaluate(mc)); + + // Test the filter for nullptr child formula handling. + // It sholud not write anything to the standard out and return an empty result. + formula = std::make_shared>(); + Result result; + + // To capture the output, redirect cout and test the written buffer content. + std::stringstream buffer; + std::streambuf *sbuf = std::cout.rdbuf(); + std::cout.rdbuf(buffer.rdbuf()); + + ASSERT_NO_THROW(result = formula->evaluate(mc)); + + // Reset cout to the original buffer. + std::cout.rdbuf(sbuf); + + ASSERT_EQ(0, buffer.str().length()); + + ASSERT_EQ(0, result.pathResult.size()); + ASSERT_EQ(0, result.stateResult.size()); + ASSERT_EQ(0, result.selection.size()); + ASSERT_EQ(0, result.stateMap.size()); +} diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index ff0a4f4d1..4d13479e1 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -9,6 +9,11 @@ #include "storm-config.h" #include "src/parser/CslParser.h" #include "src/exceptions/WrongFormatException.h" +#include "src/formula/actions/FormulaAction.h" +#include "src/formula/actions/InvertAction.h" +#include "src/formula/actions/SortAction.h" +#include "src/formula/actions/RangeAction.h" +#include "src/formula/actions/BoundAction.h" namespace csl = storm::property::csl; @@ -40,6 +45,35 @@ TEST(CslParserTest, parsePropositionalFormulaTest) { ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); } +TEST(CslParserTest, parsePathFormulaTest) { + std::string input = "X( P<0.9 (a U b))"; + std::shared_ptr> formula(nullptr); + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + + // The input was parsed correctly. + ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); + auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); + ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); + auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); + ASSERT_NE(std::dynamic_pointer_cast>(probBoundFormula->getChild()).get(), nullptr); + auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); + ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); + ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); + ASSERT_EQ("b", std::dynamic_pointer_cast>(untilFormula->getRight())->getAp()); + ASSERT_EQ(0.9, probBoundFormula->getBound()); + ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); + + + // The string representation is also correct. + ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString()); +} + TEST(CslParserTest, parseProbabilisticFormulaTest) { std::string input = "P > 0.5 [ F a ]"; std::shared_ptr> formula(nullptr); @@ -118,7 +152,46 @@ TEST(CslParserTest, parseComplexFormulaTest) { ASSERT_NE(formula.get(), nullptr); // The input was parsed correctly. - ASSERT_EQ("(S <= 0.500000 (P <= 0.500000 (a U c)) & (P > 0.500000 (G b) | !P < 0.400000 (G P > 0.900000 (F>=7.000000 (a & b)))))", formula->toString()); + ASSERT_EQ("S <= 0.500000 ((P <= 0.500000 (a U c) & (P > 0.500000 (G b) | !P < 0.400000 (G P > 0.900000 (F>=7.000000 (a & b))))))", formula->toString()); +} + +TEST(CslParserTest, parseCslFilterTest) { + std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; + std::shared_ptr> formula(nullptr); + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + + ASSERT_EQ(5, formula->getActionCount()); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); + + // The input was parsed correctly. + ASSERT_EQ("filter[formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); +} + +TEST(CslParserTest, commentTest) { + std::string input = "// This is a comment. And this is a commented out formula: P = ? [ F a ]"; + std::shared_ptr> formula(nullptr); + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + + // The parser recognized the input as a comment. + ASSERT_NE(nullptr, formula.get()); + + // Test if the parser recognizes the comment at the end of a line. + input = "P = ? [ F a ] // This is a comment."; + ASSERT_NO_THROW( + formula = storm::parser::CslParser::parseCslFormula(input) + ); + ASSERT_EQ("P = ? (F a)", formula->toString()); } TEST(CslParserTest, wrongProbabilisticFormulaTest) {