Table of contents

About TESL

TESL is a declarative language for specifying discrete event behaviors for simulation. It takes many features from CCSL, the Clock Constraints Specification Language, keeping only the synchronous operators on clocks. TESL also takes ideas from the Tagged Signal Model by adding support for time tags and relations between the time scales of different clocks. The algorithm for solving TESL specifications also relies on ideas from the constructive semantics of the Esterel synchronous language.

TESL supports a model of time in which events are modeled as clocks, and event occurrences are modeled as ticks on the corresponding clock. A distinguishing feature of TESL is that each clock has a time domain, and that each tick on a clock has a time tag belonging to the domain of its clock. Three basic features are available in TESL:

• implications, to model event-triggered behavior with instantaneous causality;
• time delays, to model time-triggered behavior;
• tag relations, to specify how time advances on different clocks.

All operators in TESL are based on these three features.

TESL can be used through its Java API to solve timing constraints in other software, but the easiest way to start is to use the TESL language provided as an Eclipse feature. The result of a simulation can be shown as text, TikZ pictures for embedding into LaTeX documents, SVG pictures for embedding into web pages, and VCD files.

The complete reference manual for TESL is available here.

To get an idea of what can be modeled using TESL, you can have a look at the TESL gallery.

A formal Isabelle/HOL theory of the semantics of TESL is available in the Archive of Formal Proofs.

Contact

frederic.boulanger@centralesupelec.fr

Downloading TESL

TESL is available as an Eclipse feature. You can install it from the update site https://wdi.centralesupelec.fr/tesl-update-site.

The latest version of Eclipse into which the TESL feature can installed is Eclipse Modeling 2024-06 (4.32).

The current version of the TESL feature requires Java 1.8. If the editor does not work after installation, check the Error Log view for errors when loading the classes of the plug-in, and update your version of Java if this is the issue.

Note: you may have to uncheck the Group items by category box to see the TESL engine and editor feature in the install dialog.

The TESL feature also comes preinstalled in Eclipse in a docker image available at:

https://hub.docker.com/r/fredblgr/docker-webtop-tesl

Reference papers

[1] BouJacHarPro2014MEMOCODEBoulanger, Frédéric, Jacquet, Christophe, Hardebolle, Cécile, Prodan, Iuliana, TESL: a Language for Reconciling Heterogeneous Execution TracesFormal Methods and Models for Codesign (MEMOCODE), 2014 Twelfth ACM/IEEE International Conference on, Lausanne, Switzerland, Oct, 2014, pages 114-123(URL), (PDF), (BibTeX)

[2] nguyenvan:hal-01583815Nguyen Van, Hai, Balabonski, Thibaut, Boulanger, Frédéric, Keller, Chantal, Valiron, Benoît, Wolff, Burkhart, A Symbolic Operational Semantics for TESL with an Application to Heterogeneous System TestingFormal Modeling and Analysis of Timed Systems, 15th International Conference FORMATS 2017, Berlin, Germany, Sep, 2017, (Alessandro Abate,Gilles Geeraerts, Ed.), Springer, pages 318-334(URL), (PDF), (BibTeX)

[3] TESL_Language-AFPHai Nguyen Van, Frédéric Boulanger, Burkhart Wolff, A Formal Development of a Polychronous Polytimed Coordination LanguageArchive of Formal Proofs, jul, 2019Formal proof development, (URL), (BibTeX)

A denotational and an operational semantics of TESL have been formally developed in the PhD thesis of Hai Nguyen Van.

Getting started with TESL Getting started

After installing the TESL feature, just create a regular project and then a file with extension .tesl. Answer yes if Eclipse asks if the XText nature should be added to your projet and you are done.

To run a TESL specification, use the Run as TESL simulation item in the Run As... section of the pop-up menu either on the file in the ressource view or in the editor pane.

To see the results of the run, the easiest thing to do is to put the following directive:

@output svg standalone

in your TESL source file to request SVG output with the creation of an HTML document which displays it (see the reference manual for details about output formats).

Then open the HTML file in your favorite web browser (the internal web browser of Eclipse works fine) to see your results.

TESL basics

TESL is about clocks (which model events), ticks (which model occurrences of an event) and time (the date at which events occur). Each clock has a time domain, and each tick on a clock has a tag (its date) in the time domain of the clock.

TESL allows three kinds of relations between clocks:

