Theory DCRExecutionEquivalence

(*  Title:       Execution equivalence state-space reduction for DCR-graphs
    Author:      Søren Debois & Axel Christfort 2023
    Maintainer:  Axel Christfort <axel@di.ku.dk>
*)

theory DCRExecutionEquivalence
  imports Main
begin


section ‹DCR processes›

text ‹Although we use the term "process", the present theory formalises DCR graphs as defined
in the original places and other papers.›


type_synonym event = nat

text ‹The static structure. This encompasss the relations, the set of event @{term dom} of the
process, and the labelling function @{term lab}. We do not explicitly enforce that relations and marking are confined to this set, except in
definitions of enabledness and execution below. ›

record rels =
  (* Relations *)
  cond :: "event rel"
  pend :: "event rel"
  incl :: "event rel"
  excl :: "event rel"
  mist :: "event rel"
  (* Other static structure *)
  dom  :: "event set"

(* abbreviation "rng T ≡ range (lab T)"  *)

text ‹The dynamic structure, called the marking›

record marking =
  Ex :: "event set"
  In :: "event set"
  Re :: "event set"


text ‹
  It will be convenient to have notation for the events
  required, excluded, etc. by a given event.
›

abbreviation conds :: "rels ⇒ event ⇒ event set"
  where
    "conds T e ≡ { f . (f,e) ∈ cond T }"


abbreviation excls :: "rels ⇒ event ⇒ event set"
  where
    "excls T e ≡ { x . (e,x) ∈ excl T ∧ (e,x) ∉ incl T }"


abbreviation incls :: "rels ⇒ event ⇒ event set"
  where
    "incls T e ≡ { x . (e,x) ∈ incl T }"


abbreviation resps :: "rels ⇒ event ⇒ event set"
  where
    "resps T e ≡ { f . (e,f) ∈ pend T }"

abbreviation mists :: "rels ⇒ event ⇒ event set"
  where
    "mists T e ≡ { f . (f,e) ∈ mist T }"

text ‹Similarly, it is convenient to be able to identify directly the currently excluded events. ›

subsection ‹Execution semantics›


definition enabled :: "rels ⇒ marking ⇒ event ⇒ bool"
  where
    "enabled T M e ≡
        e ∈ In M  ∧
        (conds T e ∩ In M) - Ex M = {} ∧
        (mists T e ∩ In M) - (dom T - Re M) = {}"

definition execute :: "rels ⇒ marking ⇒ nat ⇒ marking"
  where
    "execute T M e ≡ ⦇
       Ex = Ex M ∪ { e },
       In = (In M - excls T e) ∪ incls T e,
       Re = (Re M - { e }) ∪ resps T e
      ⦈"

subsection ‹Execution Equivalence›

definition accepting :: "marking ⇒ bool" where
  "accepting M = (Re M ∩ In M = {})"

fun acceptingrun :: "rels ⇒ marking ⇒ event list ⇒ bool" where
  "acceptingrun T M [] = accepting M"
| "acceptingrun T M (e#t) = (enabled T M e ∧ acceptingrun T (execute T M e) t)"

definition all_conds :: "rels ⇒ nat set" where
  "all_conds T = { fst rel | rel . rel ∈ cond T }"

definition execution_equivalent :: "rels ⇒ marking ⇒ marking ⇒ bool" where
  "execution_equivalent T M1 M2 = (
    (In M1 = In M2) ∧
    (Re M1 = Re M2) ∧
    ((Ex M1 ∩ all_conds T) = (Ex M2 ∩ all_conds T))
  )"

lemma conds_subset_eq_all_conds: "conds T e ⊆ all_conds T"
  using all_conds_def by auto

lemma ex_equiv_over_cond: "(Ex M1 ∩ all_conds T) = (Ex M2 ∩ all_conds T) ⟹ (Ex M1 ∩ conds T e) = (Ex M2 ∩ conds T e)"
  using conds_subset_eq_all_conds by blast

lemma enabled_ex_equiv:
  assumes "execution_equivalent T M1 M2" "enabled T M1 e"
  shows "enabled T M2 e"
proof -
  from assms(1) have
    "(Ex M1 ∩ all_conds T) = (Ex M2 ∩ all_conds T)"
    by (simp add: execution_equivalent_def)
  hence ex_eq:
    "(Ex M1 ∩ conds T e) = (Ex M2 ∩ conds T e)"
    using ex_equiv_over_cond by metis
  from assms(1) have in_eq:
    "In M1 = In M2"
    by (simp add: execution_equivalent_def)
  from assms(2) have
    "(conds T e ∩ In M1) ⊆ Ex M1"
    by(simp_all add: enabled_def)
  hence
    "(conds T e ∩ In M1) ∩ (conds T e) ⊆ Ex M1 ∩ (conds T e)"
    by auto
  hence
    "(conds T e ∩ In M1) ⊆ Ex M1 ∩ (conds T e)"
    by auto
  hence
    "(conds T e ∩ In M2) ⊆ Ex M2 ∩ (conds T e)"
    using ex_eq in_eq by auto
  hence
    "(conds T e ∩ In M2) ⊆ Ex M2"
    by simp
  then show ?thesis
    using enabled_def assms in_eq execution_equivalent_def by auto
qed

lemma execute_ex_equiv:
  assumes "execution_equivalent T M1 M2" "execute T M1 e = M3" "execute T M2 e = M4"
  shows "execution_equivalent T M3 M4"
proof-
  from assms have
    "In M3 = In M4"
    using execute_def execution_equivalent_def by fastforce
  moreover from assms have
    "Re M3 = Re M4"
    using execute_def execution_equivalent_def by force
  ultimately show ?thesis using assms execute_def execution_equivalent_def
    by fastforce
qed

lemma accepting_ex_equiv: "execution_equivalent T M1 M2 ⟹ accepting M1 ⟹ accepting M2"
  by (simp add: accepting_def execution_equivalent_def)

theorem acceptingrun_ex_equiv:
  assumes "acceptingrun T M1 seq" "execution_equivalent T M1 M2"
  shows "acceptingrun T M2 seq"
  using assms
proof(induction seq arbitrary: M1 M2 rule: acceptingrun.induct)
  case (1 T M)
  then show ?case
    by (simp add: accepting_ex_equiv)
next
  case (2 T M e t)
  then show ?case proof-
    from 2(2) obtain M1e where m1e:
      "M1e = execute T M1 e"
      by blast
    hence m1e_accept:
      "acceptingrun T M1e t"
      using 2(2) acceptingrun.simps(2) by blast
    obtain M2e where
      "M2e = execute T M2 e"
      by blast
    moreover from this m1e have
      "execution_equivalent T M1e M2e"
      using 2(3) execute_ex_equiv by blast
    moreover from this have
      "acceptingrun T M2e t"
      using 2(1) m1e_accept by blast
    ultimately show ?thesis using 2(2) enabled_ex_equiv 2(3) acceptingrun.simps(2) by blast
  qed
qed

end