added testcase rightDecision (rightDecision.nm) to SmgRpatlModelCheckerTest.cpp

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

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 = "<<hiker>> Pmax=? [ F <=3 \"target\" ]";
+        formulasString += "; <<hiker>> Pmax=? [ F <=5 \"target\" ]";
+        formulasString += "; <<hiker, native>> Pmax=? [ F <=3 \"target\" ]";
+        formulasString += "; <<hiker>> Pmin=? [ F \"target\" ]";
+
+        // testing create shielding expressions
+        formulasString += "; <preSafetyShieldLambda1, PreSafety, lambda=0.9> <<hiker>> Pmax=? [ F <=3 \"target\" ]";
+        formulasString += "; <postSafetyShieldGamma1, PostSafety, gamma=0.9> <<hiker>> Pmax=? [ F <=3 \"target\" ]";
+        formulasString += "; <preSafetyShieldLambda2, PreSafety, lambda=0.5> <<hiker>> Pmax=? [ F <=5 \"target\" ]";
+        formulasString += "; <postSafetyShieldGamma2, PostSafety, gamma=0.5> <<hiker>> Pmax=? [ F <=5 \"target\" ]";
+        formulasString += "; <preSafetyShieldLambda3, PreSafety, lambda=0> <<hiker, native>> Pmax=? [ F <=3 \"target\" ]";
+        formulasString += "; <postSafetyShieldGamma3, PostSafety, gamma=0> <<hiker, native>> Pmax=? [ F <=3 \"target\" ]";
+        formulasString += "; <preSafetyShieldLambda4, PreSafety, lambda=0.9> <<hiker>> Pmin=? [ F \"target\" ]";
+        formulasString += "; <postSafetyShieldGamma4, PostSafety, gamma=0.9> <<hiker>> 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<storm::modelchecker::CheckResult> 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)
 }