From 5d28c4cb57d7f336ea1e49b3ea003b3f9f644817 Mon Sep 17 00:00:00 2001 From: tomjanson Date: Sun, 8 Nov 2015 23:51:17 +0100 Subject: [PATCH] naive performance test on crowds5-4 (cf Comics) Former-commit-id: c1616d07fd9bfd1131b6a607349f19ce58c2dc98 [formerly e2068f5e84c369ce682008aa1d9d1070e29fa793] Former-commit-id: 158cf0a2452aebf28beddb585890691d9c97d7b4 --- test/functional/builder/crowds-5-4.pm | 69 +++++++++++++++++++++++++++ test/functional/utility/KSPTest.cpp | 7 +++ test/performance/utility/KSPTest.cpp | 44 +++++++++++++++++ 3 files changed, 120 insertions(+) create mode 100644 test/functional/builder/crowds-5-4.pm create mode 100644 test/performance/utility/KSPTest.cpp diff --git a/test/functional/builder/crowds-5-4.pm b/test/functional/builder/crowds-5-4.pm new file mode 100644 index 000000000..0eb518bf6 --- /dev/null +++ b/test/functional/builder/crowds-5-4.pm @@ -0,0 +1,69 @@ +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 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; diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp index 3a940359f..1e1dd3070 100644 --- a/test/functional/utility/KSPTest.cpp +++ b/test/functional/utility/KSPTest.cpp @@ -109,3 +109,10 @@ TEST(KSPTest, kspPathAsList) { EXPECT_EQ(list, reference); } + + +//---------------------------- +// v---- PLAYGROUND ----v +//---------------------------- + +// (empty) diff --git a/test/performance/utility/KSPTest.cpp b/test/performance/utility/KSPTest.cpp new file mode 100644 index 000000000..ea43f9826 --- /dev/null +++ b/test/performance/utility/KSPTest.cpp @@ -0,0 +1,44 @@ +#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> model = storm::builder::ExplicitPrismModelBuilder().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 startTime = std::chrono::system_clock::now(); + + auto target = "observe0Greater1"; + storm::utility::ksp::ShortestPathsGenerator 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 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 +}