sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

By performance tests, you served us well but we do not love you any longer 

Former-commit-id: 048c3447cb9c6d11d091148403bfd2da08fed0bf
tempestpy_adaptions
sjunges 9 years ago
parent
d8d8f70f0c
commit
4999cfa8a0
18 changed files with 1 additions and 1755 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      test/CMakeLists.txt
  2. 95
      test/performance/builder/crowds15_5.pm
  3. 132
      test/performance/builder/csma3_2.nm
  4. 97
      test/performance/builder/leader5.nm
  5. 89
      test/performance/builder/leader5_8.pm
  6. 79
      test/performance/graph/GraphTest.cpp
  7. 88
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  8. 142
      test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  9. 88
      test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  10. 143
      test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  11. 210
      test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
  12. 237
      test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
  13. 112
      test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
  14. 15
      test/performance/storage/BitVectorTest.cpp
  15. 28
      test/performance/storage/MaximalEndComponentDecompositionTest.cpp
  16. 96
      test/performance/storage/SparseMatrixTest.cpp
  17. 79
      test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
  18. 16
      test/performance/storm-performance-tests.cpp

10
test/CMakeLists.txt
View File

@ -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

95
test/performance/builder/crowds15_5.pm
View File

@ -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<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
// decide whether crowd member is good or bad according to given probabilities
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
// if the current member is a good member, update the last seen index (chosen uniformly)
[] phase=2 & good -> 1/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;

132
test/performance/builder/csma3_2.nm
View File

@ -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<sigma) -> (b'=2);
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
[send3] (b=1|b=2) & (y1<sigma) -> (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<sigma) -> (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<lambda) -> (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<slot) -> (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);

97
test/performance/builder/leader5.nm
View File

@ -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<N-1) -> (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<N-1) -> (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;

89
test/performance/builder/leader5_8.pm
View File

@ -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<N-1 -> (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<N-1 -> (u1'=(p1!=v2)) & (v1'=v2);
[read] s1=1 & !u1 & c<N-1 -> (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;

79
test/performance/graph/GraphTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
storm::storage::BitVector trueStates(dtmc->getNumberOfStates(), true);
std::pair<storm::storage::BitVector, storm::storage::BitVector> 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<storm::models::sparse::Dtmc<double>> dtmc2 = abstractModel->as<storm::models::sparse::Dtmc<double>>();
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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::storage::BitVector trueStates(mdp->getNumberOfStates(), true);
std::pair<storm::storage::BitVector, storm::storage::BitVector> 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<storm::models::sparse::Mdp<double>> mdp2 = abstractModel->as<storm::models::sparse::Mdp<double>>();
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;
}

88
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::GmmxxLinearEquationSolverFactory<double>()));
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.2296800237, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.22742171078, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}
TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::GmmxxLinearEquationSolverFactory<double>()));
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.025106273, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}

142
test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}

88
test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::NativeLinearEquationSolverFactory<double>()));
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.22968140721646868, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.22742305378217331, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}
TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::NativeLinearEquationSolverFactory<double>()));
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0252174454896057, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
}

143
test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}

