added testcase RobotCircle to SmgRpatlModelCheckerTest.cpp and the test file robotCircle.nm

resources/examples/testfiles/smg/robotCircle.nm

@@ -0,0 +1,61 @@
+// PRISM Model of a simple robot game
+// - A player - friendlyRobot - moves around and tries not to "crash" with another player - adversary Robot.
+// - friendlyRobot can choose the direction of movement.
+// - adversaryRobot should move in a circle counterclockwise on the grid, but has a probabilty to fail and move into the wrong direction.
+// - The movement of adversaryRobot is defined as a pseudo random movement with probabilty = 1/4 into one of the 4 possible directions.
+
+smg
+
+player friendlyRobot
+  [e1], [w1], [n1], [s1]
+endplayer
+
+player adversaryRobot
+  [e2], [w2], [n2], [s2], [middle]
+endplayer
+
+// 3x3 grid
+const int width = 2;
+const int height = 2;
+
+const int xmin = 0;
+const int xmax = width;
+const int ymin = 0;
+const int ymax = height;
+
+// probabilty to fail
+const double failProb = 1/10;
+const double notFailProb = 1-failProb;
+
+// definition of randomProb, this has to be 0.25 since it is the prob of go into one direction from the middle for the adverseryRobot
+const double randomProb = 1/4;
+
+global move : [0..1] init 0;
+
+//F__
+//___
+//__R
+
+label "crash" = x1=x2 & y1=y2;
+
+module robot1
+  x1 : [0..width] init 0;
+  y1 : [0..height] init 0;
+
+  [e1]    move=0 & x1<xmax -> (x1'=x1+1) & (move'=1);
+  [w1]    move=0 & x1>0    -> (x1'=x1-1) & (move'=1);
+  [n1]    move=0 & y1>0    -> (y1'=y1-1) & (move'=1);
+  [s1]    move=0 & y1<ymax -> (y1'=y1+1) & (move'=1);
+endmodule
+
+module robot2
+  x2 : [0..width] init width;
+  y2 : [0..height] init height;
+
+  [e2]     move=1 & x2<xmax & y2=ymax -> notFailProb : (x2'=x2+1) & (move'=0) + failProb : (y2'=y2-1) & (move'=0);
+  [w2]     move=1 & x2>0 & y2=0 -> notFailProb : (x2'=x2-1) & (move'=0) + failProb : (y2'=y2+1) & (move'=0);
+  [n2]     move=1 & x2=xmax & y2>0 -> notFailProb : (y2'=y2-1) & (move'=0) + failProb : (x2'=x2-1) & (move'=0);
+  [s2]     move=1 & x2=0 & y2<ymax -> notFailProb : (y2'=y2+1) & (move'=0) + failProb : (x2'=x2+1) & (move'=0);
+
+  [middle] move=1 & x2=1 & y2=1 -> randomProb : (x2'=x2+1) & (move'=0) + randomProb : (x2'=x2-1) & (move'=0) + randomProb : (y2'=y2-1) & (move'=0) + randomProb : (y2'=y2+1) & (move'=0);
+endmodule

src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp

@@ -229,6 +229,7 @@ namespace {
         result = checker->check(this->env(), tasks[15]);
         EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
     }
+
     TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) {
         // This test is for borders of bounded U with conversations from G and F
         // bounded G
@@ -322,5 +323,51 @@ namespace {
         EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
     }
 
+    TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) {
+        // This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound)
+        std::string formulasString = " <<friendlyRobot>> Pmax=? [ G<1 !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G<=1 !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G<=5 !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G<=6 !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G<=7 !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G<=8 !\"crash\" ]";
+
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G[1,5] !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G[5,6] !\"crash\" ]";
+        formulasString += "; <<friendlyRobot>> Pmax=? [ G[7,8] !\"crash\" ]";
+
+        auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/robotCircle.nm", formulasString);
+        auto model = std::move(modelFormulas.first);
+        auto tasks = this->getTasks(modelFormulas.second);
+        EXPECT_EQ(81ul, model->getNumberOfStates());
+        EXPECT_EQ(196ul, model->getNumberOfTransitions());
+        EXPECT_EQ(148ul, model->getNumberOfChoices());
+        ASSERT_EQ(model->getType(), storm::models::ModelType::Smg);
+        auto checker = this->createModelChecker(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+        // results for bounded globally with upper bound
+        result = checker->check(this->env(), tasks[0]);
+        EXPECT_NEAR(this->parseNumber("1"), 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.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        result = checker->check(this->env(), tasks[4]);
+        EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        result = checker->check(this->env(), tasks[5]);
+        EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+
+        // results for bounded globally with upper and lower bound
+        result = checker->check(this->env(), tasks[6]);
+        EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        result = checker->check(this->env(), tasks[7]);
+        EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+        result = checker->check(this->env(), tasks[8]);
+        EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
+    }
+
     // TODO: create more test cases (files)
 }