src/HOLCF/IOA/meta_theory/LiveIOA.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12338 de0f4a63baa5
child 17233 41eee2e7b465
permissions -rw-r--r--
Merged in license change from Isabelle2004
mueller@4559
     1
(*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
mueller@4559
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@4559
     4
wenzelm@12218
     5
Live I/O automata -- specified by temproal formulas.
mueller@4559
     6
*) 
mueller@4559
     7
  
oheimb@4816
     8
LiveIOA = TLS + 
mueller@4559
     9
wenzelm@12338
    10
default type
mueller@4559
    11
mueller@4559
    12
types
mueller@4559
    13
mueller@4559
    14
 ('a,'s)live_ioa       = "('a,'s)ioa * ('a,'s)ioa_temp"
mueller@4559
    15
 
mueller@4559
    16
consts
mueller@4559
    17
mueller@4559
    18
validLIOA   :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool"
mueller@4559
    19
mueller@4559
    20
WF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
mueller@4559
    21
SF         :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
mueller@4559
    22
mueller@4559
    23
liveexecutions    :: "('a,'s)live_ioa => ('a,'s)execution set"
mueller@4559
    24
livetraces        :: "('a,'s)live_ioa => 'a trace set"
mueller@4559
    25
live_implements   :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
mueller@4559
    26
is_live_ref_map   :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
mueller@4559
    27
mueller@4559
    28
 
mueller@4559
    29
defs
mueller@4559
    30
mueller@4559
    31
validLIOA_def
mueller@4559
    32
  "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
mueller@4559
    33
mueller@4559
    34
mueller@4559
    35
WF_def
mueller@4559
    36
  "WF A acts ==  <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
mueller@4559
    37
mueller@4559
    38
SF_def
mueller@4559
    39
  "SF A acts ==  [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
mueller@4577
    40
 
mueller@4559
    41
mueller@4559
    42
liveexecutions_def
mueller@4559
    43
   "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
mueller@4559
    44
mueller@4559
    45
livetraces_def
nipkow@10835
    46
  "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
mueller@4559
    47
mueller@4559
    48
live_implements_def
mueller@4559
    49
  "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & 
mueller@4559
    50
                            (out (fst CL) = out (fst AM)) &
mueller@4559
    51
                            livetraces CL <= livetraces AM"
mueller@4559
    52
mueller@4559
    53
is_live_ref_map_def
mueller@4559
    54
   "is_live_ref_map f CL AM ==  
mueller@4559
    55
            is_ref_map f (fst CL ) (fst AM) & 
mueller@4559
    56
            (! exec : executions (fst CL). (exec |== (snd CL)) --> 
mueller@4559
    57
                                           ((corresp_ex (fst AM) f exec) |== (snd AM)))"
mueller@4559
    58
mueller@4559
    59
mueller@4559
    60
end