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

Adapted ModelChecker test-cases and FormulaParser test-cases

tempestpy_adaptions
hannah 4 years ago
committed by Stefan Pranger
parent
1c16c17a57
commit
d5edde05a7
2 changed files with 57 additions and 49 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. 20
      src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp
  2. 82
      src/test/storm/parser/FormulaParserTest.cpp

20
src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp
View File

@ -30,7 +30,6 @@
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
#include <cstdlib> //todo
namespace {
@ -726,7 +725,7 @@ namespace {
formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]";
formulasString += "; P=? [ F (s=3 U (\"three\"))]";
formulasString += "; P=? [ F s=3 U (\"three\")]";
formulasString += "; P=? [ F (s=6) & (X \"done\")]"; // TODO without ()
formulasString += "; P=? [ F (s=6) & X \"done\"]";
formulasString += "; P=? [ (F s=6) & (X \"done\")]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
@ -758,7 +757,7 @@ namespace {
result = checker->check(tasks[5]);
EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(tasks[4]);
result = checker->check(tasks[6]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
} else {
EXPECT_FALSE(checker->canHandle(tasks[0]));
@ -769,9 +768,10 @@ namespace {
setenv("LTL2DA", "ltl2da-ltl2tgba", true);
std::string formulasString = "P=? [X (u1=true U \"elected\")]";
formulasString += "; P=? [X v1=2 & (X v1=1)]"; // (X v1=2 & (XX v1=1))
formulasString += "; P=? [X !(u1=true U \"elected\")]";
formulasString += "; P=? [X v1=2 & X v1=1]";
formulasString += "; P=? [(X v1=2) & (X v1=1)]";
// TODO (X v1=2 & XX v1=1)
formulasString += "; P=? [(!X v1=2) & (X v1=1)]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
auto model = std::move(modelFormulas.first);
@ -788,14 +788,16 @@ namespace {
EXPECT_NEAR(this->parseNumber("16/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(tasks[1]);
EXPECT_NEAR(this->parseNumber("1/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
EXPECT_NEAR(this->parseNumber("9/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(tasks[2]);
EXPECT_NEAR(this->parseNumber("1/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(tasks[3]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// TODO
// result = checker->check(tasks[3]);
// EXPECT_NEAR(this->parseNumber("1/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(tasks[4]);
EXPECT_NEAR(this->parseNumber("1/5"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
} else {
EXPECT_FALSE(checker->canHandle(tasks[0]));

82
src/test/storm/parser/FormulaParserTest.cpp
View File

@ -176,6 +176,16 @@ TEST(FormulaParserTest, WrongFormatTest) {
input = "P>0.5 [F y!=0)]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [G F]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [\"a\" U \"b\" U \"c\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [X \"a\" U G \"b\" U X \"c\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
}
TEST(FormulaParserTest, MultiObjectiveFormulaTest) {
@ -248,14 +258,22 @@ TEST(FormulaParserTest, LogicalPrecedenceTest) {
ASSERT_TRUE(nested4Subformula.getLeftSubformula().isAtomicLabelFormula());
ASSERT_TRUE(nested4Subformula.getRightSubformula().isBinaryBooleanStateFormula());
input = "P<0.9 [X \"a\" | (X \"b\")]"; // X(a|Xb) todo why is this allowed, but not [X \"a\" | X \"b\"]
input = "P<0.9 [X \"a\" | F \"b\"]"; // X (a | F b)
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
auto const &nested5 = formula->asProbabilityOperatorFormula().getSubformula();
EXPECT_TRUE(nested5.isNextFormula());
EXPECT_TRUE(nested5.asNextFormula().getSubformula().isBinaryBooleanPathFormula());
auto const &nested5Subformula = nested5.asNextFormula().getSubformula().asBinaryPathFormula();
EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isNextFormula());
EXPECT_TRUE(nested5.asNextFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isEventuallyFormula());
input = "P<0.9 [F \"a\" | G \"b\" | X \"c\" ]"; // F (a | G (b | X c))
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
auto const &nested6 = formula->asProbabilityOperatorFormula().getSubformula();
EXPECT_TRUE(nested6.isEventuallyFormula());
EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().isBinaryBooleanPathFormula());
EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getLeftSubformula().isAtomicLabelFormula());
EXPECT_TRUE(nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().isGloballyFormula());
auto const &nested6Subformula = nested6.asEventuallyFormula().getSubformula().asBinaryPathFormula().getRightSubformula().asGloballyFormula();
}
TEST(FormulaParserTest, TemporalPrecedenceTest) {
@ -278,34 +296,42 @@ TEST(FormulaParserTest, TemporalPrecedenceTest) {
EXPECT_TRUE(nested2.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isUntilFormula());
EXPECT_TRUE(nested2.asUntilFormula().getRightSubformula().isGloballyFormula());
input = "P=? [ X F \"a\" U G \"b\" U G \"c\"]"; // (X F a) U (G b) U (G c)
input = "P=? [ X F \"a\" U (G \"b\" U G \"c\")]"; // (XF a) U ((G b) U (G c))
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
EXPECT_TRUE(nested3.isUntilFormula());
EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().isUntilFormula());
EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().asUntilFormula().getLeftSubformula().isNextFormula());
EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().isGloballyFormula());
EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().isNextFormula());
EXPECT_TRUE(nested3.asUntilFormula().getLeftSubformula().asNextFormula().getSubformula().isEventuallyFormula());
EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().isUntilFormula());
EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getLeftSubformula().isGloballyFormula());
EXPECT_TRUE(nested3.asUntilFormula().getRightSubformula().asUntilFormula().getRightSubformula().isGloballyFormula());
}
TEST(FormulaParserTest, NestedUntilTest) {
TEST(FormulaParserTest, TemporalNegationTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "P<0.9 [\"a\" U (\"b\" U \"c\")]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::string input = "P<0.9 [ ! X \"a\" | \"b\"]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
auto const &nested1 = formula->asProbabilityOperatorFormula().getSubformula();
EXPECT_TRUE(nested1.isUntilFormula());
EXPECT_FALSE(nested1.isBoundedUntilFormula());
ASSERT_TRUE( nested1.asUntilFormula().getLeftSubformula().isAtomicLabelFormula());
ASSERT_TRUE(nested1.asUntilFormula().getRightSubformula().isUntilFormula());
EXPECT_TRUE(nested1.isUnaryBooleanPathFormula());
EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().isNextFormula());
EXPECT_TRUE(nested1.asUnaryPathFormula().getSubformula().asNextFormula().getSubformula().isBinaryBooleanStateFormula());
input = "P<0.9 [\"a\" U \"b\" U \"c\"]"; // Nested Until without parentheses: (a U b) U c
input ="P<0.9 [! F ! G \"b\"]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
auto const &nested2 = formula->asProbabilityOperatorFormula().getSubformula();
EXPECT_TRUE(nested2.isUntilFormula());
EXPECT_FALSE(nested2.isBoundedUntilFormula());
ASSERT_TRUE(nested2.asUntilFormula().getLeftSubformula().isUntilFormula());
ASSERT_TRUE(nested2.asUntilFormula().getRightSubformula().isAtomicLabelFormula());
EXPECT_TRUE(nested2.isUnaryBooleanPathFormula());
EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().isEventuallyFormula());
EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().isUnaryBooleanPathFormula());
EXPECT_TRUE(nested2.asUnaryPathFormula().getSubformula().asEventuallyFormula().getSubformula().asUnaryPathFormula().getSubformula().isGloballyFormula());
input ="P<0.9 [! (\"a\" U \"b\")]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
auto const &nested3 = formula->asProbabilityOperatorFormula().getSubformula();
EXPECT_TRUE(nested3.isUnaryBooleanPathFormula());
EXPECT_TRUE(nested3.asUnaryPathFormula().getSubformula().isUntilFormula());
}
TEST(FormulaParserTest, ComplexPathFormulaTest) {
@ -327,23 +353,3 @@ TEST(FormulaParserTest, ComplexPathFormulaTest) {
ASSERT_TRUE(nested2.asBinaryPathFormula().getLeftSubformula().isBinaryPathFormula());
ASSERT_TRUE(nested2.asBinaryPathFormula().getRightSubformula().isUntilFormula());
}
TEST(FormulaParserTest, LtlWrongFormatTest) {
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::string input = "P<0.9 [F \"a\" & X \"b\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [X \"a\" & G \"b\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [G \"a\" & G \"b\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [(G \"a\") & G \"b\"]"; //todo why?
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P<0.9 [! X \"b\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
}
Write Preview
Loading…
Cancel
Save