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