author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4559 | 5 |
|
12218 | 6 |
Live I/O automata -- specified by temproal formulas. |
4559 | 7 |
*) |
8 |
||
4816 | 9 |
LiveIOA = TLS + |
4559 | 10 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
4559 | 12 |
|
13 |
types |
|
14 |
||
15 |
('a,'s)live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" |
|
16 |
||
17 |
consts |
|
18 |
||
19 |
validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" |
|
20 |
||
21 |
WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" |
|
22 |
SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" |
|
23 |
||
24 |
liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" |
|
25 |
livetraces :: "('a,'s)live_ioa => 'a trace set" |
|
26 |
live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
|
27 |
is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
|
28 |
||
29 |
||
30 |
defs |
|
31 |
||
32 |
validLIOA_def |
|
33 |
"validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)" |
|
34 |
||
35 |
||
36 |
WF_def |
|
37 |
"WF A acts == <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>" |
|
38 |
||
39 |
SF_def |
|
40 |
"SF A acts == [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>" |
|
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
41 |
|
4559 | 42 |
|
43 |
liveexecutions_def |
|
44 |
"liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}" |
|
45 |
||
46 |
livetraces_def |
|
10835 | 47 |
"livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" |
4559 | 48 |
|
49 |
live_implements_def |
|
50 |
"live_implements CL AM == (inp (fst CL) = inp (fst AM)) & |
|
51 |
(out (fst CL) = out (fst AM)) & |
|
52 |
livetraces CL <= livetraces AM" |
|
53 |
||
54 |
is_live_ref_map_def |
|
55 |
"is_live_ref_map f CL AM == |
|
56 |
is_ref_map f (fst CL ) (fst AM) & |
|
57 |
(! exec : executions (fst CL). (exec |== (snd CL)) --> |
|
58 |
((corresp_ex (fst AM) f exec) |== (snd AM)))" |
|
59 |
||
60 |
||
61 |
end |