210
test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options);
EXPECT_EQ(131521ul, model->getNumberOfStates());
EXPECT_EQ(164288ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options);
EXPECT_EQ(131521ul, model->getNumberOfStates());
EXPECT_EQ(164288ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
EXPECT_EQ(586242ul, model->getNumberOfStates());
EXPECT_EQ(1753883ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
EXPECT_EQ(586242ul, model->getNumberOfStates());
EXPECT_EQ(1753883ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}

237
test/performance/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options);
EXPECT_EQ(27299ul, model->getNumberOfStates());
EXPECT_EQ(74365ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(5.0348834996352601, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options);
EXPECT_EQ(27299ul, model->getNumberOfStates());
EXPECT_EQ(74365ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(5.034920501133386, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(5.034920501133386, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("time");
storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> 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<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.4349662650631545, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.4349662650631545, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(1, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(93.624085091252454, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(93.624085091252454, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("time");
storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> 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<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [ !\"collision_max_backoff\" U \"all_delivered\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.4349666248753522, quantitativeResult1.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.4349666248753522, quantitativeResult1.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().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<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1, quantitativeResult3.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1, quantitativeResult3.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [ F \"all_delivered\" ]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
// FIXME: not optimal precision.
EXPECT_NEAR(93.624117712294478, quantitativeResult5.getMin(), 100 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(93.624117712294478, quantitativeResult5.getMax(), 100 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}

112
test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Mdp<double>> 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<storm::models::sparse::Mdp<double>>();
// 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<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(6.172433512, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
ASSERT_NEAR(6.1724344, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().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<storm::models::sparse::Mdp<double>> 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<storm::models::sparse::Mdp<double>>();
// 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<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.4374282832, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.5293286369, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.10414097, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]");
result = checker.check(*formula);
ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]");
result = checker.check(*formula);
ASSERT_NEAR(1725.593313, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"\"]");
result = checker.check(*formula);
ASSERT_NEAR(2183.142422, result->asExplicitQuantitativeCheckResult<double>()[31168], storm::settings::getModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>().getPrecision());
}

15
test/performance/storage/BitVectorTest.cpp
View File

@ -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);
}
}
}
}

28
test/performance/storage/MaximalEndComponentDecompositionTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*mdp));
ASSERT_EQ(7ul, mecDecomposition.size());
mdp = nullptr;
}
TEST(MaximalEndComponentDecomposition, Consensus) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*mdp));
ASSERT_EQ(384ul, mecDecomposition.size());
mdp = nullptr;
}

96
test/performance/storage/SparseMatrixTest.cpp
View File

@ -1,96 +0,0 @@
#include "gtest/gtest.h"
#include "src/utility/constants.h"
#include "src/storage/SparseMatrix.h"
TEST(SparseMatrix, Iteration) {
storm::storage::SparseMatrixBuilder<double> 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<double> 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<double> matrixBuilder;
for (uint_fast64_t row = 0; row < 100000; ++row) {
ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 0, storm::utility::one<double>()));
ASSERT_NO_THROW(matrixBuilder.addNextValue(row, 1, storm::utility::one<double>()));
}
storm::storage::SparseMatrix<double> matrix;
ASSERT_NO_THROW(matrix = matrixBuilder.build());
std::vector<double> x(matrix.getColumnCount(), 1.0);
std::vector<double> 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<double> 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<double> matrix;
ASSERT_NO_THROW(matrix = matrixBuilder.build());
std::vector<double> x(matrix.getColumnCount(), 1.0);
std::vector<double> 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<double> 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<double>()));
}
}
storm::storage::SparseMatrix<double> matrix;
ASSERT_NO_THROW(matrix = matrixBuilder.build());
std::vector<double> x(matrix.getColumnCount(), 1.0);
std::vector<double> 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);
}
}
}

79
test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
ASSERT_EQ(1290297ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true));
ASSERT_EQ(437690ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, true));
ASSERT_EQ(425040ul, sccDecomposition.size());
dtmc = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
ASSERT_EQ(2611835ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true));
ASSERT_EQ(2ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc, true, true));
ASSERT_EQ(1ul, sccDecomposition.size());
dtmc = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
ASSERT_EQ(1461930ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
ASSERT_EQ(127ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true, true));
ASSERT_EQ(7ul, sccDecomposition.size());
mdp = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, Consensus) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
ASSERT_EQ(121251ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true));
ASSERT_EQ(1049ul, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp, true, true));
ASSERT_EQ(384ul, sccDecomposition.size());
mdp = nullptr;
}

16
test/performance/storm-performance-tests.cpp
View File

@ -1,16 +0,0 @@
#include <iostream>
#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;
}
Write Preview
Loading…
Cancel
Save