In order to check if a process Impl refines (in a particular semantic model)
a process Spec, FDR firstly converts Impl and Spec into labelled
transition systems, as described in Compilation. FDR then
normalises the specification machine, as described in normal. FDR then
explores the states of these processes in breadth-first order, checking that the
states are related according to the semantic model. As soon as FDR finds a
counterexample it immediately reports it. Thus, thanks to the breadth-first
order, any counterexample that FDR returns will be minimal in the length of the
trace (including taus).
In order to understand exactly how FDR visits state pairs during a refinement check, consider the following script:
channel a, b, c
P1 = a -> P2
P2 = P3 |~| P4
P3 = b -> P2
P4 = a -> P1
Q1 = a -> Q2
Q2 = b -> Q1
assert Q1 [T= P1
FDR initialises the search by looking at the state pair (Q1, P1) (nb. state
pairs consist of a specification state and an implementation state). In the
traces model, FDR only has to check that the events (excluding tau) offered by
P1 are a subset of those offered by Q1, which is clearly the cases here.
Hence, FDR now adds the successor state pairs for each event offered by P1
to the search. In this case, there is only one successor state pair after a,
(Q2, P2).
When considering the state pair (Q2, P2) note that P2 does not offer any
visible events, and therefore the event check is trivially true. FDR now needs
to add any new state pairs to the search. In this case, the two state pairs
(Q2, P3) and (Q2, P4) are added to the search. Note that the
specification part of the state pair is kept the same because the implementation
performs a tau. FDR will now consider the new state pairs. In particular, when
it considers (Q2, P4) FDR will find a counterexample since the events
offered by P4 are not a subset of those offered by Q2.
In order to reconstruct the trace that the invalid state pair was reached by,
FDR stores a parent state pair of each state pair that it finds during the
search. Thus, in the above example, FDR will set the parent of (Q2, P4)
as (Q2, P2) and the parent of (Q2, P2) to (Q1, P1). Thus, FDR can
reconstruct the counterexample trace by finding events that transition between
(Q1, P1) and (Q2, P2), and (Q2, P2) and (Q2, P4). This will
yield the trace <a, tau>, in this case.
A counterexample to a refinement assertion consists of a trace leading to a particular state pair that are not related according the to semantic model in use. Thus, if the traces model is in use, then this must mean that the implementation can perform an event that the specification cannot. If the failures model is in use, then either the above case applies, or the implementation can refuse a set of events that the specification cannot. If the failures-divergences model is in use, then this must mean that either one of the above cases applies, or the implementation is divergent but the specification is not.
If FDR is asked to generate multiple counterexamples then this motivates the question of what FDR considers distinct counterexamples to be. In all cases, only a single counterexample will be generated from a single state pair. Thus, if a state pair is reachable via two different traces then only one counterexample will be generated, regardless of the number requested. Further, once FDR has found a counterexample for a given state pair, it does not look at successors of the state pair to see if they are counterexamples. Thus, for FDR to report two distinct counterexamples the counterexamples must be distinct state pairs, and the second state pair must be reachable via a path that does not include the first state pair. For example, the following has two counterexamples since the two STOP states are reachable via distinct paths:
P1 = STOP |~| P2
P2 = STOP
assert P1 :[deadlock free [F]]
However, the following only has one counterexample, since the second invalid state pair is only reachable via the first invalid state pair:
P1 = a -> P2 [] b -> STOP
P2 = a -> P1
Spec = a -> Spec
assert Spec [T= P1
Note that both P1 and` P2 violate the property, but P2 is only
reachable via P1 and thus is not considered.
As noted above, thanks to the breadth-first ordering that FDR visits the state
pairs in, FDR will always pick the counterexample that is reachable in the
fewest events (either tau or a visible event). Whilst this might imply that the
counterexample returned is chosen deterministically, this is not the case when
FDR is being used in parallel mode (i.e. refinement.bfs.workers is
greater than 1) for two reasons:
The predecessor state pair of each state pair is chosen by a race between the different processor cores on each ply. For example, if two different cores both discover the same state pair on the same ply, then the state pair that is marked as the new state pair’s predecessor is chosen non-deterministically. This can result in a different trace being returned. The following script should exhibit this behaviour:
channel a, b, c
P = a -> b -> Q [] b -> a -> Q
Q = c -> STOP
R = a -> R [] b -> R [] c -> R
assert R [F= P
Note that there is precisely one state that violates the refinement, Q,
but there are two different routes to Q, via either <a, b> or <b,
a>. Hence, since the states b -> Q and a -> Q are discovered on the
same ply of the breadth-first search the winner will be chosen
non-deterministically (assuming that they are visited by different cores).
This should result in FDR non-deterministically returning either the
counterexample trace <a, b, c> or <b, a, c>.
On each ply of the search, there is essentially a race between the processor cores to find a counterexample: the first core that finds a counterexample wins. For example, consider the following refinement check:
channel a, b
P = a -> STOP |~| b -> STOP
assert STOP [T= P
There are two different counterexamples to this assertion: either the event
a can be performed, or the event b. Since these counterexamples are
both found on the second ply of the search (the first ply simply explores
the tau transitions available from the starting state), FDR will pick the
counterexample non-deterministically, providing the two different states are
picked by different cores.
In general use, the fact that different counterexamples are produced should
hopefully not be an issue. Unfortunately, there is no efficient way to make a
parallel version of FDR deterministically return the same counterexample. If it
is important that the same counterexample is returned each time then
refinement.bfs.workers should be set to 1, thus disabling the
parallel refinement checker. This will obviously result in a decrease in
performance, but it does mean that the same counterexample will always be
returned.