From 27bf04ac5bb38ba24096deaf5503c9539836c67f Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 3 Sep 2021 13:35:18 +0200 Subject: [PATCH] added testcase RobotCircle to SmgRpatlModelCheckerTest.cpp and the test file robotCircle.nm --- .../examples/testfiles/smg/robotCircle.nm | 61 +++++++++++++++++++ .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 47 ++++++++++++++ 2 files changed, 108 insertions(+) create mode 100644 resources/examples/testfiles/smg/robotCircle.nm diff --git a/resources/examples/testfiles/smg/robotCircle.nm b/resources/examples/testfiles/smg/robotCircle.nm new file mode 100644 index 000000000..92170a97a --- /dev/null +++ b/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 (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 (y1'=y1+1) & (move'=1); +endmodule + +module robot2 + x2 : [0..width] init width; + y2 : [0..height] init height; + + [e2] move=1 & x2 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 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 diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index f46106a91..0f0a63ca6 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/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 = " <> Pmax=? [ G<1 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=1 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=5 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=6 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=7 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=8 !\"crash\" ]"; + + formulasString += "; <> Pmax=? [ G[1,5] !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G[5,6] !\"crash\" ]"; + formulasString += "; <> 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 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) }