From ea6c957030a843892d527caf7df8765fbcd4b7e8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Dec 2017 10:46:56 +0100 Subject: [PATCH] tests for multi-dimensional cost bounded DTMCs --- .../testfiles/dtmc/crowds_cost_bounded.pm | 260 ++++++++++++++++++ ...tmcMultiDimensionalRewardUnfoldingTest.cpp | 99 +++++++ 2 files changed, 359 insertions(+) create mode 100644 resources/examples/testfiles/dtmc/crowds_cost_bounded.pm create mode 100644 src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp diff --git a/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm b/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm new file mode 100644 index 000000000..d781dadc9 --- /dev/null +++ b/resources/examples/testfiles/dtmc/crowds_cost_bounded.pm @@ -0,0 +1,260 @@ +// CROWDS [Reiter,Rubin] +// Vitaly Shmatikov, 2002 + +// Note: +// Change everything marked CWDSIZ when changing the size of the crowd +// Change everything marked CWDMAX when increasing max size of the crowd + +dtmc + +// Probability of forwarding +const double PF = 0.8; + +// Probability that a crowd member is bad +const double badC = 0.091; +// const double badC = 0.167; + +const int CrowdSize; // CWDSIZ: actual number of good crowd members +const int MaxGood=20; // CWDMAX: maximum number of good crowd members + +// Process definitions +module crowds + + // Auxiliary variables + launch: bool init true; // Start modeling? + new: bool init false; // Initialize a new protocol instance? + start: bool init false; // Start the protocol? + run: bool init false; // Run the protocol? + lastSeen: [0..MaxGood] init MaxGood; // Last crowd member to touch msg + good: bool init false; // Crowd member is good? + bad: bool init false; // ... bad? + recordLast: bool init false; // Record last seen crowd member? + badObserve: bool init false; // Bad members observes who sent msg? + deliver: bool init false; // Deliver message to destination? + done: bool init false; // Protocol instance finished? + + [] launch -> (new'=true) & (launch'=false); + // Set up a new protocol instance + [newrun] new -> (new'=false) & (start'=true); + + // SENDER + // Start the protocol + [] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false); + + // CROWD MEMBERS + // Good or bad crowd member? + [] !good & !bad & !deliver & run -> + 1-badC : (good'=true) & (recordLast'=true) & (run'=false) + + badC : (bad'=true) & (badObserve'=true) & (run'=false); + + // GOOD MEMBERS + // Forward with probability PF, else deliver + [] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true); + // Record the last crowd member who touched the msg; + // all good members may appear with equal probability + // Note: This is backward. In the real protocol, each honest + // forwarder randomly chooses the next forwarder. + // Here, the identity of an honest forwarder is randomly + // chosen *after* it has forwarded the message. + [] recordLast & CrowdSize=2 -> + 1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=4 -> + 1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=5 -> + 1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=10 -> + 1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=15 -> + 1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + + 1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true); + [] recordLast & CrowdSize=20 -> + 1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) + + 1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true); + + // BAD MEMBERS + // Remember from whom the message was received and deliver + // CWDMAX: 1 rule per each good crowd member + [obs0] lastSeen=0 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs1] lastSeen=1 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs2] lastSeen=2 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs3] lastSeen=3 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs4] lastSeen=4 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs5] lastSeen=5 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs6] lastSeen=6 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs7] lastSeen=7 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs8] lastSeen=8 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs9] lastSeen=9 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs10] lastSeen=10 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs11] lastSeen=11 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs12] lastSeen=12 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs13] lastSeen=13 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs14] lastSeen=14 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs15] lastSeen=15 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs16] lastSeen=16 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs17] lastSeen=17 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs18] lastSeen=18 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + [obs19] lastSeen=19 & badObserve -> (deliver'=true) & (run'=true) & (badObserve'=false); + + // RECIPIENT + // Delivery to destination + [] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false); + // Start a new instance + [] done -> (new'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood); + +endmodule + +rewards "num_runs" + [newrun] true : 1; +endrewards + +rewards "observe0" + [obs0] true : 1; +endrewards + +rewards "observe1" + [obs1] true : 1; +endrewards + +rewards "observe2" + [obs2] true : 1; +endrewards + +rewards "observe3" + [obs3] true : 1; +endrewards + +rewards "observe4" + [obs4] true : 1; +endrewards + +rewards "observe5" + [obs5] true : 1; +endrewards + +rewards "observe6" + [obs6] true : 1; +endrewards + +rewards "observe7" + [obs7] true : 1; +endrewards + +rewards "observe8" + [obs8] true : 1; +endrewards + +rewards "observe9" + [obs9] true : 1; +endrewards + +rewards "observe10" + [obs10] true : 1; +endrewards + +rewards "observe11" + [obs11] true : 1; +endrewards + +rewards "observe12" + [obs12] true : 1; +endrewards + +rewards "observe13" + [obs13] true : 1; +endrewards + +rewards "observe14" + [obs14] true : 1; +endrewards + +rewards "observe15" + [obs15] true : 1; +endrewards + +rewards "observe16" + [obs16] true : 1; +endrewards + +rewards "observe17" + [obs17] true : 1; +endrewards + +rewards "observe18" + [obs18] true : 1; +endrewards + +rewards "observe19" + [obs19] true : 1; +endrewards + +rewards "observeI" + [obs1] true : 1; + [obs2] true : 1; + [obs3] true : 1; + [obs4] true : 1; + [obs5] true : 1; + [obs6] true : 1; + [obs7] true : 1; + [obs8] true : 1; + [obs9] true : 1; + [obs10] true : 1; + [obs11] true : 1; + [obs12] true : 1; + [obs13] true : 1; + [obs14] true : 1; + [obs15] true : 1; + [obs16] true : 1; + [obs17] true : 1; + [obs18] true : 1; + [obs19] true : 1; +endrewards + + diff --git a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp new file mode 100644 index 000000000..36ca41ff0 --- /dev/null +++ b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -0,0 +1,99 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/utility/constants.h" +#include "storm/api/storm.h" +#include "storm/environment/Environment.h" + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"; + std::string formulasAsString = "P=? [ F{\"coin_flips\"}<=2 \"two\" ] "; + formulasAsString += "; P=? [ F{\"coin_flips\"}<=3 \"two\" ] "; + formulasAsString += "; P=? [ F{\"coin_flips\"}<=8 \"two\" ] "; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("0")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("1/8")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("21/128")), result->asExplicitQuantitativeCheckResult()[initState]); +} + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"; + std::string formulasAsString = "P=? [ F{\"num_rounds\"}<=1 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}<=2 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}>2 \"elected\" ] "; + formulasAsString += "; P=? [ F{\"num_rounds\"}>=2,{\"num_rounds\"}<3 \"elected\" ] "; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("24/25")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("624/625")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("1/625")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[3], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("24/625")), result->asExplicitQuantitativeCheckResult()[initState]); +} + +TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) { + storm::Environment env; + std::string programFile = STORM_TEST_RESOURCES_DIR "/dtmc/crowds_cost_bounded.pm"; + std::string formulasAsString = "P=? [F{\"num_runs\"}<=3,{\"observe0\"}>1 true]"; + formulasAsString += "; P=? [F{\"num_runs\"}<=3,{\"observe1\"}>1 true]"; + formulasAsString += "; R{\"observe0\"}=? [C{\"num_runs\"}<=3]"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, "CrowdSize=4"); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> dtmc = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *dtmc->getInitialStates().begin();; + std::unique_ptr result; + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("78686542099694893/1268858272000000000")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("13433618626105041/1268858272000000000")), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask(formulas[2], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(std::string("620529/1364000")), result->asExplicitQuantitativeCheckResult()[initState]); +}