src/HOLCF/IOA/meta_theory/Traces.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@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Traces.thy
mueller@3275
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3071
     4
mueller@3071
     5
Executions and Traces of I/O automata in HOLCF.
mueller@3071
     6
*)   
mueller@3071
     7
mueller@3071
     8
		       
mueller@3275
     9
Traces = Sequence + Automata +
mueller@3071
    10
wenzelm@12338
    11
default type
mueller@3071
    12
 
mueller@3071
    13
types  
mueller@3071
    14
   ('a,'s)pairs            =    "('a * 's) Seq"
mueller@3071
    15
   ('a,'s)execution        =    "'s * ('a,'s)pairs"
mueller@3071
    16
   'a trace                =    "'a Seq"
mueller@3521
    17
mueller@3521
    18
   ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
mueller@3521
    19
   'a schedule_module      = "'a trace set * 'a signature"
mueller@3521
    20
   'a trace_module         = "'a trace set * 'a signature"
mueller@3071
    21
 
mueller@3071
    22
consts
mueller@3071
    23
mueller@3071
    24
   (* Executions *)
mueller@3433
    25
mueller@3433
    26
  is_exec_fragC      ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr"
mueller@3433
    27
  is_exec_frag,
mueller@3071
    28
  has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
mueller@3071
    29
  executions    :: "('a,'s)ioa => ('a,'s)execution set"
mueller@3071
    30
mueller@3071
    31
  (* Schedules and traces *)
mueller@3071
    32
  filter_act    ::"('a,'s)pairs -> 'a trace"
mueller@3071
    33
  has_schedule,
mueller@3071
    34
  has_trace     :: "[('a,'s)ioa, 'a trace] => bool"
mueller@3071
    35
  schedules,
mueller@3071
    36
  traces        :: "('a,'s)ioa => 'a trace set"
mueller@3071
    37
  mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
mueller@3071
    38
mueller@4559
    39
  laststate    ::"('a,'s)execution => 's"
mueller@4559
    40
mueller@4559
    41
  (* A predicate holds infinitely (finitely) often in a sequence *)
mueller@4559
    42
mueller@4559
    43
  inf_often      ::"('a => bool) => 'a Seq => bool"
mueller@4559
    44
  fin_often      ::"('a => bool) => 'a Seq => bool"
mueller@4559
    45
mueller@4559
    46
  (* fairness of executions *)
mueller@4559
    47
mueller@4559
    48
  wfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
mueller@4559
    49
  sfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
mueller@4559
    50
  is_wfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
mueller@4559
    51
  is_sfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
mueller@4559
    52
  fair_ex        ::"('a,'s)ioa => ('a,'s)execution => bool"
mueller@4559
    53
mueller@4559
    54
  (* fair behavior sets *)
mueller@4559
    55
 
mueller@4559
    56
  fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
mueller@4559
    57
  fairtraces     ::"('a,'s)ioa => 'a trace set"
mueller@4559
    58
mueller@4559
    59
  (* Notions of implementation *)
mueller@3071
    60
  "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12) 
mueller@4559
    61
  fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
mueller@3071
    62
mueller@3521
    63
  (* Execution, schedule and trace modules *)
mueller@3521
    64
  Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
mueller@3521
    65
  Scheds        ::  "('a,'s)ioa => 'a schedule_module"
mueller@3521
    66
  Traces        ::  "('a,'s)ioa => 'a trace_module"
mueller@3521
    67
mueller@3071
    68
mueller@3071
    69
defs
mueller@3071
    70
mueller@3071
    71
mueller@3071
    72
(*  ------------------- Executions ------------------------------ *)
mueller@3071
    73
mueller@3071
    74
mueller@3433
    75
is_exec_frag_def
nipkow@10835
    76
  "is_exec_frag A ex ==  ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"
mueller@3071
    77
mueller@3433
    78
mueller@3433
    79
is_exec_fragC_def
nipkow@10835
    80
  "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of 
mueller@3071
    81
      nil => TT
mueller@3071
    82
    | x##xs => (flift1 
nipkow@10835
    83
            (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) 
nipkow@10835
    84
             $x)
mueller@3071
    85
   )))" 
mueller@3433
    86
mueller@3433
    87
mueller@3433
    88
mueller@3071
    89
executions_def
mueller@3071
    90
  "executions ioa == {e. ((fst e) : starts_of(ioa)) &               
mueller@3433
    91
                         is_exec_frag ioa e}"
mueller@3071
    92
mueller@3071
    93
mueller@3071
    94
(*  ------------------- Schedules ------------------------------ *)
mueller@3071
    95
mueller@3071
    96
mueller@3071
    97
filter_act_def
mueller@3071
    98
  "filter_act == Map fst"
mueller@3071
    99
mueller@3071
   100
has_schedule_def
mueller@3071
   101
  "has_schedule ioa sch ==                                               
