sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

tests for multi-dimensional cost bounded DTMCs

tempestpy_adaptions
TimQu 7 years ago
parent
c59d2160ee
commit
ea6c957030
2 changed files with 359 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 260
      resources/examples/testfiles/dtmc/crowds_cost_bounded.pm
  2. 99
      src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp

260
resources/examples/testfiles/dtmc/crowds_cost_bounded.pm
View File

@ -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

99
src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp
View File

@ -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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
uint_fast64_t const initState = *dtmc->getInitialStates().begin();;
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("0")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/8")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("21/128")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
uint_fast64_t const initState = *dtmc->getInitialStates().begin();;
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/25")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("624/625")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("1/625")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("24/625")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
uint_fast64_t const initState = *dtmc->getInitialStates().begin();;
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[0], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("78686542099694893/1268858272000000000")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[1], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("13433618626105041/1268858272000000000")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(dtmc, storm::api::createTask<storm::RationalNumber>(formulas[2], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("620529/1364000")), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
}
Write Preview
Loading…
Cancel
Save