(*-------------------------------------------*
            |                DFP package                |
            |                 July 2005                 |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

1 Introduction 

CSP-Prover is extended by DFP (Deadlock Freedom Proof) package, which
contains definitions, lemmas, and theorems given in [1] for proving
deadlock freedom of networks.

2 Theory files

DFP_subseteqEX.thy : provides lemmas for proving semantic networks,
DFP_Network.thy    : defines networks,
DFP_Deadlock.thy   : provides deadlock and deadlock freedom,
DFP_Block.thy      : defines "blocked" and proves the properties,
DFP_Proof_Rule1.thy: provides Rule1 in [1],
DFP.thy            : the top of DFP

3 How to use DFP.

(note: The CSP_F heap file is required for DFP)

(1) To build the heap file for DFP:
    isatool usedir -b CSP_F DFP

(2) To start Isabelle with DFP:
    isabelle -I DFP

(3) To start ProofGeneral with DFP:
    Isabelle -l DFP

(4) To use DFP:
    theory test = DFP:

References

[1] A.W.Roscoe and N.Dathi, "The pursuit of deadlock freedom",
    Information and Computation, Vol.75, No.3, pp.289-327, 1987.