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

added first rpatl fragment checker tests 

Conflicts:
	src/test/storm/logic/FragmentCheckerTest.cpp
tempestpy_adaptions
Stefan Pranger 3 years ago
parent
fc18ea12d3
commit
9a0be7e9ca
1 changed files with 57 additions and 32 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. 89
      src/test/storm/logic/FragmentCheckerTest.cpp

89
src/test/storm/logic/FragmentCheckerTest.cpp
View File

@ -12,16 +12,16 @@ TEST(FragmentCheckerTest, Propositional) {
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
@ -42,10 +42,10 @@ TEST(FragmentCheckerTest, Pctl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification pctl = storm::logic::pctl();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
@ -63,19 +63,19 @@ TEST(FragmentCheckerTest, Prctl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification prctl = storm::logic::prctl();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
@ -90,19 +90,19 @@ TEST(FragmentCheckerTest, Csl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification csl = storm::logic::csl();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, csl));
@ -114,25 +114,25 @@ TEST(FragmentCheckerTest, Csrl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification csrl = storm::logic::csrl();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
}
@ -140,32 +140,57 @@ TEST(FragmentCheckerTest, Csrl) {
TEST(FragmentCheckerTest, MultiObjective) {
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective();
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"label\" & R<=4[F \"label\"]])]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
}
TEST(FragmentCheckerTest, Rpatl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification rpatl = storm::logic::rpatl();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_ANY_THROW(formula = formulaParser.parseSingleFormulaFromString("<<player1>> \"label\""));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1>> P=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2>> Pmin=? [ \"label1\" U \"label2\" ]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<p1, p2>> Rmax=? [ LRA ]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<player1>> R=? [C<=3]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
}
Write Preview
Loading…
Cancel
Save