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

WIP added GameFormulaParserTest.cpp

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
04dd2b2e92
commit
1b81c009c1
1 changed files with 62 additions and 0 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. 62
      src/test/storm/parser/GameFormulaParserTest.cpp

62
src/test/storm/parser/GameFormulaParserTest.cpp
View File

@ -0,0 +1,62 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/storage/expressions/ExpressionManager.h"
// TODO: write this to <<player>> inputs (games)!
TEST(GameFormulaParserTest, LabelTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "<<player>> \"label\"";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isAtomicLabelFormula());
}
TEST(GameFormulaParserTest, ComplexLabelTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\"";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
EXPECT_TRUE(formula->isBinaryBooleanStateFormula());
}
TEST(GameFormulaParserTest, ExpressionTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser formulaParser(manager);
std::string input = "!(x | y > 3)";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
EXPECT_TRUE(formula->isUnaryBooleanStateFormula());
}
TEST(GameFormulaParserTest, LabelAndExpressionTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser formulaParser(manager);
std::string input = "!\"a\" | x | y > 3";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
input = "x | y > 3 | !\"a\"";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
}
Write Preview
Loading…
Cancel
Save