--- 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
--- 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