Flash_buggy
Safety properties
Below are the safety properties we want to verify, in negated form.
∃ p. ( CacheState_home = CACHE_E ∧ CacheState[p] = CACHE_E )
∃ i,j. i≠j ∧ ( CacheState[i] = CACHE_E ∧ CacheState[j] = CACHE_E )
Options used
-brab 2 -forward-depth 6
Trace to unsafe state
pi_Remote_GetX(#2) -> ni_Local_GetX_PutX_3(#2) ->
ni_Remote_PutX(#2) -> pi_Remote_GetX(#1) ->
pi_Local_Get_Get() -> ni_Local_GetX_PutX_1(#1) ->
ni_Remote_PutX(#1) ->
unsafe[1]
= CacheState[#1] = CACHE_E &&
CacheState[#2] = CACHE_E
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.Initial
states are shown in a green circle and the error trace follows
nodes colored in pink.
