🚀 go-pugleaf

I have a question about divergences in Hoare's CSP.

I think it is easy to show that the set:

   {s | for all t in A*, X in 2^A : (s^t,X) in failures (P)}

contains divergences(P).

My question is what reason is there not to define divergences(P) to be
{s | for all t in A*, X in 2^A : (s^t,X) in failures (P)}?

On page 130, nondeterministic processes are defined to be triples
(A,F,D) satisfying 7 conditions (C0-C6).  If the divergences were
defined in terms of the failures, then only a pair (A,F) would be
needed and three of the seven conditions (C4-C6) would be consequences
of the definition of D rather than axioms.  This would give a basic
model of pairs with 4 axioms rather than tuples with 7 axioms which would
seem to be an advantage.

The only advantage I can see to keeping D is that it is more general.
But, I cannot see any use for using a D other than the one I have
defined in terms of A and F.  If there really is no use making other
choices for D, then doesn't it make sense to use the simpler model?
If there are other meaningful choices for D, I would be interested
in knowing what they are.

Since there probably is little interest in this, it might be best to respond
through e-mail...

Todd Fine
fine@sctc.com