Theory bpel_semantics

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

section ‹Small-step semantics of BPEL v2.0 language›

theory bpel_semantics
imports bpel_ast
begin

subsection ‹ Definition of Small-step Semantics ›

type_synonym ('s,'l) bpelconf = "('s,'l) Activity × ('s,'l) State"
type_synonym ('s,'l) evthandlerconf = "('s,'l) EventHandler × ('s,'l) State"

inductive_set
    activity_tran :: "(('s,'l) bpelconf × ('s,'l) bpelconf) set"
and activity_tran' :: "('s,'l) bpelconf ⇒ ('s,'l) bpelconf ⇒ bool" ("_ ⟶⇩b⇩p⇩e⇩l _" [81,81] 80)
and evthandler_tran :: "(('s,'l) evthandlerconf × ('s,'l) bpelconf) set"
and evthandler_tran' :: "('s,'l) evthandlerconf ⇒ ('s,'l) bpelconf ⇒ bool" ("_ ⟶⇩e⇩h _" [81,81] 80)
where
  "P ⟶⇩b⇩p⇩e⇩l Q ≡ (P,Q) ∈ activity_tran"
| "P ⟶⇩e⇩h Q ≡ (P,Q) ∈ evthandler_tran"

(*
three cases of Invoke:
(1) invoke successfully
(2) invoke returns exception which is caught
(3) invoke returns exception which is not caught
However, we assume that all exceptions will be caught.
*)
| invoke_suc: "⟦targets_sat (targets fls) s; t = fire_sources (sources fls) (spc s)⟧
    ⟹ (Invoke fls ptl ptt opn spc cts cta,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"

| invoke_fault: "⟦targets_sat (targets fls) s; t = fire_sources (sources fls) s;
    evh ∈ set (map snd cts) ∪ set_option cta⟧
    ⟹ (Invoke fls ptl ptt opn spc cts cta,s) ⟶⇩b⇩p⇩e⇩l (evh,t)"
(*
| invoke_fault_notcatch: "⟦targets_sat (targets fls) s; t = fire_sources (sources fls) s;
    set (map snd cts) ∪ set_option cta = {}⟧
    ⟹ (Invoke fls ptl ptt opn spc cts cta,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"
*)
| receive: "⟦targets_sat (targets fls) s; r = spc s; t = fire_sources (sources fls) r⟧
    ⟹ (Receive fls ptl ptt opn spc,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"

| reply: "⟦targets_sat (targets fls) s; t = fire_sources (sources fls) s⟧
    ⟹ (Reply fls ptl ptt opn,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"

| assign: "⟦targets_sat (targets fls) s; r = spc s; t = fire_sources (sources fls) r⟧
    ⟹ (Assign fls spc,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"

| wait: "⟦tm > tick s; targets_sat (targets fls) s; t = fire_sources (sources fls) s⟧
    ⟹ (Wait fls tm,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"

| empty: "⟦targets_sat (targets fls) s; t = fire_sources (sources fls) s⟧
    ⟹ (Empty fls,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"

| seq: "⟦(P,s) ⟶⇩b⇩p⇩e⇩l (P',t); P' ≠ ActTerminator ⟧ ⟹ (Seqb P Q,s) ⟶⇩b⇩p⇩e⇩l (Seqb P' Q,t)"
| seq_fin: "⟦(P,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)⟧ ⟹(Seqb P Q,s) ⟶⇩b⇩p⇩e⇩l (Q,t)"

(*
| ifT: "s∈c ⟹ (If c P Q,s) ⟶⇩b⇩p⇩e⇩l (P,s)"
| ifF: "s∉c ⟹ (If c P Q,s) ⟶⇩b⇩p⇩e⇩l (Q,s)"
*)
(* This is to work around a quirk in the semantics of PiCore *)
| ifT: "s∈c ⟹ (If c P Q, s) ⟶⇩b⇩p⇩e⇩l (P, s)"
| ifF: "s∉c ⟹ (If c P Q, s) ⟶⇩b⇩p⇩e⇩l (Q, s)"

| whileT: "s∈c ⟹ P ≠ ActTerminator ⟹ (While c P,s) ⟶⇩b⇩p⇩e⇩l (Seqb P (While c P),s)"
| whileF: "s∉c ⟹ (While c P,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,s)"

| pick1: "(a,s)⟶⇩e⇩h(Q,t) ⟹ (Pick a b,s)⟶⇩b⇩p⇩e⇩l (Q,t)"
| pick2: "(b,s)⟶⇩e⇩h(Q,t) ⟹ (Pick a b,s)⟶⇩b⇩p⇩e⇩l (Q,t)"
(*| pick: "⟦i < length ehs; (ehs!i,s) ⟶⇩e⇩h (Q,t) ⟧ ⟹ (Pick ehs,s) ⟶⇩b⇩p⇩e⇩l (Q,t)"*)

| flow1: "(a,s)⟶⇩b⇩p⇩e⇩l(c,t) ⟹ (Flow a b,s)⟶⇩b⇩p⇩e⇩l(Flow c b,t)"
| flow2: "(b,s)⟶⇩b⇩p⇩e⇩l(c,t) ⟹ (Flow a b,s)⟶⇩b⇩p⇩e⇩l(Flow a c,t)"
| flow_fin: "(Flow ActTerminator ActTerminator,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,s)"
(*| flow: "⟦i < length as; (as!i,s) ⟶⇩b⇩p⇩e⇩l (b,t); bs = as[i := b] ⟧ ⟹ (Flow as,s) ⟶⇩b⇩p⇩e⇩l (Flow bs,t)"
| flow_fin: "⟦∀i < length as. as ! i = ActTerminator ⟧ ⟹ (Flow as,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,s)"*)

| on_message: "⟦t = spc s⟧ ⟹ (OnMessage ptl ptt opn spc a,s) ⟶⇩e⇩h (a,t)"

| on_alarm: "⟦tm > tick s⟧ ⟹ (OnAlarm tm a,s) ⟶⇩e⇩h (a,s)"

subsection ‹ Lemmas of Small-step Semantics ›

inductive_cases bpel_recv_cases: "(Receive fls ptl ptt opn spc,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t)"
thm bpel_recv_cases
thm receive

lemma recv_to_termi: "(Receive a b c d e, s) ⟶⇩b⇩p⇩e⇩l (Q, t) ⟹ Q = ActTerminator"
apply(rule activity_tran.cases) by auto

lemma termi_has_no_tran: "(P,s)⟶⇩b⇩p⇩e⇩l(Q,t) ⟹ P ≠ ActTerminator"
apply(rule activity_tran.cases)
by auto

inductive_cases bpel_seq: "(Seqb P Q,s) ⟶⇩b⇩p⇩e⇩l (R,t)"
thm bpel_seq

inductive_cases bpel_seq1: "(Seqb P Q,s) ⟶⇩b⇩p⇩e⇩l (Seqb P' Q,t)"
thm bpel_seq1

inductive_cases bpel_seq_fin: "(Seqb ActTerminator Q,s) ⟶⇩b⇩p⇩e⇩l (Q,s)"
thm bpel_seq_fin

lemma bpel_seq_cases: "(Seqb P Q,s) ⟶⇩b⇩p⇩e⇩l (R,t) ⟹
  R = Q ∧ (P,s) ⟶⇩b⇩p⇩e⇩l (ActTerminator,t) ∨ (∃P'. P' ≠ ActTerminator ∧ (P,s) ⟶⇩b⇩p⇩e⇩l (P',t) ∧ R = Seqb P' Q)"
  apply(rule activity_tran.cases) by auto

lemma bpel_pick_cases: "(Pick a b,s)⟶⇩b⇩p⇩e⇩l (Q,t) ⟹ (a,s)⟶⇩e⇩h(Q,t) ∨ (b,s)⟶⇩e⇩h(Q,t)"
  apply(rule activity_tran.cases) by auto

inductive_cases bpel_flow_case: "(Flow a b,s)⟶⇩b⇩p⇩e⇩l (Q,t)"
thm bpel_flow_case

lemma bpel_flow_cases1: "(Flow a b,s)⟶⇩b⇩p⇩e⇩l (Flow c d,t) ⟹
  (a,s)⟶⇩b⇩p⇩e⇩l(c,t) ∧ b = d ∨ (b,s)⟶⇩b⇩p⇩e⇩l(d,t) ∧ a = c"
apply(rule activity_tran.cases) by fast+

lemma bpel_flow_cases2: "(Flow a b,s)⟶⇩b⇩p⇩e⇩l (ActTerminator,t) ⟹
  a = ActTerminator ∧ b = ActTerminator ∧ s = t"
apply(rule activity_tran.cases) by auto

lemma bpel_flow_cases3: "(Flow a b,s)⟶⇩b⇩p⇩e⇩l (Q,t) ⟹ Q = ActTerminator ∨ (∃c d. Q = Flow c d)"
  apply(rule activity_tran.cases) by auto

lemma bpel_flow_cases:
 "(Flow a b,s)⟶⇩b⇩p⇩e⇩l (Q,t) ⟹ (∃c. Q = Flow c b ∧ (a,s)⟶⇩b⇩p⇩e⇩l(c,t))
      ∨ (∃d. Q = Flow a d ∧ (b,s)⟶⇩b⇩p⇩e⇩l(d,t))
      ∨ Q = ActTerminator ∧ a = ActTerminator ∧ b = ActTerminator ∧ s = t"
apply(rule activity_tran.cases) by auto

lemma bpel_while_cases:
  "(While c P,s) ⟶⇩b⇩p⇩e⇩l (Q,t) ⟹
    s∈c ∧ Q = Seqb P (While c P) ∧ s = t ∧ P≠ActTerminator
  ∨ s∉c ∧ Q = ActTerminator ∧ s = t"
apply(rule activity_tran.cases) by auto

lemma bpel_onmsg_cases: "(OnMessage ptl ptt opn spc a,s) ⟶⇩e⇩h (x,t) ⟹ x = a ∧ t = spc s"
  apply(rule evthandler_tran.cases) by auto

lemma bpel_onalarm_cases: "(OnAlarm tm a,s) ⟶⇩e⇩h (x,t) ⟹ x = a ∧ t = s ∧ tm > tick s"
  apply(rule evthandler_tran.cases) by auto

subsection ‹ Constructing the BPEL process by adding a Tick ›
(* we add a parallel tick activity to simulate timer *)
definition bpel_system :: "('s,'l) BPELProc ⇒ ('s,'l) BPELProc"
where "bpel_system proc ≡ Flow (While UNIV (Assign ⦇targets=None,sources=None⦈ (λs. s⦇tick := tick s + 1⦈))) proc"

end