diff --git a/test/functional/builder/crowds-5-4.pm b/test/functional/builder/crowds-5-4.pm deleted file mode 100644 index 0eb518bf6..000000000 --- a/test/functional/builder/crowds-5-4.pm +++ /dev/null @@ -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 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/performance/utility/KSPTest.cpp b/test/performance/utility/KSPTest.cpp deleted file mode 100644 index ea43f9826..000000000 --- a/test/performance/utility/KSPTest.cpp +++ /dev/null @@ -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> 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 -}