03-CA.mohawk.T 14.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
/* 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 {
  
}