nipkow@10835
   102
     (? ex:executions ioa. sch = filter_act$(snd ex))"
mueller@3071
   103
mueller@3071
   104
schedules_def
mueller@3071
   105
  "schedules ioa == {sch. has_schedule ioa sch}"
mueller@3071
   106
mueller@3071
   107
mueller@3071
   108
(*  ------------------- Traces ------------------------------ *)
mueller@3071
   109
mueller@3071
   110
has_trace_def
mueller@3071
   111
  "has_trace ioa tr ==                                               
nipkow@10835
   112
     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"
mueller@4559
   113
 
mueller@3071
   114
traces_def
mueller@3071
   115
  "traces ioa == {tr. has_trace ioa tr}"
mueller@3071
   116
mueller@3071
   117
mueller@3071
   118
mk_trace_def
mueller@3071
   119
  "mk_trace ioa == LAM tr. 
nipkow@10835
   120
     Filter (%a. a:ext(ioa))$(filter_act$tr)"
mueller@3071
   121
mueller@3071
   122
mueller@4559
   123
(*  ------------------- Fair Traces ------------------------------ *)
mueller@4559
   124
mueller@4559
   125
laststate_def
nipkow@10835
   126
  "laststate ex == case Last$(snd ex) of
wenzelm@12028
   127
                      UU  => fst ex
mueller@4559
   128
                    | Def at => snd at"
mueller@4559
   129
mueller@4559
   130
inf_often_def
nipkow@10835
   131
  "inf_often P s == Infinite (Filter P$s)"
mueller@4559
   132
mueller@4559
   133
(*  filtering P yields a finite or partial sequence *)
mueller@4559
   134
fin_often_def
mueller@4559
   135
  "fin_often P s == ~inf_often P s"
mueller@4559
   136
mueller@4559
   137
(* Note that partial execs cannot be wfair as the inf_often predicate in the 
mueller@4559
   138
   else branch prohibits it. However they can be sfair in the case when all W 
mueller@5976
   139
   are only finitely often enabled: Is this the right model?  
mueller@5976
   140
   See LiveIOA for solution conforming with the literature and superseding this one *)
mueller@4559
   141
wfair_ex_def
mueller@4559
   142
  "wfair_ex A ex == ! W : wfair_of A.  
mueller@4559
   143
                      if   Finite (snd ex) 
mueller@4559
   144
                      then ~Enabled A W (laststate ex)
mueller@4559
   145
                      else is_wfair A W ex"
mueller@4559
   146
mueller@4559
   147
is_wfair_def
mueller@4559
   148
  "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
mueller@4559
   149
                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
mueller@4559
   150
mueller@4559
   151
sfair_ex_def
mueller@4559
   152
  "sfair_ex A ex == ! W : sfair_of A.
mueller@4559
   153
                      if   Finite (snd ex) 
mueller@4559
   154
                      then ~Enabled A W (laststate ex)
mueller@4559
   155
                      else is_sfair A W ex"
mueller@4559
   156
mueller@4559
   157
is_sfair_def
mueller@4559
   158
  "is_sfair A W ex ==  (inf_often (%x. fst x:W) (snd ex)
mueller@4559
   159
                      | fin_often (%x. Enabled A W (snd x)) (snd ex))"
mueller@4559
   160
mueller@4559
   161
fair_ex_def
mueller@4559
   162
  "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"
mueller@4559
   163
mueller@4559
   164
fairexecutions_def
mueller@4559
   165
  "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
mueller@4559
   166
mueller@4559
   167
fairtraces_def
nipkow@10835
   168
  "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"
mueller@4559
   169
mueller@4559
   170
mueller@3071
   171
(*  ------------------- Implementation ------------------------------ *)
mueller@3071
   172
mueller@3071
   173
ioa_implements_def
mueller@3071
   174
  "ioa1 =<| ioa2 ==   
mueller@3071
   175
    (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   
mueller@3071
   176
     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
mueller@3071
   177
      traces(ioa1) <= traces(ioa2))"
mueller@3071
   178
mueller@4559
   179
fair_implements_def
mueller@4559
   180
  "fair_implements C A == inp(C) = inp(A) &  out(C)=out(A) &
mueller@4559
   181
                          fairtraces(C) <= fairtraces(A)"
mueller@4559
   182
mueller@3521
   183
(*  ------------------- Modules ------------------------------ *)
mueller@3521
   184
mueller@3521
   185
Execs_def
mueller@3521
   186
  "Execs A  == (executions A, asig_of A)"
mueller@3521
   187
mueller@3521
   188
Scheds_def
mueller@3521
   189
  "Scheds A == (schedules A, asig_of A)"
mueller@3521
   190
mueller@3521
   191
Traces_def
mueller@3521
   192
  "Traces A == (traces A,asig_of A)"
mueller@3521
   193
mueller@3071
   194
mueller@3071
   195
end