Theory StutteringDefs

chapter ‹Properties of TESL›

section ‹Stuttering Invariance›

theory StutteringDefs

imports Denotational


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
  dilating_fun (f::nat  nat) (r::'a::linordered_field run)
     strict_mono f  (f 0 = 0)  (n. f n  n
     ((n0. f n0 = n)  (c. ¬(hamlet ((Rep_run r) n c))))
     ((n0. f n0 = (Suc n))  (c. time ((Rep_run r) (Suc n) c)
                                      = time ((Rep_run r) n c)))

  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
  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)
  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}:
    \caption{Dilating and contracting functions}\label{fig:dilating-run}
― ‹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
  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
  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
  tick_count_strict r c n = card {i. i < n  hamlet ((Rep_run r) i c)}