DIET: Implementing FULL using Ergo

To use the Ergo based model checker for FULL you need the most recent releases of Ergo and Qu-prolog. These are available from http://www.svrc.uq.edu.au/Software/.

Theory files required are contained in latest.tgz. The contents of this archive is as follows:
drwxr-xr-x 1002/1002 0 Nov 16 04:01 2002 latest/
drwxr-xr-x 1002/1002 0 Nov 14 06:02 2002 latest/sts/
-rw-r--r-- 1002/1002 88 Apr 25 22:48 2001 latest/sts/wi_sts_op.ql
-rw-r--r-- 1002/1002 75 Nov 14 06:02 2002 latest/sts/wi_support.gum
-rw-r--r-- 1002/1002 116 Nov 15 01:18 2002 latest/b1
-rw-r--r-- 1002/1002 1126 Nov 15 05:05 2002 latest/b1_sts.thy
-rw-r--r-- 1002/1002 6637 Nov 15 05:05 2002 latest/e1_sts.thy
-rw-r--r-- 1002/1002 725 Apr 25 22:41 2001 latest/eg1
-rw-r--r-- 1002/1002 4689 Nov 15 03:41 2002 latest/gen_sts_theory.ql
-rw-r--r-- 1002/1002 4750 Nov 15 05:05 2002 latest/sts.thy
-rw-r--r-- 1002/1002 721 Nov 16 04:00 2002 latest/sts_proofs.thy
-rw-r--r-- 1002/1002 16744 Nov 15 04:35 2002 latest/sts_support.ql
-rw-r--r-- 1002/1002 7436 Nov 16 03:41 2002 latest/sts_tactics.gum
-rw-rw-r-- 1002/1002 5799 Nov 15 03:44 2002 latest/eg1_sts.thy
-rwxrwxr-x 1002/1002 77 Nov 15 03:41 2002 latest/gen_sts_theory

This includes the simple example files for the one place buffer (b1) and the example from the Computer Journal paper (eg1).

Find out more about the DIET project achievements.

[] Research   [] Teaching   [] CV   [] Personal   [Home] Home
Dr Carron Shankland    Email: ces@cs.stir.ac.uk [email me]    Last revision: 18th November 2002