theory LTS
imports Graph Labels SymExec
begin

section‹Labelled Transition Systems›

text‹This theory is motivated by the need of an abstract representation of control-flow graphs
 CFG). It is a refinement of the prior theory of (unlabelled) graphs and proceeds by decorating
  edges with \emph{labels} expressing assumptions and effects (assignments) on an underlying
 . In this theory, we define LTSs and introduce a number of abbreviations that will ease
  and proving lemmas in the following theories.›

subsection‹Basic definitions›

text‹
  ‹rgraph›'s by a labelling function of the edges, using Isabelle extensible
 .›

record ('vert,'var,'d) lts = "'vert rgraph" +
  labelling :: "'vert edge → ('var,'d) label"

text ‹We call \emph{initial location} the root of the underlying graph.›

abbreviation init :: 
"('vert,'var,'d,'x) lts_scheme → 'vert" 
where
  "init lts ≡ root lts"

text ‹The set of labels of a LTS is the image set of its labelling function over its set of edges.
 ›

abbreviation labels :: 
  "('vert,'var,'d,'x) lts_scheme → ('var,'d) label set" 
where
  "labels lts ≡ labelling lts ` edges lts"

text ‹In the following, we will sometimes need to use the notion of \emph{trace} of
  given sequence of edges with respect to the transition relation of an LTS.›

abbreviation trace :: 
  "'vert edge list → ('vert edge → ('var,'d) label) → ('var,'d) label list" 
where
  "trace as L ≡ map L as"


text‹We are interested in a special form of Labelled Transition Systems; the prior
  definition is too liberal. We will constrain it to \emph{well-formed labelled transition
 }.›

text ‹We first define an application that, given an LTS, returns its underlying graph.›

abbreviation graph :: 
  "('vert,'var,'d,'x) lts_scheme → 'vert rgraph"
where
  "graph lts ≡ rgraph.truncate lts"

text‹An LTS is well-formed if its underlying ‹rgraph› is well-formed.›

abbreviation wf_lts :: 
  "('vert,'var,'d,'x) lts_scheme → bool" 
where 
  "wf_lts lts ≡ wf_rgraph (graph lts)"

text ‹In the following theories, we will sometimes need to account for the fact that we consider
  with a finite number of edges.›

abbreviation finite_lts :: 
  "('vert,'var,'d,'x) lts_scheme → bool" 
where
  "finite_lts lts ≡ ∀ l ∈ range (labelling lts). finite_label l"


subsection ‹Feasible sub-paths and paths›

text ‹A sequence of edges is a feasible sub-path of an LTS ‹lts› from a configuration
 ‹c› if it is a sub-path of the underlying graph of ‹lts› and if it is feasible
  the configuration ‹c›.›

abbreviation feasible_subpath ::
  "('vert,'var,'d,'x) lts_scheme → ('var,'d) conf → 'vert → 'vert edge list → 'vert → bool"
where
  "feasible_subpath lts pc l1 as l2 ≡ Graph.subpath lts l1 as l2
                                    ∧ feasible pc (trace as (labelling lts))"
  
text ‹Similarly to sub-paths in rooted-graphs, we will not be always interested in the final
  of a feasible sub-path. We use the following notion when we are not interested in this
 .›

abbreviation feasible_subpath_from ::
  "('vert,'var,'d,'x) lts_scheme → ('var,'d) conf → 'vert → 'vert edge list → bool"
where
  "feasible_subpath_from lts pc l as ≡ ∃ l'. feasible_subpath lts pc l as l'"

abbreviation feasible_subpaths_from ::
  "('vert,'var,'d,'x) lts_scheme → ('var,'d) conf → 'vert → 'vert edge list set"
where
  "feasible_subpaths_from lts pc l ≡ {ts. feasible_subpath_from lts pc l ts}"

text ‹As earlier, feasible paths are defined as feasible sub-paths starting at the initial
  of the LTS.›

abbreviation feasible_path ::
  "('vert,'var,'d,'x) lts_scheme → ('var,'d) conf → 'vert edge list → 'vert → bool"
where
  "feasible_path lts pc as l ≡ feasible_subpath lts pc (init lts) as l"

abbreviation feasible_paths ::
  "('vert,'var,'d,'x) lts_scheme → ('var,'d) conf → 'vert eilerdIc'tora2)
where
  "feasible_paths lts pc ≡ {as. ∃ l. feasible_path lts pc as l}"

end