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

removed some test cases 

for now we do not support bounded globally formulas explicitely, as well
    as `multi()`-formulae for SMGs
main
Stefan Pranger 4 years ago
parent
776dd502ac
commit
564cb6b9b1
3 changed files with 13 additions and 66 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. 6
      src/test/storm/logic/FragmentCheckerTest.cpp
  2. 42
      src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp
  3. 31
      src/test/storm/parser/GameFormulaParserTest.cpp

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

@ -88,7 +88,7 @@ TEST(FragmentCheckerTest, Prctl) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PostSafety, gamma=0.678> Pmax=? [\"label1\" U [5,7] \"label2\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.9> Pmax=? [G <=10 \"label\"]"));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.9> Pmax=? [G \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> Pmin=? [F <5 \"label\"]"));
@ -205,10 +205,10 @@ TEST(FragmentCheckerTest, Rpatl) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PostSafety, gamma=0.749> <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.749> <<a,b,c>> Pmax=? [G <=5 \"label\"]"));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.749> <<a,b,c>> Pmax=? [G \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> <<p1,p2>> Pmin=? [G [0,1] \"label\"]"));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> <<p1,p2>> Pmin=? [G \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
}

42
src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp
View File

@ -232,16 +232,8 @@ namespace {
TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) {
// This test is for borders of bounded U with conversations from G and F
// bounded G
// G
std::string formulasString = "<<bob, alice>> Pmax=? [ G !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=1 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=2 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=10 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=17 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=32 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=47 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=61 !\"hacked\" ]";
formulasString += "; <<bob, alice>> Pmax=? [ G <=62 !\"hacked\" ]";
// bounded F
formulasString += "; <<bob, alice>> Pmin=? [ F \"hacked\" ]";
@ -260,38 +252,22 @@ namespace {
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// bounded G results
// G results
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1.99379598e-05"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("0.9025"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("0.857375"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[7]);
EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[8]);
EXPECT_NEAR(this->parseNumber("0.7737809375"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// bounded F results
result = checker->check(this->env(), tasks[9]);
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("0.999980062"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[10]);
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[11]);
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[12]);
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[13]);
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[14]);
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
@ -323,6 +299,7 @@ namespace {
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
/*
TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) {
// This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound)
std::string formulasString = " <<friendlyRobot>> Pmax=? [ G<1 !\"crash\" ]";
@ -368,6 +345,7 @@ namespace {
result = checker->check(this->env(), tasks[8]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
*/
// TODO: create more test cases (files)
}

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

@ -202,34 +202,3 @@ TEST(GameFormulaParserTest, WrongFormatTest) {
input = "<< 1,2,3 >> P>0.5 [F y!=0)]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
}
TEST(GameFormulaParserTest, MultiObjectiveFormulaTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "multi(<<p1>> P<0.9 [ F \"a\" ], <<p2>> R<42 [ F \"b\" ], <<p1,p2>> Pmin=? [ F\"c\" ])";
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
ASSERT_TRUE(formula->isMultiObjectiveFormula());
storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula();
EXPECT_FALSE(formula->isInFragment(storm::logic::rpatl()));
ASSERT_EQ(3ull, mof.getNumberOfSubformulas());
ASSERT_TRUE(mof.getSubformula(0).isGameFormula());
ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().isProbabilityOperatorFormula());
ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasBound());
ASSERT_TRUE(mof.getSubformula(1).isGameFormula());
ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().isRewardOperatorFormula());
ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isEventuallyFormula());
ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().hasBound());
ASSERT_TRUE(mof.getSubformula(2).isGameFormula());
ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().isProbabilityOperatorFormula());
ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasOptimalityType());
ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getOptimalityType()));
}
Write Preview
Loading…
Cancel
Save