diff --git a/examples/dtmc/crowds/crowds.pm b/examples/dtmc/crowds/crowds.pm new file mode 100644 index 000000000..53eb7b75e --- /dev/null +++ b/examples/dtmc/crowds/crowds.pm @@ -0,0 +1,177 @@ +// 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 TotalRuns; // Total number of protocol runs to analyze +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? + runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances + 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? + + // Counters for attackers' observations + // CWDMAX: 1 counter per each good crowd member + 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; + observe5: [0..TotalRuns] init 0; + observe6: [0..TotalRuns] init 0; + observe7: [0..TotalRuns] init 0; + observe8: [0..TotalRuns] init 0; + observe9: [0..TotalRuns] init 0; + observe10: [0..TotalRuns] init 0; + observe11: [0..TotalRuns] init 0; + observe12: [0..TotalRuns] init 0; + observe13: [0..TotalRuns] init 0; + observe14: [0..TotalRuns] init 0; + observe15: [0..TotalRuns] init 0; + observe16: [0..TotalRuns] init 0; + observe17: [0..TotalRuns] init 0; + observe18: [0..TotalRuns] init 0; + observe19: [0..TotalRuns] init 0; + + [] launch -> (new'=true) & (runCount'=TotalRuns) & (launch'=false); + // Set up a new protocol instance + [] new & runCount>0 -> (runCount'=runCount-1) & (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 + [] lastSeen=0 & badObserve & observe0 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); + [] lastSeen=19 & badObserve & observe19 (observe19'=observe19+1) & (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 diff --git a/examples/pmdp/coin8/coin8.pm b/examples/pmdp/coin8/coin8.pm new file mode 100644 index 000000000..fa843d202 --- /dev/null +++ b/examples/pmdp/coin8/coin8.pm @@ -0,0 +1,72 @@ +//Randomised Consensus Protocol + +mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] +const double p3; // in [0.2 , 0.8] +const double p4; // in [0.2 , 0.8] +const double p5; +const double p6; +const double p7; +const double p8; + + +const int N=8; +const int K; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +module process3 = process1[pc1=pc3,coin1=coin3,p1=p3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule +module process5 = process1[pc1=pc5,coin1=coin5,p1=p5] endmodule +module process6 = process1[pc1=pc6,coin1=coin6,p1=p6] endmodule +module process7 = process1[pc1=pc7,coin1=coin7,p1=p7] endmodule +module process8 = process1[pc1=pc8,coin1=coin8,p1=p8] endmodule + +label "finished" = pc1=3 &pc2=3 &pc3=3 &pc4=3 & pc5=3 & pc6=3 & pc7=3 & pc8=3; +label "all_coins_equal_1" = coin1 = 1 & coin2 = 1 & coin3 = 1 & coin4 = 1 & coin5 = 1 & coin6 = 1 & coin7 = 1 & coin8 = 1; +label "all_coins_equal_0" = coin1 = 0 & coin2 = 0 & coin3 = 0 & coin4 = 0 & coin5 = 0 & coin6 = 0 & coin7 = 0 & coin8 = 0; +label "agree" = coin1=coin2 & coin2=coin3 & coin3 = coin4 & coin4 = coin5 & coin5 = coin6 & coin6 = coin7 & coin7 = coin8; + +rewards "steps" + true : 1; +endrewards + + + diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake index 161e365ad..1d7b91b81 100644 --- a/resources/3rdparty/include_xerces.cmake +++ b/resources/3rdparty/include_xerces.cmake @@ -33,6 +33,8 @@ if(USE_XERCES) if(APPLE) FIND_LIBRARY(COREFOUNDATION_LIBRARY CoreFoundation ) FIND_LIBRARY(CORESERVICES_LIBRARY CoreServices ) + mark_as_advanced(COREFOUNDATION_LIBRARY) + mark_as_advanced(CORESERVICES_LIBRARY) endif() find_package(CURL) list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES}) diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index d5cc0ce5c..29e46f109 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -7,7 +7,16 @@ #include #ifdef STORM_HAVE_CLN +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wmismatched-tags" + +#pragma GCC diagnostic push + #include + +#pragma GCC diagnostic pop +#pragma clang diagnostic pop + #endif #ifdef STORM_HAVE_CARL diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h index 2ae6800ba..2b4f867ef 100755 --- a/src/storage/expressions/ExprtkExpressionEvaluator.h +++ b/src/storage/expressions/ExprtkExpressionEvaluator.h @@ -1,5 +1,4 @@ -#ifndef STORM_STORAGE_EXPRESSIONS_EXPRTKEXPRESSIONEVALUATOR_H_ -#define STORM_STORAGE_EXPRESSIONS_EXPRTKEXPRESSIONEVALUATOR_H_ +#pragma once #include #include @@ -7,7 +6,16 @@ #include "src/storage/expressions/ExpressionEvaluatorBase.h" +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wunused-variable" + +#pragma GCC diagnostic push + #include "exprtk.hpp" + +#pragma GCC diagnostic pop +#pragma clang diagnostic pop + #include "src/storage/expressions/ToExprtkStringVisitor.h" namespace storm { @@ -64,5 +72,3 @@ namespace storm { }; } } - -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRTKEXPRESSIONEVALUATOR_H_ */ \ No newline at end of file diff --git a/src/utility/gmm.h b/src/utility/gmm.h index 39fbd21c0..626a598a5 100644 --- a/src/utility/gmm.h +++ b/src/utility/gmm.h @@ -3,6 +3,8 @@ #pragma clang diagnostic push #pragma clang diagnostic ignored "-Wunused-variable" +#pragma clang diagnostic ignored "-Wunused-parameter" + #pragma GCC diagnostic push #pragma GCC diagnostic ignored "-Wdeprecated-declarations"