A development snapshot (4.00) of CSP-Prover 4.0

(to CSP-Prover's homepage)

Introduction

We theoretically studied how to express recursions by replicated internal choices instead of process names in CSP-Prover-3.0, and then we got some interesting results. However, now we realized that it would be better to use process names for expressing recursions more naturally in practice. Therefore, the next version of CSP-Prover would includes process names in a more smart way than the previous versions 1 and 2. This is a development snapshot, but all the theory-files have already been available.

Download

You can download a development snapshot of the next version of CSP-Prover:              download [CSP-Prover-4.00.tar.gz] (223KB) (04/04/2007--)


Test CSP-Prover-4.00

This version is a development snapshot of ver.4.0, but it has almost been stable. You can test to prove that ep2 is deadlock free by CSP-Prover as follows:

It is assumed that "CSP-Prover-4.00" has been downloaded and has been unpacked (e.g. tar zxvf CSP-Prover-4.00.tar.gz) to the directory (or your appropriate directory:

   ~/tool/CSP-Prover-4.00

The directory CSP-Prover-4.00 has the tree shown in the following Figure:

     CSP-Prover-4.00 ---+--- CSP      (README)
                        |
                        +--- CSP_T    (README)
                        |
                        +--- CSP_F    (README)
                        |
                        +--- FNF_F    (README)
                        |
                        +--- DFP      (README)
                        |
                        +--- ep2      (README)
                        |
                        +--- DM       (README)
                        |
                        +--- SA_Kung  (README)
                        |
                        +--- Test     (README)

At first, it would be better to make heap files of CSP, CSP_T, CSP_F, FNF_F, and DFP by

       make_heaps

at ~/tool/CSP-Prover-4.00 (it requires Isabelle(2005)/HOL-Complex).

The deadlock freedom of ep2 can be proven as follows:

  1. Execute ProofGeneral (2005) with CSP_F as follows:

      Isabelle -l CSP_F

    at ~/tool/CSP-Prover-4.00/ep2

  2. Load the theory file "ep2_nucleus.thy" by C-x C-f.

  3. Prove the theorem by C-c C-n until the bottom.
    (or Finish the proof by C-c C-b at one step)
If you cannot use ProofGeneral, then you can also start isabelle with CSP_F as follows:

       isabelle -I CSP_F

at ~/tool/CSP-Prover-4.00/ep2 in a shell window. Then, cut and past commands from ep2_nucleus.thy to the shell window step by step.

Last modified: 04 April 2007
(since 04/04/2007)