--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/Example.thy Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,33 @@
+(* Title: HOL/Modelcheck/Example.thy
+ ID: $Id$
+ Author: Olaf Mueller, Jan Philipps, Robert Sandner
+ Copyright 1997 TU Muenchen
+*)
+
+Example = MCSyn +
+
+
+types
+ state = "bool * bool * bool"
+
+consts
+
+ INIT :: "state pred"
+ N :: "[state,state] => bool"
+ reach:: "state pred"
+
+defs
+
+ INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+
+ N_def "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
+ y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
+ in (~x1&~x2&~x3 & y1&~y2&~y3) |
+ (x1&~x2&~x3 & ~y1&~y2&~y3) |
+ (x1&~x2&~x3 & y1&y2&y3) "
+
+ reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
+
+
+end
+