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

Changed PrctlParser to directly parse the input string as formula, and 

added PrctlFileParser to parse formulae from a file
tempestpy_adaptions
Lanchid 12 years ago
parent
f35fff7061
commit
ab4174183b
5 changed files with 112 additions and 53 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. 32
      src/parser/PrctlFileParser.cpp
  2. 24
      src/parser/PrctlFileParser.h
  3. 20
      src/parser/PrctlParser.cpp
  4. 10
      src/parser/PrctlParser.h
  5. 79
      test/parser/PrctlParserTest.cpp

32
src/parser/PrctlFileParser.cpp
View File

@ -0,0 +1,32 @@
/*
* PrctlFileParser.cpp
*
* Created on: 06.02.2013
* Author: Thomas Heinemann
*/
#include "PrctlFileParser.h"
namespace storm {
namespace parser {
PrctlFileParser::PrctlFileParser(std::string filename) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
// Prepare iterators to input.
// TODO: Right now, this parses the whole contents of the file into a string first.
// While this is usually not necessary, because there exist adapters that make an input stream
// iterable in both directions without storing it into a string, using the corresponding
// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
parse(fileContent);
}
PrctlFileParser::~PrctlFileParser() {
//intentionally left empty
//formulas are not deleted with the parser!
}
} /* namespace parser */
} /* namespace storm */

24
src/parser/PrctlFileParser.h
View File

@ -0,0 +1,24 @@
/*
* PrctlFileParser.h
*
* Created on: 06.02.2013
* Author: Thomas Heinemann
*/
#ifndef STORM_PARSER_PRCTLFILEPARSER_H_
#define STORM_PARSER_PRCTLFILEPARSER_H_
#include "PrctlParser.h"
namespace storm {
namespace parser {
class PrctlFileParser: public storm::parser::PrctlParser {
public:
PrctlFileParser(std::string filename);
virtual ~PrctlFileParser();
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_PRCTLFILEPARSER_H_ */

20
src/parser/PrctlParser.cpp
View File

@ -124,19 +124,10 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
} //namespace storm
} //namespace parser
storm::parser::PrctlParser::PrctlParser(std::string filename) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
// Prepare iterators to input.
// TODO: Right now, this parses the whole contents of the file into a string first.
// While this is usually not necessary, because there exist adapters that make an input stream
// iterable in both directions without storing it into a string, using the corresponding
// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
BaseIteratorType stringIteratorBegin = fileContent.begin();
BaseIteratorType stringIteratorEnd = fileContent.end();
PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename);
void storm::parser::PrctlParser::parse(std::string formulaString) {
BaseIteratorType stringIteratorBegin = formulaString.begin();
BaseIteratorType stringIteratorEnd = formulaString.end();
PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString);
PositionIteratorType positionIteratorEnd;
@ -148,5 +139,8 @@ storm::parser::PrctlParser::PrctlParser(std::string filename) {
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer);
formula = result_pointer;
}
storm::parser::PrctlParser::PrctlParser(std::string formula) {
parse(formula);
}

10
src/parser/PrctlParser.h
View File

@ -15,7 +15,8 @@ namespace parser {
class PrctlParser : Parser
{
public:
PrctlParser(std::string filename);
PrctlParser() { }
PrctlParser(std::string formulaString);
/*!
* @brief return formula object parsed from file.
@ -25,6 +26,13 @@ class PrctlParser : Parser
return this->formula;
}
protected:
/*!
* Parses a formula and stores the result in the field "formula"
* @param formula The string representation of the formula to parse
*/
void parse(std::string formula);
private:
storm::formula::AbstractFormula<double>* formula;

79
test/parser/PrctlParserTest.cpp
View File

@ -9,11 +9,12 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/PrctlParser.h"
#include "src/parser/PrctlFileParser.h"
TEST(PrctlParserTest, parseApOnlyTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/apOnly.prctl")
prctlParser = new storm::parser::PrctlParser("P");
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
@ -27,103 +28,103 @@ TEST(PrctlParserTest, parseApOnlyTest) {
}
TEST(PrctlParserTest, parsePropositionalFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::parser::PrctlFileParser* prctlFileParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl")
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "(!(a && b) || (a && !c))");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a && b) || (a && !c))");
delete prctlParser->getFormula();
delete prctlParser;
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::parser::PrctlFileParser* prctlFileParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl")
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(prctlParser->getFormula());
storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(prctlFileParser->getFormula());
ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER, op->getComparisonOperator());
ASSERT_EQ(0.5, op->getBound());
ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P > 0.500000 [F a]");
delete prctlParser->getFormula();
delete prctlParser;
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
TEST(PrctlParserTest, parseRewardFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::parser::PrctlFileParser* prctlFileParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl")
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlParser->getFormula());
storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlFileParser->getFormula());
ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
ASSERT_EQ(15.0, op->getBound());
ASSERT_EQ(prctlParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]");
delete prctlParser->getFormula();
delete prctlParser;
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::parser::PrctlFileParser* prctlFileParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl")
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]");
delete prctlParser->getFormula();
delete prctlParser;
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::parser::PrctlFileParser* prctlFileParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl")
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [F<=42 !a]");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P = ? [F<=42 !a]");
delete prctlParser->getFormula();
delete prctlParser;
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
TEST(PrctlParserTest, parseComplexFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::parser::PrctlFileParser* prctlFileParser = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl")
prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl")
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G P > 0.900000 [F<=7 (a && b)]] || !P < 0.400000 [G !b]))");
delete prctlParser->getFormula();
delete prctlParser;
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G P > 0.900000 [F<=7 (a && b)]] || !P < 0.400000 [G !b]))");
delete prctlFileParser->getFormula();
delete prctlFileParser;
}
Write Preview
Loading…
Cancel
Save