diff --git a/resources/examples/testfiles/smg/messageHack.nm b/resources/examples/testfiles/smg/messageHack.nm new file mode 100644 index 000000000..e67352bef --- /dev/null +++ b/resources/examples/testfiles/smg/messageHack.nm @@ -0,0 +1,52 @@ +// PRISM Model of hacking a communication +// - Bob and Alice are chatting. +// - Eve wants to hack the messages from Bob. +// - The propability of successfull hacking is 0.05. + +smg + +player bob + [receiveB], [readWriteB], [sendB], [waitB] +endplayer + +player alice + [receiveA], [readWriteA], [sendA], [waitA] +endplayer + +player eve + [hackE], [waitE] +endplayer + +// 0 bob, 1 eve, 2 alice +global move : [0..2] init 0; +// +global bobSent : [0..1] init 0; +global hacked : [0..1] init 0; + +label "hacked" = hacked=1; + +module communication + bobReceived : [0..1] init 0; + bobWroteMessage : [0..1] init 1; + aliceReceived : [0..1] init 0; + aliceWroteMessage : [0..1] init 0; + aliceSent : [0..1] init 0; + + // bob's communication part + [receiveB] move=0 & aliceSent=1 -> (bobReceived'=1) & (aliceSent'=0) & (move'=1); + [readWriteB] move=0 & bobReceived=1 -> (bobWroteMessage'=1) & (bobReceived'=0) & (move'=1); + [sendB] move=0 & bobWroteMessage=1 -> (bobSent'=1) & (bobWroteMessage'=0) & (move'=1); + [waitB] move=0 & !(aliceSent=1 | bobReceived=1 | bobWroteMessage=1) -> (move'=1); + + // alice's communication part + [receiveA] move=2 & bobSent=1 -> (aliceReceived'=1) & (bobSent'=0) & (move'=0); + [readWriteA] move=2 & aliceReceived=1 -> (aliceWroteMessage'=1) & (aliceReceived'=0) & (move'=0); + [sendA] move=2 & aliceWroteMessage=1 -> (aliceSent'=1) & (aliceWroteMessage'=0) & (move'=0); + [waitA] move=2 & !(bobSent=1 | aliceReceived=1 | aliceWroteMessage=1) -> (move'=0); + +endmodule + +module hacking + [hackE] move=1 & bobSent=1 -> 0.05: (hacked'=1) & (move'=2) + 0.95: (move'=2); + [waitE] move=1 & !(bobSent=1) -> (move'=2); +endmodule diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index b3c4bbcb7..63fc4e1b4 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -235,6 +235,71 @@ 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 + std::string formulasString = "<> Pmax=? [ G !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=1 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=2 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=10 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=17 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=32 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=47 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=61 !\"hacked\" ]"; + formulasString += "; <> Pmax=? [ G <=62 !\"hacked\" ]"; + + // bounded F + formulasString += "; <> Pmin=? [ F \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [1,2] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [3,16] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [0,17] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [17,31] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [17,32] \"hacked\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/messageHack.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(30ul, model->getNumberOfStates()); + EXPECT_EQ(31ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Smg); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // bounded G results + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("1.99379598e-05"), 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("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[4]); + EXPECT_NEAR(this->parseNumber("0.9025"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("0.857375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[6]); + EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[7]); + EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[8]); + EXPECT_NEAR(this->parseNumber("0.7737809375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + // bounded F results + result = checker->check(this->env(), tasks[9]); + EXPECT_NEAR(this->parseNumber("0.999980062"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[10]); + EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[11]); + EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[12]); + EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[13]); + EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + result = checker->check(this->env(), tasks[14]); + EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + // TODO: create more test cases (files) }