German_pfs

Cubicle model

Safety properties

Below are the safety properties we want to verify, in negated form.
∃ z1,z2. z1≠z2 ∧ ( Cache[z1] = Exclusive ∧ Cache[z2] ≠ Invalid )

Options used

-brab 2

Inferred invariants

All invariants are shown in their negated form, where #1 and #2 are distinct existentially quantified variables. 

Curcmd = Empty1 && Flag = True

Cache[#1] = Exclusive && Shrset[#2] = True

Chan2[#1] = Gnte && Shrset[#2] = True

Cache[#1] = Exclusive && Invset[#2] = True

Chan2[#1] = Gnte && Invset[#2] = True

Exgntd = True && Chan2[#1] = Gnts

Cache[#1] = Exclusive && Chan2[#2] = Inv

Chan2[#1] = Gnte && Chan2[#2] = Inv

Cache[#1] = Exclusive && Chan3[#2] = Invack

Chan2[#1] = Gnte && Chan3[#2] = Invack

Flag = True && Chan2[#1] = Inv

Chan2[#1] = Inv && Invset[#1] = True

Flag = True && Chan3[#1] = Invack

Chan3[#1] = Invack && Invset[#1] = True

Curcmd = Empty1 && Chan2[#1] = Inv

Chan2[#1] = Inv && Chan3[#1] = Invack

Shrset[#1] = False && Invset[#1] = True

Exgntd = False && Curcmd = Reqs && Chan2[#1] = Inv

Curcmd = Empty1 && Chan3[#1] = Invack

Chan2[#1] = Inv && Shrset[#1] = False

Exgntd = False && Curcmd = Reqs && Chan3[#1] = Invack

Chan3[#1] = Invack && Shrset[#1] = False

Chan2[#1] = Gnts && Chan3[#1] = Invack

Chan2[#1] = Gnte && Chan3[#1] = Invack

Chan2[#1] = Gnte && Shrset[#1] = False

Cache[#1] <> Invalid && Chan3[#1] = Invack

Chan2[#1] = Gnts && Shrset[#1] = False

Exgntd = False && Chan2[#1] = Gnte

Cache[#1] = Exclusive && Chan3[#1] = Invack

Chan2[#1] = Gnte && Chan2[#2] = Gnte

Cache[#1] <> Invalid && Shrset[#1] = False

Chan2[#1] = Gnte && Chan2[#2] = Gnts

Exgntd = False && Cache[#1] = Exclusive

Cache[#2] <> Invalid && Chan2[#1] = Gnte

Cache[#1] = Exclusive && Chan2[#2] = Gnts

You can find the list of all invariants that can be extracted from BRAB here (also in negated form), this collection being inductive.

Search graph

The algorithm starts from the formula located at the bottom, inside a red octagon. Variables #1, #2, … that appear in the nodes are distinct skolem variables so we show a formula φ(#1, #2) as equivalent to ∃ z1, z2. z1 ≠ z2 ∧ φ(z1, z2). Plain black edges represent pre-image relations and are annotated by the transition instance that was considered. Black circles denote nodes that were obtained by pre-image computation and were not covered by already visited nodes. The nodes circled in gray are the one that were not useful because they were subsumed by formulas pointed by the gray dashed arrows. Approximations are shown in blue rectangles. Each approximation originates from the node that connects its rectangle with a bold dashed blue edge.