# HG changeset patch
# User mueller
# Date 876990596 -7200
# Node ID d93c62ec97a6694fc9cde0278a14eee3c84f8ebe
# Parent  de18c0c1141c28513d6b79253c89724358371567
lala

diff -r de18c0c1141c -r d93c62ec97a6 src/HOL/Modelcheck/CTL.thy
--- a/src/HOL/Modelcheck/CTL.thy	Thu Oct 16 10:22:37 1997 +0200
+++ b/src/HOL/Modelcheck/CTL.thy	Thu Oct 16 10:29:56 1997 +0200
@@ -15,17 +15,29 @@
 
   CEX   ::"['a trans,'a pred, 'a]=>bool" 
   EG    ::"['a trans,'a pred]=> 'a pred" 
+  EU    ::"['a trans,'a pred,'a pred]=> 'a pred" 
+  EF    ::"['a trans,'a pred]=> 'a pred" 
+  AX    ::"['a trans,'a pred]=> 'a pred" 
+  AF    ::"['a trans,'a pred]=> 'a pred" 
+  AG    ::"['a trans,'a pred]=> 'a pred" 
+  AU    ::"['a trans,'a pred,'a pred]=> 'a pred" 
+FairEG  ::"['a trans,'a pred,'a pred]=> 'a pred" 
 
 
 
 defs
  
-CEX_def  "CEX N f u == (? v. (f v & (u,v):N))"
-EG_def   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
-
-
+CEX_def  "CEX N f x  == (? y. (f y & (x,y):N))"
+EG_def   "EG N f     == nu (% Q. % x.(f x & CEX N Q x))"
+EU_def   "EU N f g   == mu (% Q. % x.(g x | (g x & CEX N Q x)))"
+EF_def   "EF N f     == EU N (%x. True) f"
 
-
+AX_def   "AX N f x   == ~ CEX N (%x. ~ f x) x"
+AF_def   "AF N f x   == ~ EG N (%x. ~ f x) x"
+AG_def   "AG N f x   == ~ EF N (%x. ~ f x) x"
+AU_def   "AU N f g x == ~ EU N (%x. ~ g x) (%x. (~ f x) & (~ g x)) x & AF N g x"
 
-
+FairEG_def "FairEG N f fc == nu (% Q. %x. (f x & 
+             (mu (% P. CEX N (%y. f y & ((fc y & Q y) | P y)))) x))" 
+ 
 end
diff -r de18c0c1141c -r d93c62ec97a6 src/HOL/Modelcheck/Example.thy
--- a/src/HOL/Modelcheck/Example.thy	Thu Oct 16 10:22:37 1997 +0200
+++ b/src/HOL/Modelcheck/Example.thy	Thu Oct 16 10:29:56 1997 +0200
@@ -2,6 +2,11 @@
     ID:         $Id$
     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     Copyright   1997  TU Muenchen
+
+Example:
+
+    000    --->   100    ---> 110
+           <---    
 *)
 
 Example = CTL + MCSyn + 
@@ -14,7 +19,7 @@
 
   INIT :: "state pred"
   N    :: "[state,state] => bool"
-  reach:: "state pred"
+  reach,restart,infinitely,toggle:: "state pred"
 
 defs
   
@@ -26,7 +31,16 @@
 	                ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)    "
   
   reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
-  
+
+  (* always possible to return to the start state: has to be false *)
+  restart_def "restart == AG N (EF N (%x. INIT x))"
+
+  (* infinitily often through the second state: has to be true *)
+  inf_def "infinitely == AG N (AF N (%x. fst x & ~ fst (snd x) & ~ snd (snd x)))"
+
+  (* There is a path on which toggling between the first and second state that passes 
+     infinitely often the first state: should be true, nested fixpoints!! *)
+  toggle_def "toggle == FairEF N (%x. ~ fst (snd x) & ~ snd (snd x)) INIT"
 
 end