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

Ltl testng. 

Former-commit-id: 57f486db59
tempestpy_adaptions
masawei 10 years ago
parent
2687809591
commit
0a2a759932
6 changed files with 98 additions and 50 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/formula/csl/CslFilter.h
  2. 62
      src/formula/ltl/LtlFilter.h
  3. 10
      src/parser/LtlParser.cpp
  4. 6
      test/functional/parser/CslParserTest.cpp
  5. 60
      test/functional/parser/LtlParserTest.cpp
  6. 8
      test/functional/parser/PrctlParserTest.cpp

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

@ -52,7 +52,7 @@ public:
} }
virtual ~CslFilter() { virtual ~CslFilter() {
this->actions.clear();
// Intentionally left empty.
} }
void check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const { void check(storm::modelchecker::csl::AbstractModelChecker<T> const & modelchecker) const {

62
src/formula/ltl/LtlFilter.h
View File

@ -42,7 +42,7 @@ public:
} }
LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) { LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::shared_ptr<action::AbstractAction<T>> const & action, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(action, opt), child(child) {
this->actions.push_back(action);
// Intentionally left empty.
} }
LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) { LtlFilter(std::shared_ptr<AbstractLtlFormula<T>> const & child, std::vector<std::shared_ptr<action::AbstractAction<T>>> const & actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter<T>(actions, opt), child(child) {
@ -50,7 +50,7 @@ public:
} }
virtual ~LtlFilter() { virtual ~LtlFilter() {
this->actions.clear();
// Intentionally left empty.
} }
@ -83,6 +83,35 @@ public:
} }
Result evaluate(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
// First, get the model checking result.
Result result;
if(this->opt != UNDEFINED) {
// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
LOG4CPLUS_ERROR(logger, "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.");
throw storm::exceptions::NotImplementedException() << "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.";
} else {
result.pathResult = child->check(modelchecker);
}
// Now apply all filter actions and return the result.
// 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());
for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
result.stateMap[i] = i;
}
// Now apply all filter actions and return the result.
for(auto action : this->actions) {
result = action->evaluate(result, modelchecker);
}
return result;
}
std::string toString() const override { std::string toString() const override {
std::string desc = ""; std::string desc = "";
@ -142,35 +171,6 @@ public:
private: private:
Result evaluate(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
// First, get the model checking result.
Result result;
if(this->opt != UNDEFINED) {
// If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker.
LOG4CPLUS_ERROR(logger, "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.");
throw storm::exceptions::NotImplementedException() << "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented.";
} else {
result.stateResult = child->check(modelchecker);
}
// Now apply all filter actions and return the result.
// 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());
for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
result.stateMap[i] = i;
}
// Now apply all filter actions and return the result.
for(auto action : this->actions) {
result = action->evaluate(result, modelchecker);
}
return result;
}
void writeOut(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const { void writeOut(Result const & result, storm::modelchecker::ltl::AbstractModelChecker<T> const & modelchecker) const {
// Test for the kind of result. Values or states. // Test for the kind of result. Values or states.

10
src/parser/LtlParser.cpp
View File

@ -62,13 +62,13 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::prop
(qi::lit("index"))[qi::_val = storm::property::action::SortAction<double>::INDEX] | (qi::lit("index"))[qi::_val = storm::property::action::SortAction<double>::INDEX] |
(qi::lit("value"))[qi::_val = storm::property::action::SortAction<double>::VALUE] (qi::lit("value"))[qi::_val = storm::property::action::SortAction<double>::VALUE]
); );
//Comment: Empty line or line starting with "//"
// Comment: Empty line or line starting with "//"
comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr];
freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
//This block defines rules for parsing state formulas
formula %= orFormula;
// This block defines rules for parsing state formulas
formula %= orFormula | qi::lit("(") >> formula >> qi::lit(")")| qi::lit("[") >> formula >> qi::lit("]");
formula.name("LTL formula"); formula.name("LTL formula");
orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val =
MAKE(ltl::Or<double>, qi::_val, qi::_1)]; MAKE(ltl::Or<double>, qi::_val, qi::_1)];
@ -85,7 +85,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::prop
//This block defines rules for "atomic" state formulas //This block defines rules for "atomic" state formulas
//(Propositions, probabilistic/reward formulas, and state formulas in brackets) //(Propositions, probabilistic/reward formulas, and state formulas in brackets)
atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> formula >> qi::lit(")");
atomicLtlFormula %= pathFormula | atomicProposition;
atomicLtlFormula.name("LTL formula"); atomicLtlFormula.name("LTL formula");
atomicProposition = (freeIdentifierName)[qi::_val = atomicProposition = (freeIdentifierName)[qi::_val =
MAKE(ltl::Ap<double>, qi::_1)]; MAKE(ltl::Ap<double>, qi::_1)];
@ -133,7 +133,7 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::prop
); );
sortAction.name("sort action"); sortAction.name("sort action");
abstractAction = (boundAction | invertAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps);
abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps);
abstractAction.name("filter action"); abstractAction.name("filter action");
filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =

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

