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