• implication relations, which create a tick on the slave clock when a tick is present on the master clock;
• time delayed implication relations, which create a tick on the slave clock a given time delay (measured as a duration, not as a number of ticks) after a tick is present on the master clock;
• tag relations, which define the relative speed at which time flows on different clocks.

The TESL runtime library supports clocks with any time domain on which comparison, addition, subtraction, product and quotient are defined. The TESL language has currently only unit clocks (only one possible tag, for pure events without a notion of date), int clocks (with integer time tags in {$\mathbb{Z}$}), decimal clocks (with finite but arbitrary long decimal development for tags in {$\mathbb{D}$}), rational clocks (with rational tags in {$\mathbb{Q}$}), and float clocks (with floating point time tags). Similarly, the TESL runtime library supports any tag relation which is an increasing function of tags (in order to preserve causality), but the TESL language only has the same tags relation and affine tags relations (with a positive coefficient).

The TESL language also provides some syntactic sugar to build periodic and sporadic clocks which are useful to run simulations.

A first example

Let us start with a very simple example: Line 1 declares a clock with integer tags which has sporadic ticks at tags 1, 2 and 3.
Line 2 declares a clock with the unit time domain, a domain with only one value, so it amounts to having no time tags on this clock.
Line 4 says that each time there is a tick on the master clock, there is one on the slave clock.
Line 6 is an indication to the simulator stating that the master clock should be used as the time reference for the display of the VCD

Running this file through TESL produces the following output:

As expected, the master clock ticks at dates 1, 2 and 3, and the slave clock ticks each time the master clock ticks.

Understanding implications and time scales Time scales

Here is another simple example which illustrates the effect of implications, and also shows that each clock has its own time scale: Here, clock master1 ticks at 1, 4 and 7, and clock master2 ticks at 2 and 5. Both clocks imply the slave clock. Let's have a look at the output:

This result is surprising at first sight because there are only 3 instants where the clocks tick. This is because the time scales of master1 and master2 are unrelated, so at the first instant, both master clocks tick, but the date is 1 on master1 and 2 on master2. At the second instant, both clocks also tick, and the date is 4 on master1 and 5 on master2. At the third instant, there are no more ticks on master2, so only master1 ticks at date 7. Since master1 is used as the tag reference in the display, the three instants are displayed according to the time scale of master1.

Since both clocks imply slave, there is a tick on this clock at each of the 3 instants in the simulation.

In order to get what we could expect, we have to state that the time scales are the same on master1 and master2. This is done on line 5 in the following specification: which gives the following result:

This time, since master1 and master2 share the same time scale, the tick at 2 on master2 is between the ticks at 1 and 4 on master1, and the tick at 4 on master2 is between the ticks at 4 and 7 on master1. slave ticks when master1 or master2 ticks.

For more details about tag relations and some surprising effects, see the relativistic effects page.

Computed implications Implications

When specifying an implication between two clocks, it is possible to compute the master clock of the implication from source clocks. In the TESL model, the computation is performed by a state machine which reacts to the ticks from the source clocks and produces the ticks of the master of the implication. In the TESL language, four computations are available:

• the filtered by implication which computes the master clock by filtering the source clock according to a pattern;
• the delayed by on implication which delays the ticks of a source clock by counting a given number of ticks on another source clock before producing a tick on the master clock;
• the sustained from to implication which copies ticks from the first source clock to the master clock when they occur between a tick of the second source clock and a tick of the third source clock;
• the when implication which copies ticks from the source first clock to the master clock only when the second source clock has a tick (it computes the logical AND of the two source clocks);
• the time delayed by on implication which delays the ticks of the first source clock by a duration measured on the time scale of the second source clock before producing a tick on the master clock.

Filtered implication Filtered

A filtered implication filters a source clock according to a pattern to compute the master clock of the implication. In the TESL language, this pattern has the form skip,keep (repskip, repkeep)*, where skip is the initial number of ticks to skip, keep is the number of ticks to keep after skipping, and repskip and repkeep is a repeated pattern of ticks to skip and to keep for the master clock. The repeat part is optional, so the pattern 999,1 produces only one tick on the master clock at the 1000^th tick of the source clock.

Here is an illustrative example of filtered implication: Here, master is a clock with integer tags which is periodic with period 1 and offset 1. This means that it will have ticks tagged 1, 2, 3 and son on. The slave clock is a unit clock which is implied by master from which the first 3 ticks are skipped, the 4 following ticks are kept, and then, 1 tick is skipped and 2 are kept repeatedly.

