# Theory SymbolicPrimitive

chapter ‹Symbolic Primitives for Building Runs›
theory SymbolicPrimitive
imports Run
begin
text‹
We define here the primitive constraints on runs, towards which we translate
TESL specifications in the operational semantics.
These constraints refer to a specific symbolic run and can therefore access
properties of the run at particular instants (for instance, the fact that a clock
ticks at instant @{term ‹n›} of the run, or the time on a given clock at
that instant).
In the previous chapters, we had no reference to particular instants of a run
because the TESL language should be invariant by stuttering in order to allow
the composition of specifications: adding an instant where no clock ticks to
a run that satisfies a formula should yield another run that satisfies the
same formula. However, when constructing runs that satisfy a formula, we
need to be able to refer to the time or hamlet of a clock at a given instant.
›
text‹
Counter expressions are used to get the number of ticks of a clock up to
(strictly or not) a given instant index.
›