Wed, 03 Nov 1999 17:40:26 +0100
changeset 7994 1e9a13d5375a
parent 7993 4d176363e39a
child 7995 612352dad48e
--- a/src/HOL/Modelcheck/README.html	Tue Nov 02 17:28:24 1999 +0100
+++ b/src/HOL/Modelcheck/README.html	Wed Nov 03 17:40:26 1999 +0100
@@ -1,28 +1,29 @@
-<H3>Invoking Model Checkers in Isabelle/HOL </H3>
+<h2>Invoking Model Checkers in Isabelle/HOL</h2>
-Authors:     Olaf M&uuml;ller, Jan Philipps, Robert Sandner<BR>
-Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
+This directory contains the basic setup for integration of some model
+checkers in Isabelle/HOL, together with a few basic examples.
-This directory contains four theories:
-  <li>MuCalculus: A formalization of the relational mu calculus using the fixed point 
-      theory Lfp and Gfp of HOL.<P>
-  <li>CTL: A formulation of some CTL operators in the mu calculus.<P>
-  <li>MCSyn: The definition of the output syntax "Eindhoven" tailored for the the model checker due to G. Janssen from Eindhoven using
-         the print_mode facilities provided by Isabelle. <P>
-  <li>Example: A simple reachability property is formulated in the mu calculus and checked 
-       by the model checker simply by invoking the tactic mc_tac.
+Currently, best results are achieved with the <a
+href=""><em>Mucke</em></a> model
+checker (version 0.3.5 is known to work).  Theory <tt>MuCalculus</tt>
+provides the syntactic and oracle interfaces, while
+<tt>MuckeExample1</tt> and <tt>MuckeExample2</tt> demonstrate the
+model checker tactic <tt>mc_mucke_tac</tt> at work.
-Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="">model checker binary</A>) as a Sparc SunOS4 binary which also runs under Solaris2.x, or directly from Eindhoven (<A HREF="">model checker sources</A>), where you get the C sources and documentation. 
+In order to support more realistic applications, the <a
+session augments this basic mechanism by further infrastructure to
+support proofs about I/O automata.  There is a separate <a
+available, describing model checking in Isabelle/IOA in more detail.