The result of the simulation (stopped after 15 steps) is as follows:

Delayed implication Delayed

A delayed implication simply delays the first source clock by counting n ticks on the second (or counting) source clock :

The result of the simulation (stopped after 10 steps) is as follows:

We see that the slave clock ticks at the 3^rd tick of couting after a tick on master.

The delayed implication has two variants:

• the immediately variant, which counts a tick on the counting clock even if it is simultaneous with a tick on the master clock;
• the with reset variant, which resets the delay each time the master clock ticks.

The two variants can be combined as in: master immediately delayed by 5 with reset on counting implies slave

Example:

gives the following result:

The delayed implication on slave2 counts the tick on couting which occurs simultaneously with the tick on master, therefore, slave2 ticks one tick on counting before slave1.

Sustained implication Sustained

A sustained implication is an implication which is started by a tick on a first source clock and stopped by a tick on a second source clock. For instance: gives the following result:

This example shows that ticks on the begin and end clocks are not taken into account immediately: on tick on the starting clock activates the implication for the strict future and a tick on the stopping clock deactivates the implication for the strict future.

The immediately variant of the sustained implication starts the implication at the very instant where the starting clock ticks. The weakly variant of the sustained implication is an experimental feature (it reacts to the absence of a tick) which stops the implication at the very instant where the stopping clock ticks.

The following example allows to compare these variants:

Which gives:

Here slave_imm ticks at 2 because the implication is started immediately by the tick on start, so the tick on master implies a tick on slave_imm. slave_weak does not tick at 2 and 3 because it was started at 2 by the tick on begin, but since the sustained implication is weak, it is killed instantaneously at 3 by the tick on end. slave_imm_weak combined both behaviors: the implication starts immediately when begin ticks, and stops immediately when end ticks.

When implication When

The when implication computes the logical AND of two clocks: the slave clock is implied when both source clocks have a tick.

gives the following result:

The when not implication is also available as an experimental feature (it reacts to the absence of ticks). It implies a tick when there is a tick on the master clock and no tick on the sampling clock:

gives the following result:

The when not implication can be used to compute leap years:

Await implication Await

The await implication implies a tick on its slave clock when all its master clocks have ticked. For instance:

gives:

clock s ticks each time clocks m1 and m2 have ticked. It ticks at 2 because m1 ticked at 1 and m2 ticked at 2, it ticks at 3 because both m1 and m2 ticked at 3, and it ticks at 6 because m2 ticked at 4 and m1 ticked at 6. It does not tick at 7 because it is still waiting for m1 to tick.

The await implication allows one to wait for the occurrence of some events without bothering about the order in which they occur.

It is possible to reset the await implication when some event occurs. The reset can be strong when no tick should be implied on the slave clock when the reset event occurs, even if all master clocks have ticked at this instant. It can also be weak when a tick should be implied on the slave clock when the reset event occurs at the instant at which all the master clocks have ticked. The following example shows the different variants:

At 2, s has a tick because the corresponding await implication has no reset clock. sr also has a tick because the reset is weak. However, srw has no tick because the reset is strong and preempts the (weak) await implication although both m1 and m2 have ticked.

The tick on m2 at 4 is cleared by the occurrence of r at 4 for the two await with reset implications. Therefore, sr and srw tick only at 7, when the respective await implications have seen both m1 and m2. However, s ticks at 6 when it sees an occurrence of m1 because it has already seen an occurrence of m2 at 4 and was not reset.

Time delayed implication Time delayed

Instead of delaying ticks by counting a given number of ticks on a clock, the time delayed implication delays ticks by a given duration on a measuring clock's time scale. This kind of implication therefore relies on tags: when a tick is present on the source clock, the delay duration is added to current date on the measuring clock, and a tick is scheduled at the resulting date on the slave clock. The source and slave clocks may be unit clocks or have time scales unrelated with the the time scale of the measuring clock.

Example:

gives:

In this example, we use unit clocks for the master and the slave to illustrate the fact that the time delay is measured on the measuring clock. We use a periodic clock gen to make the unit clock master tick every other tick of gen. To ease the understanding of the example, the measuring clock has the same time scale as the gen clock (line 3). The slave clock always ticks 1.5 units of time measured on measuring after a tick on master. You may notice that no tick is produced on the measuring clock. It is only used as a time reference for durations.

