From 4999cfa8a0d1391d21f980ad4219dfea0e817780 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 4 Aug 2016 13:25:55 +0200 Subject: [PATCH] By performance tests, you served us well but we do not love you any longer Former-commit-id: 048c3447cb9c6d11d091148403bfd2da08fed0bf --- test/CMakeLists.txt | 10 +- test/performance/builder/crowds15_5.pm | 95 ------- test/performance/builder/csma3_2.nm | 132 ---------- test/performance/builder/leader5.nm | 97 ------- test/performance/builder/leader5_8.pm | 89 ------- test/performance/graph/GraphTest.cpp | 79 ------ .../GmmxxDtmcPrctModelCheckerTest.cpp | 88 ------- .../GmmxxMdpPrctlModelCheckerTest.cpp | 142 ----------- .../NativeDtmcPrctlModelCheckerTest.cpp | 88 ------- .../NativeMdpPrctlModelCheckerTest.cpp | 143 ----------- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 210 ---------------- .../SymbolicMdpPrctlModelCheckerTest.cpp | 237 ------------------ ...ValueIterationMdpPrctlModelCheckerTest.cpp | 112 --------- test/performance/storage/BitVectorTest.cpp | 15 -- .../MaximalEndComponentDecompositionTest.cpp | 28 --- test/performance/storage/SparseMatrixTest.cpp | 96 ------- ...glyConnectedComponentDecompositionTest.cpp | 79 ------ test/performance/storm-performance-tests.cpp | 16 -- 18 files changed, 1 insertion(+), 1755 deletions(-) delete mode 100644 test/performance/builder/crowds15_5.pm delete mode 100644 test/performance/builder/csma3_2.nm delete mode 100644 test/performance/builder/leader5.nm delete mode 100644 test/performance/builder/leader5_8.pm delete mode 100644 test/performance/graph/GraphTest.cpp delete mode 100644 test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp delete mode 100644 test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp delete mode 100644 test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp delete mode 100644 test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp delete mode 100644 test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp delete mode 100644 test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp delete mode 100644 test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp delete mode 100644 test/performance/storage/BitVectorTest.cpp delete mode 100644 test/performance/storage/MaximalEndComponentDecompositionTest.cpp delete mode 100644 test/performance/storage/SparseMatrixTest.cpp delete mode 100644 test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp delete mode 100644 test/performance/storm-performance-tests.cpp diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index a2f77a882..615b253e3 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -2,27 +2,19 @@ # Note that the tests also need the source files, except for the main file file(GLOB STORM_FUNCTIONAL_TEST_MAIN_FILE ${STORM_CPP_TESTS_BASE_PATH}/functional/storm-functional-tests.cpp) file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/functional/*.h ${STORM_CPP_TESTS_BASE_PATH}/functional/*.cpp) -file(GLOB STORM_PERFORMANCE_TEST_MAIN_FILE ${STORM_CPP_TESTS_BASE_PATH}/performance/storm-performance-tests.cpp) -file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/performance/*.h ${STORM_CPP_TESTS_BASE_PATH}/performance/*.cpp) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) -source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES} ${}) add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES}) target_link_libraries(storm-functional-tests storm) -add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_MAIN_FILE} ${STORM_PERFORMANCE_TEST_FILES}) -target_link_libraries(storm-performance-tests storm) add_dependencies(storm-functional-tests test-resources) -add_dependencies(storm-performance-tests test-resources) include_directories(${GTEST_INCLUDE_DIR}) enable_testing() target_link_libraries(storm-functional-tests ${STORM_TEST_LINK_LIBRARIES}) -target_link_libraries(storm-performance-tests ${STORM_TEST_LINK_LIBRARIES}) add_test(NAME storm-functional-tests COMMAND storm-functional-tests) -add_test(NAME storm-performance-tests COMMAND storm-performance-tests) -INSTALL(TARGETS storm-functional-tests storm-performance-tests +INSTALL(TARGETS storm-functional-tests RUNTIME DESTINATION bin LIBRARY DESTINATION lib ARCHIVE DESTINATION lib diff --git a/test/performance/builder/crowds15_5.pm b/test/performance/builder/crowds15_5.pm deleted file mode 100644 index 95ab8a910..000000000 --- a/test/performance/builder/crowds15_5.pm +++ /dev/null @@ -1,95 +0,0 @@ -dtmc - -// probability of forwarding -const double PF = 0.8; -const double notPF = 0.2; // must be 1-PF -// probability that a crowd member is bad -const double badC = 0.167; - // probability that a crowd member is good -const double goodC = 0.833; -// Total number of protocol runs to analyze -const int TotalRuns = 5; -// size of the crowd -const int CrowdSize = 15; - -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; - - 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; - - // 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/15 : (lastSeen'=0) & (phase'=3) + 1/15 : (lastSeen'=1) & (phase'=3) + 1/15 : (lastSeen'=2) & (phase'=3) + 1/15 : (lastSeen'=3) & (phase'=3) + 1/15 : (lastSeen'=4) & (phase'=3) + 1/15 : (lastSeen'=5) & (phase'=3) + 1/15 : (lastSeen'=6) & (phase'=3) + 1/15 : (lastSeen'=7) & (phase'=3) + 1/15 : (lastSeen'=8) & (phase'=3) + 1/15 : (lastSeen'=9) & (phase'=3) + 1/15 : (lastSeen'=10) & (phase'=3) + 1/15 : (lastSeen'=11) & (phase'=3) + 1/15 : (lastSeen'=12) & (phase'=3) + 1/15 : (lastSeen'=13) & (phase'=3) + 1/15 : (lastSeen'=14) & (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); - [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4); - [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4); - [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4); - [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4); - [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4); - [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1: (observe10'=observe10+1) & (phase'=4); - [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1: (observe11'=observe11+1) & (phase'=4); - [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1: (observe12'=observe12+1) & (phase'=4); - [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1: (observe13'=observe13+1) & (phase'=4); - [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1: (observe14'=observe14+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 "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1; -label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1; diff --git a/test/performance/builder/csma3_2.nm b/test/performance/builder/csma3_2.nm deleted file mode 100644 index 6411b6a85..000000000 --- a/test/performance/builder/csma3_2.nm +++ /dev/null @@ -1,132 +0,0 @@ -// CSMA/CD protocol - probabilistic version of kronos model (3 stations) -// gxn/dxp 04/12/01 - -mdp - -// note made changes since cannot have strict inequalities -// in digital clocks approach and suppose a station only sends one message - -// simplified parameters scaled -const int sigma=1; // time for messages to propagate along the bus -const int lambda=30; // time to send a message - -// actual parameters -const int N = 3; // number of processes -const int K = 2; // exponential backoff limit -const int slot = 2*sigma; // length of slot -const int M = floor(pow(2, K))-1 ; // max number of slots to wait -//const int lambda=782; -//const int sigma=26; - -//---------------------------------------------------------------------------------------------------------------------------- -// the bus -module bus - - b : [0..2]; - // b=0 - idle - // b=1 - active - // b=2 - collision - - // clocks of bus - y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) - y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) - - // a sender sends (ok - no other message being sent) - [send1] (b=0) -> (b'=1); - [send2] (b=0) -> (b'=1); - [send3] (b=0) -> (b'=1); - - // a sender sends (bus busy - collision) - [send1] (b=1|b=2) & (y1 (b'=2); - [send2] (b=1|b=2) & (y1 (b'=2); - [send3] (b=1|b=2) & (y1 (b'=2); - - // finish sending - [end1] (b=1) -> (b'=0) & (y1'=0); - [end2] (b=1) -> (b'=0) & (y1'=0); - [end3] (b=1) -> (b'=0) & (y1'=0); - - // bus busy - [busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); - [busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); - [busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b); - - // collision detected - [cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); - - // time passage - [time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 - [time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 - [time] (b=2) & (y2 (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) - -endmodule - -//---------------------------------------------------------------------------------------------------------------------------- -// model of first sender -module station1 - - // LOCAL STATE - s1 : [0..5]; - // s1=0 - initial state - // s1=1 - transmit - // s1=2 - collision (set backoff) - // s1=3 - wait (bus busy) - // s1=4 - successfully sent - - // LOCAL CLOCK - x1 : [0..max(lambda,slot)]; - - // BACKOFF COUNTER (number of slots to wait) - bc1 : [0..M]; - - // COLLISION COUNTER - cd1 : [0..K]; - - // start sending - [send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending - [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff - - // transmitting - [time] (s1=1) & (x1 (x1'=min(x1+1,lambda)); // let time pass - [end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished - [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) - [cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important - - // set backoff (no time can pass in this state) - // probability depends on which transmission this is (cd1) - [] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; - [] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; - - // wait until backoff counter reaches 0 then send again - [time] (s1=3) & (x1 (x1'=x1+1); // let time pass (in slot) - [time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) - [send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) - [busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) - - // once finished nothing matters - [time] (s1>=4) -> (x1'=0); - -endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// construct further stations through renaming -module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule -module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// reward structure for expected time -rewards "time" - [time] true : 1; -endrewards - -//---------------------------------------------------------------------------------------------------------------------------- - -// labels/formulae -label "all_delivered" = s1=4&s2=4&s3=4; -label "one_delivered" = s1=4|s2=4|s3=4; -label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); -formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); -formula min_collisions = min(cd1,cd2,cd3); -formula max_collisions = max(cd1,cd2,cd3); diff --git a/test/performance/builder/leader5.nm b/test/performance/builder/leader5.nm deleted file mode 100644 index 26316affa..000000000 --- a/test/performance/builder/leader5.nm +++ /dev/null @@ -1,97 +0,0 @@ -// asynchronous leader election -// 4 processes -// gxn/dxp 29/01/01 - -mdp - -const int N= 5; // number of processes - -//---------------------------------------------------------------------------------------------------------------------------- -module process1 - - // COUNTER - c1 : [0..5-1]; - - // STATES - s1 : [0..4]; - // 0 make choice - // 1 have not received neighbours choice - // 2 active - // 3 inactive - // 4 leader - - // PREFERENCE - p1 : [0..1]; - - // VARIABLES FOR SENDING AND RECEIVING - receive1 : [0..2]; - // not received anything - // received choice - // received counter - sent1 : [0..2]; - // not send anything - // sent choice - // sent counter - - // pick value - [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); - - // send preference - [p12] (s1=1) & (sent1=0) -> (sent1'=1); - // receive preference - // stay active - [p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1); - // become inactive - [p51] (s1=1) & (receive1=0) & (p1=0) & (p5=1) -> (s1'=3) & (receive1'=1); - - // send preference (can now reset preference) - [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); - // send counter (already sent preference) - // not received counter yet - [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); - // received counter (pick again) - [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - - // receive counter and not sent yet (note in this case do not pass it on as will send own counter) - [c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); - // receive counter and sent counter - // only active process (decide) - [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - // other active process (pick again) - [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - - // send preference (must have received preference) and can now reset - [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); - // send counter (must have received counter first) and can now reset - [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - - // receive preference - [p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1); - // receive counter - [c51] (s1=3) & (receive1=1) & (c5 (c1'=c5+1) & (receive1'=2); - - // done - [done] (s1=4) -> (s1'=s1); - // add loop for processes who are inactive - [done] (s1=3) -> (s1'=s1); - -endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// construct further stations through renaming -module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule -module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule -module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule -module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// reward - expected number of rounds (equals the number of times a process receives a counter) -rewards "rounds" - [c12] true : 1; -endrewards - -//---------------------------------------------------------------------------------------------------------------------------- -formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); -label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; diff --git a/test/performance/builder/leader5_8.pm b/test/performance/builder/leader5_8.pm deleted file mode 100644 index eb7dd9fd7..000000000 --- a/test/performance/builder/leader5_8.pm +++ /dev/null @@ -1,89 +0,0 @@ -// synchronous leader election protocol (itai & Rodeh) -// dxp/gxn 25/01/01 - -dtmc - -// CONSTANTS -const int N = 5; // number of processes -const int K = 8; // range of probabilistic choice - -// counter module used to count the number of processes that have been read -// and to know when a process has decided -module counter - - // counter (c=i means process j reading process (i-1)+j next) - c : [1..N-1]; - - // reading - [read] c (c'=c+1); - // finished reading - [read] c=N-1 -> (c'=c); - //decide - [done] u1|u2|u3|u4|u5 -> (c'=c); - // pick again reset counter - [retry] !(u1|u2|u3|u4|u5) -> (c'=1); - // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (c'=c); - -endmodule - -// processes form a ring and suppose: -// process 1 reads process 2 -// process 2 reads process 3 -// process 3 reads process 1 -module process1 - - // local state - s1 : [0..3]; - // s1=0 make random choice - // s1=1 reading - // s1=2 deciding - // s1=3 finished - - // has a unique id so far (initially true) - u1 : bool; - - // value to be sent to next process in the ring (initially sets this to its own value) - v1 : [0..K-1]; - - // random choice - p1 : [0..K-1]; - - // pick value - [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) - + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) - + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) - + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) - + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true) - + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) - + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) - + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); - // read - [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); - [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); - // read and move to decide - [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); - [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); - // deciding - // done - [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); - //retry - [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); - // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (s1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule -module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule -module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule -module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule - -// expected number of rounds -rewards "num_rounds" - [pick] true : 1; -endrewards - -// labels -label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp deleted file mode 100644 index dc825efc6..000000000 --- a/test/performance/graph/GraphTest.cpp +++ /dev/null @@ -1,79 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/settings/SettingsManager.h" -#include "src/parser/AutoParser.h" -#include "src/utility/graph.h" -#include "src/storage/StronglyConnectedComponentDecomposition.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/StandardRewardModel.h" - -TEST(GraphTest, ExplicitProb01) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); - - std::shared_ptr> dtmc = abstractModel->as>(); - storm::storage::BitVector trueStates(dtmc->getNumberOfStates(), true); - - std::pair prob01(storm::utility::graph::performProb01(*dtmc, trueStates, dtmc->getStates("observe0Greater1"))); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046ull); - - prob01 = storm::utility::graph::performProb01(*dtmc, trueStates, dtmc->getStates("observeIGreater1")); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797ull); - - prob01 = storm::utility::graph::performProb01(*dtmc, trueStates, dtmc->getStates("observeOnlyTrueSender")); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992ull); - - dtmc = nullptr; - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", ""); - - std::shared_ptr> dtmc2 = abstractModel->as>(); - trueStates = storm::storage::BitVector(dtmc2->getNumberOfStates(), true); - - prob01 = storm::utility::graph::performProb01(*dtmc2, trueStates, storm::storage::BitVector(dtmc2->getStates("elected"))); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334ull); - - dtmc2 = nullptr; -} - -TEST(GraphTest, PerformProb01MinMax) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); - storm::storage::BitVector trueStates(mdp->getNumberOfStates(), true); - - std::pair prob01(storm::utility::graph::performProb01Min(*mdp, trueStates, mdp->getStates("elected"))); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783ull); - - prob01 = storm::utility::graph::performProb01Max(*mdp, trueStates, mdp->getStates("elected")); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783ull); - - mdp = nullptr; - - abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); - std::shared_ptr> mdp2 = abstractModel->as>(); - trueStates = storm::storage::BitVector(mdp2->getNumberOfStates(), true); - - prob01 = storm::utility::graph::performProb01Min(*mdp2, trueStates, mdp2->getStates("finished")); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616ull); - - prob01 = storm::utility::graph::performProb01Max(*mdp2, trueStates, mdp2->getStates("finished")); - - ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0ull); - ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616ull); - - mdp2 = nullptr; -} diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp deleted file mode 100644 index df5f4dde6..000000000 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ /dev/null @@ -1,88 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/GmmxxEquationSolverSettings.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" -#include "src/settings/SettingMemento.h" -#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/utility/solver.h" -#include "src/parser/AutoParser.h" -#include "src/parser/FormulaParser.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/solver/GmmxxLinearEquationSolver.h" - -TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); - ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolverFactory())); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.2296800237, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.22742171078, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - - -TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); - ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolverFactory())); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.025106273, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index 3ae471fa3..000000000 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,142 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/utility/solver.h" -#include "src/parser/AutoParser.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/solver/MinMaxLinearEquationSolver.h" -#include "src/parser/FormulaParser.h" - -TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); - ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::getModule().getPrecision()); -} - -TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(63616ull, mdp->getNumberOfStates()); - ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index ea1d839f0..000000000 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,88 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/GmmxxEquationSolverSettings.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" -#include "src/settings/SettingMemento.h" -#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/utility/solver.h" -#include "src/parser/AutoParser.h" -#include "src/parser/FormulaParser.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/solver/NativeLinearEquationSolver.h" - -TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); - ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolverFactory())); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.22968140721646868, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.22742305378217331, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} - - -TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = abstractModel->as>(); - - ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); - ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - - storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolverFactory())); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0252174454896057, quantitativeResult3[0], storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index 0b62a805a..000000000 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,143 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/settings/SettingsManager.h" -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" - -#include "src/settings/modules/NativeEquationSolverSettings.h" -#include "src/utility/solver.h" -#include "src/parser/AutoParser.h" -#include "src/models/sparse/StandardRewardModel.h" - -#include "src/parser/FormulaParser.h" - -TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); - ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::getModule().getPrecision()); -} - -TEST(SparseMdpPrctlModelCheckerTest, Consensus) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); - - ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> mdp = abstractModel->as>(); - - ASSERT_EQ(63616ull, mdp->getNumberOfStates()); - ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); - - std::unique_ptr result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"]"); - - result = checker.check(*formula); - storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); - - EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp deleted file mode 100644 index 22c6532a8..000000000 --- a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,210 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/parser/FormulaParser.h" -#include "src/logic/Formulas.h" -#include "src/utility/solver.h" -#include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" -#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "src/parser/PrismParser.h" -#include "src/builder/DdPrismModelBuilder.h" -#include "src/models/symbolic/StandardRewardModel.h" -#include "src/models/symbolic/Dtmc.h" -#include "src/settings/SettingsManager.h" - -#include "src/settings/modules/NativeEquationSolverSettings.h" - -#include "src/settings/modules/GeneralSettings.h" - -TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5_8.pm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(131521ul, model->getNumberOfStates()); - EXPECT_EQ(164288ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5_8.pm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("num_rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(131521ul, model->getNumberOfStates()); - EXPECT_EQ(164288ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/crowds15_5.pm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(586242ul, model->getNumberOfStates()); - EXPECT_EQ(1753883ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/crowds15_5.pm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program); - EXPECT_EQ(586242ul, model->getNumberOfStates()); - EXPECT_EQ(1753883ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); - - std::shared_ptr> dtmc = model->as>(); - - storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index 0a706fc58..000000000 --- a/test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,237 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/logic/Formulas.h" -#include "src/utility/solver.h" -#include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" -#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" -#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "src/parser/FormulaParser.h" -#include "src/parser/PrismParser.h" -#include "src/builder/DdPrismModelBuilder.h" -#include "src/models/symbolic/Dtmc.h" -#include "src/models/symbolic/StandardRewardModel.h" -#include "src/settings/SettingsManager.h" - -#include "src/settings/modules/NativeEquationSolverSettings.h" - -#include "src/settings/modules/GeneralSettings.h" - -TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(27299ul, model->getNumberOfStates()); - EXPECT_EQ(74365ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("rounds"); - std::shared_ptr> model = storm::builder::DdPrismModelBuilder().build(program, options); - EXPECT_EQ(27299ul, model->getNumberOfStates()); - EXPECT_EQ(74365ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(5.034920501133386, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(5.034920501133386, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Cudd) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/csma3_2.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser(program); - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("time"); - - storm::builder::DdPrismModelBuilder builder; - std::shared_ptr> model = builder.build(program, options); - storm::prism::Program translatedProgram = builder.getTranslatedProgram(); - - EXPECT_EQ(36850ul, model->getNumberOfStates()); - EXPECT_EQ(55862ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.4349662650631545, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4349662650631545, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ F (min_backoff_after_success < 4) ]"); - formula = formula->substitute(translatedProgram.getConstantsSubstitution()); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(93.624085091252454, quantitativeResult5.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(93.624085091252454, quantitativeResult5.getMax(), storm::settings::getModule().getPrecision()); -} - -TEST(SymbolicMdpPrctlModelCheckerTest, CSMA_Sylvan) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/csma3_2.nm"); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser(program); - - // Build the die model with its reward model. -#ifdef WINDOWS - storm::builder::DdPrismModelBuilder::Options options; -#else - typename storm::builder::DdPrismModelBuilder::Options options; -#endif - options.buildAllRewardModels = false; - options.rewardModelsToBuild.insert("time"); - - storm::builder::DdPrismModelBuilder builder; - std::shared_ptr> model = builder.build(program, options); - storm::prism::Program translatedProgram = builder.getTranslatedProgram(); - - EXPECT_EQ(36850ul, model->getNumberOfStates()); - EXPECT_EQ(55862ul, model->getNumberOfTransitions()); - - ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); - - std::shared_ptr> mdp = model->as>(); - - storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]"); - - std::unique_ptr result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(0.4349666248753522, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4349666248753522, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ F (min_backoff_after_success < 4) ]"); - formula = formula->substitute(translatedProgram.getConstantsSubstitution()); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - - EXPECT_NEAR(1, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]"); - - result = checker.check(*formula); - result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); - storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult(); - - // FIXME: not optimal precision. - EXPECT_NEAR(93.624117712294478, quantitativeResult5.getMin(), 100 * storm::settings::getModule().getPrecision()); - EXPECT_NEAR(93.624117712294478, quantitativeResult5.getMax(), 100 * storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp deleted file mode 100644 index 67809f12c..000000000 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ /dev/null @@ -1,112 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "src/utility/solver.h" -#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" -#include "src/settings/SettingMemento.h" -#include "src/parser/AutoParser.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/parser/FormulaParser.h" - -TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> mdp = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as>(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); - - std::unique_ptr result = checker.check(*formula); - - ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - - ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(6.172433512, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(6.1724344, result->asExplicitQuantitativeCheckResult()[0], storm::settings::getModule().getPrecision()); -} - -TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { - // Increase the maximal number of iterations, because the solver does not converge otherwise. - // This is done in the main cpp unit - - std::shared_ptr> mdp = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as>(); - - // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser formulaParser; - - ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory())); - - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); - - std::unique_ptr result = checker.check(*formula); - - ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(0.4374282832, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(0.5293286369, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(0.10414097, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(1725.593313, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); - - formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"\"]"); - - result = checker.check(*formula); - ASSERT_NEAR(2183.142422, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::getModule().getPrecision()); -} diff --git a/test/performance/storage/BitVectorTest.cpp b/test/performance/storage/BitVectorTest.cpp deleted file mode 100644 index 2aca461b2..000000000 --- a/test/performance/storage/BitVectorTest.cpp +++ /dev/null @@ -1,15 +0,0 @@ -#include "gtest/gtest.h" -#include "src/storage/BitVector.h" - -TEST(BitVectorTest, Iteration) { - storm::storage::BitVector vector(819200, true); - - for (uint_fast64_t i = 0; i < 10000; ++i) { - for (auto bit : vector) { - // The following can never be true, but prevents the compiler from optimizing away the loop. - if (bit == 819200) { - ASSERT_TRUE(false); - } - } - } -} \ No newline at end of file diff --git a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp deleted file mode 100644 index afa61fab8..000000000 --- a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp +++ /dev/null @@ -1,28 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/AutoParser.h" -#include "src/storage/MaximalEndComponentDecomposition.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/StandardRewardModel.h" - -TEST(MaximalEndComponentDecomposition, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); - - storm::storage::MaximalEndComponentDecomposition mecDecomposition; - ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); - - ASSERT_EQ(7ul, mecDecomposition.size()); - mdp = nullptr; -} - -TEST(MaximalEndComponentDecomposition, Consensus) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); - - storm::storage::MaximalEndComponentDecomposition mecDecomposition; - ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); - - ASSERT_EQ(384ul, mecDecomposition.size()); - mdp = nullptr; -} diff --git a/test/performance/storage/SparseMatrixTest.cpp b/test/performance/storage/SparseMatrixTest.cpp deleted file mode 100644 index dbeedb05a..000000000 --- a/test/performance/storage/SparseMatrixTest.cpp +++ /dev/null @@ -1,96 +0,0 @@ -#include "gtest/gtest.h" -#include "src/utility/constants.h" -#include "src/storage/SparseMatrix.h" - -TEST(SparseMatrix, Iteration) { - storm::storage::SparseMatrixBuilder matrixBuilder; - for (uint_fast64_t row = 0; row < 10000; ++row) { - for (uint_fast64_t column = 0; column < row; ++column) { - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, row+column)); - } - } - - storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix = matrixBuilder.build()); - - for (uint_fast64_t row = 0; row < matrix.getRowCount(); ++row) { - for (auto const& entry : matrix.getRow(row)) { - // The following can never be true, but prevents the compiler from optimizing away the loop. - if (entry.getColumn() > matrix.getColumnCount()) { - ASSERT_TRUE(false); - } - } - } -} - -TEST(SparseMatrix, SparseMultiplication) { - storm::storage::SparseMatrixBuilder matrixBuilder; - for (uint_fast64_t row = 0; row < 100000; ++row) { - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 0, storm::utility::one())); - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 1, storm::utility::one())); - } - - storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix = matrixBuilder.build()); - - std::vector x(matrix.getColumnCount(), 1.0); - std::vector result(matrix.getRowCount()); - - for (uint_fast64_t i = 0; i < 30000; ++i) { - matrix.multiplyWithVector(x, result); - - // The following can never be true, but prevents the compiler from optimizing away the loop. - if (result.size() > matrix.getRowCount()) { - ASSERT_TRUE(false); - } - } -} - -TEST(SparseMatrix, HalfSparseMultiplication) { - storm::storage::SparseMatrixBuilder matrixBuilder; - for (uint_fast64_t row = 0; row < 2000; ++row) { - for (uint_fast64_t column = 0; column < row; ++column) { - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, row+column)); - } - } - - storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix = matrixBuilder.build()); - - std::vector x(matrix.getColumnCount(), 1.0); - std::vector result(matrix.getRowCount()); - - for (uint_fast64_t i = 0; i < 5000; ++i) { - matrix.multiplyWithVector(x, result); - - // The following can never be true, but prevents the compiler from optimizing away the loop. - if (result.size() > matrix.getRowCount()) { - ASSERT_TRUE(false); - } - } -} - -TEST(SparseMatrix, DenseMultiplication) { - storm::storage::SparseMatrixBuilder matrixBuilder; - uint_fast64_t const size = 2000; - for (uint_fast64_t row = 0; row < size; ++row) { - for (uint_fast64_t column = 0; column < size; ++column) { - ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, storm::utility::one())); - } - } - - storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix = matrixBuilder.build()); - - std::vector x(matrix.getColumnCount(), 1.0); - std::vector result(matrix.getRowCount()); - - for (uint_fast64_t i = 0; i < 1000; ++i) { - matrix.multiplyWithVector(x, result); - - // The following can never be true, but prevents the compiler from optimizing away the loop. - if (result.size() > matrix.getRowCount()) { - ASSERT_TRUE(false); - } - } -} \ No newline at end of file diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp deleted file mode 100644 index 259dae563..000000000 --- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp +++ /dev/null @@ -1,79 +0,0 @@ -#include "gtest/gtest.h" -#include "storm-config.h" -#include "src/parser/AutoParser.h" -#include "src/storage/StronglyConnectedComponentDecomposition.h" -#include "src/models/sparse/Mdp.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/StandardRewardModel.h" - -TEST(StronglyConnectedComponentDecomposition, Crowds) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); - std::shared_ptr> dtmc = abstractModel->as>(); - - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc)); - ASSERT_EQ(1290297ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true)); - ASSERT_EQ(437690ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, true)); - ASSERT_EQ(425040ul, sccDecomposition.size()); - - dtmc = nullptr; -} - -TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.lab", "", ""); - std::shared_ptr> dtmc = abstractModel->as>(); - - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc)); - ASSERT_EQ(2611835ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true)); - ASSERT_EQ(2ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, true)); - ASSERT_EQ(1ul, sccDecomposition.size()); - - dtmc = nullptr; -} - -TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); - - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); - ASSERT_EQ(1461930ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); - ASSERT_EQ(127ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true, true)); - ASSERT_EQ(7ul, sccDecomposition.size()); - - mdp = nullptr; -} - -TEST(StronglyConnectedComponentDecomposition, Consensus) { - std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); - - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); - ASSERT_EQ(121251ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); - ASSERT_EQ(1049ul, sccDecomposition.size()); - - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true, true)); - ASSERT_EQ(384ul, sccDecomposition.size()); - - mdp = nullptr; -} diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp deleted file mode 100644 index 4c198c3d6..000000000 --- a/test/performance/storm-performance-tests.cpp +++ /dev/null @@ -1,16 +0,0 @@ -#include - -#include "gtest/gtest.h" -#include "storm-config.h" - -#include "src/settings/SettingsManager.h" - -int main(int argc, char* argv[]) { - storm::settings::initializeAll("StoRM (Performance) Testing Suite", "storm-performance-tests"); - std::cout << "StoRM (Performance) Testing Suite" << std::endl; - - testing::InitGoogleTest(&argc, argv); - - int result = RUN_ALL_TESTS(); - return result; -}