# Theory Traces

Up to index of Isabelle/HOLCF/IOA

theory Traces
imports Sequence Automata
uses [Traces.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/Traces.thy
        ID:         $Id: Traces.thy,v 1.13 2005/09/02 15:24:03 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Executions and Traces of I/O automata in HOLCF *}

    theory Traces
    imports Sequence Automata
    begin

    defaultsort type

    types
       ('a,'s)pairs            =    "('a * 's) Seq"
       ('a,'s)execution        =    "'s * ('a,'s)pairs"
       'a trace                =    "'a Seq"

       ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
       'a schedule_module      = "'a trace set * 'a signature"
       'a trace_module         = "'a trace set * 'a signature"

    consts

       (* Executions *)

      is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr"
      is_exec_frag  ::"[('a,'s)ioa, ('a,'s)execution] => bool"
      has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
      executions    :: "('a,'s)ioa => ('a,'s)execution set"

      (* Schedules and traces *)
      filter_act    ::"('a,'s)pairs -> 'a trace"
      has_schedule  :: "[('a,'s)ioa, 'a trace] => bool"
      has_trace     :: "[('a,'s)ioa, 'a trace] => bool"
      schedules     :: "('a,'s)ioa => 'a trace set"
      traces        :: "('a,'s)ioa => 'a trace set"
      mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"

      laststate    ::"('a,'s)execution => 's"

      (* A predicate holds infinitely (finitely) often in a sequence *)

      inf_often      ::"('a => bool) => 'a Seq => bool"
      fin_often      ::"('a => bool) => 'a Seq => bool"

      (* fairness of executions *)

      wfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
      sfair_ex       ::"('a,'s)ioa => ('a,'s)execution => bool"
      is_wfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
      is_sfair       ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
      fair_ex        ::"('a,'s)ioa => ('a,'s)execution => bool"

      (* fair behavior sets *)

      fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
      fairtraces     ::"('a,'s)ioa => 'a trace set"

      (* Notions of implementation *)
      "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12)
      fair_implements  :: "('a,'s1)ioa => ('a,'s2)ioa => bool"

      (* Execution, schedule and trace modules *)
      Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
      Scheds        ::  "('a,'s)ioa => 'a schedule_module"
      Traces        ::  "('a,'s)ioa => 'a trace_module"

    defs

    (*  ------------------- Executions ------------------------------ *)

    is_exec_frag_def:
      "is_exec_frag A ex ==  ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"

    is_exec_fragC_def:
      "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of
          nil => TT
        | x##xs => (flift1
                (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p))
                 $x)
       )))"

    executions_def:
      "executions ioa == {e. ((fst e) : starts_of(ioa)) &
                             is_exec_frag ioa e}"

    (*  ------------------- Schedules ------------------------------ *)

    filter_act_def:
      "filter_act == Map fst"

    has_schedule_def:
      "has_schedule ioa sch ==
         (? ex:executions ioa. sch = filter_act$(snd ex))"

    schedules_def:
      "schedules ioa == {sch. has_schedule ioa sch}"

    (*  ------------------- Traces ------------------------------ *)

    has_trace_def:
      "has_trace ioa tr ==
         (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"

    traces_def:
      "traces ioa == {tr. has_trace ioa tr}"

    mk_trace_def:
      "mk_trace ioa == LAM tr.
         Filter (%a. a:ext(ioa))$(filter_act$tr)"

    (*  ------------------- Fair Traces ------------------------------ *)

    laststate_def:
      "laststate ex == case Last$(snd ex) of
                          UU  => fst ex
                        | Def at => snd at"

    inf_often_def:
      "inf_often P s == Infinite (Filter P$s)"

    (*  filtering P yields a finite or partial sequence *)
    fin_often_def:
      "fin_often P s == ~inf_often P s"

    (* Note that partial execs cannot be wfair as the inf_often predicate in the
       else branch prohibits it. However they can be sfair in the case when all W
       are only finitely often enabled: Is this the right model?
       See LiveIOA for solution conforming with the literature and superseding this one *)
    wfair_ex_def:
      "wfair_ex A ex == ! W : wfair_of A.
                          if   Finite (snd ex)
                          then ~Enabled A W (laststate ex)
                          else is_wfair A W ex"

    is_wfair_def:
      "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
                         | inf_often (%x.~Enabled A W (snd x)) (snd ex))"

    sfair_ex_def:
      "sfair_ex A ex == ! W : sfair_of A.
                          if   Finite (snd ex)
                          then ~Enabled A W (laststate ex)
                          else is_sfair A W ex"

    is_sfair_def:
      "is_sfair A W ex ==  (inf_often (%x. fst x:W) (snd ex)
                          | fin_often (%x. Enabled A W (snd x)) (snd ex))"

    fair_ex_def:
      "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"

    fairexecutions_def:
      "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"

    fairtraces_def:
      "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"

    (*  ------------------- Implementation ------------------------------ *)

    ioa_implements_def:
      "ioa1 =<| ioa2 ==
        (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
         (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
          traces(ioa1) <= traces(ioa2))"

    fair_implements_def:
      "fair_implements C A == inp(C) = inp(A) &  out(C)=out(A) &
                              fairtraces(C) <= fairtraces(A)"

    (*  ------------------- Modules ------------------------------ *)

    Execs_def:
      "Execs A  == (executions A, asig_of A)"

    Scheds_def:
      "Scheds A == (schedules A, asig_of A)"

    Traces_def:
      "Traces A == (traces A,asig_of A)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## recursive equations of operators

theorem filter_act_UU:

      filter_act·UU = UU

theorem filter_act_nil:

      filter_act·nil = nil

theorem filter_act_cons:

      filter_act·(x>>xs) = fst x>>filter_act·xs

theorem mk_trace_UU:

      mk_trace A·UU = UU

theorem mk_trace_nil:

      mk_trace A·nil = nil

theorem mk_trace_cons:

      mk_trace A·(at>>xs) =
      (if fst at ∈ ext A then fst at>>mk_trace A·xs else mk_trace A·xs)

theorem is_exec_fragC_unfold:

      is_exec_fragC A =
      (LAM ex.
          (%s. case ex of nil => TT
               | x ## xs =>
                   (FLIFT p.
                       Def ((s, p)
                            ∈ trans_of A) andalso (is_exec_fragC A·xs) (snd p))·x))

theorem is_exec_fragC_UU:

      (is_exec_fragC A·UU) s = UU

theorem is_exec_fragC_nil:

      (is_exec_fragC A·nil) s = TT

theorem is_exec_fragC_cons:

      (is_exec_fragC A·(pr>>xs)) s =
      (Def ((s, pr) ∈ trans_of A) andalso (is_exec_fragC A·xs) (snd pr))

theorem is_exec_frag_UU:

      is_exec_frag A (s, UU)

theorem is_exec_frag_nil:

      is_exec_frag A (s, nil)

theorem is_exec_frag_cons:

      is_exec_frag A (s, (a, t)>>ex) = (s -a--A-> t ∧ is_exec_frag A (t, ex))

## laststate

theorem laststate_UU:

      laststate (s, UU) = s

theorem laststate_nil:

      laststate (s, nil) = s

theorem laststate_cons:

      Finite ex ==> laststate (s, at>>ex) = laststate (snd at, ex)

theorem exists_laststate:

      Finite ex ==> ∀s. ∃u. laststate (s, ex) = u

## has_trace, mk_trace

theorem has_trace_def2:

      has_trace A b = (∃ex∈executions A. b = mk_trace A·(snd ex))

## signatures and executions, schedules

theorem execfrag_in_sig:

      is_trans_of A
      ==> ∀s. is_exec_frag A (s, xs) --> Forall (%a. a ∈ act A) (filter_act·xs)

theorem exec_in_sig:

      [| is_trans_of A; x ∈ executions A |]
      ==> Forall (%a. a ∈ act A) (filter_act·(snd x))

theorem scheds_in_sig:

      [| is_trans_of A; x ∈ schedules A |] ==> Forall (%a. a ∈ act A) x

## executions are prefix closed

theorem execfrag_prefixclosed:

      ∀x s. is_exec_frag A (s, x) ∧ y << x --> is_exec_frag A (s, y)

theorem exec_prefixclosed:

      [| is_exec_frag A (x, xa); y << xa |] ==> is_exec_frag A (x, y)

theorem exec_prefix2closed:

      is_exec_frag A (s, x @@ y) ==> is_exec_frag A (s, x)