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

Added testfiles for stormpy

tempestpy_adaptions
Matthias Volk 8 years ago
parent
200c23b00a
commit
6629099260
15 changed files with 968 additions and 28 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. 69
      resources/examples/testfiles/dtmc/crowds5_5.pm
  2. 10
      resources/examples/testfiles/dtmc/die.lab
  3. 32
      resources/examples/testfiles/dtmc/die.pm
  4. 21
      resources/examples/testfiles/dtmc/die.tra
  5. 40
      resources/examples/testfiles/mdp/two_dice.lab
  6. 437
      resources/examples/testfiles/mdp/two_dice.tra
  7. 137
      resources/examples/testfiles/pdtmc/brp16_2.pm
  8. 194
      resources/examples/testfiles/pdtmc/crowds3_5.pm
  9. 4
      stormpy/tests/core/test_bisimulation.py
  10. 6
      stormpy/tests/core/test_modelchecking.py
  11. 6
      stormpy/tests/core/test_parse.py
  12. 2
      stormpy/tests/helpers/helper.py
  13. 8
      stormpy/tests/storage/test_matrix.py
  14. 16
      stormpy/tests/storage/test_model.py
  15. 14
      stormpy/tests/storage/test_model_iterators.py

69
resources/examples/testfiles/dtmc/crowds5_5.pm
View File

