# HG changeset patch # User wenzelm # Date 877001284 -7200 # Node ID acc1347cf2a088ec5a7949f25d987f4fd7ce7ce1 # Parent 6d7df9b98537373b3f85a5a43eea48a5ab7ddb03 revert to 1.3; diff -r 6d7df9b98537 -r acc1347cf2a0 src/HOL/Modelcheck/Example.thy --- 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 -