sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Finished testing of Csl. 

Former-commit-id: 91172a1b89
tempestpy_adaptions
masawei 11 years ago
parent
33386f4c5f
commit
2687809591
10 changed files with 350 additions and 64 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/formula/AbstractFilter.h
  2. 51
      src/formula/csl/CslFilter.h
  3. 4
      src/formula/csl/Next.h
  4. 30
      src/formula/csl/ProbabilisticBoundOperator.h
  5. 2
      src/modelchecker/csl/AbstractModelChecker.h
  6. 2
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  7. 34
      src/parser/CslParser.cpp
  8. 4
      src/parser/PrctlParser.cpp
  9. 210
      test/functional/modelchecker/FilterTest.cpp
  10. 75
      test/functional/parser/CslParserTest.cpp

2
src/formula/AbstractFilter.h
View File

@ -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<std::shared_ptr<action::AbstractAction<T>>>(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){

51
src/formula/csl/CslFilter.h
View File

@ -55,13 +55,18 @@ public:
this->actions.clear();
}
void check(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
void check(storm::modelchecker::csl::AbstractModelChecker<T> 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<T> 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<T> const & modelchecker, std::shared_ptr<AbstractStateFormula<T>> const & formula) const {
Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractStateFormula<T>> 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<T> evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractPathFormula<T>> const & formula) const {
Result evaluate(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker, std::shared_ptr<AbstractPathFormula<T>> const & formula) const {
// First, get the model checking result.
std::vector<T> 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<T> const & modelchecker) const {
// Init the state selection and state map vectors.
result.selection = storm::storage::BitVector(result.stateResult.size(), true);
result.stateMap = std::vector<uint_fast64_t>(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<uint_fast64_t>(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<T> const & modelchecker) const {
void writeOut(Result const & result, storm::modelchecker::csl::AbstractModelChecker<T> 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()) {

4
src/formula/csl/Next.h
View File

@ -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;
}

30
src/formula/csl/ProbabilisticBoundOperator.h
View File

@ -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<AbstractPathFormula<T>> const & pathFormula)
: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & child)
: comparisonOperator(comparisonOperator), bound(bound), child(child) {
// Intentionally left empty.
}
@ -97,7 +97,7 @@ public:
std::shared_ptr<ProbabilisticBoundOperator<T>> result(new ProbabilisticBoundOperator<T>());
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<T> 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<AbstractPathFormula<T>> const & getPathFormula () const {
return pathFormula;
std::shared_ptr<AbstractPathFormula<T>> 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<AbstractPathFormula<T>> const & pathFormula) {
this->pathFormula = pathFormula;
void setChild(std::shared_ptr<AbstractPathFormula<T>> 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<AbstractPathFormula<T>> pathFormula;
std::shared_ptr<AbstractPathFormula<T>> child;
};
} //namespace csl

2
src/modelchecker/csl/AbstractModelChecker.h
View File

@ -174,7 +174,7 @@ public:
*/
virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator<Type> const& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state.
std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
std::vector<Type> 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());

2
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -65,7 +65,7 @@ public:
}
// First, we need to compute the probability for satisfying the path formula for each state.
std::vector<ValueType> quantitativeResult = formula.getPathFormula()->check(*this, false);
std::vector<ValueType> quantitativeResult = formula.getChild()->check(*this, false);
//Remove the minimizing operator entry from the stack.
this->minimumOperatorStack.pop();

34
src/parser/CslParser.cpp
View File

@ -78,27 +78,27 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFil
//This block defines rules for "atomic" state formulas
//(Propositions, probabilistic/reward formulas, and state formulas in brackets)
atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | qi::lit("(") >> 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<double>, 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<double> , 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<double> , qi::_1, qi::_2, qi::_3)]
(qi::lit("S") >> comparisonType > qi::double_ > stateFormula )[qi::_val =
MAKE(csl::SteadyStateBoundOperator<double> , 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<double>, qi::_1, qi::_2, qi::_3)] |
(qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val =
MAKE(csl::TimeBoundedEventually<double>, 0, qi::_1, qi::_2)] |
@ -116,11 +116,11 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFil
MAKE(csl::Globally<double> , 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<double>, 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<double>, 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<double>, qi::_2, std::numeric_limits<double>::infinity(), qi::_a, qi::_3)]
);
timeBoundedUntil.name("time bounded until");
@ -135,14 +135,14 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFil
noBoundOperator = (probabilisticNoBoundOperator | steadyStateNoBoundOperator);
noBoundOperator.name("no bound operator");
probabilisticNoBoundOperator =
(qi::lit("P") >> 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<double>, 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<double>, 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<double>, 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<double>, qi::_1, storm::property::UNDEFINED, true)];
steadyStateNoBoundOperator.name("steady state no bound operator");
@ -176,11 +176,15 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFil
);
sortAction.name("sort action");
abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (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<double>, 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<double>, 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<double>, qi::_2, qi::_1, storm::property::MINIMIZE)] |
(noBoundOperator)[qi::_val =
qi::_1] |
(formula)[qi::_val =
@ -188,7 +192,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, std::shared_ptr<csl::CslFil
filter.name("CSL formula filter");
start = (((filter) > (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<double>, nullptr)] ) > qi::eoi;
start.name("CSL formula filter start");
}

