diff -r 87b5dfe00387 -r 982b0668dcbd src/HOL/Modelcheck/README.html --- a/src/HOL/Modelcheck/README.html Mon Jul 12 20:21:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ - - - - - - - - - HOL/Modelcheck - - - - -

Invoking Model Checkers in Isabelle/HOL

- -This directory contains the basic setup for integration of some model -checkers in Isabelle/HOL, together with a few basic examples. - -

- -Currently, best results are achieved with the Mucke model -checker (version 0.3.5 is known to work). Theory MuCalculus -provides the syntactic and oracle interfaces, while -MuckeExample1 and MuckeExample2 demonstrate the -model checker tactic mc_mucke_tac in action. To run the -examples yourself, you only have to point MUCKE_HOME in -Isabelle's etc/settings to the place where the Mucke binary -has been installed. - -

- -In order to support more realistic applications, the HOLCF/IOA/Modelcheck -session augments this basic mechanism by further infrastructure for -proofs about I/O automata. There is a separate paper -available, describing model checking in Isabelle/IOA in more detail. - - - -