(*-------------------------------------------*
            |                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.

[2] Y.Isobe, M.Roggenbach, and S.Gruner, Extending CSP-Prover by
    deadlock-analysis: Towards the verification of systolic arrays,
    FOSE 2005 (12th Workshop on Foundation of Software Engineering),
    Japanese Lecture Notes Series 31, pp.257-266, Kindai-kagaku-sha,
    November 2005.