author | nipkow |
Tue, 09 Jan 2001 15:36:30 +0100 | |
changeset 10835 | f4745d77e620 |
parent 4816 | 64f075872f69 |
child 12218 | 6597093b77e7 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/LiveIOA.thy |
2 |
ID: $Id$ |
|
3 |
Author: Olaf M"uller |
|
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
6 |
Live I/O automata -- specified by temproal formulas |
|
7 |
||
8 |
*) |
|
9 |
||
4816 | 10 |
LiveIOA = TLS + |
4559 | 11 |
|
12 |
default term |
|
13 |
||
14 |
types |
|
15 |
||
16 |
('a,'s)live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" |
|
17 |
||
18 |
consts |
|
19 |
||
20 |
validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" |
|
21 |
||
22 |
WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" |
|
23 |
SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" |
|
24 |
||
25 |
liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" |
|
26 |
livetraces :: "('a,'s)live_ioa => 'a trace set" |
|
27 |
live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
|
28 |
is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" |
|
29 |
||
30 |
||
31 |
defs |
|
32 |
||
33 |
validLIOA_def |
|
34 |
"validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)" |
|
35 |
||
36 |
||
37 |
WF_def |
|
38 |
"WF A acts == <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>" |
|
39 |
||
40 |
SF_def |
|
41 |
"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
|
42 |
|
4559 | 43 |
|
44 |
liveexecutions_def |
|
45 |
"liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}" |
|
46 |
||
47 |
livetraces_def |
|
10835 | 48 |
"livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}" |
4559 | 49 |
|
50 |
live_implements_def |
|
51 |
"live_implements CL AM == (inp (fst CL) = inp (fst AM)) & |
|
52 |
(out (fst CL) = out (fst AM)) & |
|
53 |
livetraces CL <= livetraces AM" |
|
54 |
||
55 |
is_live_ref_map_def |
|
56 |
"is_live_ref_map f CL AM == |
|
57 |
is_ref_map f (fst CL ) (fst AM) & |
|
58 |
(! exec : executions (fst CL). (exec |== (snd CL)) --> |
|
59 |
((corresp_ex (fst AM) f exec) |== (snd AM)))" |
|
60 |
||
61 |
||
62 |
end |