|
@ -3,72 +3,6 @@ |
|
|
#include "storm/logic/FragmentSpecification.h"
|
|
|
#include "storm/logic/FragmentSpecification.h"
|
|
|
#include "storm/storage/expressions/ExpressionManager.h"
|
|
|
#include "storm/storage/expressions/ExpressionManager.h"
|
|
|
|
|
|
|
|
|
TEST(GameFormulaParserTest, LabelTest) { |
|
|
|
|
|
storm::parser::FormulaParser formulaParser; |
|
|
|
|
|
|
|
|
|
|
|
std::string input = "<<p1>> Pmax=? [F \"label\"]"; |
|
|
|
|
|
|
|
|
|
|
|
std::shared_ptr<storm::logic::Formula const> gameFormula(nullptr); |
|
|
|
|
|
ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); |
|
|
|
|
|
|
|
|
|
|
|
EXPECT_TRUE(gameFormula->isStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isUnaryStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isGameFormula()); |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
TEST(GameFormulaParserTest, ComplexLabelTest) { |
|
|
|
|
|
storm::parser::FormulaParser formulaParser; |
|
|
|
|
|
|
|
|
|
|
|
std::string input = "<<p1,p2>> Pmin=? [X !(\"a\" & \"b\") | \"a\" & !\"c\"]"; |
|
|
|
|
|
|
|
|
|
|
|
std::shared_ptr<storm::logic::Formula const> gameFormula(nullptr); |
|
|
|
|
|
ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); |
|
|
|
|
|
|
|
|
|
|
|
EXPECT_TRUE(gameFormula->isStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isUnaryStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isGameFormula()); |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
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 = "<<p1, p2, p3>> Pmin=? [G !(x | y > 3)]"; |
|
|
|
|
|
|
|
|
|
|
|
std::shared_ptr<storm::logic::Formula const> gameFormula(nullptr); |
|
|
|
|
|
ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); |
|
|
|
|
|
|
|
|
|
|
|
EXPECT_TRUE(gameFormula->isStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isUnaryStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isGameFormula()); |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
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 = "<<p1, p2, p3>> Pmax=? [\"b\" U !\"a\" | x | y > 3]"; |
|
|
|
|
|
std::shared_ptr<storm::logic::Formula const> gameFormula(nullptr); |
|
|
|
|
|
ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); |
|
|
|
|
|
|
|
|
|
|
|
EXPECT_TRUE(gameFormula->isStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isUnaryStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isGameFormula()); |
|
|
|
|
|
|
|
|
|
|
|
input = "<<p1, p2, p3>> Pmax=? [x | y > 3 | !\"a\" U \"b\"]"; |
|
|
|
|
|
ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); |
|
|
|
|
|
|
|
|
|
|
|
EXPECT_TRUE(gameFormula->isStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isUnaryStateFormula()); |
|
|
|
|
|
EXPECT_TRUE(gameFormula->isGameFormula()); |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
TEST(GameFormulaParserTest, OnePlayerCoalitionTest) { |
|
|
TEST(GameFormulaParserTest, OnePlayerCoalitionTest) { |
|
|
storm::parser::FormulaParser formulaParser; |
|
|
storm::parser::FormulaParser formulaParser; |
|
|
|
|
|
|
|
|