--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/IOA.thy Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,180 @@
+(* 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