Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Modelcheck/README.html
author berghofe
Fri, 24 Jul 1998 13:19:38 +0200
changeset 5184 9b8547a9496a
parent 3279 815ef5848324
child 7994 1e9a13d5375a
permissions -rw-r--r--
Adapted to new datatype package.

<HTML><HEAD><TITLE>HOL/Modelcheck/Readme</TITLE></HEAD><BODY>

<H3>Invoking Model Checkers in Isabelle/HOL </H3>

Authors:     Olaf M&uuml;ller, Jan Philipps, Robert Sandner<BR>
Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>


This directory contains four theories:

<UL>
  <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.
</UL>

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="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">model checker binary</A>) as a Sparc SunOS4 binary which also runs under Solaris2.x, or directly from Eindhoven (<A HREF="http://www.es.ele.tue.nl/geert/research/research_index.html">model checker sources</A>), where you get the C sources and documentation. 



</BODY></HTML>
isabelle