(* 1 *) Cache[#1] = Exclusive &&
        Cache[#2] <> Invalid

(* 2 *) Chan2[#2] = Gnts &&
        Cache[#1] = Exclusive

(* 3 *) Chan2[#1] = Gnte &&
        Cache[#2] <> Invalid

(* 4 *) Exgntd = False &&
        Cache[#1] = Exclusive

(* 5 *) Chan2[#1] = Gnte &&
        Chan2[#2] = Gnts

(* 6 *) Cache[#1] <> Invalid &&
        Shrset[#1] = False

(* 7 *) Chan2[#1] = Gnte &&
        Chan2[#2] = Gnte

(* 8 *) Chan3[#1] = Invack &&
        Cache[#1] = Exclusive

(* 9 *) Exgntd = False &&
        Chan2[#1] = Gnte

(* 10 *) Chan2[#1] = Gnts &&
         Shrset[#1] = False

(* 11 *) Chan3[#1] = Invack &&
         Cache[#1] <> Invalid

(* 12 *) Chan2[#1] = Gnte &&
         Shrset[#1] = False

(* 13 *) Chan2[#1] = Gnte &&
         Chan3[#1] = Invack

(* 14 *) Chan2[#1] = Gnts &&
         Chan3[#1] = Invack

(* 15 *) Chan3[#1] = Invack &&
         Shrset[#1] = False

(* 16 *) Exgntd = False &&
         Curcmd = Reqs &&
         Chan3[#1] = Invack

(* 17 *) Chan2[#1] = Inv &&
         Shrset[#1] = False

(* 18 *) Curcmd = Empty &&
         Chan3[#1] = Invack

(* 19 *) Exgntd = False &&
         Curcmd = Reqs &&
         Chan2[#1] = Inv

(* 20 *) Invset[#1] = True &&
         Shrset[#1] = False

(* 21 *) Chan2[#1] = Inv &&
         Chan3[#1] = Invack

(* 22 *) Curcmd = Empty &&
         Chan2[#1] = Inv

(* 23 *) Chan3[#1] = Invack &&
         Invset[#1] = True

(* 24 *) Chan2[#1] = Inv &&
         Invset[#1] = True

(* 25 *) Curcmd = Reqs &&
         Chan2[#1] = Inv &&
         Chan3[#2] = Invack

(* 26 *) Curcmd = Reqs &&
         Chan3[#1] = Invack &&
         Chan3[#2] = Invack

(* 27 *) Chan2[#1] = Gnte &&
         Chan3[#2] = Invack

(* 28 *) Chan3[#2] = Invack &&
         Cache[#1] = Exclusive

(* 29 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2[#1] = Empty &&
         Chan3[#2] = Invack &&
         Invset[#1] = True

(* 30 *) Curcmd = Reqs &&
         Chan2[#1] = Inv &&
         Chan2[#2] = Inv &&
         Chan3[#2] = Empty

(* 31 *) Chan2[#1] = Gnte &&
         Chan2[#2] = Inv

(* 32 *) Chan2[#2] = Inv &&
         Cache[#1] = Exclusive

(* 33 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2[#1] = Empty &&
         Chan2[#2] = Inv &&
         Chan3[#2] = Empty &&
         Invset[#1] = True

(* 34 *) Exgntd = True &&
         Chan2[#1] = Gnts

(* 35 *) Chan2[#1] = Gnte &&
         Invset[#2] = True

(* 36 *) Cache[#1] = Exclusive &&
         Invset[#2] = True

(* 37 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2[#1] = Empty &&
         Chan2[#2] = Empty &&
         Chan3[#2] = Empty &&
         Invset[#1] = True &&
         Invset[#2] = True

(* 38 *) Chan2[#1] = Gnte &&
         Shrset[#2] = True

(* 39 *) Cache[#1] = Exclusive &&
         Shrset[#2] = True

(* 40 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1[#1] = Reqs &&
         Chan2[#1] = Empty &&
         Chan2[#2] = Empty &&
         Chan3[#2] = Empty &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 41 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1[#1] = Empty &&
         Chan2[#1] = Empty &&
         Chan2[#2] = Empty &&
         Chan3[#2] = Empty &&
         Cache[#1] = Invalid &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 42 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1[#3] = Reqs &&
         Chan2[#1] = Empty &&
         Chan2[#2] = Empty &&
         Chan3[#2] = Empty &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 43 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1[#3] = Empty &&
         Chan2[#1] = Empty &&
         Chan2[#2] = Empty &&
         Chan3[#2] = Empty &&
         Cache[#3] = Invalid &&
         Shrset[#1] = True &&
         Shrset[#2] = True