Theory StutteringDefs

chapter ‹Properties of TESL›

section ‹Stuttering Invariance›

theory StutteringDefs

imports Denotational

begin

text ‹
  When composing systems into more complex systems, it may happen that one system 
  has to perform some action while the rest of the complex system does nothing.
  In order to support the composition of TESL specifications, we want to be able 
  to insert stuttering instants in a run without breaking the conformance of a run 
  to its specification. This is what we call the ∗‹stuttering invariance› of TESL.
›

subsection ‹Definition of stuttering›

text ‹
  We consider stuttering as the insertion of empty instants (instants at which no 
  clock ticks) in a run. We caracterize this insertion with a dilating function,
  which maps the instant indices of the original run to the corresponding instant
  indices of the dilated run.
  The properties of a dilating function are:
  ▪ it is strictly increasing because instants are inserted into the run,
  ▪ the image of an instant index is greater than it because stuttering instants 
    can only delay the original instants of the run, 
  ▪ no instant is inserted before the first one in order to have a well defined 
    initial date on each clock,
  ▪ if @{term ‹n›} is not in the image of the function, no clock ticks at 
    instant @{term ‹n›} and the date on the clocks do not change.
›
definition dilating_fun
where
  ‹dilating_fun (f::nat ⇒ nat) (r::'a::linordered_field run)
    ≡ strict_mono f ∧ (f 0 = 0) ∧ (∀n. f n ≥ n
    ∧ ((∄n⇩0. f n⇩0 = n) ⟶ (∀c. ¬(hamlet ((Rep_run r) n c))))
    ∧ ((∄n⇩0. f n⇩0 = (Suc n)) ⟶ (∀c. time ((Rep_run r) (Suc n) c)
                                      = time ((Rep_run r) n c)))
   )›

text‹
  A run @{term r} is a dilation of a run @{term sub} by 
  function @{term f} if:
  ▪ @{term f} is a dilating function for @{term r} 
  ▪ the time in @{term r} is the time in @{term sub} dilated by @{term f}
  ▪ the hamlet in @{term r} is the hamlet in sub dilated by @{term f}
›
definition dilating
where
  ‹dilating f sub r ≡ dilating_fun f r
                    ∧ (∀n c. time ((Rep_run sub) n c) = time ((Rep_run r) (f n) c))
                    ∧ (∀n c. hamlet ((Rep_run sub) n c) = hamlet ((Rep_run r) (f n) c))›

text ‹
  A ∗‹run› is a ∗‹subrun› of another run if there exists a dilation between them.
›
definition is_subrun ::‹'a::linordered_field run ⇒ 'a run ⇒ bool› (infixl ‹≪› 60)
where
  ‹sub ≪ r ≡ (∃f. dilating f sub r)›

text ‹
  A contracting function is the reverse of a dilating fun, it maps an instant index 
  of a dilated run to the index of the last instant of a non stuttering run that
  precedes it. Since several successive stuttering instants are mapped to the same
  instant of the non stuttering run, such a function is monotonous, but not strictly.
  The image of the first instant of the dilated run is necessarily the first instant
  of the non stuttering run, and the image of an instant index is less that this 
  index because we remove stuttering instants. 
›
definition contracting_fun
  where ‹contracting_fun g ≡ mono g ∧ g 0 = 0 ∧ (∀n. g n ≤ n)›

text ‹
  \autoref{fig:dilating-run} illustrates the relations between the instants of 
  a run and the instants of a dilated run, with the mappings by the dilating 
  function @{term ‹f›} and the contracting function @{term ‹g›}:
  \begin{figure}
    \centering
    \includegraphics{dilating.pdf}
    \caption{Dilating and contracting functions}\label{fig:dilating-run}
  \end{figure}
›
(*<*)
― ‹Constants and notation to be able to write what we want as Isabelle terms, not as LaTeX maths›
consts dummyf    :: ‹nat ⇒ nat›
consts dummyg    :: ‹nat ⇒ nat›
consts dummytwo  :: ‹nat›
notation dummyf    (‹f›) 
notation dummyg    (‹g›)
notation dummytwo  (‹2›)
(*>*)
text ‹
  A function @{term ‹g›} is contracting with respect to the dilation of run
  @{term ‹sub›} into run @{term ‹r›} by the dilating function @{term ‹f›} if:
  ▪ it is a contracting function ;
  ▪ @{term ‹(f ∘ g) n›} is the index of the last original instant before instant 
    @{term ‹n›} in run @{term ‹r›}, therefore:
    ▪ @{term ‹(f ∘ g) n ≤ n ›}
    ▪ the time does not change on any clock between instants @{term ‹(f ∘ g) n›}
      and @{term ‹n›} of run @{term ‹r›};
    ▪ no clock ticks before @{term ‹n›} strictly after @{term ‹(f ∘ g) n›} 
      in run @{term ‹r›}.
  See \autoref{fig:dilating-run} for a better understanding. Notice that in this 
  example, @{term ‹2›} is equal to @{term ‹(f ∘ g) 2›}, @{term ‹(f ∘ g) 3›}, 
  and @{term ‹(f ∘ g) 4›}. 
›
(*<*)
no_notation dummyf      (‹f›) 
no_notation dummyg      (‹g›) 
no_notation dummytwo    (‹2›)
(*>*)

definition contracting
where 
  ‹contracting g r sub f ≡  contracting_fun g
                          ∧ (∀n. f (g n) ≤ n)
                          ∧ (∀n c k. f (g n) ≤ k ∧ k ≤ n
                              ⟶ time ((Rep_run r) k c) = time ((Rep_run sub) (g n) c))
                          ∧ (∀n c k. f (g n) < k ∧ k ≤ n
                              ⟶ ¬ hamlet ((Rep_run r) k c))›

text ‹
  For any dilating function, we can build its ∗‹inverse›, as illustrated on
  \autoref{fig:dilating-run}, which is a contracting function:
›
definition ‹dil_inverse f::(nat ⇒ nat) ≡ (λn. Max {i. f i ≤ n})›

subsection ‹
  Alternate definitions for counting ticks.
›
text ‹
  For proving the stuttering invariance of TESL specifications, we will need
  these alternate definitions for counting ticks, which are based on sets.
›

text ‹
  @{term ‹tick_count r c n›} is the number of ticks of clock @{term c} in 
  run @{term r} upto instant @{term n}.
›
definition tick_count :: ‹'a::linordered_field run ⇒ clock ⇒ nat ⇒ nat›
where
  ‹tick_count r c n = card {i. i ≤ n ∧ hamlet ((Rep_run r) i c)}›

text ‹
  @{term ‹tick_count_strict r c n›} is the number of ticks of clock @{term c} 
  in run @{term r} upto but excluding instant @{term n}.
› 
definition tick_count_strict :: ‹'a::linordered_field run ⇒ clock ⇒ nat ⇒ nat›
where
  ‹tick_count_strict r c n = card {i. i < n ∧ hamlet ((Rep_run r) i c)}›


end