diff --git a/resources/examples/testfiles/smg/rightDecision.nm b/resources/examples/testfiles/smg/rightDecision.nm new file mode 100644 index 000000000..a47222e10 --- /dev/null +++ b/resources/examples/testfiles/smg/rightDecision.nm @@ -0,0 +1,42 @@ +// PRISM Model of a decision for a shortcut +// - A hiker has to make a decision of taking a shortcut. +// - On the shortcut a native can be asked for getting to the target waypoint. +// - The native can lead the hiker to the goal or can give a proposal for getting to 0.9 to the target. + +smg + +player hiker + [startShortcut], [startWay], [waypoint1], [waypoint2target], [waypoint2start], [target], [lost] +endplayer + +player native + [wait], [shortcutBad], [shortcutGood] +endplayer + +// 0 bob, 1 native, +global move : [0..1] init 0; + +global shortcut : [0..1] init 0; +global target : [0..1] init 0; +global lost : [0..1] init 0; + +label "target" = target=1; + +module hikerModule + startpoint : [0..1] init 1; + waypoints : [0..2] init 0; + + [startShortcut] move=0 & startpoint=1 -> (shortcut'=1) & (startpoint'=0) & (move'=1); + [startWay] move=0 & startpoint=1 -> (waypoints'=1) & (startpoint'=0) & (move'=1); + [waypoint1] move=0 & waypoints=1 -> (waypoints'=2) & (move'=1); + [waypoint2target] move=0 & waypoints=2 -> (waypoints'=0) & (target'=1) & (move'=1); + [waypoint2start] move=0 & waypoints=2 -> (waypoints'=0) & (startpoint'=1) & (move'=1); + [target] move=0 & target=1 -> (move'=1); + [lost] move=0 & lost=1 -> (move'=1); +endmodule + +module nativeModule + [wait] move=1 & !(shortcut=1) -> (move'=0); + [shortcutBad] move=1 & shortcut=1 -> 0.9: (shortcut'=0) & (target'=1) & (move'=0) + 0.1: (shortcut'=0) & (lost'=1) & (move'=0); + [shortcutGood] move=1 & shortcut=1 -> (shortcut'=0) & (target'=1) & (move'=0); +endmodule diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 63fc4e1b4..34a805537 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -300,6 +300,55 @@ namespace { EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, RightDecision) { + // This test is for making decisions and creating shields + // testing probabilities for decisions + std::string formulasString = "<> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + + // testing create shielding expressions + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(11ul, model->getNumberOfStates()); + EXPECT_EQ(15ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // probability results + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.9"), 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("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + // shielding results + result = checker->check(this->env(), tasks[4]); + result = checker->check(this->env(), tasks[5]); + result = checker->check(this->env(), tasks[6]); + result = checker->check(this->env(), tasks[7]); + result = checker->check(this->env(), tasks[8]); + result = checker->check(this->env(), tasks[9]); + result = checker->check(this->env(), tasks[10]); + result = checker->check(this->env(), tasks[11]); + + //TODO: check the shields + } // TODO: create more test cases (files) }