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
Reference papers
[1] BouJacHarPro2014MEMOCODE, 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-01583815, 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-AFP, 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.
Downloading TESL
TESL is available as an Eclipse feature. You can install it from the update site http://wdi.supelec.fr/tesl-update-site.
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/ubuntunovnc-tesl
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:
int-clock master sporadic 1, 2, 3 unit-clock slave master implies slave @tagref master
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:
int-clock master1 sporadic 1, 4, 7 int-clock master2 sporadic 2, 5 unit-clock slave master1 implies slave master2 implies slave @tagref master1
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:
int-clock master1 sporadic 1, 4, 7 int-clock master2 sporadic 2, 5 unit-clock slave tag relation master1 = master2 master1 implies slave master2 implies slave @tagref master1
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 1000th tick of the source clock.
Here is an illustrative example of filtered implication:
int-clock master periodic 1 offset 1 unit-clock slave master filtered by 3,4 (1,2)* implies slave @maxstep 15 @tagref master
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 :
decimal-clock master periodic 2 offset 0.5 decimal-clock counting periodic 1 offset 1 tag relation master = counting unit-clock slave master delayed by 3 on counting implies slave @maxstep 10 @tagref counting
The result of the simulation (stopped after 10 steps) is as follows:
We see that the slave clock ticks at the 3rd 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:
decimal-clock master periodic 2 offset 1 decimal-clock counting periodic 1 offset 1 tag relation master = counting unit-clock slave1 unit-clock slave2 master delayed by 3 on counting implies slave1 master immediately delayed by 3 on counting implies slave2 @maxstep 10 @tagref counting
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:
int-clock master periodic 1 offset 1 int-clock begin periodic 3 offset 2 int-clock end periodic 5 offset 3 tag relation master = begin tag relation master = end unit-clock slave master sustained from begin to end implies slave @maxstep 10 @tagref master
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:
int-clock master periodic 1 offset 1 int-clock begin periodic 3 offset 2 int-clock end periodic 5 offset 3 tag relation master = begin tag relation master = end unit-clock slave unit-clock slave_imm unit-clock slave_weak unit-clock slave_imm_weak master sustained from begin to end implies slave master sustained immediately from begin to end implies slave_imm master sustained from begin to end weakly implies slave_weak master sustained immediately from begin to end weakly implies slave_imm_weak @maxstep 10 @tagref master
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.
int-clock master sporadic 1, 3, 4, 5, 7, 8 int-clock sampling sporadic 2, 4, 6, 7 tag relation sampling = master unit-clock slave master when sampling implies slave @tagref master
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:
int-clock master sporadic 1, 3, 4, 5, 7, 8 int-clock sampling sporadic 2, 4, 6, 7 tag relation sampling = master unit-clock slave master when not sampling implies slave @tagref master
gives the following result:
The when not implication can be used to compute leap years:
int-clock year periodic 1 offset 1 unit-clock year4 // every 4 years year filtered by 0,1 (3,1)* implies year4 unit-clock year100 // every 100 years year4 filtered by 0,1 (24,1)* implies year100 unit-clock year400 // every 400 years year100 filtered by 0,1 (3,1)* implies year400 unit-clock leap // leap years // years that are a multiple of 4 and not a multiple of 100 are leap year4 when not year100 implies leap // years that are a multiple of 400 are leap year400 implies leap @maxstep 2200 @tagref year
Await implication Await
The await implication implies a tick on its slave clock when all its master clocks have ticked. For instance:
Z-clock t sporadic 0, 1, 2, 3, 4, 5, 6, 7
Z-clock m1 sporadic 1, 3, 6
Z-clock m2 sporadic 2, 3, 4, 7
U-clock s
tag relation m1 = t
tag relation m2 = t
await m1 m2 implies s
@tagref t
@output svg standalone select m1, m2, s border="{10 0 0 0}"
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:
Z-clock t sporadic 0, 1, 2, 3, 4, 5, 6, 7 Z-clock m1 sporadic 1, 2, 3, 6 Z-clock m2 sporadic 2, 3, 4, 7 Z-clock r sporadic 2, 4 U-clock s U-clock sr U-clock srw tag relation m1 = t tag relation m2 = t tag relation r = t await m1 m2 implies s // await with no reset await m1 m2 with weak reset on r implies sr // (strong) await with weak reset await m1 m2 with strong reset on r implies srw // (weak) await with strong reset @tagref t @dumpres @output svg standalone select m1, m2, r, s, sr, srw
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:
decimal-clock gen periodic 1 offset 1 decimal-clock measuring tag relation gen = measuring unit-clock master gen filtered by 0,1 (1,1)* implies master unit-clock slave master time delayed by 1.5 on measuring implies slave @maxstep 10 @tagref gen
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:
decimal-clock gen periodic 1 offset 1 decimal-clock measuring tag relation gen = measuring unit-clock master gen filtered by 0,1 (1,1)* implies master unit-clock cancel gen filtered by 1,1 (2,1)* implies cancel unit-clock slave master time delayed by 1.5 on measuring with reset on cancel implies slave @maxstep 10 @tagref gen
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:
year filtered by 0,1 (3,1)* implies year4
which does not make the 4 year period appear explicitly. The TESL language provides syntactic sugar to write this filter as:
year every 4 implies year4
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.
rational-clock realtime rational-clock crankshaft rational-clock camshaft tag relation crankshaft = 2 * camshaft + 0 // 2000 rpm = 2000 * 360 / 60 = 12000 degrees per second tag relation crankshaft = 12000 * realtime + 0 rational-clock top_dead_center periodic 1 offset 0 tag relation camshaft = 360 * top_dead_center + 0 unit-clock ignition // Ignition 10ms before TDC = 50ms after TDC at 2000rpm (T = 30ms => 60ms on camshaft) top_dead_center time delayed by 0.05 on realtime implies ignition @tagref realtime @maxstep 10
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 kind1, (kindx)* 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.