@ -0,0 +1,69 @@
dtmc
// probability of forwarding
const double PF = 4/5;
const double notPF = 1/5; // must be 1-PF
// probability that a crowd member is bad
const double badC = 167/1000;
// probability that a crowd member is good
const double goodC = 833/1000;
// Total number of protocol runs to analyze
const int TotalRuns = 5;
// size of the crowd
const int CrowdSize = 5;
module crowds
// protocol phase
phase: [0..4] init 0;
// crowd member good (or bad)
good: bool init false;
// number of protocol runs
runCount: [0..TotalRuns] init 0;
// observe_i is the number of times the attacker observed crowd member i
observe0: [0..TotalRuns] init 0;
observe1: [0..TotalRuns] init 0;
observe2: [0..TotalRuns] init 0;
observe3: [0..TotalRuns] init 0;
observe4: [0..TotalRuns] init 0;
// the last seen crowd member
lastSeen: [0..CrowdSize - 1] init 0;
// get the protocol started
[] phase=0 & runCount<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/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3);
// if the current member is a bad member, record the most recently seen index
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4);
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4);
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4);
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4);
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4);
// good crowd members forward with probability PF and deliver otherwise
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4);
// deliver the message and start over
[] phase=4 -> 1: (phase'=0);
endmodule
label "observe0Greater1" = observe0>1;
label "observe1Greater1" = observe1>1;
label "observe2Greater1" = observe2>1;
label "observe3Greater1" = observe3>1;
label "observe4Greater1" = observe4>1;
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1;
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1;

10
resources/examples/testfiles/dtmc/die.lab
View File

@ -0,0 +1,10 @@
#DECLARATION
init deadlock one two three four five six done
#END
0 init
7 one done
8 two done
9 three done
10 four done
11 five done
12 six done

32
resources/examples/testfiles/dtmc/die.pm
View File

@ -0,0 +1,32 @@
// Knuth's model of a fair die using only fair coins
dtmc
module die
// local state
s : [0..7] init 0;
// value of the dice
d : [0..6] init 0;
[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
[] s=7 -> 1: (s'=7);
endmodule
rewards "coin_flips"
[] s<7 : 1;
endrewards
label "one" = s=7&d=1;
label "two" = s=7&d=2;
label "three" = s=7&d=3;
label "four" = s=7&d=4;
label "five" = s=7&d=5;
label "six" = s=7&d=6;
label "end" = s=7;

21
resources/examples/testfiles/dtmc/die.tra
View File

@ -0,0 +1,21 @@
dtmc
0 1 0.5
0 2 0.5
1 3 0.5
1 4 0.5
2 5 0.5
2 6 0.5
3 1 0.5
3 7 0.5
4 8 0.5
4 9 0.5
5 10 0.5
5 11 0.5
6 2 0.5
6 12 0.5
7 7 1
8 8 1
9 9 1
10 10 1
11 11 1
12 12 1

40
resources/examples/testfiles/mdp/two_dice.lab
View File

@ -0,0 +1,40 @@
#DECLARATION
init deadlock done two three four five six seven eight nine ten eleven twelve
#END
0 init
98 done two
99 done three
100 done four
101 done five
102 done six
103 done seven
111 done three
112 done four
113 done five
114 done six
115 done seven
116 done eight
124 done four
125 done five
126 done six
127 done seven
128 done eight
129 done nine
137 done five
138 done six
139 done seven
140 done eight
141 done nine
142 done ten
150 done six
151 done seven
152 done eight
153 done nine
154 done ten
155 done eleven
163 done seven
164 done eight
165 done nine
166 done ten
167 done eleven
168 done twelve

437
resources/examples/testfiles/mdp/two_dice.tra
View File

@ -0,0 +1,437 @@
mdp
0 0 13 0.5
0 0 26 0.5
0 1 1 0.5
0 1 2 0.5
1 0 14 0.5
1 0 27 0.5
1 1 3 0.5
1 1 4 0.5
2 0 15 0.5
2 0 28 0.5
2 1 5 0.5
2 1 6 0.5
3 0 16 0.5
3 0 29 0.5
3 1 1 0.5
3 1 7 0.5
4 0 17 0.5
4 0 30 0.5
4 1 8 0.5
4 1 9 0.5
5 0 18 0.5
5 0 31 0.5
5 1 10 0.5
5 1 11 0.5
6 0 19 0.5
6 0 32 0.5
6 1 2 0.5
6 1 12 0.5
7 0 20 0.5
7 0 33 0.5
8 0 21 0.5
8 0 34 0.5
9 0 22 0.5
9 0 35 0.5
10 0 23 0.5
10 0 36 0.5
11 0 24 0.5
11 0 37 0.5
12 0 25 0.5
12 0 38 0.5
13 0 39 0.5
13 0 52 0.5
13 1 14 0.5
13 1 15 0.5
14 0 40 0.5
14 0 53 0.5
14 1 16 0.5
14 1 17 0.5
15 0 41 0.5
15 0 54 0.5
15 1 18 0.5
15 1 19 0.5
16 0 42 0.5
16 0 55 0.5
16 1 14 0.5
16 1 20 0.5
17 0 43 0.5
17 0 56 0.5
17 1 21 0.5
17 1 22 0.5
18 0 44 0.5
18 0 57 0.5
18 1 23 0.5
18 1 24 0.5
19 0 45 0.5
19 0 58 0.5
19 1 15 0.5
19 1 25 0.5
20 0 46 0.5
20 0 59 0.5
21 0 47 0.5
21 0 60 0.5
22 0 48 0.5
22 0 61 0.5
23 0 49 0.5
23 0 62 0.5
24 0 50 0.5
24 0 63 0.5
25 0 51 0.5
25 0 64 0.5
26 0 65 0.5
26 0 78 0.5
26 1 27 0.5
26 1 28 0.5
27 0 66 0.5
27 0 79 0.5
27 1 29 0.5
27 1 30 0.5
28 0 67 0.5
28 0 80 0.5
28 1 31 0.5
28 1 32 0.5
29 0 68 0.5
29 0 81 0.5
29 1 27 0.5
29 1 33 0.5
30 0 69 0.5
30 0 82 0.5
30 1 34 0.5
30 1 35 0.5
31 0 70 0.5
31 0 83 0.5
31 1 36 0.5
31 1 37 0.5
32 0 71 0.5
32 0 84 0.5
32 1 28 0.5
32 1 38 0.5
33 0 72 0.5
33 0 85 0.5
34 0 73 0.5
34 0 86 0.5
35 0 74 0.5
35 0 87 0.5
36 0 75 0.5
36 0 88 0.5
37 0 76 0.5
37 0 89 0.5
38 0 77 0.5
38 0 90 0.5
39 0 13 0.5
39 0 91 0.5
39 1 40 0.5
39 1 41 0.5
40 0 14 0.5
40 0 92 0.5
40 1 42 0.5
40 1 43 0.5
41 0 15 0.5
41 0 93 0.5
41 1 44 0.5
41 1 45 0.5
42 0 16 0.5
42 0 94 0.5
42 1 40 0.5
42 1 46 0.5
43 0 17 0.5
43 0 95 0.5
43 1 47 0.5
43 1 48 0.5
44 0 18 0.5
44 0 96 0.5
44 1 49 0.5
44 1 50 0.5
45 0 19 0.5
45 0 97 0.5
45 1 41 0.5
45 1 51 0.5
46 0 20 0.5
46 0 98 0.5
47 0 21 0.5
47 0 99 0.5
48 0 22 0.5
48 0 100 0.5
49 0 23 0.5
49 0 101 0.5
50 0 24 0.5
50 0 102 0.5
51 0 25 0.5
51 0 103 0.5
52 0 104 0.5
52 0 117 0.5
52 1 53 0.5
52 1 54 0.5
53 0 105 0.5
53 0 118 0.5
53 1 55 0.5
53 1 56 0.5
54 0 106 0.5
54 0 119 0.5
54 1 57 0.5
54 1 58 0.5
55 0 107 0.5
55 0 120 0.5
55 1 53 0.5
55 1 59 0.5
56 0 108 0.5
56 0 121 0.5
56 1 60 0.5
56 1 61 0.5
57 0 109 0.5
57 0 122 0.5
57 1 62 0.5
57 1 63 0.5
58 0 110 0.5
58 0 123 0.5
58 1 54 0.5
58 1 64 0.5
59 0 111 0.5
59 0 124 0.5
60 0 112 0.5
60 0 125 0.5
61 0 113 0.5
61 0 126 0.5
62 0 114 0.5
62 0 127 0.5
63 0 115 0.5
63 0 128 0.5
64 0 116 0.5
64 0 129 0.5
65 0 130 0.5
65 0 143 0.5
65 1 66 0.5
65 1 67 0.5
66 0 131 0.5
66 0 144 0.5
66 1 68 0.5
66 1 69 0.5
67 0 132 0.5
67 0 145 0.5
67 1 70 0.5
67 1 71 0.5
68 0 133 0.5
68 0 146 0.5
68 1 66 0.5
68 1 72 0.5
69 0 134 0.5
69 0 147 0.5
69 1 73 0.5
69 1 74 0.5
70 0 135 0.5
70 0 148 0.5
70 1 75 0.5
70 1 76 0.5
71 0 136 0.5
71 0 149 0.5
71 1 67 0.5
71 1 77 0.5
72 0 137 0.5
72 0 150 0.5
73 0 138 0.5
73 0 151 0.5
74 0 139 0.5
74 0 152 0.5
75 0 140 0.5
75 0 153 0.5
76 0 141 0.5
76 0 154 0.5
77 0 142 0.5
77 0 155 0.5
78 0 26 0.5
78 0 156 0.5
78 1 79 0.5
78 1 80 0.5
79 0 27 0.5
79 0 157 0.5
79 1 81 0.5
79 1 82 0.5
80 0 28 0.5
80 0 158 0.5
80 1 83 0.5
80 1 84 0.5
81 0 29 0.5
81 0 159 0.5
81 1 79 0.5
81 1 85 0.5
82 0 30 0.5
82 0 160 0.5
82 1 86 0.5
82 1 87 0.5
83 0 31 0.5
83 0 161 0.5
83 1 88 0.5
83 1 89 0.5
84 0 32 0.5
84 0 162 0.5
84 1 80 0.5
84 1 90 0.5
85 0 33 0.5
85 0 163 0.5
86 0 34 0.5
86 0 164 0.5
87 0 35 0.5
87 0 165 0.5
88 0 36 0.5
88 0 166 0.5
89 0 37 0.5
89 0 167 0.5
90 0 38 0.5
90 0 168 0.5
91 0 92 0.5
91 0 93 0.5
92 0 94 0.5
92 0 95 0.5
93 0 96 0.5
93 0 97 0.5
94 0 92 0.5
94 0 98 0.5
95 0 99 0.5
95 0 100 0.5
96 0 101 0.5
96 0 102 0.5
97 0 93 0.5
97 0 103 0.5
98 0 98 1
98 1 98 1
99 0 99 1
99 1 99 1
100 0 100 1
100 1 100 1
101 0 101 1
101 1 101 1
102 0 102 1
102 1 102 1
103 0 103 1
103 1 103 1
104 0 105 0.5
104 0 106 0.5
105 0 107 0.5
105 0 108 0.5
106 0 109 0.5
106 0 110 0.5
107 0 105 0.5
107 0 111 0.5
108 0 112 0.5
108 0 113 0.5
109 0 114 0.5
109 0 115 0.5
110 0 106 0.5
110 0 116 0.5
111 0 111 1
111 1 111 1
112 0 112 1
112 1 112 1
113 0 113 1
113 1 113 1
114 0 114 1
114 1 114 1
115 0 115 1
115 1 115 1
116 0 116 1
116 1 116 1
117 0 118 0.5
117 0 119 0.5
118 0 120 0.5
118 0 121 0.5
119 0 122 0.5
119 0 123 0.5
120 0 118 0.5
120 0 124 0.5
121 0 125 0.5
121 0 126 0.5
122 0 127 0.5
122 0 128 0.5
123 0 119 0.5
123 0 129 0.5
124 0 124 1
124 1 124 1
125 0 125 1
125 1 125 1
126 0 126 1
126 1 126 1
127 0 127 1
127 1 127 1
128 0 128 1
128 1 128 1
129 0 129 1
129 1 129 1
130 0 131 0.5
130 0 132 0.5
131 0 133 0.5
131 0 134 0.5
132 0 135 0.5
132 0 136 0.5
133 0 131 0.5
133 0 137 0.5
134 0 138 0.5
134 0 139 0.5
135 0 140 0.5
135 0 141 0.5
136 0 132 0.5
136 0 142 0.5
137 0 137 1
137 1 137 1
138 0 138 1
138 1 138 1
139 0 139 1
139 1 139 1
140 0 140 1
140 1 140 1
141 0 141 1
141 1 141 1
142 0 142 1
142 1 142 1
143 0 144 0.5
143 0 145 0.5
144 0 146 0.5
144 0 147 0.5
145 0 148 0.5
145 0 149 0.5
146 0 144 0.5
146 0 150 0.5
147 0 151 0.5
147 0 152 0.5
148 0 153 0.5
148 0 154 0.5
149 0 145 0.5
149 0 155 0.5
150 0 150 1
150 1 150 1
151 0 151 1
151 1 151 1
152 0 152 1
152 1 152 1
153 0 153 1
153 1 153 1
154 0 154 1
154 1 154 1
155 0 155 1
155 1 155 1
156 0 157 0.5
156 0 158 0.5
157 0 159 0.5
157 0 160 0.5
158 0 161 0.5
158 0 162 0.5
159 0 157 0.5
159 0 163 0.5
160 0 164 0.5
160 0 165 0.5
161 0 166 0.5
161 0 167 0.5
162 0 158 0.5
162 0 168 0.5
163 0 163 1
163 1 163 1
164 0 164 1
164 1 164 1
165 0 165 1
165 1 165 1
166 0 166 1
166 1 166 1
167 0 167 1
167 1 167 1
168 0 168 1
168 1 168 1

137
resources/examples/testfiles/pdtmc/brp16_2.pm
View File

@ -0,0 +1,137 @@
// bounded retransmission protocol [D'AJJL01]
// gxn/dxp 23/05/2001
dtmc
// number of chunks
const int N = 16;
// maximum number of retransmissions
const int MAX = 2;
// reliability of channels
const double pL;
const double pK;
module sender
s : [0..6];
// 0 idle
// 1 next_frame
// 2 wait_ack
// 3 retransmit
// 4 success
// 5 error
// 6 wait sync
srep : [0..3];
// 0 bottom
// 1 not ok (nok)
// 2 do not know (dk)
// 3 ok (ok)
nrtr : [0..MAX];
i : [0..N];
bs : bool;
s_ab : bool;
fs : bool;
ls : bool;
// idle
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
// next_frame
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
// wait_ack
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
[TO_Msg] (s=2) -> (s'=3);
[TO_Ack] (s=2) -> (s'=3);
// retransmit
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
// error
[SyncWait] (s=5) -> (s'=6);
// wait sync
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
endmodule
module receiver
r : [0..5];
// 0 new_file
// 1 fst_safe
// 2 frame_received
// 3 frame_reported
// 4 idle
// 5 resync
rrep : [0..4];
// 0 bottom
// 1 fst
// 2 inc
// 3 ok
// 4 nok
fr : bool;
lr : bool;
br : bool;
r_ab : bool;
recv : bool;
// new_file
[SyncWait] (r=0) -> (r'=0);
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
// fst_safe_frame
[] (r=1) -> (r'=2) & (r_ab'=br);
// frame_received
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
[aA] (r=2) & !(r_ab=br) -> (r'=4);
// frame_reported
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
// idle
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
[SyncWait] (r=4) & (ls=true) -> (r'=5);
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
// resync
[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
endmodule
// prevents more than one file being sent
module tester
T : bool;
[NewFile] (T=false) -> (T'=true);
endmodule
module channelK
k : [0..2];
// idle
[aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2);
// sending
[aG] (k=1) -> (k'=0);
// lost
[TO_Msg] (k=2) -> (k'=0);
endmodule
module channelL
l : [0..2];
// idle
[aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2);
// sending
[aB] (l=1) -> (l'=0);
// lost
[TO_Ack] (l=2) -> (l'=0);
endmodule
label "error" = s=5;

194
resources/examples/testfiles/pdtmc/crowds3_5.pm
View File

@ -0,0 +1,194 @@
// CROWDS [Reiter,Rubin]
// Vitaly Shmatikov, 2002
// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de)
// note:
// Change everything marked CWDSIZ when changing the size of the crowd
// Change everything marked CWDMAX when increasing max size of the crowd
dtmc
// Model parameters
const double PF; // forwarding probability
const double badC; // probability that member is untrustworthy
// 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.1;
// const double badC = 0.091;
// const double badC = 0.167;
// const double goodC = 0.909; // must be 1-badC
// const double goodC = 0.833; // must be 1-badC
const int CrowdSize = 3; // CWDSIZ: actual number of good crowd members
const int TotalRuns = 5; // Total number of protocol runs to analyze
const int MaxGood=20; // CWDMAX: maximum number of good crowd members
// Process definitions
module crowds
// Auxiliary variables
launch: bool init true; // Start modeling?
newInstance: bool init false; // Initialize a new protocol instance?
runCount: [0..TotalRuns] init TotalRuns; // Counts protocol instances
start: bool init false; // Start the protocol?
run: bool init false; // Run the protocol?
lastSeen: [0..MaxGood] init 0; // Last crowd member to touch msg
good: bool init false; // Crowd member is good?
bad: bool init false; // ... bad?
recordLast: bool init false; // Record last seen crowd member?
badObserve: bool init false; // Bad members observes who sent msg?
deliver: bool init false; // Deliver message to destination?
done: bool init false; // Protocol instance finished?
// Counters for attackers' observations
// CWDMAX: 1 counter per each good crowd member
observe0: [0..TotalRuns];
observe1: [0..TotalRuns];
observe2: [0..TotalRuns];
observe3: [0..TotalRuns];
observe4: [0..TotalRuns];
observe5: [0..TotalRuns];
observe6: [0..TotalRuns];
observe7: [0..TotalRuns];
observe8: [0..TotalRuns];
observe9: [0..TotalRuns];
observe10: [0..TotalRuns];
observe11: [0..TotalRuns];
observe12: [0..TotalRuns];
observe13: [0..TotalRuns];
observe14: [0..TotalRuns];
observe15: [0..TotalRuns];
observe16: [0..TotalRuns];
observe17: [0..TotalRuns];
observe18: [0..TotalRuns];
observe19: [0..TotalRuns];
[] launch -> (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false);
// Set up a newInstance protocol instance
[] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true);
// SENDER
// Start the protocol
[] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false);
// CROWD MEMBERS
// Good or bad crowd member?
[] !good & !bad & !deliver & run ->
1-badC : (good'=true) & (recordLast'=true) & (run'=false) +
badC : (bad'=true) & (badObserve'=true) & (run'=false);
// GOOD MEMBERS
// Forward with probability PF, else deliver
[] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true);
// Record the last crowd member who touched the msg;
// all good members may appear with equal probability
// Note: This is backward. In the real protocol, each honest
// forwarder randomly chooses the next forwarder.
// Here, the identity of an honest forwarder is randomly
// chosen *after* it has forwarded the message.
[] recordLast & CrowdSize=2 ->
1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=3 ->
1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=4 ->
1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=5 ->
1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=10 ->
1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=15 ->
1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true);
[] recordLast & CrowdSize=20 ->
1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) +
1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true);
// BAD MEMBERS
// Remember from whom the message was received and deliver
// CWDMAX: 1 rule per each good crowd member
[] lastSeen=0 & badObserve & observe0 <TotalRuns -> (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=1 & badObserve & observe1 <TotalRuns -> (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=2 & badObserve & observe2 <TotalRuns -> (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=3 & badObserve & observe3 <TotalRuns -> (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=4 & badObserve & observe4 <TotalRuns -> (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=5 & badObserve & observe5 <TotalRuns -> (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=6 & badObserve & observe6 <TotalRuns -> (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=7 & badObserve & observe7 <TotalRuns -> (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=8 & badObserve & observe8 <TotalRuns -> (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=9 & badObserve & observe9 <TotalRuns -> (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=10 & badObserve & observe10<TotalRuns -> (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=11 & badObserve & observe11<TotalRuns -> (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=12 & badObserve & observe12<TotalRuns -> (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=13 & badObserve & observe13<TotalRuns -> (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=14 & badObserve & observe14<TotalRuns -> (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=15 & badObserve & observe15<TotalRuns -> (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=16 & badObserve & observe16<TotalRuns -> (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=17 & badObserve & observe17<TotalRuns -> (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=18 & badObserve & observe18<TotalRuns -> (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
[] lastSeen=19 & badObserve & observe19<TotalRuns -> (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
// RECIPIENT
// Delivery to destination
[] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false);
// Start a newInstance instance
[] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood);
endmodule
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1>1|observe2>1;
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1;

4
stormpy/tests/core/test_bisimulation.py
View File

@ -4,7 +4,7 @@ from helpers.helper import get_example_path
class TestBisimulation:
def test_bisimulation(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds", "crowds5_5.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm"))
assert program.nr_modules == 1
assert program.model_type == stormpy.PrismModelType.DTMC
prop = "P=? [F \"observe0Greater1\"]"
@ -21,7 +21,7 @@ class TestBisimulation:
assert not model_bisim.supports_parameters
def test_parametric_bisimulation(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds", "crowds3_5.pm"))
program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm"))
assert program.nr_modules == 1
assert program.model_type == stormpy.PrismModelType.DTMC
assert program.has_undefined_constants

6
stormpy/tests/core/test_modelchecking.py
View File

@ -4,7 +4,7 @@ from helpers.helper import get_example_path
class TestModelChecking:
def test_model_checking_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
assert model.nr_states == 13
@ -13,7 +13,7 @@ class TestModelChecking:
assert result == 0.16666666666666663
def test_model_checking_all_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
assert model.nr_states == 13
@ -25,7 +25,7 @@ class TestModelChecking:
def test_parametric_state_elimination(self):
import pycarl
import pycarl.formula
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm"))
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
prop = "P=? [F s=5]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program)
model = stormpy.build_parametric_model_from_prism_program(program, formulas)

6
stormpy/tests/core/test_parse.py
View File

@ -4,7 +4,7 @@ from helpers.helper import get_example_path
class TestParse:
def test_parse_prism_program(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
assert program.nr_modules == 1
assert program.model_type == stormpy.PrismModelType.DTMC
assert not program.has_undefined_constants
@ -16,7 +16,7 @@ class TestParse:
assert str(formulas[0]) == prop
def test_parse_explicit_dtmc(self):
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
assert model.nr_states == 13
assert model.nr_transitions == 20
assert model.model_type == stormpy.ModelType.DTMC
@ -24,7 +24,7 @@ class TestParse:
assert type(model) is stormpy.SparseDtmc
def test_parse_explicit_mdp(self):
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
assert model.nr_states == 169
assert model.nr_transitions == 436
assert model.model_type == stormpy.ModelType.MDP

2
stormpy/tests/helpers/helper.py
View File

@ -1,5 +1,5 @@
import os
example_dir = os.path.abspath(os.path.join(os.path.dirname(__file__), os.pardir, os.pardir, os.pardir, "examples"))
example_dir = os.path.abspath(os.path.join(os.path.dirname(__file__), os.pardir, os.pardir, os.pardir, "resources", "examples", "testfiles"))
def get_example_path(*paths):
return os.path.join(example_dir, *paths)

8
stormpy/tests/storage/test_matrix.py
View File

@ -3,7 +3,7 @@ from helpers.helper import get_example_path
class TestMatrix:
def test_sparse_matrix(self):
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
matrix = model.transition_matrix
assert type(matrix) is stormpy.storage.SparseMatrix
assert matrix.nr_rows == model.nr_states
@ -13,7 +13,7 @@ class TestMatrix:
assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6)
def test_change_sparse_matrix(self):
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
matrix = model.transition_matrix
for e in matrix:
assert e.value() == 0.5 or e.value() == 0 or e.value() == 1
@ -28,7 +28,7 @@ class TestMatrix:
def test_change_sparse_matrix_modelchecking(self):
import stormpy.logic
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
matrix = model.transition_matrix
# Check matrix
for e in matrix:
@ -68,7 +68,7 @@ class TestMatrix:
def test_change_parametric_sparse_matrix_modelchecking(self):
import stormpy.logic
import pycarl
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm"))
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
matrix = model.transition_matrix

16
stormpy/tests/storage/test_model.py
View File

@ -4,7 +4,7 @@ from helpers.helper import get_example_path
class TestModel:
def test_build_dtmc_from_prism_program(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
prop = "P=? [F \"one\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program)
model = stormpy.build_model_from_prism_program(program, formulas)
@ -15,7 +15,7 @@ class TestModel:
assert type(model) is stormpy.SparseDtmc
def test_build_parametric_dtmc_from_prism_program(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm"))
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
assert program.nr_modules == 5
assert program.model_type == stormpy.PrismModelType.DTMC
assert program.has_undefined_constants
@ -30,7 +30,7 @@ class TestModel:
assert type(model) is stormpy.SparseParametricDtmc
def test_build_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
assert model.nr_states == 13
@ -40,7 +40,7 @@ class TestModel:
assert type(model) is stormpy.SparseDtmc
def test_build_parametric_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm"))
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
assert model.nr_states == 613
@ -51,7 +51,7 @@ class TestModel:
assert type(model) is stormpy.SparseParametricDtmc
def test_build_dtmc_supporting_parameters(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
assert model.nr_states == 13
@ -62,7 +62,7 @@ class TestModel:
assert type(model) is stormpy.SparseParametricDtmc
def test_label(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
labels = model.labels
@ -73,7 +73,7 @@ class TestModel:
assert "one" in model.labels_state(7)
def test_initial_states(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
initial_states = model.initial_states
@ -81,7 +81,7 @@ class TestModel:
assert 0 in initial_states
def test_label_parametric(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm"))
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
labels = model.labels

14
stormpy/tests/storage/test_model_iterators.py
View File

@ -3,7 +3,7 @@ from helpers.helper import get_example_path
class TestModelIterators:
def test_states_dtmc(self):
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
s = stormpy.state.State(0, model)
i = 0
for state in stormpy.state.State(0, model):
@ -12,7 +12,7 @@ class TestModelIterators:
assert i == model.nr_states
def test_states_mdp(self):
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
s = stormpy.state.State(0, model)
i = 0
for state in stormpy.state.State(0, model):
@ -21,14 +21,14 @@ class TestModelIterators:
assert i == model.nr_states
def test_actions_dtmc(self):
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
s = stormpy.state.State(0, model)
for state in stormpy.state.State(0, model):
for action in state.actions():
assert action.row == 0
def test_actions_mdp(self):
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
s = stormpy.state.State(0, model)
for state in stormpy.state.State(0, model):
for action in state.actions():
@ -41,7 +41,7 @@ class TestModelIterators:
(6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1),
(9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
]
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
s = stormpy.state.State(0, model)
i = 0
for state in stormpy.state.State(0, model):
@ -54,7 +54,7 @@ class TestModelIterators:
assert transition.value() == transition_orig[2]
def test_transitions_mdp(self):
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
s = stormpy.state.State(0, model)
for state in stormpy.state.State(0, model):
i = 0
@ -71,7 +71,7 @@ class TestModelIterators:
(6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1),
(9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
]
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
i = 0
for state in stormpy.state.State(0, model):
for transition in model.transition_matrix.row_iter(state.id, state.id):

Write Preview
Loading…
Cancel
Save