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

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

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

(* 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 *) Cache[#1] = Exclusive &&
        Chan3[#1] = Invack

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

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

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

(* 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 = Empty1 &&
         Chan3[#1] = Invack

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

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

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

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

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

(* 24 *) Flag = True &&
         Chan3[#1] = Invack

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

(* 26 *) Flag = True &&
         Chan2[#1] = Inv

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

(* 28 *) Curcmd = Reqs &&
         Flag = False &&
         Chan3[#1] = Invack &&
         Chan3[#2] = Invack

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

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

(* 31 *) Exgntd = True &&
         Curcmd = Reqs &&
         Flag = False &&
         Chan2[#1] = Empty2 &&
         Chan3[#2] = Invack &&
         Invset[#1] = True

(* 32 *) Curcmd = Reqs &&
         Flag = False &&
         Chan2[#1] = Inv &&
         Chan2[#2] = Inv &&
         Chan3[#2] = Empty3

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

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

(* 35 *) Exgntd = True &&
         Curcmd = Reqs &&
         Flag = False &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Inv &&
         Chan3[#2] = Empty3 &&
         Invset[#1] = True

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

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

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

(* 39 *) Exgntd = True &&
         Curcmd = Reqs &&
         Flag = False &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Invset[#1] = True &&
         Invset[#2] = True

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

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

(* 42 *) Exgntd = True &&
         Curcmd = Reqs &&
         Flag = True &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Invset[#1] = True &&
         Invset[#1] = Shrset[#1] &&
         Invset[#2] = True &&
         Invset[#2] = Shrset[#2]

(* 43 *) Exgntd = True &&
         Curcmd = Empty1 &&
         Flag = False &&
         Chan1[#1] = Reqs &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 44 *) Exgntd = True &&
         Curcmd = Reqs &&
         Flag = True &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Shrset[#1] = True &&
         Invset[#2] = True &&
         Invset[#2] = Shrset[#2]

(* 45 *) Curcmd = Empty1 &&
         Flag = True

(* 46 *) Exgntd = True &&
         Curcmd = Empty1 &&
         Flag = False &&
         Cache[#1] = Invalid &&
         Chan1[#1] = Empty1 &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 47 *) Exgntd = True &&
         Curcmd = Reqs &&
         Flag = True &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 48 *) Exgntd = True &&
         Curcmd = Empty1 &&
         Flag = False &&
         Chan1[#3] = Reqs &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 49 *) Exgntd = True &&
         Curcmd = Empty1 &&
         Flag = False &&
         Cache[#3] = Invalid &&
         Chan1[#3] = Empty1 &&
         Chan2[#1] = Empty2 &&
         Chan2[#2] = Empty2 &&
         Chan3[#2] = Empty3 &&
         Shrset[#1] = True &&
         Shrset[#2] = True