diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 79b635845..24267e80d 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -167,9 +167,12 @@ namespace { TYPED_TEST(SmgRpatlModelCheckerTest, Walker) { std::string formulasString = "<> Pmax=? [X \"s2\"]"; formulasString += "; <> Pmin=? [X \"s2\"]"; + formulasString += "; <> Pmax=? [G !\"s3\"]"; + formulasString += "; <> Pmin=? [G !\"s3\"]"; + formulasString += "; <> Pmax=? [G a=0 ]"; + formulasString += "; <> Pmin=? [G a=0 ]"; - // TODO: bounded eventually causes wrong compuations for native multipliers - // TODO: do some more checks for comutation + // TODO: check why computation with nativeMultiplier does not work /* formulasString += "; <> Pmax=? [F \"s3\"]"; formulasString += "; <> Pmin=? [F \"s3\"]"; @@ -191,6 +194,18 @@ namespace { result = checker->check(this->env(), tasks[1]); EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0.65454565"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[5]); + 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());