Theory bpel_ast

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

section ‹Abstract Syntax of BPEL v2.0 language›

theory bpel_ast
imports Main
begin

type_synonym QName = string
type_synonym NCName = string

type_synonym Time = nat

record ('s,'l) State =
  vars :: 's             (* variables declared in BPEL process *)
  links :: "'l ⇒ bool"  (* links declared in BPEL flow, we assume they are identified *)
  tick :: nat            (* the global time, we have a Tick event to simulate the clock *)
  (* loopc :: "'c ⇒ nat"   (* counter for ForEach activity *) *)


record ('s,'l) Flow_Ele =
  targets :: "((('s,'l) State ⇒ bool) × 'l list) option"
  (* join condition ('s ⇒ bool) is a bool exp. True: logical AND of targets, False : OR of targets *)
  sources :: "('l × (('s,'l) State ⇒ bool)) list option"
  (* transition condition ('s ⇒ bool) is a bool exp *)

text ‹We only permit Flow Element for basic activities.
Although it is allowed in BPEL standard for structured activities, we did not find examples in the standard.
The important thing is that flow element for structured activities
can be transformed into flow element only in basic activities.›

datatype ('s,'l) Activity =
  Invoke (se:"('s,'l) Flow_Ele") (ptlink:NCName) (pttype:QName) (op:NCName)
         (*inputvar:BPELVariableName*)
         "('s,'l) State ⇒ ('s,'l) State"
         (catches:"(QName × (('s,'l) Activity)) list") (catchall:"('s,'l) Activity option")
        (*comphandler:"'s Activity option"*)
  (* if invocation returns sucessfully, the result is assigned to vars. Otherwise it returns a Fault.
     the effect is presented as ``spec''. QName option is None, means success invocation *)
| Receive (se:"('s,'l) Flow_Ele") (ptlink:NCName) (pttype:QName) (op:NCName)
          (*var:BPELVariableName*) (spec:"('s,'l) State ⇒ ('s,'l) State")
  (* Receive will assign data to vars. The ``spec'' presents this effect *)
| Reply (se:"('s,'l) Flow_Ele") (ptlink:NCName) (pttype:QName) (op:NCName)
        (*var:BPELVariableName*) (*fault:"QName option"*)
  (* ``Reply'' does not modified the BPEL states. It only may affect other BPEL processes.
     So we omit some information here *)
| Assign (se:"('s,'l) Flow_Ele") "('s,'l) State ⇒ ('s,'l) State"
(*| Throw (se:StdEle)*)
(*| Exit (se:StdEle)*)
(*| WaitFor (se:StdEle) Time
| WaitUntil (se:StdEle) Time*)
| Wait (se:"('s,'l) Flow_Ele") Time (* we unify wait for/until *)
| Empty (se:"('s,'l) Flow_Ele")
| Seqb (*se:"('s,'l) Flow_Ele"*) "('s,'l) Activity" "('s,'l) Activity"
| If (*se:"('s,'l) Flow_Ele"*) (cond:"('s,'l) State set") "('s,'l) Activity" "('s,'l) Activity"
| While (*se:"('s,'l) Flow_Ele"*) (cond:"('s,'l) State set") "('s,'l) Activity"
(* | RepeatUntil (*se:"('s,'l) Flow_Ele"*) "('s,'l) Activity" (cond:"('s,'l) State set")  *)
(* we lift RepeatUntil to syntax. its Seqb P (While c P) *)
(* | ForEach (*se:"('s,'l) Flow_Ele"*) (startv:nat) (endv:nat) 'c "('s,'l) Activity" *)
(* 'c is the temporal counter *)
(* | ForEach (*se:"('s,'l) Flow_Ele"*) bool (count:"('s,'l) State ⇒ nat") "('s,'l) Activity" *)
| Pick (*se:"('s,'l) Flow_Ele"*) "(('s,'l) EventHandler)" "(('s,'l) EventHandler)"
  (* at least one OnMesage, zero or more OnAlarm*)
| Flow (*se:"('s,'l) Flow_Ele"*) (*links:"NCName set"*) "('s,'l) Activity" "('s,'l) Activity"
(*| Compensate (se:StdEle)*)

| ActTerminator  (* the final act of bpel activities. *)

and ('s,'l) EventHandler =
  OnMessage (ptlink:NCName) (pttype:QName) (op:NCName) (*var:BPELVariableName*)
            (spec:"('s,'l) State ⇒ ('s,'l) State") "('s,'l) Activity"
(*| OnAlarmFor Time (* nat : seconds *)
| OnAlarmUntil Time (* Time : nat (seconds from 0000) *)*)
| OnAlarm Time "('s,'l) Activity" (* we unify alarm for/until *)
(* | RepeatEvery Time *) (* repeatevery is used at top level of BPEL process, but not by Pick *)


definition "repeatUntil c P ≡ Seqb P (While c P)"
(*
fun forEachPar' :: "nat ⇒ ('s,'l) Activity ⇒ ('s,'l) Activity"
  where "forEachPar' n P = Flow P (forEachPar' (n-1) P)" |
        "forEachPar' 2 P = Flow P P"

definition "forEachPar m n P ≡ Flow (replicate (n + 1 - m) P)"
*)
function forEach :: "nat ⇒ nat ⇒ ('s,'l) Activity ⇒ ('s,'l) Activity"
where "forEach m n P = (if m = n then P
                        else if m > n then ActTerminator
                        else Seqb P (forEach (m + 1) n P))"
by auto
termination forEach
apply(relation "measure (λ(m,n,P). n - m)")
by auto

primrec seqs :: "nat ⇒ ('s,'l) Activity ⇒ ('s,'l) Activity"
where "seqs 0 P = P" |
      "seqs (Suc n) P = Seqb P (seqs n P)"

type_synonym ('s,'l) BPELProc = "('s,'l) Activity"

(* all incoming links of an activity have been fired *)
definition targets_sat ::
  "((('s,'l) State ⇒ bool) × 'l list) option ⇒ ('s,'l) State ⇒ bool"
where "targets_sat tgs s ≡
  tgs ≠ None ⟶
      (fst (the tgs) s ⟶
        (∀i<length (snd (the tgs)). links s ((snd (the tgs))!i)))
    ∧ (¬ fst (the tgs) s ⟶
          (∃i<length (snd (the tgs)). links s ((snd (the tgs))!i)))"

(* fire outcoming links of an activity *)
definition fire_sources ::
  "('l × (('s,'l) State ⇒ bool)) list option
  ⇒ ('s,'l) State ⇒ ('s,'l) State"
where "fire_sources srcs s ≡
  (if srcs ≠ None then
      s⦇links := foldl (λf l. f(fst l := snd l s)) (links s) (the srcs)⦈
   else s)"

end