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

added tests for fragment checker 

Former-commit-id: 2de76ee5a5
tempestpy_adaptions
dehnert 9 years ago
parent
7b643fe166
commit
e40cc65117
2 changed files with 124 additions and 7 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/parser/FormulaParser.cpp
  2. 128
      test/functional/logic/FragmentCheckerTest.cpp

1
src/parser/FormulaParser.cpp
View File

@ -351,7 +351,6 @@ namespace storm {
debug(labelFormula); debug(labelFormula);
debug(expressionFormula); debug(expressionFormula);
debug(rewardPathFormula); debug(rewardPathFormula);
debug(reachabilityRewardFormula);
debug(cumulativeRewardFormula); debug(cumulativeRewardFormula);
debug(instantaneousRewardFormula); debug(instantaneousRewardFormula);
*/ */

128
test/functional/logic/FragmentCheckerTest.cpp
View File

@ -1,14 +1,132 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "src/parser/FormulaParser.h" #include "src/parser/FormulaParser.h"
#include "src/logic/FragmentSpecification.h"
#include "src/logic/FragmentChecker.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
TEST(FragmentCheckerTest, PctlTest) {
TEST(FragmentCheckerTest, Propositional) {
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification prop = storm::logic::propositional();
storm::parser::FormulaParser formulaParser;
std::shared_ptr<const storm::logic::Formula> 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));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F true]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("false | P>0.5 [G \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
}
TEST(FragmentCheckerTest, Pctl) {
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification pctl = storm::logic::pctl();
storm::parser::FormulaParser formulaParser;
std::shared_ptr<const storm::logic::Formula> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl));
}
TEST(FragmentCheckerTest, Prctl) {
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification prctl = storm::logic::prctl();
storm::parser::FormulaParser formulaParser;
std::shared_ptr<const storm::logic::Formula> 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));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, prctl));
}
TEST(FragmentCheckerTest, Csl) {
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification csl = storm::logic::csl();
storm::parser::FormulaParser formulaParser;
std::shared_ptr<const storm::logic::Formula> 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));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
}
TEST(FragmentCheckerTest, Csrl) {
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification csrl = storm::logic::csrl();
storm::parser::FormulaParser formulaParser; storm::parser::FormulaParser formulaParser;
std::shared_ptr<const storm::logic::Formula> 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));
std::string input = "\"label\"";
std::shared_ptr<const storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
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));
} }
Write Preview
Loading…
Cancel
Save