4
src/parser/PrctlParser.cpp
View File

@ -146,7 +146,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
MAKE(prctl::PrctlFilter<double>, qi::_1, storm::property::MINIMIZE)] |
(qi::lit("R") >> qi::lit("max") >> qi::lit("=") > qi::lit("?") >> rewardPathFormula )[qi::_val =
MAKE(prctl::PrctlFilter<double>, 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<double>, qi::_1)]
);
@ -183,7 +183,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
);
sortAction.name("sort action");
abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (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 =

210
test/functional/modelchecker/FilterTest.cpp
View File

@ -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 <memory>
@ -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<storm::property::prctl::Ap<double>>("a");
// Test the filter for nullptr action handling.
auto formula = std::make_shared<storm::property::prctl::PrctlFilter<double>>(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<std::shared_ptr<storm::property::action::AbstractAction<double>>> actions(4, nullptr);
actions[1] = std::make_shared<storm::property::action::InvertAction<double>>();
formula = std::make_shared<storm::property::prctl::PrctlFilter<double>>(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<storm::property::prctl::PrctlFilter<double>>();
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<double> 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<double> mc(model, std::make_shared<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>());
// 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<storm::property::csl::CslFilter<double>> 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<double> 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<double> mc(model, std::make_shared<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>());
// Make a stub formula as child.
auto apFormula = std::make_shared<storm::property::csl::Ap<double>>("r1");
// Test the filter for nullptr action handling.
auto formula = std::make_shared<storm::property::csl::CslFilter<double>>(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<std::shared_ptr<storm::property::action::AbstractAction<double>>> actions(4, nullptr);
actions[1] = std::make_shared<storm::property::action::InvertAction<double>>();
formula = std::make_shared<storm::property::csl::CslFilter<double>>(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<storm::property::csl::CslFilter<double>>();
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());
}

75
test/functional/parser/CslParserTest.cpp
View File

@ -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<csl::CslFilter<double>> 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<csl::Next<double>>(formula->getChild()).get(), nullptr);
auto nextFormula = std::dynamic_pointer_cast<csl::Next<double>>(formula->getChild());
ASSERT_NE(std::dynamic_pointer_cast<csl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
auto probBoundFormula = std::dynamic_pointer_cast<csl::ProbabilisticBoundOperator<double>>(nextFormula->getChild());
ASSERT_NE(std::dynamic_pointer_cast<csl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
auto untilFormula = std::dynamic_pointer_cast<csl::Until<double>>(probBoundFormula->getChild());
ASSERT_NE(std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
ASSERT_EQ("a", std::dynamic_pointer_cast<csl::Ap<double>>(untilFormula->getLeft())->getAp());
ASSERT_EQ("b", std::dynamic_pointer_cast<csl::Ap<double>>(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<csl::CslFilter<double>> 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<csl::CslFilter<double>> 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<storm::property::action::FormulaAction<double>>(formula->getAction(0)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::BoundAction<double>>(formula->getAction(2)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::SortAction<double>>(formula->getAction(3)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(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<csl::CslFilter<double>> 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) {

Write Preview
Loading…
Cancel
Save