IOA/meta_theory/IOA.thy

added IOA to isabelle/HOL

(* The I/O automata of Lynch and Tuttle. *)

IOA = Asig +

types
   'a seq            =   "nat => 'a"
   'a oseq           =   "nat => 'a option"
   ('a,'b)execution  =   "'a oseq * 'b seq"
   ('a,'s)transition =   "('s * 'a * 's)"
   ('a,'s)ioa        =   "'a signature * 's set * ('a,'s)transition set"

consts

  (* IO automata *)
  state_trans::"['action signature, ('action,'state)transition set] => bool"
  asig_of    ::"('action,'state)ioa => 'action signature"
  starts_of  ::"('action,'state)ioa => 'state set"
  trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
  IOA	     ::"('action,'state)ioa => bool"

  (* Executions, schedules, and behaviours *)

  is_execution_fragment,
  has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool"
  executions    :: "('action,'state)ioa => ('action,'state)execution set"
  mk_behaviour  :: "[('action,'state)ioa, 'action oseq] => 'action oseq"
  reachable     :: "[('action,'state)ioa, 'state] => bool"
  invariant     :: "[('action,'state)ioa, 'state=>bool] => bool"
  has_behaviour :: "[('action,'state)ioa, 'action oseq] => bool"
  behaviours    :: "('action,'state)ioa => 'action oseq set"

  (* Composition of action signatures and automata *)
  compatible_asigs ::"('a => 'action signature) => bool"
  asig_composition ::"('a => 'action signature) => 'action signature"
  compatible_ioas  ::"('a => ('action,'state)ioa) => bool"
  ioa_composition  ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa"

  (* binary composition of action signatures and automata *)
  compat_asigs ::"['action signature, 'action signature] => bool"
  asig_comp    ::"['action signature, 'action signature] => 'action signature"
  compat_ioas  ::"[('action,'state)ioa, ('action,'state)ioa] => bool"
  "||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr 10)

  (* Filtering and hiding *)
  filter_oseq  :: "('a => bool) => 'a oseq => 'a oseq"

  restrict_asig :: "['a signature, 'a set] => 'a signature"
  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"

  (* Notions of correctness *)
  ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"


rules

state_trans_def
  "state_trans(asig,R) == \
  \  (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
  \  (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"


ioa_projections_def
   "asig_of = fst  &  starts_of = (fst o snd)  &  trans_of = (snd o snd)"


ioa_def
  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            \
  \             (~ starts_of(ioa) = {})    &                            \
  \             state_trans(asig_of(ioa),trans_of(ioa)))"


(* An execution fragment is modelled with a pair of sequences:
 * the first is the action options, the second the state sequence.
 * Finite executions have None actions from some point on.
 *******)
is_execution_fragment_def
  "is_execution_fragment(A,ex) ==                                       \
  \  let act = fst(ex); state = snd(ex)                                 \
  \  in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              \
  \           (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"


executions_def
  "executions(ioa) == {e. snd(e,0):starts_of(ioa) &                     \
\                        is_execution_fragment(ioa,e)}"


(* Is a state reachable. Using an inductive definition, this could be defined
 * by the following 2 rules
 *
 *      x:starts_of(ioa)
 *      ----------------
 *      reachable(ioa,x)  
 *
 *      reachable(ioa,s) & ? <s,a,s'>:trans_of(ioa)
 *      -------------------------------------------
 *               reachable(ioa,s')
 *
 * A direkt definition follows.
 *******************************)
reachable_def
  "reachable(ioa,s) == (? ex:executions(ioa). ? n. snd(ex,n) = s)"


invariant_def "invariant(A,P) == (!s. reachable(A,s) --> P(s))"


(* Restrict the trace to those members of the set s *)
filter_oseq_def
  "filter_oseq(p,s) ==                                                  \
\   (%i.case s(i)                                                       \
\         of None => None                                               \
\          | Some(x) => if(p(x),Some(x),None))"


mk_behaviour_def
  "mk_behaviour(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))"


(* Does an ioa have an execution with the given behaviour *)
has_behaviour_def
  "has_behaviour(ioa,b) ==                                              \
\     (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"


(* All the behaviours of an ioa *)
behaviours_def
  "behaviours(ioa) == {b. has_behaviour(ioa,b)}"


compat_asigs_def
  "compat_asigs (a1,a2) ==                                              \
 \ (((outputs(a1) Int outputs(a2)) = {}) &                              \
 \  ((internals(a1) Int actions(a2)) = {}) &                            \
 \  ((internals(a2) Int actions(a1)) = {}))"


compat_ioas_def
  "compat_ioas(ioa1,ioa2) == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"


asig_comp_def
  "asig_comp (a1,a2) ==                                                 \
  \   (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      \
  \     (outputs(a1) Un outputs(a2)),                                   \
  \     (internals(a1) Un internals(a2))>)"


par_def
  "(ioa1 || ioa2) ==                                                    \
  \    <asig_comp(asig_of(ioa1),asig_of(ioa2)),                         \
  \     {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        \
  \     {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        \
  \          in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
  \             if(a:actions(asig_of(ioa1)),                            \
  \                <fst(s),a,fst(t)>:trans_of(ioa1),                    \
  \                fst(t) = fst(s))                                     \
  \             &                                                       \
  \             if(a:actions(asig_of(ioa2)),                            \
  \                <snd(s),a,snd(t)>:trans_of(ioa2),                    \
  \                snd(t) = snd(s))}>"


restrict_asig_def
  "restrict_asig(asig,actns) ==                                         \
\    <inputs(asig) Int actns, outputs(asig) Int actns,                  \
\     internals(asig) Un (externals(asig) - actns)>"


restrict_def
  "restrict(ioa,actns) ==                                               \
\    <restrict_asig(asig_of(ioa),actns), starts_of(ioa), trans_of(ioa)>"


ioa_implements_def
  "ioa_implements(ioa1,ioa2) ==        \
\     (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \
\      behaviours(ioa1) <= behaviours(ioa2))"

end