src/HOL/Modelcheck/Example.thy
author wenzelm
Thu, 26 Jun 1997 11:14:46 +0200
changeset 3462 3472fa00b1d4
parent 3380 2986e3b1f86a
child 3880 d93c62ec97a6
permissions -rw-r--r--
rearrange pages of ps file to be printed as booklet (duplex);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/Modelcheck/Example.thy
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     2
    ID:         $Id$
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     5
*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     6
3380
2986e3b1f86a trivial changes to incorporate CTL.thy and Example.ML in html file;
mueller
parents: 3225
diff changeset
     7
Example = CTL + MCSyn + 
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     8
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     9
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    10
types
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    11
    state = "bool * bool * bool"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    12
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    13
consts
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    14
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    15
  INIT :: "state pred"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    16
  N    :: "[state,state] => bool"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    17
  reach:: "state pred"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    18
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    19
defs
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    20
  
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    21
  INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    22
3225
cee363fc07d7 little changes
mueller
parents: 3210
diff changeset
    23
   N_def   "N      == % (x1,x2,x3) (y1,y2,y3).
cee363fc07d7 little changes
mueller
parents: 3210
diff changeset
    24
                        (~x1 & ~x2 & ~x3 &   y1 & ~y2 & ~y3) |   
cee363fc07d7 little changes
mueller
parents: 3210
diff changeset
    25
	                ( x1 & ~x2 & ~x3 &  ~y1 & ~y2 & ~y3) |   
cee363fc07d7 little changes
mueller
parents: 3210
diff changeset
    26
	                ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)    "
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    27
  
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    28
  reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    29
  
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    30
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    31
end
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    32