Skip to content

GitLab

mohawk-2.0
mohawk-2.0
Commit 1735aaef authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files
Options

Bug data added; this is required to show the bug that occurs when SkipRefine... 

Bug data added; this is required to show the bug that occurs when SkipRefine is turned ON; remove from repo after bug is fixed!
parent 43a793e3
Expand all Show whitespace changes
Inline Side-by-side
Showing with 2857 additions and 0 deletions
data/bug/01-orig.mohawk.T 0 → 100644
View file @ 1735aaef
This diff is collapsed.
data/bug/01-orig.mohawk.T.mohawk 0 → 100644
View file @ 1735aaef
This diff is collapsed.
data/bug/02-CA259.mohawk.T 0 → 100644
View file @ 1735aaef
/* Generated On : 2015/02/07 20:24:43.536
* Generated With : Mohawk Reverse Converter: ASAPTime NSA
* Number of Roles : 15
* Number of Timeslots : 30
* Number of Rules : 552
*
* Roles : |Size=15| [role1, role2, role3, role4, role5, role6, role7, role8, role9, role10, role11, role12, role13, role14, role15]
* Timeslots : |Size=30| [t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30]
*
*
* TESTCASE COMMENTS:
*
*/
Query: t2, [role3]
Expected: REACHABLE
/*
* Number of Rules : 282
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 200
* Truly Startable Rules : 36
*/
CanAssign {
/* 259 */ <TRUE, t27, NOT ~ role12, t2, role3>
}
/*
* Number of Rules : 134
* Largest Precondition : 0
* Largest Role Schedule : 1
* Startable Rules : 134
* Truly Startable Rules : 25
*/
CanRevoke {
}
/*
* Number of Rules : 91
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 76
* Truly Startable Rules : 16
*/
CanEnable {
}
/*
* Number of Rules : 45
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 31
* Truly Startable Rules : 1
*/
CanDisable {
}
\ No newline at end of file
data/bug/02-CA259.mohawk.T.mohawk 0 → 100644
View file @ 1735aaef
Roles role3_AL0_t2 __u0goalRole_t2 role12_AL0_t2 AdminRole;
Users AdminUser User;
UA <AdminUser,AdminRole>;
CR ;
CA <AdminRole,-role12_AL0_t2,role3_AL0_t2> <AdminRole,role3_AL0_t2,__u0goalRole_t2>;
ADMIN AdminUser;
SPEC User __u0goalRole_t2;
data/bug/03-CA.mohawk.T 0 → 100644
View file @ 1735aaef
/* Generated On : 2015/02/07 20:24:43.536
* Generated With : Mohawk Reverse Converter: ASAPTime NSA
* Number of Roles : 15
* Number of Timeslots : 30
* Number of Rules : 552
*
* Roles : |Size=15| [role1, role2, role3, role4, role5, role6, role7, role8, role9, role10, role11, role12, role13, role14, role15]
* Timeslots : |Size=30| [t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30]
*
*
* TESTCASE COMMENTS:
*
*/
Query: t2, [role3]
Expected: UNKNOWN
/*
* Number of Rules : 282
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 200
* Truly Startable Rules : 36
*/
CanAssign {
/* 1 */ <role1, t13, role12 & role3, t25, role15>
/* 2 */ <role1, t11, role12 & role3, t16, role15>
/* 3 */ <role1, t27, role12 & role3, t15, role15>
/* 4 */ <TRUE, t22, role12 & role3, t24, role15>
/* 5 */ <role1, t21, role12 & role3, t29, role15>
/* 6 */ <role1, t6, role12 & role3, t20, role15>
/* 7 */ <role3, t21, TRUE, t28, role14>
/* 8 */ <role3, t30, TRUE, t3, role14>
/* 9 */ <role3, t18, TRUE, t8, role14>
/* 10 */ <role3, t22, TRUE, t17, role14>
/* 11 */ <role3, t7, TRUE, t15, role14>
/* 12 */ <role3, t1, TRUE, t11, role14>
/* 13 */ <role3, t8, TRUE, t30, role14>
/* 14 */ <role13, t27, NOT ~ role12, t2, role3>
/* 15 */ <TRUE, t12, TRUE, t26, role14>
/* 16 */ <TRUE, t9, TRUE, t6, role14>
/* 17 */ <TRUE, t29, TRUE, t12, role14>
/* 18 */ <TRUE, t25, TRUE, t19, role14>
/* 19 */ <role3, t24, TRUE, t24, role14>
/* 20 */ <role5, t18, TRUE, t27, role4>
/* 21 */ <role5, t16, TRUE, t30, role4>
/* 22 */ <role5, t4, TRUE, t3, role4>
/* 23 */ <role5, t10, TRUE, t5, role4>
/* 24 */ <role5, t17, TRUE, t4, role4>
/* 25 */ <role5, t9, TRUE, t22, role4>
/* 26 */ <role5, t8, TRUE, t6, role4>
/* 27 */ <TRUE, t11, TRUE, t8, role4>
/* 28 */ <role5, t12, TRUE, t7, role4>
/* 29 */ <role5, t19, TRUE, t19, role4>
/* 30 */ <role12, t27, NOT ~ role12, t2, role3>
/* 31 */ <role5, t13, TRUE, t25, role4>
/* 32 */ <role5, t7, TRUE, t13, role4>
/* 33 */ <role5, t28, TRUE, t7, role6>
/* 34 */ <role5, t19, TRUE, t20, role6>
/* 35 */ <role5, t9, TRUE, t21, role6>
/* 36 */ <role5, t7, TRUE, t1, role6>
/* 37 */ <role5, t16, TRUE, t23, role6>
/* 38 */ <role5, t12, TRUE, t17, role6>
/* 39 */ <role5, t6, TRUE, t25, role6>
/* 40 */ <role5, t23, TRUE, t6, role6>
/* 41 */ <role5, t2, TRUE, t9, role6>
/* 42 */ <role5, t26, TRUE, t23, role8>
/* 43 */ <role5, t20, TRUE, t14, role8>
/* 44 */ <role5, t24, TRUE, t13, role8>
/* 45 */ <role5, t3, TRUE, t18, role8>
/* 46 */ <TRUE, t17, TRUE, t5, role8>
/* 47 */ <role5, t12, TRUE, t8, role8>
/* 48 */ <role9, t27, NOT ~ role12, t2, role3>
/* 49 */ <role5, t27, TRUE, t26, role8>
/* 50 */ <role5, t10, TRUE, t6, role8>
/* 51 */ <role5, t16, TRUE, t30, role8>
/* 52 */ <TRUE, t29, TRUE, t19, role8>
/* 53 */ <role5, t21, TRUE, t8, role8>
/* 54 */ <TRUE, t28, TRUE, t9, role8>
/* 55 */ <role5, t7, TRUE, t26, role8>
/* 56 */ <role5, t3, TRUE, t24, role8>
/* 57 */ <role5, t24, TRUE, t27, role8>
/* 58 */ <role5, t30, TRUE, t4, role8>
/* 59 */ <role5, t1, TRUE, t25, role8>
/* 60 */ <role5, t4, TRUE, t28, role8>
/* 61 */ <role5, t20, TRUE, t29, role8>
/* 62 */ <role5, t5, TRUE, t18, role8>
/* 63 */ <role5, t25, TRUE, t17, role8>
/* 64 */ <role5, t16, TRUE, t30, role8>
/* 65 */ <TRUE, t22, TRUE, t1, role8>
/* 66 */ <TRUE, t13, TRUE, t11, role8>
/* 67 */ <TRUE, t8, TRUE, t20, role4>
/* 68 */ <role5, t9, TRUE, t21, role4>
/* 69 */ <role5, t27, NOT ~ role12, t21, role4>
/* 70 */ <TRUE, t6, TRUE, t7, role4>
/* 71 */ <TRUE, t11, TRUE, t25, role12>
/* 72 */ <TRUE, t25, TRUE, t18, role12>
/* 73 */ <role9, t17, TRUE, t28, role12>
/* 74 */ <role9, t7, TRUE, t16, role12>
/* 75 */ <role3, t1, role3, t3, role1>
/* 76 */ <role3, t4, role3, t26, role3>
/* 77 */ <role3, t11, role3, t6, role3>
/* 78 */ <TRUE, t3, role3, t16, role3>
/* 79 */ <TRUE, t5, role3, t28, role3>
/* 80 */ <role3, t16, role3, t29, role3>
/* 81 */ <role3, t17, role3, t10, role3>
/* 82 */ <role3, t18, role3, t17, role3>
/* 83 */ <role3, t8, role3, t11, role3>
/* 84 */ <role3, t13, role3, t30, role3>
/* 85 */ <TRUE, t19, role3, t27, role3>
/* 86 */ <role3, t23, role3, t13, role3>
/* 87 */ <role3, t10, role3, t8, role3>
/* 88 */ <role3, t20, role3, t1, role3>
/* 89 */ <role3, t12, role3, t15, role3>
/* 90 */ <role3, t14, role3, t14, role3>
/* 91 */ <TRUE, t15, role3, t22, role3>
/* 92 */ <role6, t3, role3, t30, role5>
/* 93 */ <TRUE, t27, role3, t10, role5>
/* 94 */ <TRUE, t23, role3, t8, role5>
/* 95 */ <role6, t28, role3, t5, role5>
/* 96 */ <role6, t4, role8, t1, role5>
/* 97 */ <role6, t5, role8, t3, role5>
/* 98 */ <role6, t11, role8, t28, role5>
/* 99 */ <role6, t25, role8, t2, role5>
/* 100 */ <role14, t2, NOT ~ role12, t12, role13>
/* 101 */ <TRUE, t14, role8, t13, role5>
/* 102 */ <role6, t15, role8, t25, role5>
/* 103 */ <role6, t8, role8, t30, role5>
/* 104 */ <role6, t6, role8, t4, role5>
/* 105 */ <role6, t7, role8, t5, role5>
/* 106 */ <role6, t20, role8, t15, role5>
/* 107 */ <role5, t16, NOT ~ role3, t27, role2>
/* 108 */ <TRUE, t14, NOT ~ role3, t28, role2>
/* 109 */ <role5, t4, NOT ~ role3, t8, role2>
/* 110 */ <role5, t23, NOT ~ role3, t12, role1>
/* 111 */ <role5, t2, NOT ~ role12, t12, role13>
/* 112 */ <role5, t25, NOT ~ role3, t7, role2>
/* 113 */ <role5, t7, NOT ~ role3, t29, role1>
/* 114 */ <TRUE, t18, NOT ~ role3, t3, role1>
/* 115 */ <role5, t15, NOT ~ role3, t14, role1>
/* 116 */ <role5, t8, NOT ~ role3, t30, role1>
/* 117 */ <role5, t1, NOT ~ role12, t29, role4>
/* 118 */ <TRUE, t25, NOT ~ role12, t16, role4>
/* 119 */ <role5, t24, NOT ~ role12, t11, role4>
/* 120 */ <role5, t26, NOT ~ role12, t17, role4>
/* 121 */ <role5, t28, NOT ~ role12, t10, role4>
/* 122 */ <role5, t17, NOT ~ role12, t7, role4>
/* 123 */ <role5, t14, TRUE, t5, role7>
/* 124 */ <role5, t2, TRUE, t16, role7>
/* 125 */ <role5, t15, TRUE, t15, role7>
/* 126 */ <role5, t16, TRUE, t28, role7>
/* 127 */ <role5, t20, TRUE, t24, role7>
/* 128 */ <role5, t17, TRUE, t19, role7>
/* 129 */ <role5, t6, TRUE, t25, role7>
/* 130 */ <role5, t29, TRUE, t29, role7>
/* 131 */ <role5, t8, TRUE, t30, role7>
/* 132 */ <role5, t3, TRUE, t2, role7>
/* 133 */ <TRUE, t29, TRUE, t19, role9>
/* 134 */ <role5, t21, TRUE, t8, role9>
/* 135 */ <TRUE, t28, TRUE, t9, role9>
/* 136 */ <role5, t7, TRUE, t26, role9>
/* 137 */ <role5, t3, TRUE, t24, role9>
/* 138 */ <role5, t24, TRUE, t27, role9>
/* 139 */ <role5, t30, TRUE, t4, role9>
/* 140 */ <role5, t1, TRUE, t25, role9>
/* 141 */ <role5, t4, TRUE, t28, role9>
/* 142 */ <role5, t20, TRUE, t29, role9>
/* 143 */ <role5, t5, TRUE, t18, role9>
/* 144 */ <role5, t25, TRUE, t17, role9>
/* 145 */ <role5, t16, TRUE, t30, role9>
/* 146 */ <TRUE, t22, TRUE, t1, role9>
/* 147 */ <TRUE, t13, TRUE, t11, role9>
/* 148 */ <TRUE, t8, TRUE, t20, role9>
/* 149 */ <role5, t9, TRUE, t21, role9>
/* 150 */ <role9, t13, TRUE, t28, role2>
/* 151 */ <role9, t28, TRUE, t3, role2>
/* 152 */ <role9, t5, TRUE, t4, role2>
/* 153 */ <role9, t10, TRUE, t24, role2>
/* 154 */ <role9, t2, TRUE, t8, role2>
/* 155 */ <role9, t1, TRUE, t10, role2>
/* 156 */ <role9, t24, TRUE, t29, role2>
/* 157 */ <role9, t3, TRUE, t11, role2>
/* 158 */ <role9, t6, TRUE, t22, role2>
/* 159 */ <role3, t4, TRUE, t16, role14>
/* 160 */ <role3, t16, TRUE, t2, role14>
/* 161 */ <role5, t5, TRUE, t27, role4>
/* 162 */ <role5, t4, TRUE, t22, role4>
/* 163 */ <role5, t12, TRUE, t6, role4>
/* 164 */ <role5, t9, TRUE, t17, role4>
/* 165 */ <role5, t8, TRUE, t14, role4>
/* 166 */ <role5, t3, TRUE, t9, role4>
/* 167 */ <role5, t6, TRUE, t21, role4>
/* 168 */ <TRUE, t22, TRUE, t10, role4>
/* 169 */ <role5, t19, TRUE, t23, role6>
/* 170 */ <role5, t12, TRUE, t13, role6>
/* 171 */ <role5, t26, TRUE, t7, role6>
/* 172 */ <role5, t5, TRUE, t8, role6>
/* 173 */ <role5, t27, TRUE, t21, role6>
/* 174 */ <TRUE, t11, TRUE, t27, role6>
/* 175 */ <role5, t13, TRUE, t9, role6>
/* 176 */ <role5, t7, TRUE, t14, role6>
/* 177 */ <role6, t27, NOT ~ role12, t2, role3>
/* 178 */ <role5, t14, TRUE, t5, role6>
/* 179 */ <role5, t2, TRUE, t16, role6>
/* 180 */ <role5, t15, TRUE, t15, role6>
/* 181 */ <role5, t16, TRUE, t28, role6>
/* 182 */ <role5, t20, TRUE, t24, role6>
/* 183 */ <role5, t17, TRUE, t19, role6>
/* 184 */ <role5, t6, TRUE, t25, role6>
/* 185 */ <role5, t29, TRUE, t29, role6>
/* 186 */ <role5, t8, TRUE, t30, role6>
/* 187 */ <role5, t3, TRUE, t2, role6>
/* 188 */ <TRUE, t29, TRUE, t19, role8>
/* 189 */ <role5, t21, TRUE, t8, role8>
/* 190 */ <TRUE, t28, TRUE, t9, role8>
/* 191 */ <role5, t7, TRUE, t26, role8>
/* 192 */ <role5, t3, TRUE, t24, role8>
/* 193 */ <role5, t24, TRUE, t27, role8>
/* 194 */ <role5, t30, TRUE, t4, role8>
/* 195 */ <role5, t1, TRUE, t25, role8>
/* 196 */ <role5, t4, TRUE, t28, role8>
/* 197 */ <role5, t20, TRUE, t29, role8>
/* 198 */ <role5, t5, TRUE, t18, role8>
/* 199 */ <role5, t25, TRUE, t17, role8>
/* 200 */ <role5, t16, TRUE, t30, role8>
/* 201 */ <TRUE, t22, TRUE, t1, role8>
/* 202 */ <TRUE, t13, TRUE, t11, role8>
/* 203 */ <TRUE, t8, TRUE, t20, role8>
/* 204 */ <role5, t9, TRUE, t21, role8>
/* 205 */ <role5, t27, NOT ~ role12, t2, role3>
/* 206 */ <TRUE, t6, TRUE, t7, role8>
/* 207 */ <TRUE, t11, TRUE, t25, role2>
/* 208 */ <TRUE, t25, TRUE, t18, role2>
/* 209 */ <role9, t17, TRUE, t28, role2>
/* 210 */ <role9, t7, TRUE, t16, role2>
/* 211 */ <role3, t1, role3, t3, role13>
/* 212 */ <role3, t4, role3, t26, role13>
/* 213 */ <role3, t11, role3, t6, role13>
/* 214 */ <TRUE, t3, role3, t16, role13>
/* 215 */ <TRUE, t5, role3, t28, role13>
/* 216 */ <role3, t16, role3, t29, role13>
/* 217 */ <role3, t17, role3, t10, role13>
/* 218 */ <role3, t18, role3, t17, role13>
/* 219 */ <role3, t8, role3, t11, role13>
/* 220 */ <role3, t13, role3, t30, role13>
/* 221 */ <TRUE, t19, role3, t27, role13>
/* 222 */ <role3, t23, role3, t13, role13>
/* 223 */ <role3, t10, role3, t8, role13>
/* 224 */ <role3, t20, role3, t1, role13>
/* 225 */ <role3, t12, role3, t15, role13>
/* 226 */ <role3, t14, role3, t14, role13>
/* 227 */ <TRUE, t15, role3, t22, role13>
/* 228 */ <role6, t3, role3, t30, role7>
/* 229 */ <TRUE, t27, role3, t10, role7>
/* 230 */ <TRUE, t23, role3, t8, role7>
/* 231 */ <role6, t28, role3, t5, role7>
/* 232 */ <role6, t4, role8, t1, role7>
/* 233 */ <role6, t5, role8, t3, role7>
/* 234 */ <role6, t11, role8, t28, role7>
/* 235 */ <role6, t25, role8, t2, role7>
/* 236 */ <role14, t2, NOT ~ role12, t2, role3>
/* 237 */ <TRUE, t14, role8, t13, role7>
/* 238 */ <role6, t15, role8, t25, role7>
/* 239 */ <role6, t8, role8, t30, role7>
/* 240 */ <role6, t6, role8, t4, role7>
/* 241 */ <role6, t7, role8, t5, role7>
/* 242 */ <role6, t20, role8, t15, role7>
/* 243 */ <role5, t16, NOT ~ role3, t27, role12>
/* 244 */ <TRUE, t14, NOT ~ role3, t28, role12>
/* 245 */ <role5, t4, NOT ~ role3, t8, role12>
/* 246 */ <role5, t23, NOT ~ role3, t12, role12>
/* 247 */ <role5, t2, NOT ~ role12, t2, role3>
/* 248 */ <role5, t25, NOT ~ role3, t7, role12>
/* 249 */ <role5, t7, NOT ~ role3, t29, role12>
/* 250 */ <TRUE, t18, NOT ~ role3, t3, role12>
/* 251 */ <role5, t15, NOT ~ role3, t14, role12>
/* 252 */ <role5, t8, NOT ~ role3, t30, role12>
/* 253 */ <role5, t1, NOT ~ role12, t29, role3>
/* 254 */ <TRUE, t25, NOT ~ role12, t16, role3>
/* 255 */ <role5, t24, NOT ~ role12, t11, role3>
/* 256 */ <role5, t26, NOT ~ role12, t17, role3>
/* 257 */ <role5, t28, NOT ~ role12, t10, role3>
/* 258 */ <role5, t17, NOT ~ role12, t7, role3>
/* 259 */ <TRUE, t27, NOT ~ role12, t2, role3>
/* 260 */ <role5, t5, NOT ~ role12, t9, role3>
/* 261 */ <role5, t11, NOT ~ role12, t23, role3>
/* 262 */ <role5, t29, NOT ~ role12, t12, role3>
/* 263 */ <role5, t19, NOT ~ role12, t30, role3>
/* 264 */ <role9, t18, role3 & NOT ~ role9, t6, role11>
/* 265 */ <role9, t10, role3 & NOT ~ role9, t3, role11>
/* 266 */ <role9, t13, role3 & NOT ~ role9, t14, role11>
/* 267 */ <role9, t8, role3 & NOT ~ role9, t1, role11>
/* 268 */ <role9, t17, role3 & NOT ~ role9, t18, role11>
/* 269 */ <role9, t6, role3 & NOT ~ role9, t22, role11>
/* 270 */ <role12, t25, NOT ~ role11, t13, role9>
/* 271 */ <role12, t15, NOT ~ role11, t7, role9>
/* 272 */ <role12, t8, NOT ~ role11, t11, role9>
/* 273 */ <role12, t4, NOT ~ role11, t14, role9>
/* 274 */ <role14, t30, role9, t25, role10>
/* 275 */ <TRUE, t25, role9, t8, role10>
/* 276 */ <role14, t7, NOT ~ role12, t2, role3>
/* 277 */ <role14, t7, role9, t29, role10>
/* 278 */ <role14, t5, role9, t17, role10>
/* 279 */ <role14, t17, role9, t1, role10>
/* 280 */ <TRUE, t13, role9, t2, role10>
/* 281 */ <role14, t15, role9, t5, role10>
/* 282 */ <role14, t19, role9, t12, role10>
}
/*
* Number of Rules : 134
* Largest Precondition : 0
* Largest Role Schedule : 1
* Startable Rules : 134
* Truly Startable Rules : 25
*/
CanRevoke {
}
/*
* Number of Rules : 91
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 76
* Truly Startable Rules : 16
*/
CanEnable {
}
/*
* Number of Rules : 45
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 31
* Truly Startable Rules : 1
*/
CanDisable {
}
\ No newline at end of file
data/bug/03-CA.mohawk.T.mohawk 0 → 100644
View file @ 1735aaef
This diff is collapsed.
data/bug/04-CA259-CR.mohawk.T 0 → 100644
View file @ 1735aaef
/* Generated On : 2015/02/07 20:24:43.536
* Generated With : Mohawk Reverse Converter: ASAPTime NSA
* Number of Roles : 15
* Number of Timeslots : 30
* Number of Rules : 552
*
* Roles : |Size=15| [role1, role2, role3, role4, role5, role6, role7, role8, role9, role10, role11, role12, role13, role14, role15]
* Timeslots : |Size=30| [t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30]
*
*
* TESTCASE COMMENTS:
*
*/
Query: t2, [role3]
Expected: REACHABLE
/*
* Number of Rules : 282
* Largest Precondition : 2
* Largest Role Schedule : 1
* Startable Rules : 200
* Truly Startable Rules : 36
*/
CanAssign {
/* 259 */ <TRUE, t27, NOT ~ role12, t2, role3>
}
/*
* Number of Rules : 134
* Largest Precondition : 0
* Largest Role Schedule : 1
* Startable Rules : 134
* Truly Startable Rules : 25
*/
CanRevoke {
/* 1 */ <role3, t11, TRUE, t10, role14>
/* 2 */ <TRUE, t1, TRUE, t27, role14>
/* 3 */ <role3, t16, TRUE, t15, role14>
/* 4 */ <role3, t13, TRUE, t30, role14>
/* 5 */ <TRUE, t29, TRUE, t1, role14>
/* 6 */ <role3, t2, TRUE, t24, role14>
/* 7 */ <TRUE, t7, TRUE, t29, role14>
/* 8 */ <TRUE, t26, TRUE, t25, role14>
/* 9 */ <role3, t4, TRUE, t2, role14>
/* 10 */ <TRUE, t14, TRUE, t5, role14>
/* 11 */ <role3, t8, TRUE, t4, role14>
/* 12 */ <role3, t15, TRUE, t9, role14>
/* 13 */ <role3, t12, TRUE, t20, role14>
/* 14 */ <role3, t9, TRUE, t28, role14>
/* 15 */ <role3, t27, TRUE, t8, role14>
/* 16 */ <role3, t21, TRUE, t11, role14>
/* 17 */ <role3, t6, TRUE, t12, role14>
/* 18 */ <TRUE, t10, TRUE, t19, role14>
/* 19 */ <role3, t17, TRUE, t3, role14>
/* 20 */ <role3, t3, TRUE, t6, role14>
/* 21 */ <TRUE, t6, TRUE, t14, role13>
/* 22 */ <role3, t24, TRUE, t3, role13>
/* 23 */ <role3, t22, TRUE, t28, role13>
/* 24 */ <role3, t19, TRUE, t10, role13>
/* 25 */ <role3, t14, TRUE, t6, role13>
/* 26 */ <role3, t7, TRUE, t16, role13>
/* 27 */ <role3, t30, TRUE, t15, role13>
/* 28 */ <role3, t1, TRUE, t24, role13>
/* 29 */ <role3, t27, TRUE, t18, role13>
/* 30 */ <role3, t18, TRUE, t9, role13>
/* 31 */ <role6, t2, TRUE, t29, role7>
/* 32 */ <role6, t16, TRUE, t10, role7>
/* 33 */ <role6, t7, TRUE, t28, role7>
/* 34 */ <role6, t23, TRUE, t28, role7>
/* 35 */ <role6, t16, TRUE, t5, role7>
/* 36 */ <role6, t27, TRUE, t3, role7>
/* 37 */ <role6, t13, TRUE, t6, role7>
/* 38 */ <role6, t10, TRUE, t7, role7>
/* 39 */ <role6, t9, TRUE, t27, role7>
/* 40 */ <role6, t14, TRUE, t8, role7>
/* 41 */ <TRUE, t17, TRUE, t11, role7>
/* 42 */ <role5, t3, TRUE, t14, role4>
/* 43 */ <role5, t19, TRUE, t9, role4>
/* 44 */ <TRUE, t12, TRUE, t15, role4>
/* 45 */ <role5, t30, TRUE, t12, role4>
/* 46 */ <role5, t8, TRUE, t16, role4>
/* 47 */ <TRUE, t15, TRUE, t17, role4>
/* 48 */ <role5, t10, TRUE, t25, role4>
/* 49 */ <role5, t24, TRUE, t10, role4>
/* 50 */ <role5, t9, TRUE, t6, role4>
/* 51 */ <role5, t1, TRUE, t18, role4>
/* 52 */ <role5, t28, TRUE, t26, role4>
/* 53 */ <role5, t11, TRUE, t27, role4>
/* 54 */ <role5, t12, TRUE, t14, role6>
/* 55 */ <role5, t24, TRUE, t24, role6>
/* 56 */ <role5, t20, TRUE, t8, role12>
/* 57 */ <TRUE, t6, TRUE, t4, role12>
/* 58 */ <role5, t14, TRUE, t27, role12>
/* 59 */ <role5, t15, TRUE, t10, role12>
/* 60 */ <role5, t8, TRUE, t16, role12>
/* 61 */ <role5, t27, TRUE, t12, role12>
/* 62 */ <role5, t3, TRUE, t14, role5>
/* 63 */ <role5, t19, TRUE, t9, role5>
/* 64 */ <TRUE, t12, TRUE, t15, role5>
/* 65 */ <role5, t30, TRUE, t12, role5>
/* 66 */ <role5, t8, TRUE, t16, role5>
/* 67 */ <TRUE, t15, TRUE, t17, role5>
/* 68 */ <role5, t10, TRUE, t25, role5>
/* 69 */ <role5, t24, TRUE, t10, role5>
/* 70 */ <role5, t9, TRUE, t6, role5>
/* 71 */ <role5, t1, TRUE, t18, role5>
/* 72 */ <role5, t28, TRUE, t26, role5>
/* 73 */ <role5, t11, TRUE, t27, role5>
/* 74 */ <role9, t2, TRUE, t4, role3>
/* 75 */ <role9, t10, TRUE, t20, role1>
/* 76 */ <TRUE, t25, TRUE, t22, role1>
/* 77 */ <role3, t4, TRUE, t4, role10>
/* 78 */ <role3, t29, TRUE, t3, role10>
/* 79 */ <TRUE, t28, TRUE, t20, role10>
/* 80 */ <role3, t12, TRUE, t16, role10>
/* 81 */ <role3, t1, TRUE, t9, role10>
/* 82 */ <role3, t19, TRUE, t5, role10>
/* 83 */ <role3, t30, TRUE, t13, role10>
/* 84 */ <role3, t2, TRUE, t23, role10>
/* 85 */ <role5, t12, TRUE, t14, role7>
/* 86 */ <role5, t24, TRUE, t24, role7>
/* 87 */ <role5, t20, TRUE, t8, role2>
/* 88 */ <TRUE, t6, TRUE, t4, role2>
/* 89 */ <role5, t14, TRUE, t27, role2>
/* 90 */ <role5, t15, TRUE, t10, role2>
/* 91 */ <role5, t8, TRUE, t16, role2>
/* 92 */ <role5, t27, TRUE, t12, role2>
/* 93 */ <role5, t2, TRUE, t19, role9>
/* 94 */ <role5, t13, TRUE, t2, role9>
/* 95 */ <role5, t7, TRUE, t10, role9>
/* 96 */ <TRUE, t26, TRUE, t8, role9>
/* 97 */ <role5, t23, TRUE, t12, role9>
/* 98 */ <role5, t5, TRUE, t3, role9>
/* 99 */ <role5, t10, TRUE, t15, role9>
/* 100 */ <role5, t2, TRUE, t19, role8>
/* 101 */ <role5, t13, TRUE, t2, role8>
/* 102 */ <role5, t7, TRUE, t10, role8>
/* 103 */ <TRUE, t26, TRUE, t8, role8>
/* 104 */ <role5, t23, TRUE, t12, role8>
/* 105 */ <role5, t5, TRUE, t3, role8>
/* 106 */ <role5, t10, TRUE, t15, role8>
/* 107 */ <TRUE, t12, TRUE, t13, role3>
/* 108 */ <role5, t19, TRUE, t11, role3>
/* 109 */ <role5, t9, TRUE, t16, role3>
/* 110 */ <role5, t18, TRUE, t23, role3>
/* 111 */ <role9, t23, TRUE, t29, role2>
/* 112 */ <role9, t2, TRUE, t4, role2>
/* 113 */ <role9, t10, TRUE, t20, role11>
/* 114 */ <TRUE, t25, TRUE, t22, role11>
/* 115 */ <role3, t4, TRUE, t4, role9>
/* 116 */ <role3, t29, TRUE, t3, role9>
/* 117 */ <TRUE, t28, TRUE, t20, role9>
/* 118 */ <role3, t12, TRUE, t16, role9>
/* 119 */ <role3, t1, TRUE, t9, role9>
/* 120 */ <role3, t19, TRUE, t5, role9>