--- a/src/HOL/Modelcheck/Example.thy Thu Oct 16 13:20:31 1997 +0200
+++ b/src/HOL/Modelcheck/Example.thy Thu Oct 16 13:28:04 1997 +0200
@@ -2,11 +2,6 @@
ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
-
-Example:
-
- 000 ---> 100 ---> 110
- <---
*)
Example = CTL + MCSyn +
@@ -19,7 +14,7 @@
INIT :: "state pred"
N :: "[state,state] => bool"
- reach,restart,infinitely,toggle:: "state pred"
+ reach:: "state pred"
defs
@@ -31,16 +26,6 @@
( 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
-