From b49dd5910119fac84a1573a79a3c571ae708155e Mon Sep 17 00:00:00 2001 From: lukpo Date: Wed, 11 Aug 2021 11:35:33 +0200 Subject: [PATCH] WIP added testcases for globally probabilities for SmgRpatlModelCheckerTest "Walker" --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) 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());