From 662909926098c1784c5cf20a6271c63152f84d93 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 18 Nov 2016 15:38:23 +0100
Subject: [PATCH] Added testfiles for stormpy

---
 .../examples/testfiles/dtmc/crowds5_5.pm      |  69 +++
 resources/examples/testfiles/dtmc/die.lab     |  10 +
 resources/examples/testfiles/dtmc/die.pm      |  32 ++
 resources/examples/testfiles/dtmc/die.tra     |  21 +
 resources/examples/testfiles/mdp/two_dice.lab |  40 ++
 resources/examples/testfiles/mdp/two_dice.tra | 437 ++++++++++++++++++
 resources/examples/testfiles/pdtmc/brp16_2.pm | 137 ++++++
 .../examples/testfiles/pdtmc/crowds3_5.pm     | 194 ++++++++
 stormpy/tests/core/test_bisimulation.py       |   4 +-
 stormpy/tests/core/test_modelchecking.py      |   6 +-
 stormpy/tests/core/test_parse.py              |   6 +-
 stormpy/tests/helpers/helper.py               |   2 +-
 stormpy/tests/storage/test_matrix.py          |   8 +-
 stormpy/tests/storage/test_model.py           |  16 +-
 stormpy/tests/storage/test_model_iterators.py |  14 +-
 15 files changed, 968 insertions(+), 28 deletions(-)
 create mode 100644 resources/examples/testfiles/dtmc/crowds5_5.pm
 create mode 100644 resources/examples/testfiles/dtmc/die.lab
 create mode 100644 resources/examples/testfiles/dtmc/die.pm
 create mode 100644 resources/examples/testfiles/dtmc/die.tra
 create mode 100644 resources/examples/testfiles/mdp/two_dice.lab
 create mode 100644 resources/examples/testfiles/mdp/two_dice.tra
 create mode 100644 resources/examples/testfiles/pdtmc/brp16_2.pm
 create mode 100644 resources/examples/testfiles/pdtmc/crowds3_5.pm

diff --git a/resources/examples/testfiles/dtmc/crowds5_5.pm b/resources/examples/testfiles/dtmc/crowds5_5.pm
new file mode 100644
index 000000000..be995c528
--- /dev/null
+++ b/resources/examples/testfiles/dtmc/crowds5_5.pm
@@ -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;
diff --git a/resources/examples/testfiles/dtmc/die.lab b/resources/examples/testfiles/dtmc/die.lab
new file mode 100644
index 000000000..452adfb14
--- /dev/null
+++ b/resources/examples/testfiles/dtmc/die.lab
@@ -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
diff --git a/resources/examples/testfiles/dtmc/die.pm b/resources/examples/testfiles/dtmc/die.pm
new file mode 100644
index 000000000..c5634bf4f
--- /dev/null
+++ b/resources/examples/testfiles/dtmc/die.pm
@@ -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;
diff --git a/resources/examples/testfiles/dtmc/die.tra b/resources/examples/testfiles/dtmc/die.tra
new file mode 100644
index 000000000..78fdeb62d
--- /dev/null
+++ b/resources/examples/testfiles/dtmc/die.tra
@@ -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
diff --git a/resources/examples/testfiles/mdp/two_dice.lab b/resources/examples/testfiles/mdp/two_dice.lab
new file mode 100644
index 000000000..8261e69d5
--- /dev/null
+++ b/resources/examples/testfiles/mdp/two_dice.lab
@@ -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
diff --git a/resources/examples/testfiles/mdp/two_dice.tra b/resources/examples/testfiles/mdp/two_dice.tra
new file mode 100644
index 000000000..a0dffa091
--- /dev/null
+++ b/resources/examples/testfiles/mdp/two_dice.tra
@@ -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 
diff --git a/resources/examples/testfiles/pdtmc/brp16_2.pm b/resources/examples/testfiles/pdtmc/brp16_2.pm
new file mode 100644
index 000000000..0fc99d05e
--- /dev/null
+++ b/resources/examples/testfiles/pdtmc/brp16_2.pm
@@ -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;
diff --git a/resources/examples/testfiles/pdtmc/crowds3_5.pm b/resources/examples/testfiles/pdtmc/crowds3_5.pm
new file mode 100644
index 000000000..f9eaf9f75
--- /dev/null
+++ b/resources/examples/testfiles/pdtmc/crowds3_5.pm
@@ -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;
diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py
index 017436584..3776f54d2 100644
--- a/stormpy/tests/core/test_bisimulation.py
+++ b/stormpy/tests/core/test_bisimulation.py
@@ -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
diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py
index 503788a26..56ccdc93e 100644
--- a/stormpy/tests/core/test_modelchecking.py
+++ b/stormpy/tests/core/test_modelchecking.py
@@ -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)
diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py
index e9a18a0b9..83aff42e1 100644
--- a/stormpy/tests/core/test_parse.py
+++ b/stormpy/tests/core/test_parse.py
@@ -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
diff --git a/stormpy/tests/helpers/helper.py b/stormpy/tests/helpers/helper.py
index d07b6ef0f..a7c2d295c 100644
--- a/stormpy/tests/helpers/helper.py
+++ b/stormpy/tests/helpers/helper.py
@@ -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)
diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py
index 0f13fbf9d..e6e2e6360 100644
--- a/stormpy/tests/storage/test_matrix.py
+++ b/stormpy/tests/storage/test_matrix.py
@@ -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
diff --git a/stormpy/tests/storage/test_model.py b/stormpy/tests/storage/test_model.py
index 823c0c506..44a4c9c0e 100644
--- a/stormpy/tests/storage/test_model.py
+++ b/stormpy/tests/storage/test_model.py
@@ -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
diff --git a/stormpy/tests/storage/test_model_iterators.py b/stormpy/tests/storage/test_model_iterators.py
index 52a76736a..8023b86d0 100644
--- a/stormpy/tests/storage/test_model_iterators.py
+++ b/stormpy/tests/storage/test_model_iterators.py
@@ -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):