equal
deleted
inserted
replaced
1 (* Title: HOL/Modelcheck/Example.thy |
1 (* Title: HOL/Modelcheck/Example.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 |
|
6 Example: |
|
7 |
|
8 000 ---> 100 ---> 110 |
|
9 <--- |
|
10 *) |
5 *) |
11 |
6 |
12 Example = CTL + MCSyn + |
7 Example = CTL + MCSyn + |
13 |
8 |
14 |
9 |
17 |
12 |
18 consts |
13 consts |
19 |
14 |
20 INIT :: "state pred" |
15 INIT :: "state pred" |
21 N :: "[state,state] => bool" |
16 N :: "[state,state] => bool" |
22 reach,restart,infinitely,toggle:: "state pred" |
17 reach:: "state pred" |
23 |
18 |
24 defs |
19 defs |
25 |
20 |
26 INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
21 INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))" |
27 |
22 |
29 (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | |
24 (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) | |
30 ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | |
25 ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) | |
31 ( x1 & ~x2 & ~x3 & y1 & y2 & y3) " |
26 ( x1 & ~x2 & ~x3 & y1 & y2 & y3) " |
32 |
27 |
33 reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
28 reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))" |
34 |
29 |
35 (* always possible to return to the start state: has to be false *) |
|
36 restart_def "restart == AG N (EF N (%x. INIT x))" |
|
37 |
|
38 (* infinitily often through the second state: has to be true *) |
|
39 inf_def "infinitely == AG N (AF N (%x. fst x & ~ fst (snd x) & ~ snd (snd x)))" |
|
40 |
|
41 (* There is a path on which toggling between the first and second state that passes |
|
42 infinitely often the first state: should be true, nested fixpoints!! *) |
|
43 toggle_def "toggle == FairEF N (%x. ~ fst (snd x) & ~ snd (snd x)) INIT" |
|
44 |
30 |
45 end |
31 end |
46 |
|