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