Tom Janson
8 years ago
2 changed files with 0 additions and 113 deletions
@ -1,69 +0,0 @@ |
|||||
dtmc |
|
||||
|
|
||||
// probability of forwarding |
|
||||
const double PF = 0.8; |
|
||||
const double notPF = .2; // must be 1-PF |
|
||||
// probability that a crowd member is bad |
|
||||
const double badC = .167; |
|
||||
// probability that a crowd member is good |
|
||||
const double goodC = 0.833; |
|
||||
// Total number of protocol runs to analyze |
|
||||
const int TotalRuns = 4; |
|
||||
// size of the crowd |
|
||||
const int CrowdSize = 5; |
|
||||
|
|
||||
module crowds |
|
||||
// protocol phase |
|
||||
phase: [0..4] init 0; |
|
||||
|
|
||||
// crowd member good (or bad) |
|
||||
good: bool init false; |
|
||||
|
|
||||
// number of protocol runs |
|
||||
runCount: [0..TotalRuns] init 0; |
|
||||
|
|
||||
// observe_i is the number of times the attacker observed crowd member i |
|
||||
observe0: [0..TotalRuns] init 0; |
|
||||
|
|
||||
observe1: [0..TotalRuns] init 0; |
|
||||
|
|
||||
observe2: [0..TotalRuns] init 0; |
|
||||
|
|
||||
observe3: [0..TotalRuns] init 0; |
|
||||
|
|
||||
observe4: [0..TotalRuns] init 0; |
|
||||
|
|
||||
// the last seen crowd member |
|
||||
lastSeen: [0..CrowdSize - 1] init 0; |
|
||||
|
|
||||
// get the protocol started |
|
||||
[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); |
|
||||
|
|
||||
// decide whether crowd member is good or bad according to given probabilities |
|
||||
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); |
|
||||
|
|
||||
// if the current member is a good member, update the last seen index (chosen uniformly) |
|
||||
[] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); |
|
||||
|
|
||||
// if the current member is a bad member, record the most recently seen index |
|
||||
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); |
|
||||
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); |
|
||||
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); |
|
||||
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); |
|
||||
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); |
|
||||
|
|
||||
// good crowd members forward with probability PF and deliver otherwise |
|
||||
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); |
|
||||
|
|
||||
// deliver the message and start over |
|
||||
[] phase=4 -> 1: (phase'=0); |
|
||||
|
|
||||
endmodule |
|
||||
|
|
||||
label "observe0Greater1" = observe0>1; |
|
||||
label "observe1Greater1" = observe1>1; |
|
||||
label "observe2Greater1" = observe2>1; |
|
||||
label "observe3Greater1" = observe3>1; |
|
||||
label "observe4Greater1" = observe4>1; |
|
||||
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; |
|
||||
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; |
|
||||
@ -1,44 +0,0 @@ |
|||||
#include "gtest/gtest.h"
|
|
||||
#include "storm-config.h"
|
|
||||
|
|
||||
#include "src/parser/PrismParser.h"
|
|
||||
#include "src/models/sparse/Dtmc.h"
|
|
||||
#include "src/builder/ExplicitPrismModelBuilder.h"
|
|
||||
#include "src/utility/graph.h"
|
|
||||
#include "src/utility/shortestPaths.cpp"
|
|
||||
|
|
||||
const bool VERBOSE = true; |
|
||||
|
|
||||
TEST(KSPTest, crowdsSpeed) { |
|
||||
if (VERBOSE) std::cout << "Parsing crowds-5-4.pm file and building model ... " << std::endl; |
|
||||
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-4.pm"); |
|
||||
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program); |
|
||||
|
|
||||
if (VERBOSE) std::cout << "Initializing ShortestPathsGenerator ..." << std::endl; |
|
||||
// timekeeping taken from http://en.cppreference.com/w/cpp/chrono#Example
|
|
||||
std::chrono::time_point<std::chrono::system_clock> startTime = std::chrono::system_clock::now(); |
|
||||
|
|
||||
auto target = "observe0Greater1"; |
|
||||
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, target); |
|
||||
|
|
||||
storm::storage::BitVector accStates(model->getNumberOfStates(), false); |
|
||||
double accumProb = 0; |
|
||||
|
|
||||
if (VERBOSE) std::cout << "Accumulating shortest paths ..." << std::endl; |
|
||||
for (int i = 1; accumProb < 0.15; i++) { |
|
||||
double pathProb = spg.getDistance(i); |
|
||||
accumProb += pathProb; |
|
||||
|
|
||||
storm::storage::BitVector statesInPath = spg.getStates(i); |
|
||||
accStates |= statesInPath; |
|
||||
|
|
||||
if (i % 50000 == 0) { |
|
||||
if (VERBOSE) std::cout << " --> It/States/AccProb/PathProb: " << i << " / " << accStates.getNumberOfSetBits() << " / " << accumProb << " / " << pathProb << std::endl; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
std::chrono::duration<double> elapsedSeconds = std::chrono::system_clock::now() - startTime; |
|
||||
if (VERBOSE) std::cout << "Done. Num of states: " << accStates.getNumberOfSetBits() << ". Seconds: " << elapsedSeconds.count() << std::endl; |
|
||||
|
|
||||
EXPECT_LE(elapsedSeconds.count(), 5); // should take less than 5 seconds on a modern PC
|
|
||||
} |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue