src/HOLCF/IOA/meta_theory/LiveIOA.thy
author wenzelm
Fri Sep 02 17:23:59 2005 +0200 (2005-09-02)
changeset 17233 41eee2e7b465
parent 14981 e73f8140af78
child 19741 f65265d71426
permissions -rw-r--r--
converted specifications to Isar theories;
     1 (*  Title:      HOLCF/IOA/meta_theory/LiveIOA.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4 *)
     5 
     6 header {* Live I/O automata -- specified by temproal formulas *}
     7 
     8 theory LiveIOA
     9 imports TLS
    10 begin
    11 
    12 defaultsort type
    13 
    14 types
    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))>"
    41 
    42 
    43 liveexecutions_def:
    44    "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    45 
    46 livetraces_def:
    47   "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    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 ML {* use_legacy_bindings (the_context ()) *}
    61 
    62 end