It is possible to cancel the creation of a time delayed tick when some event occurs by using the with reset option in the time delayed implication. For instance:

gives the following result:

The tick which should have occurred on slave at 2.5 (delayed from the tick on master at 1) has been canceled by the occurrence of cancel at 2. However, since there is not occurrence of cancel between 3 and 4.5, the delay of 1.5 from the tick on master at 3 creates a tick at 4.5 on slave. The immediate and strong option of with reset allow you to specify how to handle occurrences of the reset clock which coincide with either a tick on the master clock or a delayed tick. See the reference manual for details.

Syntactic sugar

The TESL language provides constructions that are not directly available in the TESL runtime library. These constructions help in the writing of TESL specifications.

Periodic and sporadic clocks Periodic clocks

Periodic clocks do not exist as primitive objects in TESL. They are built as clocks with a time delayed implication of the clock to itself, with the period of the clock as duration. An initial tick is created at the offset date for bootstrapping the periodic creation of ticks on the clock. Therefore, int-clock c periodic T offset O is translated into int-clock c sporadic O; c time delayed by T implies c.

However, sporadic clocks do not exist either. The sporadic clock modifier is just a TESL language construction which relies on the possibility to create ticks at any date on a clock in the TESL runtime library.

Special case of filtered implications: every Every implication

A frequent use of the filtered by construction is to build a clock which ticks periodically with respect to a master clock. For instance, in the leap year example, we have: which does not make the 4 year period appear explicitly. The TESL language provides syntactic sugar to write this filter as:

More generally, master every N starting at X implies slave is equivalent to master filtered by X,1 (N-1,1)* implies slave.

Next to operator

Another construction provided by the TESL language is the next to operator.

It happens often that you want to find the next tick on some clock after a tick on another clock. For instance, the next sunday after the Easter new moon is the Easter day. This can be expressed in TESL using: Sunday sustained immediately from EasterMoon to Sunday implies Easter, however, this is cumbersome. So the pattern C sustained immediately from T to C is available in the TESL language as C next to T. The variant C strictly next to T requires T to tick strictly after C and is equivalent to C sustained from T to C.

Here is the full specification for computing the Easter day in TESL (valid only for 2014 and 2015):

The result of this specification is shown on the picture below, with the occurrences of Easter marked in red, and the corresponding date added:

Tag relations

Tag relations in TESL allows us to specify how time flows on different clocks. In the previous examples, we have only used the = tag relation, which species that two clocks share the same time scale. In the TESL runtime library, any non-decreasing relation between time scales is supported (this condition is necessary to preserve causality). However, in the TESL language, only affine tag relations (with a positive coefficient) are supported for now.

In the following example, we show how tag relations can be used to model different time scales in a model of an engine.

In this model, time is measured in degrees on the crankshaft and on the camshafts. Since the camshafts turn twice as slow as the crankshaft, time flows twice as fast on the crankshaft clock as on the camshaft clock.

The top dead center is reached every 360 degrees on the camshaft clock, and the ignition must occur 10ms before top dead center. If we assume that the engine runs at 2000rpm, time on the crankshaft clock runs 12000 times faster as real time, and the ignition must occur 50ms after TDC (the period on the camshaft clock is 60ms).

The result of the simulation si given on the following picture:

There is no tick on the realtime, crankshaft and camshaft clocks. They are only used to define time scales. The only real events are top_dead_center and ignition.

Debugging

If the result provided by the TESL solver is not what you expect, this may be because you do not understand your specification as the solver does, or because there is a bug in either the TESL solver or in the TESL language front-end. If you think you have found a bug, please send the simplest specification you can find which exhibits the bug, as well as why you consider it as a bug to the bug receptionist

But first, you should investigate the behavior of your model using the @trace directive.

• @trace _help_ give a message explaining how you can use @trace
• @trace _lets_ dumps the value of let definitions, so that you can inspect what the solver sees
• @trace _all_ makes the solver very verbose (and it slows down the run), showing every detail of the solving steps
• @trace kind₁, (kind_x)* makes the solver display only some kinds of information. Currently available kinds are:
  • info displays the solver state at the beginning and at the end of each instant
  • fine displays how the solver builds time islands, handles implications, tag relations and choses how time advances on each clock
  • finer displays the state of the solver before and after each change in the model
  • error displays only error messages

You may also check the result of your simulation using @dumpres because some VCD display tools may hide details or show artifacts.

For more details, see the reference manual.