@ -156,7 +156,7 @@ TEST(CslParserTest, parseComplexFormulaTest) {
} }
TEST(CslParserTest, parseCslFilterTest) { TEST(CslParserTest, parseCslFilterTest) {
std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
std::shared_ptr<csl::CslFilter<double>> formula(nullptr); std::shared_ptr<csl::CslFilter<double>> formula(nullptr);
ASSERT_NO_THROW( ASSERT_NO_THROW(
formula = storm::parser::CslParser::parseCslFormula(input) formula = storm::parser::CslParser::parseCslFormula(input)
@ -165,6 +165,8 @@ TEST(CslParserTest, parseCslFilterTest) {
// The parser did not falsely recognize the input as a comment. // The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr); ASSERT_NE(formula, nullptr);
ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator());
ASSERT_EQ(5, formula->getActionCount()); 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::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::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
@ -173,7 +175,7 @@ TEST(CslParserTest, parseCslFilterTest) {
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr);
// The input was parsed correctly. // The input was parsed correctly.
ASSERT_EQ("filter[formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
} }
TEST(CslParserTest, commentTest) { TEST(CslParserTest, commentTest) {

60
test/functional/parser/LtlParserTest.cpp
View File

@ -9,6 +9,10 @@
#include "storm-config.h" #include "storm-config.h"
#include "src/parser/LtlParser.h" #include "src/parser/LtlParser.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.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 ltl = storm::property::ltl; namespace ltl = storm::property::ltl;
@ -20,7 +24,7 @@ TEST(LtlParserTest, parseApOnlyTest) {
); );
ASSERT_NE(ltlFormula.get(), nullptr); ASSERT_NE(ltlFormula.get(), nullptr);
ASSERT_EQ(ltlFormula->toString(), formula);
ASSERT_EQ(formula, ltlFormula->toString());
} }
TEST(LtlParserTest, parsePropositionalFormulaTest) { TEST(LtlParserTest, parsePropositionalFormulaTest) {
@ -31,7 +35,7 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) {
); );
ASSERT_NE(ltlFormula.get(), nullptr); ASSERT_NE(ltlFormula.get(), nullptr);
ASSERT_EQ(ltlFormula->toString(), "(!(a & b) | (a & !c))");
ASSERT_EQ("(!(a & b) | (a & !c))", ltlFormula->toString());
} }
/*! /*!
@ -46,7 +50,7 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) {
); );
ASSERT_NE(ltlFormula.get(), nullptr); ASSERT_NE(ltlFormula.get(), nullptr);
ASSERT_EQ(ltlFormula->toString(), "(F & b)");
ASSERT_EQ("(F & b)", ltlFormula->toString());
} }
/*! /*!
@ -61,7 +65,7 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest2) {
); );
ASSERT_NE(ltlFormula.get(), nullptr); ASSERT_NE(ltlFormula.get(), nullptr);
ASSERT_EQ(ltlFormula->toString(), "F F");
ASSERT_EQ("F F", ltlFormula->toString());
} }
TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
@ -78,7 +82,7 @@ TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) {
ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound()); ASSERT_EQ(static_cast<uint_fast64_t>(5), op->getBound());
ASSERT_EQ(ltlFormula->toString(), "F<=5 a");
ASSERT_EQ("F<=5 a", ltlFormula->toString());
} }
TEST(LtlParserTest, parseBoundedUntilFormulaTest) { TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
@ -95,7 +99,47 @@ TEST(LtlParserTest, parseBoundedUntilFormulaTest) {
ASSERT_EQ(static_cast<uint_fast64_t>(3), op->getBound()); ASSERT_EQ(static_cast<uint_fast64_t>(3), op->getBound());
ASSERT_EQ(ltlFormula->toString(), "(a U<=3 b)");
ASSERT_EQ("(a U<=3 b)", ltlFormula->toString());
}
TEST(LtlParserTest, parseLtlFilterTest) {
std::string input = "filter[max; invert; bound(<, 0.5); sort(value); range(0,3)](X a)";
std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
ASSERT_NO_THROW(
formula = storm::parser::LtlParser::parseLtlFormula(input)
);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator());
ASSERT_EQ(4, formula->getActionCount());
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::InvertAction<double>>(formula->getAction(0)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::BoundAction<double>>(formula->getAction(1)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::SortAction<double>>(formula->getAction(2)).get(), nullptr);
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(3)).get(), nullptr);
// The input was parsed correctly.
ASSERT_EQ("filter[max; invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](X a)", formula->toString());
}
TEST(PrctlParserTest, commentTest) {
std::string input = "// This is a comment. And this is a commented out formula: F X a";
std::shared_ptr<ltl::LtlFilter<double>> formula(nullptr);
ASSERT_NO_THROW(
formula = storm::parser::LtlParser::parseLtlFormula(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 = "F X a // This is a comment.";
ASSERT_NO_THROW(
formula = storm::parser::LtlParser::parseLtlFormula(input)
);
ASSERT_EQ("F X a", formula->toString());
} }
TEST(LtlParserTest, parseComplexUntilTest) { TEST(LtlParserTest, parseComplexUntilTest) {
@ -106,7 +150,7 @@ TEST(LtlParserTest, parseComplexUntilTest) {
); );
ASSERT_NE(ltlFormula.get(), nullptr); ASSERT_NE(ltlFormula.get(), nullptr);
ASSERT_EQ(ltlFormula->toString(), "((a U b) U<=3 c)");
ASSERT_EQ("((a U b) U<=3 c)", ltlFormula->toString());
} }
TEST(LtlParserTest, parseComplexFormulaTest) { TEST(LtlParserTest, parseComplexFormulaTest) {
@ -117,7 +161,7 @@ TEST(LtlParserTest, parseComplexFormulaTest) {
); );
ASSERT_NE(ltlFormula.get(), nullptr); ASSERT_NE(ltlFormula.get(), nullptr);
ASSERT_EQ(ltlFormula->toString(), "(a U F (b | G (a & F<=3 (a U<=7 b))))");
ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlFormula->toString());
} }
TEST(LtlParserTest, wrongFormulaTest) { TEST(LtlParserTest, wrongFormulaTest) {

8
test/functional/parser/PrctlParserTest.cpp
View File

@ -159,7 +159,7 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
} }
TEST(PrctlParserTest, parsePrctlFilterTest) { TEST(PrctlParserTest, parsePrctlFilterTest) {
std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr); std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
ASSERT_NO_THROW( ASSERT_NO_THROW(
formula = storm::parser::PrctlParser::parsePrctlFormula(input) formula = storm::parser::PrctlParser::parsePrctlFormula(input)
@ -168,6 +168,8 @@ TEST(PrctlParserTest, parsePrctlFilterTest) {
// The parser did not falsely recognize the input as a comment. // The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr); ASSERT_NE(formula, nullptr);
ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator());
ASSERT_EQ(5, formula->getActionCount()); 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::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::InvertAction<double>>(formula->getAction(1)).get(), nullptr);
@ -176,10 +178,10 @@ TEST(PrctlParserTest, parsePrctlFilterTest) {
ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast<storm::property::action::RangeAction<double>>(formula->getAction(4)).get(), nullptr);
// The input was parsed correctly. // The input was parsed correctly.
ASSERT_EQ("filter[formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
} }
TEST(PrctlParserTest, commentTest) {
TEST(LtlParserTest, commentTest) {
std::string input = "// This is a comment. And this is a commented out formula: R = ? [ F a ]"; std::string input = "// This is a comment. And this is a commented out formula: R = ? [ F a ]";
std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr); std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
ASSERT_NO_THROW( ASSERT_NO_THROW(

Write Preview
Loading…
Cancel
Save