diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 24267e80d..67fd4336a 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -165,19 +165,26 @@ namespace { TYPED_TEST_SUITE(SmgRpatlModelCheckerTest, TestingTypes,); TYPED_TEST(SmgRpatlModelCheckerTest, Walker) { + // NEXT tests std::string formulasString = "<> Pmax=? [X \"s2\"]"; formulasString += "; <> Pmin=? [X \"s2\"]"; + formulasString += "; <> Pmax=? [X !\"s1\"]"; + formulasString += "; <> Pmin=? [X !\"s1\"]"; + // UNTIL tests + formulasString += "; <> Pmax=? [ a=0 U a=1 ]"; + formulasString += "; <> Pmin=? [ a=0 U a=1 ]"; + formulasString += "; <> Pmax=? [ b=0 U b=1 ]"; + formulasString += "; <> Pmin=? [ b=0 U b=1 ]"; + // GLOBALLY tests formulasString += "; <> Pmax=? [G !\"s3\"]"; formulasString += "; <> Pmin=? [G !\"s3\"]"; formulasString += "; <> Pmax=? [G a=0 ]"; formulasString += "; <> Pmin=? [G a=0 ]"; - - // TODO: check why computation with nativeMultiplier does not work -/* formulasString += "; <> Pmax=? [F \"s3\"]"; + // EVENTUALLY tests + formulasString += "; <> Pmax=? [F \"s3\"]"; formulasString += "; <> Pmin=? [F \"s3\"]"; - formulasString += "; <> Pmax=? [F [3,4] \"s4\"]"; - formulasString += "; <> Pmax=? [F [3,5] \"s4\"]";*/ + formulasString += "; <> Pmax=? [F [3,5] \"s4\"]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/walker.nm", formulasString); auto model = std::move(modelFormulas.first); @@ -188,36 +195,46 @@ namespace { auto checker = this->createModelChecker(model); std::unique_ptr result; - result = checker->check(this->env(), tasks[0]); + // NEXT results + result = checker->check(this->env(), tasks[0]); //OK + EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[1]); //OK + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); //OK + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); //OK EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[1]); + // UNTIL results + result = checker->check(this->env(), tasks[4]); //FAIL -> 0.99999922964892118 this may happen if the walker does not get caught in s4 + EXPECT_NEAR(this->parseNumber("0.52"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[5]); //OK + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[6]); //OK + EXPECT_NEAR(this->parseNumber("0.9999996417"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[7]); //OK EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); + // GLOBALLY tests + result = checker->check(this->env(), tasks[8]); //FAIL -> 2.686012256170045e-06 this may happen if the walker does not stay in s0 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); + result = checker->check(this->env(), tasks[9]); //FAIL -> 1 this is maybe exactly the other way round (by minimizing leaving) EXPECT_NEAR(this->parseNumber("0.65454565"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); + result = checker->check(this->env(), tasks[10]); //FAIL -> 7.7035107881595621e-07 EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[5]); + result = checker->check(this->env(), tasks[11]); //FAIL -> 1 EXPECT_NEAR(this->parseNumber("0.48"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); -/* result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("0.345454"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[3]); + // EVENTUALLY tests + result = checker->check(this->env(), tasks[12]); //FAIL -> 0.99999731398774383 + EXPECT_NEAR(this->parseNumber("0.34545435"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[13]); //OK EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[4]); + result = checker->check(this->env(), tasks[14]); //FAIL -> 0.63359999999999994 here is maybe an offset of 1 step EXPECT_NEAR(this->parseNumber("0.576"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision());*/ + result = checker->check(this->env(), tasks[15]); //FAIL -> 0.64511999999999992 + EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } - // TODO: create more test cases + // TODO: create more test cases (files) }