src/HOLCF/IOA/meta_theory/LiveIOA.thy
author mueller
Wed Jan 14 16:38:04 1998 +0100 (1998-01-14)
changeset 4577 674b0b354feb
parent 4559 8e604d885b54
child 4816 64f075872f69
permissions -rw-r--r--
added thms wrt weakening and strengthening in Abstraction;
     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   
    10 LiveIOA = IOA + TLS + 
    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))>"
    42  
    43 
    44 liveexecutions_def
    45    "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    46 
    47 livetraces_def
    48   "livetraces AP == {mk_trace (fst AP)`(snd ex) | ex. ex:liveexecutions AP}"
    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