Browse Source

Changed the output function of the formulae to produce a string in the

same format as the input
tempestpy_adaptions
Lanchid 12 years ago
parent
commit
bb34e94eac
  1. 2
      src/formula/And.h
  2. 2
      src/formula/Or.h
  3. 11
      test/parser/PrctlParserTest.cpp
  4. 2
      test/parser/prctl_files/complexFormula.prctl

2
src/formula/And.h

@ -129,7 +129,7 @@ public:
virtual std::string toString() const { virtual std::string toString() const {
std::string result = "("; std::string result = "(";
result += left->toString(); result += left->toString();
result += " && ";
result += " & ";
result += right->toString(); result += right->toString();
result += ")"; result += ")";
return result; return result;

2
src/formula/Or.h

@ -127,7 +127,7 @@ public:
virtual std::string toString() const { virtual std::string toString() const {
std::string result = "("; std::string result = "(";
result += left->toString(); result += left->toString();
result += " || ";
result += " | ";
result += right->toString(); result += right->toString();
result += ")"; result += ")";
return result; return result;

11
test/parser/PrctlParserTest.cpp

@ -12,15 +12,16 @@
#include "src/parser/PrctlFileParser.h" #include "src/parser/PrctlFileParser.h"
TEST(PrctlParserTest, parseApOnlyTest) { TEST(PrctlParserTest, parseApOnlyTest) {
std::string ap = "P";
storm::parser::PrctlParser* prctlParser = nullptr; storm::parser::PrctlParser* prctlParser = nullptr;
ASSERT_NO_THROW( ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("P");
prctlParser = new storm::parser::PrctlParser(ap);
); );
ASSERT_NE(prctlParser->getFormula(), nullptr); ASSERT_NE(prctlParser->getFormula(), nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "P");
ASSERT_EQ(ap, prctlParser->getFormula()->toString());
delete prctlParser->getFormula(); delete prctlParser->getFormula();
delete prctlParser; delete prctlParser;
@ -36,7 +37,7 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) {
ASSERT_NE(prctlFileParser->getFormula(), nullptr); ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a && b) || (a && !c))");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
delete prctlFileParser->getFormula(); delete prctlFileParser->getFormula();
delete prctlFileParser; delete prctlFileParser;
@ -91,7 +92,7 @@ TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
ASSERT_NE(prctlFileParser->getFormula(), nullptr); ASSERT_NE(prctlFileParser->getFormula(), nullptr);
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]");
ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b & !c))]");
delete prctlFileParser->getFormula(); delete prctlFileParser->getFormula();
delete prctlFileParser; delete prctlFileParser;
@ -123,7 +124,7 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
ASSERT_NE(prctlFileParser->getFormula(), nullptr); ASSERT_NE(prctlFileParser->getFormula(), nullptr);
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]))");
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->getFormula();
delete prctlFileParser; delete prctlFileParser;

2
test/parser/prctl_files/complexFormula.prctl

@ -1 +1 @@
(P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ]))
P<=0.5 [ F a ] & (R > 15 [ G P>0.9 [F<=7 a & b] ] | !P < 0.4 [ G !b ])
Loading…
Cancel
Save