From 0cdd32ff9fac6091fa69dcf1294fdb9224e60dd5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 30 May 2017 17:00:07 +0200 Subject: [PATCH] added two test cases for the drn parser --- .../examples/testfiles/ctmc/cluster2.drn | 1680 +++++++++++++++++ resources/examples/testfiles/mdp/two_dice.drn | 867 +++++++++ src/test/parser/DirectEncodingParserTest.cpp | 38 + 3 files changed, 2585 insertions(+) create mode 100644 resources/examples/testfiles/ctmc/cluster2.drn create mode 100644 resources/examples/testfiles/mdp/two_dice.drn create mode 100644 src/test/parser/DirectEncodingParserTest.cpp diff --git a/resources/examples/testfiles/ctmc/cluster2.drn b/resources/examples/testfiles/ctmc/cluster2.drn new file mode 100644 index 000000000..a58875e50 --- /dev/null +++ b/resources/examples/testfiles/ctmc/cluster2.drn @@ -0,0 +1,1680 @@ +// Exported by storm +// Original model type: CTMC +@type: CTMC +@parameters + +@nr_states +276 +@model +state 0 [0] init minimum premium + action 0 [0] + 1 : 0.004 + 2 : 0.004 + 3 : 0.0002 + 4 : 0.00025 + 5 : 0.00025 +state 1 [0] minimum premium + action 0 [0] + 6 : 0.002 + 7 : 0.004 + 8 : 0.0002 + 9 : 0.00025 + 10 : 0.00025 + 11 : 10 +state 2 [0] minimum premium + action 0 [0] + 7 : 0.004 + 12 : 0.002 + 13 : 0.0002 + 14 : 0.00025 + 15 : 0.00025 + 16 : 10 +state 3 [0] minimum premium + action 0 [0] + 8 : 0.004 + 13 : 0.004 + 17 : 0.00025 + 18 : 0.00025 + 19 : 10 +state 4 [0] minimum premium + action 0 [0] + 9 : 0.004 + 14 : 0.004 + 17 : 0.0002 + 20 : 0.00025 + 21 : 10 +state 5 [0] minimum premium + action 0 [0] + 10 : 0.004 + 15 : 0.004 + 18 : 0.0002 + 20 : 0.00025 + 22 : 10 +state 6 [0] minimum premium + action 0 [0] + 23 : 0.004 + 24 : 0.0002 + 25 : 0.00025 + 26 : 0.00025 + 27 : 10 +state 7 [0] minimum premium + action 0 [0] + 23 : 0.002 + 28 : 0.002 + 29 : 0.0002 + 30 : 0.00025 + 31 : 0.00025 + 32 : 10 + 33 : 10 +state 8 [0] minimum premium + action 0 [0] + 24 : 0.002 + 29 : 0.004 + 34 : 0.00025 + 35 : 0.00025 + 36 : 10 + 37 : 10 +state 9 [0] minimum premium + action 0 [0] + 25 : 0.002 + 30 : 0.004 + 34 : 0.0002 + 38 : 0.00025 + 39 : 10 + 40 : 10 +state 10 [0] minimum + action 0 [0] + 26 : 0.002 + 31 : 0.004 + 35 : 0.0002 + 38 : 0.00025 + 41 : 10 + 42 : 10 +state 11 [0] minimum premium + action 0 [0.996661] + 0 : 2 + 27 : 0.002 + 32 : 0.004 + 36 : 0.0002 + 39 : 0.00025 + 41 : 0.00025 +state 12 [0] minimum premium + action 0 [0] + 28 : 0.004 + 43 : 0.0002 + 44 : 0.00025 + 45 : 0.00025 + 46 : 10 +state 13 [0] minimum premium + action 0 [0] + 29 : 0.004 + 43 : 0.002 + 47 : 0.00025 + 48 : 0.00025 + 49 : 10 + 50 : 10 +state 14 [0] minimum + action 0 [0] + 30 : 0.004 + 44 : 0.002 + 47 : 0.0002 + 51 : 0.00025 + 52 : 10 + 53 : 10 +state 15 [0] minimum premium + action 0 [0] + 31 : 0.004 + 45 : 0.002 + 48 : 0.0002 + 51 : 0.00025 + 54 : 10 + 55 : 10 +state 16 [0] minimum premium + action 0 [0.996661] + 0 : 2 + 33 : 0.004 + 46 : 0.002 + 49 : 0.0002 + 52 : 0.00025 + 54 : 0.00025 +state 17 [0] minimum premium + action 0 [0] + 34 : 0.004 + 47 : 0.004 + 56 : 0.00025 + 57 : 10 + 58 : 10 +state 18 [0] minimum premium + action 0 [0] + 35 : 0.004 + 48 : 0.004 + 56 : 0.00025 + 59 : 10 + 60 : 10 +state 19 [0] minimum premium + action 0 [0.93633] + 0 : 0.125 + 37 : 0.004 + 50 : 0.004 + 58 : 0.00025 + 60 : 0.00025 +state 20 [0] + action 0 [0] + 38 : 0.004 + 51 : 0.004 + 56 : 0.0002 + 61 : 10 + 62 : 10 +state 21 [0] minimum premium + action 0 [0.967305] + 0 : 0.25 + 40 : 0.004 + 53 : 0.004 + 57 : 0.0002 + 61 : 0.00025 +state 22 [0] minimum premium + action 0 [0.967305] + 0 : 0.25 + 42 : 0.004 + 55 : 0.004 + 59 : 0.0002 + 62 : 0.00025 +state 23 [0] minimum + action 0 [0] + 63 : 0.002 + 64 : 0.0002 + 65 : 0.00025 + 66 : 0.00025 + 67 : 10 + 68 : 10 +state 24 [0] minimum premium + action 0 [0] + 64 : 0.004 + 69 : 0.00025 + 70 : 0.00025 + 71 : 10 + 72 : 10 +state 25 [0] minimum premium + action 0 [0] + 65 : 0.004 + 69 : 0.0002 + 73 : 0.00025 + 74 : 10 + 75 : 10 +state 26 [0] + action 0 [0] + 66 : 0.004 + 70 : 0.0002 + 73 : 0.00025 + 76 : 10 + 77 : 10 +state 27 [0] minimum premium + action 0 [0.997656] + 1 : 2 + 67 : 0.004 + 71 : 0.0002 + 74 : 0.00025 + 76 : 0.00025 +state 28 [0] minimum + action 0 [0] + 63 : 0.002 + 78 : 0.0002 + 79 : 0.00025 + 80 : 0.00025 + 81 : 10 + 82 : 10 +state 29 [0] minimum + action 0 [0] + 64 : 0.002 + 78 : 0.002 + 83 : 0.00025 + 84 : 0.00025 + 85 : 10 + 86 : 10 + 87 : 10 +state 30 [0] minimum + action 0 [0] + 65 : 0.002 + 79 : 0.002 + 83 : 0.0002 + 88 : 0.00025 + 89 : 10 + 90 : 10 + 91 : 10 +state 31 [0] minimum + action 0 [0] + 66 : 0.002 + 80 : 0.002 + 84 : 0.0002 + 88 : 0.00025 + 92 : 10 + 93 : 10 + 94 : 10 +state 32 [0] minimum premium + action 0 [0.997656] + 2 : 2 + 67 : 0.002 + 81 : 0.002 + 85 : 0.0002 + 89 : 0.00025 + 92 : 0.00025 +state 33 [0] minimum premium + action 0 [0.997656] + 1 : 2 + 68 : 0.002 + 82 : 0.002 + 86 : 0.0002 + 90 : 0.00025 + 93 : 0.00025 +state 34 [0] minimum premium + action 0 [0] + 69 : 0.002 + 83 : 0.004 + 95 : 0.00025 + 96 : 10 + 97 : 10 + 98 : 10 +state 35 [0] minimum + action 0 [0] + 70 : 0.002 + 84 : 0.004 + 95 : 0.00025 + 99 : 10 + 100 : 10 + 101 : 10 +state 36 [0] minimum premium + action 0 [0.996761] + 3 : 2 + 71 : 0.002 + 85 : 0.004 + 96 : 0.00025 + 99 : 0.00025 +state 37 [0] minimum premium + action 0 [0.95057] + 1 : 0.125 + 72 : 0.002 + 87 : 0.004 + 98 : 0.00025 + 101 : 0.00025 +state 38 [0] + action 0 [0] + 73 : 0.002 + 88 : 0.004 + 95 : 0.0002 + 102 : 10 + 103 : 10 + 104 : 10 +state 39 [0] minimum premium + action 0 [0.996785] + 4 : 2 + 74 : 0.002 + 89 : 0.004 + 96 : 0.0002 + 102 : 0.00025 +state 40 [0] minimum premium + action 0 [0.974849] + 1 : 0.25 + 75 : 0.002 + 91 : 0.004 + 97 : 0.0002 + 103 : 0.00025 +state 41 [0] minimum + action 0 [0.996785] + 5 : 2 + 76 : 0.002 + 92 : 0.004 + 99 : 0.0002 + 102 : 0.00025 +state 42 [0] minimum + action 0 [0.974849] + 1 : 0.25 + 77 : 0.002 + 94 : 0.004 + 100 : 0.0002 + 104 : 0.00025 +state 43 [0] minimum premium + action 0 [0] + 78 : 0.004 + 105 : 0.00025 + 106 : 0.00025 + 107 : 10 + 108 : 10 +state 44 [0] + action 0 [0] + 79 : 0.004 + 105 : 0.0002 + 109 : 0.00025 + 110 : 10 + 111 : 10 +state 45 [0] minimum premium + action 0 [0] + 80 : 0.004 + 106 : 0.0002 + 109 : 0.00025 + 112 : 10 + 113 : 10 +state 46 [0] minimum premium + action 0 [0.997656] + 2 : 2 + 82 : 0.004 + 107 : 0.0002 + 110 : 0.00025 + 112 : 0.00025 +state 47 [0] minimum + action 0 [0] + 83 : 0.004 + 105 : 0.002 + 114 : 0.00025 + 115 : 10 + 116 : 10 + 117 : 10 +state 48 [0] minimum premium + action 0 [0] + 84 : 0.004 + 106 : 0.002 + 114 : 0.00025 + 118 : 10 + 119 : 10 + 120 : 10 +state 49 [0] minimum premium + action 0 [0.996761] + 3 : 2 + 86 : 0.004 + 107 : 0.002 + 115 : 0.00025 + 118 : 0.00025 +state 50 [0] minimum premium + action 0 [0.95057] + 2 : 0.125 + 87 : 0.004 + 108 : 0.002 + 117 : 0.00025 + 120 : 0.00025 +state 51 [0] + action 0 [0] + 88 : 0.004 + 109 : 0.002 + 114 : 0.0002 + 121 : 10 + 122 : 10 + 123 : 10 +state 52 [0] minimum + action 0 [0.996785] + 4 : 2 + 90 : 0.004 + 110 : 0.002 + 115 : 0.0002 + 121 : 0.00025 +state 53 [0] minimum + action 0 [0.974849] + 2 : 0.25 + 91 : 0.004 + 111 : 0.002 + 116 : 0.0002 + 122 : 0.00025 +state 54 [0] minimum premium + action 0 [0.996785] + 5 : 2 + 93 : 0.004 + 112 : 0.002 + 118 : 0.0002 + 121 : 0.00025 +state 55 [0] minimum premium + action 0 [0.974849] + 2 : 0.25 + 94 : 0.004 + 113 : 0.002 + 119 : 0.0002 + 123 : 0.00025 +state 56 [0] + action 0 [0] + 95 : 0.004 + 114 : 0.004 + 124 : 10 + 125 : 10 + 126 : 10 +state 57 [0] minimum premium + action 0 [0.968054] + 3 : 0.25 + 97 : 0.004 + 116 : 0.004 + 124 : 0.00025 +state 58 [0] minimum premium + action 0 [0.938086] + 4 : 0.125 + 98 : 0.004 + 117 : 0.004 + 126 : 0.00025 +state 59 [0] minimum premium + action 0 [0.968054] + 3 : 0.25 + 100 : 0.004 + 119 : 0.004 + 125 : 0.00025 +state 60 [0] minimum premium + action 0 [0.938086] + 5 : 0.125 + 101 : 0.004 + 120 : 0.004 + 126 : 0.00025 +state 61 [0] + action 0 [0.968242] + 5 : 0.25 + 103 : 0.004 + 122 : 0.004 + 124 : 0.0002 +state 62 [0] + action 0 [0.968242] + 4 : 0.25 + 104 : 0.004 + 123 : 0.004 + 125 : 0.0002 +state 63 [0] + action 0 [0] + 127 : 0.0002 + 128 : 0.00025 + 129 : 0.00025 + 130 : 10 + 131 : 10 +state 64 [0] minimum + action 0 [0] + 127 : 0.002 + 132 : 0.00025 + 133 : 0.00025 + 134 : 10 + 135 : 10 + 136 : 10 +state 65 [0] minimum + action 0 [0] + 128 : 0.002 + 132 : 0.0002 + 137 : 0.00025 + 138 : 10 + 139 : 10 + 140 : 10 +state 66 [0] + action 0 [0] + 129 : 0.002 + 133 : 0.0002 + 137 : 0.00025 + 141 : 10 + 142 : 10 + 143 : 10 +state 67 [0] minimum + action 0 [0.998652] + 7 : 2 + 130 : 0.002 + 134 : 0.0002 + 138 : 0.00025 + 141 : 0.00025 +state 68 [0] minimum + action 0 [0.998652] + 6 : 2 + 131 : 0.002 + 135 : 0.0002 + 139 : 0.00025 + 142 : 0.00025 +state 69 [0] minimum premium + action 0 [0] + 132 : 0.004 + 144 : 0.00025 + 145 : 10 + 146 : 10 + 147 : 10 +state 70 [0] + action 0 [0] + 133 : 0.004 + 144 : 0.00025 + 148 : 10 + 149 : 10 + 150 : 10 +state 71 [0] minimum premium + action 0 [0.997755] + 8 : 2 + 134 : 0.004 + 145 : 0.00025 + 148 : 0.00025 +state 72 [0] minimum premium + action 0 [0.965251] + 6 : 0.125 + 136 : 0.004 + 147 : 0.00025 + 150 : 0.00025 +state 73 [0] + action 0 [0] + 137 : 0.004 + 144 : 0.0002 + 151 : 10 + 152 : 10 + 153 : 10 +state 74 [0] minimum premium + action 0 [0.99778] + 9 : 2 + 138 : 0.004 + 145 : 0.0002 + 151 : 0.00025 +state 75 [0] minimum premium + action 0 [0.982511] + 6 : 0.25 + 140 : 0.004 + 146 : 0.0002 + 152 : 0.00025 +state 76 [0] + action 0 [0.99778] + 10 : 2 + 141 : 0.004 + 148 : 0.0002 + 151 : 0.00025 +state 77 [0] + action 0 [0.982511] + 6 : 0.25 + 143 : 0.004 + 149 : 0.0002 + 153 : 0.00025 +state 78 [0] minimum + action 0 [0] + 127 : 0.002 + 154 : 0.00025 + 155 : 0.00025 + 156 : 10 + 157 : 10 + 158 : 10 +state 79 [0] + action 0 [0] + 128 : 0.002 + 154 : 0.0002 + 159 : 0.00025 + 160 : 10 + 161 : 10 + 162 : 10 +state 80 [0] minimum + action 0 [0] + 129 : 0.002 + 155 : 0.0002 + 159 : 0.00025 + 163 : 10 + 164 : 10 + 165 : 10 +state 81 [0] minimum + action 0 [0.998652] + 12 : 2 + 130 : 0.002 + 156 : 0.0002 + 160 : 0.00025 + 163 : 0.00025 +state 82 [0] minimum + action 0 [0.998652] + 7 : 2 + 131 : 0.002 + 157 : 0.0002 + 161 : 0.00025 + 164 : 0.00025 +state 83 [0] minimum + action 0 [0] + 132 : 0.002 + 154 : 0.002 + 166 : 0.00025 + 167 : 10 + 168 : 10 + 169 : 10 + 170 : 10 +state 84 [0] minimum + action 0 [0] + 133 : 0.002 + 155 : 0.002 + 166 : 0.00025 + 171 : 10 + 172 : 10 + 173 : 10 + 174 : 10 +state 85 [0] minimum + action 0 [0.997755] + 13 : 2 + 134 : 0.002 + 156 : 0.002 + 167 : 0.00025 + 171 : 0.00025 +state 86 [0] minimum + action 0 [0.997755] + 8 : 2 + 135 : 0.002 + 157 : 0.002 + 168 : 0.00025 + 172 : 0.00025 +state 87 [0] minimum + action 0 [0.965251] + 7 : 0.125 + 136 : 0.002 + 158 : 0.002 + 170 : 0.00025 + 174 : 0.00025 +state 88 [0] + action 0 [0] + 137 : 0.002 + 159 : 0.002 + 166 : 0.0002 + 175 : 10 + 176 : 10 + 177 : 10 + 178 : 10 +state 89 [0] minimum + action 0 [0.99778] + 14 : 2 + 138 : 0.002 + 160 : 0.002 + 167 : 0.0002 + 175 : 0.00025 +state 90 [0] minimum + action 0 [0.99778] + 9 : 2 + 139 : 0.002 + 161 : 0.002 + 168 : 0.0002 + 176 : 0.00025 +state 91 [0] minimum + action 0 [0.982511] + 7 : 0.25 + 140 : 0.002 + 162 : 0.002 + 169 : 0.0002 + 177 : 0.00025 +state 92 [0] minimum + action 0 [0.99778] + 15 : 2 + 141 : 0.002 + 163 : 0.002 + 171 : 0.0002 + 175 : 0.00025 +state 93 [0] minimum + action 0 [0.99778] + 10 : 2 + 142 : 0.002 + 164 : 0.002 + 172 : 0.0002 + 176 : 0.00025 +state 94 [0] minimum + action 0 [0.982511] + 7 : 0.25 + 143 : 0.002 + 165 : 0.002 + 173 : 0.0002 + 178 : 0.00025 +state 95 [0] + action 0 [0] + 144 : 0.002 + 166 : 0.004 + 179 : 10 + 180 : 10 + 181 : 10 + 182 : 10 +state 96 [0] minimum premium + action 0 [0.996885] + 17 : 2 + 145 : 0.002 + 167 : 0.004 + 179 : 0.00025 +state 97 [0] minimum premium + action 0 [0.97561] + 8 : 0.25 + 146 : 0.002 + 169 : 0.004 + 180 : 0.00025 +state 98 [0] minimum premium + action 0 [0.952381] + 9 : 0.125 + 147 : 0.002 + 170 : 0.004 + 182 : 0.00025 +state 99 [0] minimum + action 0 [0.996885] + 18 : 2 + 148 : 0.002 + 171 : 0.004 + 179 : 0.00025 +state 100 [0] minimum + action 0 [0.97561] + 8 : 0.25 + 149 : 0.002 + 173 : 0.004 + 181 : 0.00025 +state 101 [0] minimum + action 0 [0.952381] + 10 : 0.125 + 150 : 0.002 + 174 : 0.004 + 182 : 0.00025 +state 102 [0] + action 0 [0.99691] + 20 : 2 + 151 : 0.002 + 175 : 0.004 + 179 : 0.0002 +state 103 [0] + action 0 [0.9758] + 10 : 0.25 + 152 : 0.002 + 177 : 0.004 + 180 : 0.0002 +state 104 [0] + action 0 [0.9758] + 9 : 0.25 + 153 : 0.002 + 178 : 0.004 + 181 : 0.0002 +state 105 [0] + action 0 [0] + 154 : 0.004 + 183 : 0.00025 + 184 : 10 + 185 : 10 + 186 : 10 +state 106 [0] minimum premium + action 0 [0] + 155 : 0.004 + 183 : 0.00025 + 187 : 10 + 188 : 10 + 189 : 10 +state 107 [0] minimum premium + action 0 [0.997755] + 13 : 2 + 157 : 0.004 + 184 : 0.00025 + 187 : 0.00025 +state 108 [0] minimum premium + action 0 [0.965251] + 12 : 0.125 + 158 : 0.004 + 186 : 0.00025 + 189 : 0.00025 +state 109 [0] + action 0 [0] + 159 : 0.004 + 183 : 0.0002 + 190 : 10 + 191 : 10 + 192 : 10 +state 110 [0] + action 0 [0.99778] + 14 : 2 + 161 : 0.004 + 184 : 0.0002 + 190 : 0.00025 +state 111 [0] + action 0 [0.982511] + 12 : 0.25 + 162 : 0.004 + 185 : 0.0002 + 191 : 0.00025 +state 112 [0] minimum premium + action 0 [0.99778] + 15 : 2 + 164 : 0.004 + 187 : 0.0002 + 190 : 0.00025 +state 113 [0] minimum premium + action 0 [0.982511] + 12 : 0.25 + 165 : 0.004 + 188 : 0.0002 + 192 : 0.00025 +state 114 [0] + action 0 [0] + 166 : 0.004 + 183 : 0.002 + 193 : 10 + 194 : 10 + 195 : 10 + 196 : 10 +state 115 [0] minimum + action 0 [0.996885] + 17 : 2 + 168 : 0.004 + 184 : 0.002 + 193 : 0.00025 +state 116 [0] minimum + action 0 [0.97561] + 13 : 0.25 + 169 : 0.004 + 185 : 0.002 + 194 : 0.00025 +state 117 [0] minimum + action 0 [0.952381] + 14 : 0.125 + 170 : 0.004 + 186 : 0.002 + 196 : 0.00025 +state 118 [0] minimum premium + action 0 [0.996885] + 18 : 2 + 172 : 0.004 + 187 : 0.002 + 193 : 0.00025 +state 119 [0] minimum premium + action 0 [0.97561] + 13 : 0.25 + 173 : 0.004 + 188 : 0.002 + 195 : 0.00025 +state 120 [0] minimum premium + action 0 [0.952381] + 15 : 0.125 + 174 : 0.004 + 189 : 0.002 + 196 : 0.00025 +state 121 [0] + action 0 [0.99691] + 20 : 2 + 176 : 0.004 + 190 : 0.002 + 193 : 0.0002 +state 122 [0] + action 0 [0.9758] + 15 : 0.25 + 177 : 0.004 + 191 : 0.002 + 194 : 0.0002 +state 123 [0] + action 0 [0.9758] + 14 : 0.25 + 178 : 0.004 + 192 : 0.002 + 195 : 0.0002 +state 124 [0] + action 0 [0.968992] + 18 : 0.25 + 180 : 0.004 + 194 : 0.004 +state 125 [0] + action 0 [0.968992] + 17 : 0.25 + 181 : 0.004 + 195 : 0.004 +state 126 [0] + action 0 [0.93985] + 20 : 0.125 + 182 : 0.004 + 196 : 0.004 +state 127 [0] + action 0 [0] + 197 : 0.00025 + 198 : 0.00025 + 199 : 10 + 200 : 10 + 201 : 10 +state 128 [0] + action 0 [0] + 197 : 0.0002 + 202 : 0.00025 + 203 : 10 + 204 : 10 + 205 : 10 +state 129 [0] + action 0 [0] + 198 : 0.0002 + 202 : 0.00025 + 206 : 10 + 207 : 10 + 208 : 10 +state 130 [0] + action 0 [0.99965] + 28 : 2 + 199 : 0.0002 + 203 : 0.00025 + 206 : 0.00025 +state 131 [0] + action 0 [0.99965] + 23 : 2 + 200 : 0.0002 + 204 : 0.00025 + 207 : 0.00025 +state 132 [0] minimum + action 0 [0] + 197 : 0.002 + 209 : 0.00025 + 210 : 10 + 211 : 10 + 212 : 10 + 213 : 10 +state 133 [0] + action 0 [0] + 198 : 0.002 + 209 : 0.00025 + 214 : 10 + 215 : 10 + 216 : 10 + 217 : 10 +state 134 [0] minimum + action 0 [0.998752] + 29 : 2 + 199 : 0.002 + 210 : 0.00025 + 214 : 0.00025 +state 135 [0] minimum + action 0 [0.998752] + 24 : 2 + 200 : 0.002 + 211 : 0.00025 + 215 : 0.00025 +state 136 [0] minimum + action 0 [0.980392] + 23 : 0.125 + 201 : 0.002 + 213 : 0.00025 + 217 : 0.00025 +state 137 [0] + action 0 [0] + 202 : 0.002 + 209 : 0.0002 + 218 : 10 + 219 : 10 + 220 : 10 + 221 : 10 +state 138 [0] minimum + action 0 [0.998776] + 30 : 2 + 203 : 0.002 + 210 : 0.0002 + 218 : 0.00025 +state 139 [0] minimum + action 0 [0.998776] + 25 : 2 + 204 : 0.002 + 211 : 0.0002 + 219 : 0.00025 +state 140 [0] minimum + action 0 [0.990295] + 23 : 0.25 + 205 : 0.002 + 212 : 0.0002 + 220 : 0.00025 +state 141 [0] + action 0 [0.998776] + 31 : 2 + 206 : 0.002 + 214 : 0.0002 + 218 : 0.00025 +state 142 [0] + action 0 [0.998776] + 26 : 2 + 207 : 0.002 + 215 : 0.0002 + 219 : 0.00025 +state 143 [0] + action 0 [0.990295] + 23 : 0.25 + 208 : 0.002 + 216 : 0.0002 + 221 : 0.00025 +state 144 [0] + action 0 [0] + 209 : 0.004 + 222 : 10 + 223 : 10 + 224 : 10 + 225 : 10 +state 145 [0] minimum premium + action 0 [0.99788] + 34 : 2 + 210 : 0.004 + 222 : 0.00025 +state 146 [0] minimum premium + action 0 [0.983284] + 24 : 0.25 + 212 : 0.004 + 223 : 0.00025 +state 147 [0] minimum premium + action 0 [0.967118] + 25 : 0.125 + 213 : 0.004 + 225 : 0.00025 +state 148 [0] + action 0 [0.99788] + 35 : 2 + 214 : 0.004 + 222 : 0.00025 +state 149 [0] + action 0 [0.983284] + 24 : 0.25 + 216 : 0.004 + 224 : 0.00025 +state 150 [0] + action 0 [0.967118] + 26 : 0.125 + 217 : 0.004 + 225 : 0.00025 +state 151 [0] + action 0 [0.997904] + 38 : 2 + 218 : 0.004 + 222 : 0.0002 +state 152 [0] + action 0 [0.983478] + 26 : 0.25 + 220 : 0.004 + 223 : 0.0002 +state 153 [0] + action 0 [0.983478] + 25 : 0.25 + 221 : 0.004 + 224 : 0.0002 +state 154 [0] + action 0 [0] + 197 : 0.002 + 226 : 0.00025 + 227 : 10 + 228 : 10 + 229 : 10 + 230 : 10 +state 155 [0] minimum + action 0 [0] + 198 : 0.002 + 226 : 0.00025 + 231 : 10 + 232 : 10 + 233 : 10 + 234 : 10 +state 156 [0] minimum + action 0 [0.998752] + 43 : 2 + 199 : 0.002 + 227 : 0.00025 + 231 : 0.00025 +state 157 [0] minimum + action 0 [0.998752] + 29 : 2 + 200 : 0.002 + 228 : 0.00025 + 232 : 0.00025 +state 158 [0] minimum + action 0 [0.980392] + 28 : 0.125 + 201 : 0.002 + 230 : 0.00025 + 234 : 0.00025 +state 159 [0] + action 0 [0] + 202 : 0.002 + 226 : 0.0002 + 235 : 10 + 236 : 10 + 237 : 10 + 238 : 10 +state 160 [0] + action 0 [0.998776] + 44 : 2 + 203 : 0.002 + 227 : 0.0002 + 235 : 0.00025 +state 161 [0] + action 0 [0.998776] + 30 : 2 + 204 : 0.002 + 228 : 0.0002 + 236 : 0.00025 +state 162 [0] + action 0 [0.990295] + 28 : 0.25 + 205 : 0.002 + 229 : 0.0002 + 237 : 0.00025 +state 163 [0] minimum + action 0 [0.998776] + 45 : 2 + 206 : 0.002 + 231 : 0.0002 + 235 : 0.00025 +state 164 [0] minimum + action 0 [0.998776] + 31 : 2 + 207 : 0.002 + 232 : 0.0002 + 236 : 0.00025 +state 165 [0] minimum + action 0 [0.990295] + 28 : 0.25 + 208 : 0.002 + 233 : 0.0002 + 238 : 0.00025 +state 166 [0] + action 0 [0] + 209 : 0.002 + 226 : 0.002 + 239 : 10 + 240 : 10 + 241 : 10 + 242 : 10 + 243 : 10 +state 167 [0] minimum + action 0 [0.99788] + 47 : 2 + 210 : 0.002 + 227 : 0.002 + 239 : 0.00025 +state 168 [0] minimum + action 0 [0.99788] + 34 : 2 + 211 : 0.002 + 228 : 0.002 + 240 : 0.00025 +state 169 [0] minimum + action 0 [0.983284] + 29 : 0.25 + 212 : 0.002 + 229 : 0.002 + 241 : 0.00025 +state 170 [0] minimum + action 0 [0.967118] + 30 : 0.125 + 213 : 0.002 + 230 : 0.002 + 243 : 0.00025 +state 171 [0] minimum + action 0 [0.99788] + 48 : 2 + 214 : 0.002 + 231 : 0.002 + 239 : 0.00025 +state 172 [0] minimum + action 0 [0.99788] + 35 : 2 + 215 : 0.002 + 232 : 0.002 + 240 : 0.00025 +state 173 [0] minimum + action 0 [0.983284] + 29 : 0.25 + 216 : 0.002 + 233 : 0.002 + 242 : 0.00025 +state 174 [0] minimum + action 0 [0.967118] + 31 : 0.125 + 217 : 0.002 + 234 : 0.002 + 243 : 0.00025 +state 175 [0] + action 0 [0.997904] + 51 : 2 + 218 : 0.002 + 235 : 0.002 + 239 : 0.0002 +state 176 [0] + action 0 [0.997904] + 38 : 2 + 219 : 0.002 + 236 : 0.002 + 240 : 0.0002 +state 177 [0] + action 0 [0.983478] + 31 : 0.25 + 220 : 0.002 + 237 : 0.002 + 241 : 0.0002 +state 178 [0] + action 0 [0.983478] + 30 : 0.25 + 221 : 0.002 + 238 : 0.002 + 242 : 0.0002 +state 179 [0] + action 0 [0.997009] + 56 : 2 + 222 : 0.002 + 239 : 0.004 +state 180 [0] + action 0 [0.976562] + 35 : 0.25 + 223 : 0.002 + 241 : 0.004 +state 181 [0] + action 0 [0.976562] + 34 : 0.25 + 224 : 0.002 + 242 : 0.004 +state 182 [0] + action 0 [0.954198] + 38 : 0.125 + 225 : 0.002 + 243 : 0.004 +state 183 [0] + action 0 [0] + 226 : 0.004 + 244 : 10 + 245 : 10 + 246 : 10 + 247 : 10 +state 184 [0] + action 0 [0.99788] + 47 : 2 + 228 : 0.004 + 244 : 0.00025 +state 185 [0] + action 0 [0.983284] + 43 : 0.25 + 229 : 0.004 + 245 : 0.00025 +state 186 [0] + action 0 [0.967118] + 44 : 0.125 + 230 : 0.004 + 247 : 0.00025 +state 187 [0] minimum premium + action 0 [0.99788] + 48 : 2 + 232 : 0.004 + 244 : 0.00025 +state 188 [0] minimum premium + action 0 [0.983284] + 43 : 0.25 + 233 : 0.004 + 246 : 0.00025 +state 189 [0] minimum premium + action 0 [0.967118] + 45 : 0.125 + 234 : 0.004 + 247 : 0.00025 +state 190 [0] + action 0 [0.997904] + 51 : 2 + 236 : 0.004 + 244 : 0.0002 +state 191 [0] + action 0 [0.983478] + 45 : 0.25 + 237 : 0.004 + 245 : 0.0002 +state 192 [0] + action 0 [0.983478] + 44 : 0.25 + 238 : 0.004 + 246 : 0.0002 +state 193 [0] + action 0 [0.997009] + 56 : 2 + 240 : 0.004 + 244 : 0.002 +state 194 [0] + action 0 [0.976562] + 48 : 0.25 + 241 : 0.004 + 245 : 0.002 +state 195 [0] + action 0 [0.976562] + 47 : 0.25 + 242 : 0.004 + 246 : 0.002 +state 196 [0] + action 0 [0.954198] + 51 : 0.125 + 243 : 0.004 + 247 : 0.002 +state 197 [0] + action 0 [0] + 248 : 0.00025 + 249 : 10 + 250 : 10 + 251 : 10 + 252 : 10 +state 198 [0] + action 0 [0] + 248 : 0.00025 + 253 : 10 + 254 : 10 + 255 : 10 + 256 : 10 +state 199 [0] + action 0 [0.99975] + 78 : 2 + 249 : 0.00025 + 253 : 0.00025 +state 200 [0] + action 0 [0.99975] + 64 : 2 + 250 : 0.00025 + 254 : 0.00025 +state 201 [0] + action 0 [0.996016] + 63 : 0.125 + 252 : 0.00025 + 256 : 0.00025 +state 202 [0] + action 0 [0] + 248 : 0.0002 + 257 : 10 + 258 : 10 + 259 : 10 + 260 : 10 +state 203 [0] + action 0 [0.999775] + 79 : 2 + 249 : 0.0002 + 257 : 0.00025 +state 204 [0] + action 0 [0.999775] + 65 : 2 + 250 : 0.0002 + 258 : 0.00025 +state 205 [0] + action 0 [0.998203] + 63 : 0.25 + 251 : 0.0002 + 259 : 0.00025 +state 206 [0] + action 0 [0.999775] + 80 : 2 + 253 : 0.0002 + 257 : 0.00025 +state 207 [0] + action 0 [0.999775] + 66 : 2 + 254 : 0.0002 + 258 : 0.00025 +state 208 [0] + action 0 [0.998203] + 63 : 0.25 + 255 : 0.0002 + 260 : 0.00025 +state 209 [0] + action 0 [0] + 248 : 0.002 + 261 : 10 + 262 : 10 + 263 : 10 + 264 : 10 + 265 : 10 +state 210 [0] minimum + action 0 [0.998876] + 83 : 2 + 249 : 0.002 + 261 : 0.00025 +state 211 [0] minimum + action 0 [0.998876] + 69 : 2 + 250 : 0.002 + 262 : 0.00025 +state 212 [0] minimum + action 0 [0.99108] + 64 : 0.25 + 251 : 0.002 + 263 : 0.00025 +state 213 [0] minimum + action 0 [0.982318] + 65 : 0.125 + 252 : 0.002 + 265 : 0.00025 +state 214 [0] + action 0 [0.998876] + 84 : 2 + 253 : 0.002 + 261 : 0.00025 +state 215 [0] + action 0 [0.998876] + 70 : 2 + 254 : 0.002 + 262 : 0.00025 +state 216 [0] + action 0 [0.99108] + 64 : 0.25 + 255 : 0.002 + 264 : 0.00025 +state 217 [0] + action 0 [0.982318] + 66 : 0.125 + 256 : 0.002 + 265 : 0.00025 +state 218 [0] + action 0 [0.998901] + 88 : 2 + 257 : 0.002 + 261 : 0.0002 +state 219 [0] + action 0 [0.998901] + 73 : 2 + 258 : 0.002 + 262 : 0.0002 +state 220 [0] + action 0 [0.991277] + 66 : 0.25 + 259 : 0.002 + 263 : 0.0002 +state 221 [0] + action 0 [0.991277] + 65 : 0.25 + 260 : 0.002 + 264 : 0.0002 +state 222 [0] + action 0 [0.998004] + 95 : 2 + 261 : 0.004 +state 223 [0] + action 0 [0.984252] + 70 : 0.25 + 263 : 0.004 +state 224 [0] + action 0 [0.984252] + 69 : 0.25 + 264 : 0.004 +state 225 [0] + action 0 [0.968992] + 73 : 0.125 + 265 : 0.004 +state 226 [0] + action 0 [0] + 248 : 0.002 + 266 : 10 + 267 : 10 + 268 : 10 + 269 : 10 + 270 : 10 +state 227 [0] + action 0 [0.998876] + 105 : 2 + 249 : 0.002 + 266 : 0.00025 +state 228 [0] + action 0 [0.998876] + 83 : 2 + 250 : 0.002 + 267 : 0.00025 +state 229 [0] + action 0 [0.99108] + 78 : 0.25 + 251 : 0.002 + 268 : 0.00025 +state 230 [0] + action 0 [0.982318] + 79 : 0.125 + 252 : 0.002 + 270 : 0.00025 +state 231 [0] minimum + action 0 [0.998876] + 106 : 2 + 253 : 0.002 + 266 : 0.00025 +state 232 [0] minimum + action 0 [0.998876] + 84 : 2 + 254 : 0.002 + 267 : 0.00025 +state 233 [0] minimum + action 0 [0.99108] + 78 : 0.25 + 255 : 0.002 + 269 : 0.00025 +state 234 [0] minimum + action 0 [0.982318] + 80 : 0.125 + 256 : 0.002 + 270 : 0.00025 +state 235 [0] + action 0 [0.998901] + 109 : 2 + 257 : 0.002 + 266 : 0.0002 +state 236 [0] + action 0 [0.998901] + 88 : 2 + 258 : 0.002 + 267 : 0.0002 +state 237 [0] + action 0 [0.991277] + 80 : 0.25 + 259 : 0.002 + 268 : 0.0002 +state 238 [0] + action 0 [0.991277] + 79 : 0.25 + 260 : 0.002 + 269 : 0.0002 +state 239 [0] + action 0 [0.998004] + 114 : 2 + 261 : 0.002 + 266 : 0.002 +state 240 [0] + action 0 [0.998004] + 95 : 2 + 262 : 0.002 + 267 : 0.002 +state 241 [0] + action 0 [0.984252] + 84 : 0.25 + 263 : 0.002 + 268 : 0.002 +state 242 [0] + action 0 [0.984252] + 83 : 0.25 + 264 : 0.002 + 269 : 0.002 +state 243 [0] + action 0 [0.968992] + 88 : 0.125 + 265 : 0.002 + 270 : 0.002 +state 244 [0] + action 0 [0.998004] + 114 : 2 + 267 : 0.004 +state 245 [0] + action 0 [0.984252] + 106 : 0.25 + 268 : 0.004 +state 246 [0] + action 0 [0.984252] + 105 : 0.25 + 269 : 0.004 +state 247 [0] + action 0 [0.968992] + 109 : 0.125 + 270 : 0.004 +state 248 [0] + action 0 [0] + 271 : 10 + 272 : 10 + 273 : 10 + 274 : 10 + 275 : 10 +state 249 [0] + action 0 [0.999875] + 154 : 2 + 271 : 0.00025 +state 250 [0] + action 0 [0.999875] + 132 : 2 + 272 : 0.00025 +state 251 [0] + action 0 [0.999001] + 127 : 0.25 + 273 : 0.00025 +state 252 [0] + action 0 [0.998004] + 128 : 0.125 + 275 : 0.00025 +state 253 [0] + action 0 [0.999875] + 155 : 2 + 271 : 0.00025 +state 254 [0] + action 0 [0.999875] + 133 : 2 + 272 : 0.00025 +state 255 [0] + action 0 [0.999001] + 127 : 0.25 + 274 : 0.00025 +state 256 [0] + action 0 [0.998004] + 129 : 0.125 + 275 : 0.00025 +state 257 [0] + action 0 [0.9999] + 159 : 2 + 271 : 0.0002 +state 258 [0] + action 0 [0.9999] + 137 : 2 + 272 : 0.0002 +state 259 [0] + action 0 [0.999201] + 129 : 0.25 + 273 : 0.0002 +state 260 [0] + action 0 [0.999201] + 128 : 0.25 + 274 : 0.0002 +state 261 [0] + action 0 [0.999001] + 166 : 2 + 271 : 0.002 +state 262 [0] + action 0 [0.999001] + 144 : 2 + 272 : 0.002 +state 263 [0] + action 0 [0.992063] + 133 : 0.25 + 273 : 0.002 +state 264 [0] + action 0 [0.992063] + 132 : 0.25 + 274 : 0.002 +state 265 [0] + action 0 [0.984252] + 137 : 0.125 + 275 : 0.002 +state 266 [0] + action 0 [0.999001] + 183 : 2 + 271 : 0.002 +state 267 [0] + action 0 [0.999001] + 166 : 2 + 272 : 0.002 +state 268 [0] + action 0 [0.992063] + 155 : 0.25 + 273 : 0.002 +state 269 [0] + action 0 [0.992063] + 154 : 0.25 + 274 : 0.002 +state 270 [0] + action 0 [0.984252] + 159 : 0.125 + 275 : 0.002 +state 271 [0] + action 0 [1] + 226 : 2 +state 272 [0] + action 0 [1] + 209 : 2 +state 273 [0] + action 0 [1] + 198 : 0.25 +state 274 [0] + action 0 [1] + 197 : 0.25 +state 275 [0] + action 0 [1] + 202 : 0.125 diff --git a/resources/examples/testfiles/mdp/two_dice.drn b/resources/examples/testfiles/mdp/two_dice.drn new file mode 100644 index 000000000..74d13d03b --- /dev/null +++ b/resources/examples/testfiles/mdp/two_dice.drn @@ -0,0 +1,867 @@ +// Exported by storm +// Original model type: MDP +@type: MDP +@parameters + +@nr_states +169 +@model +state 0 [0] init + action 0 [1] + 1 : 0.5 + 2 : 0.5 + action 1 [1] + 3 : 0.5 + 4 : 0.5 +state 1 [0] + action 0 [1] + 5 : 0.5 + 6 : 0.5 + action 1 [1] + 7 : 0.5 + 8 : 0.5 +state 2 [0] + action 0 [1] + 9 : 0.5 + 10 : 0.5 + action 1 [1] + 11 : 0.5 + 12 : 0.5 +state 3 [0] + action 0 [1] + 7 : 0.5 + 11 : 0.5 + action 1 [1] + 13 : 0.5 + 14 : 0.5 +state 4 [0] + action 0 [1] + 8 : 0.5 + 12 : 0.5 + action 1 [1] + 15 : 0.5 + 16 : 0.5 +state 5 [0] + action 0 [1] + 1 : 0.5 + 17 : 0.5 + action 1 [1] + 18 : 0.5 + 19 : 0.5 +state 6 [0] + action 0 [1] + 20 : 0.5 + 21 : 0.5 + action 1 [1] + 22 : 0.5 + 23 : 0.5 +state 7 [0] + action 0 [1] + 18 : 0.5 + 22 : 0.5 + action 1 [1] + 24 : 0.5 + 25 : 0.5 +state 8 [0] + action 0 [1] + 19 : 0.5 + 23 : 0.5 + action 1 [1] + 26 : 0.5 + 27 : 0.5 +state 9 [0] + action 0 [1] + 28 : 0.5 + 29 : 0.5 + action 1 [1] + 30 : 0.5 + 31 : 0.5 +state 10 [0] + action 0 [1] + 2 : 0.5 + 32 : 0.5 + action 1 [1] + 33 : 0.5 + 34 : 0.5 +state 11 [0] + action 0 [1] + 30 : 0.5 + 33 : 0.5 + action 1 [1] + 35 : 0.5 + 36 : 0.5 +state 12 [0] + action 0 [1] + 31 : 0.5 + 34 : 0.5 + action 1 [1] + 37 : 0.5 + 38 : 0.5 +state 13 [0] + action 0 [1] + 24 : 0.5 + 35 : 0.5 + action 1 [1] + 3 : 0.5 + 39 : 0.5 +state 14 [0] + action 0 [1] + 25 : 0.5 + 36 : 0.5 + action 1 [1] + 40 : 0.5 + 41 : 0.5 +state 15 [0] + action 0 [1] + 26 : 0.5 + 37 : 0.5 + action 1 [1] + 42 : 0.5 + 43 : 0.5 +state 16 [0] + action 0 [1] + 27 : 0.5 + 38 : 0.5 + action 1 [1] + 4 : 0.5 + 44 : 0.5 +state 17 [0] + action 0 [1] + 45 : 0.5 + 46 : 0.5 +state 18 [0] + action 0 [1] + 7 : 0.5 + 45 : 0.5 + action 1 [1] + 47 : 0.5 + 48 : 0.5 +state 19 [0] + action 0 [1] + 8 : 0.5 + 46 : 0.5 + action 1 [1] + 49 : 0.5 + 50 : 0.5 +state 20 [0] + action 0 [1] + 51 : 0.5 + 52 : 0.5 +state 21 [0] + action 0 [1] + 53 : 0.5 + 54 : 0.5 +state 22 [0] + action 0 [1] + 51 : 0.5 + 53 : 0.5 + action 1 [1] + 55 : 0.5 + 56 : 0.5 +state 23 [0] + action 0 [1] + 52 : 0.5 + 54 : 0.5 + action 1 [1] + 57 : 0.5 + 58 : 0.5 +state 24 [0] + action 0 [1] + 47 : 0.5 + 55 : 0.5 + action 1 [1] + 7 : 0.5 + 59 : 0.5 +state 25 [0] + action 0 [1] + 48 : 0.5 + 56 : 0.5 + action 1 [1] + 60 : 0.5 + 61 : 0.5 +state 26 [0] + action 0 [1] + 49 : 0.5 + 57 : 0.5 + action 1 [1] + 62 : 0.5 + 63 : 0.5 +state 27 [0] + action 0 [1] + 50 : 0.5 + 58 : 0.5 + action 1 [1] + 8 : 0.5 + 64 : 0.5 +state 28 [0] + action 0 [1] + 65 : 0.5 + 66 : 0.5 +state 29 [0] + action 0 [1] + 67 : 0.5 + 68 : 0.5 +state 30 [0] + action 0 [1] + 65 : 0.5 + 67 : 0.5 + action 1 [1] + 69 : 0.5 + 70 : 0.5 +state 31 [0] + action 0 [1] + 66 : 0.5 + 68 : 0.5 + action 1 [1] + 71 : 0.5 + 72 : 0.5 +state 32 [0] + action 0 [1] + 73 : 0.5 + 74 : 0.5 +state 33 [0] + action 0 [1] + 11 : 0.5 + 73 : 0.5 + action 1 [1] + 75 : 0.5 + 76 : 0.5 +state 34 [0] + action 0 [1] + 12 : 0.5 + 74 : 0.5 + action 1 [1] + 77 : 0.5 + 78 : 0.5 +state 35 [0] + action 0 [1] + 69 : 0.5 + 75 : 0.5 + action 1 [1] + 11 : 0.5 + 79 : 0.5 +state 36 [0] + action 0 [1] + 70 : 0.5 + 76 : 0.5 + action 1 [1] + 80 : 0.5 + 81 : 0.5 +state 37 [0] + action 0 [1] + 71 : 0.5 + 77 : 0.5 + action 1 [1] + 82 : 0.5 + 83 : 0.5 +state 38 [0] + action 0 [1] + 72 : 0.5 + 78 : 0.5 + action 1 [1] + 12 : 0.5 + 84 : 0.5 +state 39 [0] + action 0 [1] + 59 : 0.5 + 79 : 0.5 +state 40 [0] + action 0 [1] + 60 : 0.5 + 80 : 0.5 +state 41 [0] + action 0 [1] + 61 : 0.5 + 81 : 0.5 +state 42 [0] + action 0 [1] + 62 : 0.5 + 82 : 0.5 +state 43 [0] + action 0 [1] + 63 : 0.5 + 83 : 0.5 +state 44 [0] + action 0 [1] + 64 : 0.5 + 84 : 0.5 +state 45 [0] + action 0 [1] + 85 : 0.5 + 86 : 0.5 +state 46 [0] + action 0 [1] + 87 : 0.5 + 88 : 0.5 +state 47 [0] + action 0 [1] + 24 : 0.5 + 85 : 0.5 + action 1 [1] + 18 : 0.5 + 89 : 0.5 +state 48 [0] + action 0 [1] + 25 : 0.5 + 86 : 0.5 + action 1 [1] + 90 : 0.5 + 91 : 0.5 +state 49 [0] + action 0 [1] + 26 : 0.5 + 87 : 0.5 + action 1 [1] + 92 : 0.5 + 93 : 0.5 +state 50 [0] + action 0 [1] + 27 : 0.5 + 88 : 0.5 + action 1 [1] + 19 : 0.5 + 94 : 0.5 +state 51 [0] + action 0 [1] + 95 : 0.5 + 96 : 0.5 +state 52 [0] + action 0 [1] + 97 : 0.5 + 98 : 0.5 +state 53 [0] + action 0 [1] + 99 : 0.5 + 100 : 0.5 +state 54 [0] + action 0 [1] + 101 : 0.5 + 102 : 0.5 +state 55 [0] + action 0 [1] + 95 : 0.5 + 99 : 0.5 + action 1 [1] + 22 : 0.5 + 103 : 0.5 +state 56 [0] + action 0 [1] + 96 : 0.5 + 100 : 0.5 + action 1 [1] + 104 : 0.5 + 105 : 0.5 +state 57 [0] + action 0 [1] + 97 : 0.5 + 101 : 0.5 + action 1 [1] + 106 : 0.5 + 107 : 0.5 +state 58 [0] + action 0 [1] + 98 : 0.5 + 102 : 0.5 + action 1 [1] + 23 : 0.5 + 108 : 0.5 +state 59 [0] + action 0 [1] + 89 : 0.5 + 103 : 0.5 +state 60 [0] + action 0 [1] + 90 : 0.5 + 104 : 0.5 +state 61 [0] + action 0 [1] + 91 : 0.5 + 105 : 0.5 +state 62 [0] + action 0 [1] + 92 : 0.5 + 106 : 0.5 +state 63 [0] + action 0 [1] + 93 : 0.5 + 107 : 0.5 +state 64 [0] + action 0 [1] + 94 : 0.5 + 108 : 0.5 +state 65 [0] + action 0 [1] + 109 : 0.5 + 110 : 0.5 +state 66 [0] + action 0 [1] + 111 : 0.5 + 112 : 0.5 +state 67 [0] + action 0 [1] + 113 : 0.5 + 114 : 0.5 +state 68 [0] + action 0 [1] + 115 : 0.5 + 116 : 0.5 +state 69 [0] + action 0 [1] + 109 : 0.5 + 113 : 0.5 + action 1 [1] + 30 : 0.5 + 117 : 0.5 +state 70 [0] + action 0 [1] + 110 : 0.5 + 114 : 0.5 + action 1 [1] + 118 : 0.5 + 119 : 0.5 +state 71 [0] + action 0 [1] + 111 : 0.5 + 115 : 0.5 + action 1 [1] + 120 : 0.5 + 121 : 0.5 +state 72 [0] + action 0 [1] + 112 : 0.5 + 116 : 0.5 + action 1 [1] + 31 : 0.5 + 122 : 0.5 +state 73 [0] + action 0 [1] + 123 : 0.5 + 124 : 0.5 +state 74 [0] + action 0 [1] + 125 : 0.5 + 126 : 0.5 +state 75 [0] + action 0 [1] + 35 : 0.5 + 123 : 0.5 + action 1 [1] + 33 : 0.5 + 127 : 0.5 +state 76 [0] + action 0 [1] + 36 : 0.5 + 124 : 0.5 + action 1 [1] + 128 : 0.5 + 129 : 0.5 +state 77 [0] + action 0 [1] + 37 : 0.5 + 125 : 0.5 + action 1 [1] + 130 : 0.5 + 131 : 0.5 +state 78 [0] + action 0 [1] + 38 : 0.5 + 126 : 0.5 + action 1 [1] + 34 : 0.5 + 132 : 0.5 +state 79 [0] + action 0 [1] + 117 : 0.5 + 127 : 0.5 +state 80 [0] + action 0 [1] + 118 : 0.5 + 128 : 0.5 +state 81 [0] + action 0 [1] + 119 : 0.5 + 129 : 0.5 +state 82 [0] + action 0 [1] + 120 : 0.5 + 130 : 0.5 +state 83 [0] + action 0 [1] + 121 : 0.5 + 131 : 0.5 +state 84 [0] + action 0 [1] + 122 : 0.5 + 132 : 0.5 +state 85 [0] + action 0 [1] + 45 : 0.5 + 133 : 0.5 +state 86 [0] + action 0 [1] + 134 : 0.5 + 135 : 0.5 +state 87 [0] + action 0 [1] + 136 : 0.5 + 137 : 0.5 +state 88 [0] + action 0 [1] + 46 : 0.5 + 138 : 0.5 +state 89 [0] + action 0 [1] + 59 : 0.5 + 133 : 0.5 +state 90 [0] + action 0 [1] + 60 : 0.5 + 134 : 0.5 +state 91 [0] + action 0 [1] + 61 : 0.5 + 135 : 0.5 +state 92 [0] + action 0 [1] + 62 : 0.5 + 136 : 0.5 +state 93 [0] + action 0 [1] + 63 : 0.5 + 137 : 0.5 +state 94 [0] + action 0 [1] + 64 : 0.5 + 138 : 0.5 +state 95 [0] + action 0 [1] + 51 : 0.5 + 139 : 0.5 +state 96 [0] + action 0 [1] + 140 : 0.5 + 141 : 0.5 +state 97 [0] + action 0 [1] + 142 : 0.5 + 143 : 0.5 +state 98 [0] + action 0 [1] + 52 : 0.5 + 144 : 0.5 +state 99 [0] + action 0 [1] + 53 : 0.5 + 145 : 0.5 +state 100 [0] + action 0 [1] + 146 : 0.5 + 147 : 0.5 +state 101 [0] + action 0 [1] + 148 : 0.5 + 149 : 0.5 +state 102 [0] + action 0 [1] + 54 : 0.5 + 150 : 0.5 +state 103 [0] + action 0 [1] + 139 : 0.5 + 145 : 0.5 +state 104 [0] + action 0 [1] + 140 : 0.5 + 146 : 0.5 +state 105 [0] + action 0 [1] + 141 : 0.5 + 147 : 0.5 +state 106 [0] + action 0 [1] + 142 : 0.5 + 148 : 0.5 +state 107 [0] + action 0 [1] + 143 : 0.5 + 149 : 0.5 +state 108 [0] + action 0 [1] + 144 : 0.5 + 150 : 0.5 +state 109 [0] + action 0 [1] + 65 : 0.5 + 151 : 0.5 +state 110 [0] + action 0 [1] + 152 : 0.5 + 153 : 0.5 +state 111 [0] + action 0 [1] + 154 : 0.5 + 155 : 0.5 +state 112 [0] + action 0 [1] + 66 : 0.5 + 156 : 0.5 +state 113 [0] + action 0 [1] + 67 : 0.5 + 157 : 0.5 +state 114 [0] + action 0 [1] + 158 : 0.5 + 159 : 0.5 +state 115 [0] + action 0 [1] + 160 : 0.5 + 161 : 0.5 +state 116 [0] + action 0 [1] + 68 : 0.5 + 162 : 0.5 +state 117 [0] + action 0 [1] + 151 : 0.5 + 157 : 0.5 +state 118 [0] + action 0 [1] + 152 : 0.5 + 158 : 0.5 +state 119 [0] + action 0 [1] + 153 : 0.5 + 159 : 0.5 +state 120 [0] + action 0 [1] + 154 : 0.5 + 160 : 0.5 +state 121 [0] + action 0 [1] + 155 : 0.5 + 161 : 0.5 +state 122 [0] + action 0 [1] + 156 : 0.5 + 162 : 0.5 +state 123 [0] + action 0 [1] + 73 : 0.5 + 163 : 0.5 +state 124 [0] + action 0 [1] + 164 : 0.5 + 165 : 0.5 +state 125 [0] + action 0 [1] + 166 : 0.5 + 167 : 0.5 +state 126 [0] + action 0 [1] + 74 : 0.5 + 168 : 0.5 +state 127 [0] + action 0 [1] + 79 : 0.5 + 163 : 0.5 +state 128 [0] + action 0 [1] + 80 : 0.5 + 164 : 0.5 +state 129 [0] + action 0 [1] + 81 : 0.5 + 165 : 0.5 +state 130 [0] + action 0 [1] + 82 : 0.5 + 166 : 0.5 +state 131 [0] + action 0 [1] + 83 : 0.5 + 167 : 0.5 +state 132 [0] + action 0 [1] + 84 : 0.5 + 168 : 0.5 +state 133 [0] done two + action 0 [0] + 133 : 1 + action 1 [0] + 133 : 1 +state 134 [0] done three + action 0 [0] + 134 : 1 + action 1 [0] + 134 : 1 +state 135 [0] done four + action 0 [0] + 135 : 1 + action 1 [0] + 135 : 1 +state 136 [0] done five + action 0 [0] + 136 : 1 + action 1 [0] + 136 : 1 +state 137 [0] done six + action 0 [0] + 137 : 1 + action 1 [0] + 137 : 1 +state 138 [0] done seven + action 0 [0] + 138 : 1 + action 1 [0] + 138 : 1 +state 139 [0] done three + action 0 [0] + 139 : 1 + action 1 [0] + 139 : 1 +state 140 [0] done four + action 0 [0] + 140 : 1 + action 1 [0] + 140 : 1 +state 141 [0] done five + action 0 [0] + 141 : 1 + action 1 [0] + 141 : 1 +state 142 [0] done six + action 0 [0] + 142 : 1 + action 1 [0] + 142 : 1 +state 143 [0] done seven + action 0 [0] + 143 : 1 + action 1 [0] + 143 : 1 +state 144 [0] done eight + action 0 [0] + 144 : 1 + action 1 [0] + 144 : 1 +state 145 [0] done four + action 0 [0] + 145 : 1 + action 1 [0] + 145 : 1 +state 146 [0] done five + action 0 [0] + 146 : 1 + action 1 [0] + 146 : 1 +state 147 [0] done six + action 0 [0] + 147 : 1 + action 1 [0] + 147 : 1 +state 148 [0] done seven + action 0 [0] + 148 : 1 + action 1 [0] + 148 : 1 +state 149 [0] done eight + action 0 [0] + 149 : 1 + action 1 [0] + 149 : 1 +state 150 [0] done nine + action 0 [0] + 150 : 1 + action 1 [0] + 150 : 1 +state 151 [0] done five + action 0 [0] + 151 : 1 + action 1 [0] + 151 : 1 +state 152 [0] done six + action 0 [0] + 152 : 1 + action 1 [0] + 152 : 1 +state 153 [0] done seven + action 0 [0] + 153 : 1 + action 1 [0] + 153 : 1 +state 154 [0] done eight + action 0 [0] + 154 : 1 + action 1 [0] + 154 : 1 +state 155 [0] done nine + action 0 [0] + 155 : 1 + action 1 [0] + 155 : 1 +state 156 [0] done ten + action 0 [0] + 156 : 1 + action 1 [0] + 156 : 1 +state 157 [0] done six + action 0 [0] + 157 : 1 + action 1 [0] + 157 : 1 +state 158 [0] done seven + action 0 [0] + 158 : 1 + action 1 [0] + 158 : 1 +state 159 [0] done eight + action 0 [0] + 159 : 1 + action 1 [0] + 159 : 1 +state 160 [0] done nine + action 0 [0] + 160 : 1 + action 1 [0] + 160 : 1 +state 161 [0] done ten + action 0 [0] + 161 : 1 + action 1 [0] + 161 : 1 +state 162 [0] done eleven + action 0 [0] + 162 : 1 + action 1 [0] + 162 : 1 +state 163 [0] done seven + action 0 [0] + 163 : 1 + action 1 [0] + 163 : 1 +state 164 [0] done eight + action 0 [0] + 164 : 1 + action 1 [0] + 164 : 1 +state 165 [0] done nine + action 0 [0] + 165 : 1 + action 1 [0] + 165 : 1 +state 166 [0] done ten + action 0 [0] + 166 : 1 + action 1 [0] + 166 : 1 +state 167 [0] done eleven + action 0 [0] + 167 : 1 + action 1 [0] + 167 : 1 +state 168 [0] done twelve + action 0 [0] + 168 : 1 + action 1 [0] + 168 : 1 diff --git a/src/test/parser/DirectEncodingParserTest.cpp b/src/test/parser/DirectEncodingParserTest.cpp new file mode 100644 index 000000000..07d63b017 --- /dev/null +++ b/src/test/parser/DirectEncodingParserTest.cpp @@ -0,0 +1,38 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/parser/DirectEncodingParser.h" + +TEST(DirectEncodingParserTest, CtmcParsing) { + std::shared_ptr> modelPtr = storm::parser::DirectEncodingParser::parseModel(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn"); + + // Test if parsed correctly. + ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType()); + ASSERT_EQ(276ul, modelPtr->getNumberOfStates()); + ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions()); + ASSERT_TRUE(modelPtr->hasLabel("init")); + ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits()); + ASSERT_TRUE(modelPtr->hasLabel("premium")); + ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits()); + ASSERT_TRUE(modelPtr->hasLabel("minimum")); + ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits()); +} + +TEST(DirectEncodingParserTest, MdpParsing) { + std::shared_ptr> modelPtr = storm::parser::DirectEncodingParser::parseModel(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.drn"); + + // Test if parsed correctly. + ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType()); + ASSERT_EQ(169ul, modelPtr->getNumberOfStates()); + ASSERT_EQ(436ul, modelPtr->getNumberOfTransitions()); + ASSERT_EQ(254ul, modelPtr->as>()->getNumberOfChoices()); + ASSERT_TRUE(modelPtr->hasLabel("init")); + ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits()); + ASSERT_TRUE(modelPtr->hasLabel("six")); + ASSERT_EQ(5ul, modelPtr->getStates("six").getNumberOfSetBits()); + ASSERT_TRUE(modelPtr->hasLabel("eleven")); + ASSERT_EQ(2ul, modelPtr->getStates("eleven").getNumberOfSetBits()); +} +