Table of contents
Data types
TESL supports four data types:
- {$\mathbb{Z}$}, the set of integers
- {$\mathbb{D}$}, the set of decimal numbers {$m\times 10^{e}$} with {$m$} and {$e$} in {$\mathbb{Z}$}
- {$\mathbb{Q}$}, the set of rational numbers
- float, the set of IEEE-754 double precision floating point numbers
In order to perform computations, a calculus is associated to each type and defines the {$+$}, {$-$}, {$*$} and {$/$} operations:
- the {$\mathbb{Z}$} calculus performs the usual arithmetics on integers (so {$2/3 = 0$})
- the {$\mathbb{D}$} calculus performs exact arithmetics on decimals (so {$1/3$} raises an exception because of the non-terminating decimal expansion)
- the {$\mathbb{Q}$} calculus performs the usual arithmetics on rationals
- the float calculus performs arithmetics on IEEE-754 numbers restricted to a fixed number of decimal places (the default is 6) using a fixed rounding mode (the default is to round to the nearest representable number, unless the exact value is equidistant from two representable numbers, in which case the smallest one is chosen: see java.math.BigDecimal.ROUND_HALF_DOWN). The number of decimal places and rounding mode can be set using the @doublecalc directive.
Literals
Literals for integers consist in an optional sign ({$+$} or {$-$}) followed by a series of decimal digits: +756, 7867554378767254635467625876365765, or -675463987
Literals for decimals consist in an optional sign followed by a series of decimal digits, a decimal dot, an optional series of decimal digits, and an optional integer exponent prefixed by the letter "e" or "E". The first series of optional digits before the dot can be omitted if the optional second series is present. The dot and second series can be omitted when an exponent is present: 2.e-10, -.28, 564E-20, +36.76.
Literals for rationals consist in an optional sign followed by a fraction of two integers placed between angle brackets: <1/3>, -<5674534/98765>.
Literals for floats are the same as literals for decimals followed by the letter "F": 6.028E23F
Type conversions
Automatic type conversions are performed only when they cause no loss of information, so an integer or a double are automatically converted into a decimal when needed. An integer, a decimal or a float are automatically converted into a rational.
When needed, an integer or a decimal are converted to a double only if they can be represented exactly.
When computing an expression, the most precise type is used for the result. So an expression which contains at least a rational will be evaluated by promoting all its operands to the rational type. An expression which contains no rational but contains at least a decimal will be evaluated by promoting all its operands to the decimal type. An expression which contains only floats and integers will be evaluated by converting its operands to the float type, making an error if an integer cannot be represented exactly as a double.
Type cast operators are available for forcing a conversion (with a possible loss of information). To convert an expression to type type, place it between square brackets with type after the opening bracket: [int 5./2] yields 2, [rational 1]/3 is the same as <1/3>. Casting to floats can be performed using either [float expr] or [double expr].
Constant expressions
In order to make the code more readable and easier to maintain, it is possible to define constant expressions thanks to the let statement:
let int ten = 10 let decimal dec1 = 1.2356 + 1 // 1 is converted to a decimal let decimal dec2 = 1 + .2356 // 1 is converted to a decimal let decimal dec3 = 123.56e-2 let decimal dec4 = 123.E2 let decimal one_over_three = 1.0 / 3 // makes an error because 1.0/3 is not a decimal number let rational one_third = [rational 1] / 3 // exactly 1/3 (3 is converted to a rational) let rational two = <1/3> + <2/3> + 1.0 // exactly 2 as a rational (1.0 is converted to a rational) let float two_dec = 1.F/3 + 2.F/3 + 1 // may be 2.0 or 1.99 or other according to the settings of the float calculus let float one3 = 1.F/3 // a floating point approximation of 1/3
Constants defined by let may be used in the rest of the TESL specification by prefixing their name with "$":
let rational one_third = [rational 1] / 3 let rational two = $one_third + <2/3> + 1.0
Clocks
In TESL, clocks are series of ticks, and ticks have a tag which belongs to the tag domain of the clock. The current version of TESL supports the four types presented above as well as the unit type as tag domains for clocks. The unit type corresponds to the singleton set {$\{*\}$}, and is used as tag domain for pure clocks, with no metric time.
Clock declarations
Unit-clocks are declared using either the U-clock or the unit-clock keyword:
unit-clock a_unit_clock U-clock another_unit_clock
Integer-clocks are declared using either the int-clock or the Z-clock keyword:
int-clock an_integer_clock Z-clock another_integer_clock
Decimal-clocks are declared using either the decimal-clock or the D-clock keyword:
decimal-clock a_decimal_clock D-clock another_decimal_clock
Rational-clocks are declared using either the rational-clock or the Q-clock keyword:
rational-clock a_rational_clock Q-clock another_rational_clock
Float-clocks are declared using either the float-clock, double-clock or the F-clock keyword:
float-clock a_float_clock double-clock another_float_clock F-clock yet_another_float_clock
Clock qualifiers
A clock may be qualified as sporadic or periodic. A sporadic clock has predefined ticks with specified tags which are given as a comma separated list of values. Implicit type conversions as presented in the type conversions section are used, so it is possible to use for instance integer values for specifying the tags of a sporadic decimal-clock:
D-clock decimal_clock sporadic 1, 2.5, 10
the clock decimal_clock will have ticks with tags 1.0, 2.5 and 10.0.
A unit-clock may be sporadic, but since the unit type has only one value, no value is given after the sporadic keyword:
U-clock boot sporadic
the clock boot will have a tick (in this case at the first instant of the simulation).
A clock may be periodic, which means it has ticks with tags in the form {$\mathsf{offset}+n\times\mathsf{period}$}
D-clock clock periodic 1.5 offset 0.2
In this specification, clock clock will have ticks with tags 0.2, 1.7, 3.2, ... The period and offset must be compatible with the tag domain of the clock. If the offset is omitted, it defaults to 0 (which is compatible with all TESL data types).
Currently, a unit-clock may not be periodic (even if we could consider that a unit-clock with period {$*$} is just a clock which ticks at each instant).
Implication relations
Implication relations create ticks on a slave clock under some condition when a master clock has a tick. The condition is evaluated by a Mealy state machine.
Simple implication
The simplest implication relation has an always true condition (the state machine always outputs true):
master implies slave
Here, clock slave will have a tick at each instant where clock master has a tick.
When and when not implications When implication
The when implication has a condition which is true when a sampling clock has a tick:
master when sampling implies slave
Clock slave will have a tick at each instant where both master and sampling have a tick.
The when not implication has a condition which is true when a sampling clock does not have a tick:
master when not sampling implies slave
Clock slave will have a tick at each instant where master has a tick and sampling has no tick. Since the when not implication reacts to the absence of a tick on the sampling clock, it is forbidden to make sampling depend on slave. For instance, the following specification will be rejected because it has no constructive solution (the solution where sampling has a tick at each instant where master has a tick cannot be built only by propagating known information about the model):
master when not sampling implies slave slave implies sampling
Filtered implication
A filtered implication has a condition which is true when the trace of the master clock matches some pattern. Currently, TESL supports patterns in the form skip,keep (repSkip,repKeep)* where skip is the initial number of ticks on master for which the condition is false, keep is the number of following ticks on master for which the condition is true. repSkip and repKeep define a repeating pattern of ticks for which the condition is false, then true. The (repSkip,repKeep)* is optional. A finite pattern is obtained when it is omitted.
master filtered by 1,2 (3,4)* implies slave
In this example, slave will have a tick at the instants of the second and third ticks of master, and then at the instants of the four last ticks of master of each sequence of seven ticks.
Every implication
The every implication is syntactic sugar for a common pattern of the filtered implication where the condition is periodically true.
master every $period starting at $offset implies slave
is equivalent to:
master filtered by $offset,1 ($period-1,1)* implies slave
The starting at part can be omitted, in which case the offset defaults to 0.
Delayed implication
The delayed implication implies a tick on the slave clock when a counting clock has ticked a given number of times since the last tick of the master clock.
master delayed by $count on counting implies slave
At each instant where master ticks, a new Mealy machine is created which counts $count ticks on the counting clock before implying a tick on the slave clock. Therefore, slave has a tick at the very instant where counting has its $countth ticks after a tick on master.
By default, the first tick on counting is ignored if it occurs at the instant at which the Mealy machine is created. In order to count this first tick on counting when it occurs at the same instant as the tick on master, use the immediate variant of the delayed implication:
master immediately delayed by $count on counting implies slave
If you want the delay to be reset each time master ticks, use the with reset variant of the delayed implication:
switch_on implies light_on switch_on delayed by $duration with reset on counting implies light_off
With this variant, only one Mealy machine is used and it is reset to its initial state at each instant where master ticks. Therefore, if master ticks before $count ticks have occurred on counting, the delay is reset.
So in the previous example, the light is switched on when you push the switch_on button and will go off after $duration ticks of the counting clock, but if you push the button again before the duration has elapsed, the light will stay on for another period.
You can of course combine the immediate and the with reset variants
Sustained implication
The sustained implication has a condition which is set to true by a tick on a begin clock and set to false by a tick on an end clock. The master clock therefore implies the slave clock between an occurrence of a tick on the begin clock and an occurrence of a tick on the end clock.
master sustained from begin to end implies slave
By default, the condition becomes true at the next instant after a tick on begin and becomes false at the next instant after a tick on end. We say that the sustained implication is delayed (because it does not start immediately) and strong because it still holds when the end clock ticks. The sustained implication can be made immediate using the immediately keyword, and it can be made weak using the weakly keyword:
master sustained immediately from begin to end implies slave master sustained from begin to end weakly implies slave master sustained immediately from begin to end weakly implies slave
The sustained implication at line 1 will imply a tick on slave if master and begin tick at the same instant.
The sustained implication at line 2 will not imply a tick on slave if master and end tick at the same instant.
Line 3 shows that both variants can be combined.
The sustained implication gives priority to the end clock, therefore, if both begin and end tick in the same instant:
- a sustained implication stays off
- an immediate sustained implication goes on at this instant and will go off at the next instant
- a weak sustained implication (immediate or not) stays off
Since the weak variant reacts to the absence of end to make master imply slave, its is forbidden to make end depend on slave.
Next to implication
The next to implication is syntactic sugar for a common use of the sustained implication for finding the next tick on a clock that follows a tick on another clock:
master next to trigger implies slave
is equivalent to:
master sustained immediately from trigger to master implies slave
This implies a tick on slave at each instant where trigger ticks after master has ticked. By default, a tick is implied on slave when master and trigger tick at the same instant. A strict variant of the next to implication is available when you want a tick on slave only when trigger ticks strictly after master:
master strictly next to trigger implies slave
which is equivalent to:
master sustained from trigger to master implies slave
Await implication
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 can wait for an arbitrary number of events which are given as a space separated list of clocks after the await keyword.
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.
For efficiency reasons, the await implication is not implemented as a Mealy machine because its number of states and transitions would grow exponentially with the number of events to wait for. Instead, the occurrence of the awaited events is stored in an array, and a tick is implied on the slave clock and the array is cleared when all awaited events have occurred. The array is also cleared when the reset clock ticks. An await implication with a weak reset is said to be strong (because the implication holds at the instant at which it is reset), and an await implication with a strong reset is said to be weak (because it does not hold at the instant at which it is reset).
In order to preserve causality, it is forbidden to have the reset clock of a weak await depend on its slave clock (when all master clocks have ticked, the slave clock would tick, implying a tick on the reset clock, so the weak await would be aborted and no tick should be implied on the slave clock, leading to an {$x = \neg x$} kind of equation, which has no solution).
Time delayed implication Time delays
All the implication relations we have seen so far react only to the occurrence of ticks on clocks. The time delayed implication is special because it reacts to the fact that a given duration has elapsed on the time scale of a clock. Its behavior is not described by a Mealy machine but depends on the way time flows on the measuring clock:
U-clock master U-clock slave D-clock measuring master time delayed by 1.5 on measuring implies slave
This specification implies a tick on slave when 1.5 units of time have elapsed on measuring after a tick occurred on master. Therefore, the implied tick on slave may occur at an instant where neither master nor measuring have a tick. Consider the following example:
U-clock master U-clock slave D-clock measuring periodic 2 offset 1 measuring every 2 implies master master time delayed by 1.5 on measuring implies slave @tagref measuring @maxstep 6
which gives the following result:
the measuring clock ticks every 2 units of time starting at 1, and the master clock ticks simultaneously with every other tick of measuring. slave ticks 1.5 units of time on measuring after each tick on master, although there is no other tick on any clock to trigger it. The time delay could also be larger than the period between two ticks of master.
The time delayed implication works by getting the current time on the measuring clock at each instant where the master clock ticks, by adding the time delay to this current time to obtain a value, and by creating a tick on the slave clock when the current time on the measuring clock reaches this value.
Resetting a time delayed implication
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. If the reset clock ticks between the occurrence of the master clock and the expiration of the time delay, the time delayed tick is not created. By default, the interval of sensitivity to the reset clock is open at both ends, so a tick on the reset clock which occurs at the same instant as a tick on the master clock or at the instant when the time delay expires does not cancel the time delayed tick. We say that the reset is delayed (because it becomes active strictly after the occurrence of the master clock) and weak (because it is no longer active at the expiration of the time delay). The immediate and strong options of the reset make the sensitivity interval closed at respectively the starting and the closing ends. The following example illustrates the effect of the different variants of the time delayed implication:
D-clock measuring
D-clock master sporadic 0, 2, 4, 6
tag relation master = measuring
D-clock doreset sporadic 2, 5.5, 9
tag relation doreset = measuring
U-clock slave // no reset
master time delayed by 3 on measuring
implies slave
U-clock slave_reset // default delayed weak reset
master time delayed by 3 on measuring
with reset on doreset
implies slave_reset
U-clock slave_imm // immediate (and weak) reset
master time delayed by 3 on measuring
with immediate reset on doreset
implies slave_imm
U-clock slave_strong // strong (and delayed) reset
master time delayed by 3 on measuring
with strong reset on doreset
implies slave_strong
U-clock slave_immstrong // immediate and strong reset
master time delayed by 3 on measuring
with immediate strong reset on doreset
implies slave_immstrong
@tagref measuring
@output svg standalone
which gives:
The tick at 3 on slave_reset is missing because the occurrence of doreset at 2 cancelled the tick delayed from master at 0. Similarly, the tick at 7 (delayed from master at 4) was canceled by the occurrence of doreset at 5.5.
The tick at 5 on slave_imm was cancelled by the occurrence of doreset at 2 because this occurrence was taken into account by the immediate form of reset although is was simultaneous with the triggering occurrence of master.
The tick at 9 on slave_strong was cancelled by the occurrence of doreset at 9 because this occurrence was taken into account by the strong form of reset although is was simultaneous with the expiration of the delay.
Both ticks at 5 and 9 were cancelled on slave_immstrong, combining the immediate and strong forms of the reset.
Tag relations
In TESL, tag relations are used to specify how time flows on different clocks. They define an equivalence relation between tags on different clocks. Tags that are equivalent according to the tag relations occur at the same instant.
In order to preserve causality, tag relations must be non-decreasing because a decreasing tag relation would make time flow in opposite directions on the two clocks.
Same tags relation
The simplest tag relation is the same tags relation, which specifies that two clocks share the same time scale:
tag relation clock_a = clock_b
With this relation, if two ticks on clock_a and clock_b have the same tag, they belong to the same instant, and if two ticks on clock_a and clock_b occur at the same instant, they have the same tag.
The same tags relation can be used only between clocks which have the same tag domain.
Affine tag relations
Affine tag relations allow time to be offset and to flow at different paces on different clocks with a constant ratio:
tag relation clock_a = $coeff * clock_b + $offset
With this relation, if a tick on clock_b has tag {$t_b$} and a tick on clock_a has tag {$t_a$}, they belong to the same instant if {$t_a = \mathsf{coeff}\times t_b + \mathsf{offset}$}, and reciprocally.
Affine tag relations can be used only between clocks which have the same tag domain.
It is important to note that according to the tag domain of the clocks, such a tag relation may be more complicated than it seems. For instance, with integer-clocks:
int-clock clock_a sporadic 2, 5 int-clock clock_b sporadic 1, 2, 4 tag relation clock_a = 2 * clock_b + 0
if we observe the occurrence of ticks on the time scale of clock_a, which flows the faster, we see ticks on both clocks at 2, a tick on clock_b at 4 (because {$4 = 2\times 2 + 0$}), a tick on clock_a at 5 and a tick on clock_b at 8 (because {$8 = 2\times 4 + 0$}).
But if we observe the occurrence of ticks on the time scale of clock_b, which is coarser, we see ticks on both clocks at 1, a tick on clock_b at 2, a tick on clock_a at 2 and a tick on clock_b at 4. There are two instants at time 2 on the time scale of clock_b because the tick with tag 2 on clock_b and the tick with tag 5 on clock_a are equivalent since with integer calculus, {$(5 - 0)\div 2 = 2$}. Therefore, the instants that were at time 4 and 5 on clock_a are both mapped to an instant at time 2 on clock_b.
More general tag relations General tag relations
The example of an affine tag relation between integer-clocks shows that tag relations are in fact pairs of functions ({$n\mapsto 2\times n +0$} and {$n\mapsto (n-0)\div 2$} in this example) which are not necessarily bijective nor the reciprocal of each other. If {$(d,r)$} is a tag relation between two clocks {$a$} and {$b$}, {$d$} is the direct conversion from tags in the domain of {$a$} to tags in the domain of {$b$}, and {$r$} does the reverse conversion. The only constraints on these functions are:
- {$d$} and {$r$} must be non-decreasing in order to preserve causality;
- {$d\circ r\circ d = d$} and {$r\circ d\circ r = r$} so that ticks with different tags on a clock cannot be made simultaneous.
The textual syntax of the TESL language as currently no support for defining arbitrary tag relations, but the TESL library and its solver allow the definition of more general tag relations. It also supports tag relations between clocks that do not have the same tag domain. For instance, we could define a tag relation between a super-dense clock with domain {$\mathbb{Q}\times\mathbb{N}$} and an integer clock with domain {$\mathbb{Z}$} using the functions {$(t,i)\mapsto\lfloor t\rfloor$} and {$n \mapsto (\frac{n}{1}, 0)$}.
Directives (pragmas)
In order to control the execution of a TESL specification and the format of its output, several directives, or pragmas, are available. They all start with the @ character.
When to stop: @stop and @maxstep When to stop
The execution of a TESL specification automatically stops when the future of all clocks is empty: nothing will ever happen. However, many TESL specifications have an infinite behavior, so the simulator stops by default after 1000 instants. It is possible to change this value using the @maxstep directive followed by an expression which must evaluate to an integer:
@maxstep 10
stops the simulation after computing 10 instants.
It is also possible to stop the simulation when some clock ticks using the @stop directive:
@stop when some_clock
stops the simulation at the instant where some_clock ticks (this instant is still part of the simulation).
Controlling the float calculus with @doublecalc Float calculus
Computations with floating point numbers are not exact. By default, to avoid rounding errors and getting 1.99999998 instead of 2.0, TESL uses 6 decimal places and rounds results to the nearest representable value. You can control the number of decimal places and the rounding mode using the @doublecalc directive, for instance:
@doublecalc 2 (round_down)
sets the float calculus to two decimal places, and rounds results toward zero.
The rounding mode between parentheses is optional.
The available rounding modes match those of java.math.BigDecimal:
- round_ceil round to the greater nearest representable value
- round_down round to the nearest representable value closer to zero
- round_floor round to the smaller nearest representable value
- round_half_down round to the nearest representable value, choosing the closer to zero when they are equidistant
- round_half_even round to the nearest representable value, choosing the one with an even rightmost digit when they are equidistant
- round_half_up round to the nearest representable value, choosing the farther from zero when they are equidistant
- round_up round to the nearest representable value farther from zero
Choosing the time scale for the results: @tagref Time scale
By default, the instants in the output of a simulation are identified with the number of the instant, starting from 0. You can choose to identify the instants with the current time on a clock at this instant using the @tagref clock directive:
@tagref some_clock
This is specially important when using a graphical display of the results since the horizontal time axis will use the time scale of the clock, and make durations visible, while the number of the instant gives no information on durations between instants.
Debugging the specification with @trace Debugging
When a simulation triggers an error or does not provide the expected result, you can display information about what happens during the solving process at each instant using the @trace directive followed by a comma separated list of information kinds. You can get the list of available information kinds using:
@trace _help_
Currently, the following special values are available:
- _help_ display a help message for the @trace directive
- _lets_ dump the value of all let expressions
- _all_ trace all information kinds from the TESL solver
The available information kinds are:
- tags trace computations on tags (may be important when using floating point numbers)
- error trace errors (enabled by default)
- warning trace warnings (enabled by default)
- finer trace finer information about the solving phases
- fine trace fine information about the solving phases
- info trace basic information about the solving phases (state of the clocks and relations before and after solving)
The information displayed using @trace gives access to the internal representation of a specification in the TESL solver. For instance, you will see a time delayed implication for each periodic clock that you declared because periodic clocks are implemented using a time delayed implication from themselves to themselves. If you use a time delayed implication which uses clock measuring for measuring the delay, you will see a __measuring_ruler__ clock which is used internally to trigger the creation of a tick on the slave clock when the delay has elapsed.
Displaying the result with @dumpres Results
To obtain a plain dump of the list of clocks that tick at each instant, use the @dumpres directive. This is very useful to interpret results that may be represented in an ambiguous manner in a graphical tool.
Controlling the output format with @output Output formats
By default, running a simulation produces no output. You can display the results using @dumpres or trace the execution using @trace.
You may generate an output file in the Value Change Dump (VCD), LaTeX/TikZ or SVG formats using the output directive.
In these formats, tags are converted to double precision floating point values. For VCD output, this value is multiplied by 1e6 before being converted to a long integer (64-bit two's complement integer).
The most basic form of the directive is: @output format, where format is either svg, tikz, or vcd. Several @output directives can appear in a TESL file for outputting the results in different formats.
Choosing the clocks to display and their order
For all output formats, it is possible to select only some clocks, to rename them in the output, and to make them appear in a given order using the following fragment in the @output directive:
select clock (-> name)? (, clock (-> name)?)*
When select is used, only the clocks which appear after select will be displayed, and they will be put in the order in which they appear (however, some VCD viewers do not respect this order). Each clock whose name is followed by ->name will be renamed to name.
Selecting a time window
It is possible to restrict the output to an interval between two dates using:
from expr to expr
Dates corresponding to the value of the from and to expressions are included in the output.
Labeling instants
For the tikz and svg formats, it is possible to add the date as a text label along the time line when some clocks have a tick:
label if clock (, clock)*
If clocks have been renamed, the original name should be used.
Setting the horizontal scale
For the tikz and svg output formats, you can set the horizontal scale of the picture using:
xscale expr
The interpretation of the expression depends on the format. For TikZ output, the scale is the number of units along the x axis per unit of time. For the SVG format, the scale is the number of pixels per unit of time. The default value is 1 for TikZ output, 50 for SVG output.
Adjusting the space around the picture
For the TikZ and SVG formats, you can adjust the amount of white space around the picture with:
border=string
If the string is reduced to a single value, it is used for the left, right, bottom and top borders. If the string contains two values, the first one is used for the left and right borders, the second for the bottom and top borders. If the string contains four values, they are respectively use for the left, right, bottom and top borders.
For TikZ output, the string is used as the value or the border option of the standalone document class. If more than one value is given, the string must start with a { and end with a }. LaTeX units may be used in the values. This option has no effect if the standalone option (see below) is not used. If the border option is not used, the natural size of the TikZ picture is used, which works quite well in most cases.
For SVG output, the string is used for the placement of the elements of the SVG picture and the computation of its viewBox attribute. This option has therefore an effect even when no standalone document is generated. Only numerical values can be used (the implicit unit is the pixel). For consistency with the TikZ output format, curly braces are accepted but are not mandatory. You can also use border="auto" to have the borders computed automatically by some Javascript code. If the border option is not used, the placement of the elements of the picture is computed without knowing the exact dimensions of the text elements, which works rather well, except when very short or very long clock names are used.
Generating a standalone picture document
For tikz and svg output, a standalone document can be created to display the picture. A LaTeX document using the standalone document class is created for displaying a TikZ picture, and a HTML document is created for displaying an SVG picture:
standalone (overwrite)?
By default, an existing standalone document is preserved in order not to overwrite the settings you may have fine tuned. I you want to overwrite the standalone document, add the overwrite option.
SVG output with a standalone HTML document allows you to display the result of a simulation with the internal web browser of Eclipse, freeing you from the need to switch between Eclipse and an external viewer.
Custom styles for SVG output
For svg output, you may use a custom CSS style sheet and include some JavaScript code in the picture using:
css = ''name.css'
and
javascript = name.js
The CSS style sheet will be included using:
<?xml-stylesheet type="text/css" href="name.css" ?>
and the javascript code using:
<script type="text/ecmascript" xlink:href="name.js"/>
You may also suppress the default CSS styles which are embedded into the SVG picture (in order to have complete control on the display) using the no-default-css option.
Example
@output vcd select master, slave from 2 to 10
@output tikz select measuring->m, master->a, slave->b
from 4 to 8 label if master, slave
xscale 1.5
border="{5pt 2pt}"
standalone overwrite
will create a .vcd output file containing the output at instants between tags 2 and 10 and showing only clocks master and slave. It will also create a .tikz output file containing the output at instants between tags 4 and 8 and showing only clocks measuring, master and slave renamed as m, a and b. The tags will be scaled by 1.5 to build the time line. A standalone LaTeX file will be generated for displaying the TikZ picture, with extra space (5pt on the left and right sides, 2pt on the bottom and top sides), and this file will be overwritten if it already exists.
The example shows that you can split the directive on several input lines and use indentation (even if the syntax highlighter used for this page does not perform well on such input).
Details about the TikZ output
The TikZ output contains raw TikZ commands so that you can create your own tikzpicture environment with the options you want, and use \input to include these commands. This also allows you to include the output of several simulations in a given picture.
However, for checking rapidly the result of a simulation, the standalone option will create a standalone LaTeX document which includes the TikZ output in a tikzpicture. For instance, if you run a simulation on a specification stored in file demo.tesl, you will get the TikZ output in a file demo.tikz. With the standalone option, a demo.tex file will also be generated. You can then run pdflatex on demo.tex to get your picture in demo.pdf. If you want to use the tikz output in a LaTeX document, you can use the following code:
\documentclass{article}
\usepackage{tikz}
\begin{tikzpicture}
\input{demo.tikz}
\end{tikzpicture}
\end{document}
When using the standalone document, the page size is adjusted to the bounding box of the TikZ picture. However, the resulting bounding box may be too tight, and you can add borders around the picture thanks to the border option:
- border="5pt" will add 5pt on every side of the picture
- border="{5pt 7pt}" will add 5pt to the left and right of the picture, and 7pt to the bottom and top
- border="{5pt 3pt 7pt 6pt}" will add 5pt to the left, 3pt to the right, 7pt to the bottom, and 6pt to the top
In the generated TikZ code, different TikZ styles are used for the clock names, the time lines, the tick marks and so on. You may define these styles before including the TikZ file if you want to override the default definitions:
- tesl clock name is the style of the clock name nodes. It defaults to
[node font=\sffamily, above left, inner ysep=0pt] - tesl time line is the style of the global time line. It defaults to
[->, shorten >=1pt, auto, semithick] - tesl clock line is the style of the individual clock time lines. It defaults to the empty style
[](draw in black) - tesl tick helper is the style of the vertical tick helper lines. It defaults to
[loosely dotted] - tesl clock tick mark is the style of the vertical tick marks on clock time lines. It defaults to
[thick] - tesl tick mark is the style of the vertical tick marks on the global time line. It defaults to empty style
[](draw in black) - tesl tick label is the style of the tick label nodes on the global time line. It defaults to
[below, node font={\sffamily\scriptsize}]
Some commands can be defined using \newcommand in order to override default values:
- \teslclocktickheight the height of tick marks on individual clock time lines. It defaults to 0.6
- \tesltimetickheight the height of tick marks on the global time line. It defaults to 0.2
- \teslxoffsetfromtimeorigin the offset of the start of the time lines with regard to the time origin. It defaults to -1
- \teslextraclocklength the extra length of the time lines after the last displayed time. It defaults to 1
- \teslextratimelinelength the extra length of the global time line (to accommodate for an arrow). It defaults to 0.3
Some special points in the TikZ picture have named coordinates so you can place annotations easily:
- c_<clock_number> is the coordinate of the start of the time line of clock number clock_number. It is also the coordinate of the node which displays the name of the clock. Clocks are numbered from 0 from top to bottom
- c_<clock_number>_end is the coordinate of the end of the time line of clock number clock_number.
- timeline is the coordinate of the start of the global time line.
- timeline_end is the coordinate of the end of the global time line.
If you want to include several TikZ pictures produced by TESL in a LaTeX document, you may define the \teslpicid command before inputing the .tikz file. The expansion of this command will be used as a prefix to the name of the special points in each TikZ picture so that you can avoid name clashes.
Details about the SVG output
The SVG output contains an SVG picture that you can include in a web page or open with an SVG viewer or editor.
However, for checking rapidly the result of a simulation, the standalone option will create a standalone HTML document which includes the SVG output picture. For instance, if you run a simulation on a specification stored in file demo.tesl, you will get the SVG output in a file demo.svg. With the standalone option, a demo.html file will also be generated, which you can open in a web browser to display the picture. If you want to use the svg output in your own HTML document, you can use the following code:
<html> <head><title>Results from demo.tesl</title></head> <body> <object data="demo.svg" type="image/svg+xml"> <p>Text to be displayed if the browser does not support SVG</p> </object> </body> </html>
The viewBox of the svg picture is estimated by the generator, but its real size depends on the fonts used and cannot be computed beforehand. The relative positioning of the clock names and of the chronogram also depends on the fontsize. When generating a standalone HTML document, you can specify the number of px units to add (or remove) from the bounding box of the SVG picture. You can also ask the generator to add some JavaScript to the picture, which will compute the effective bounding box of the picture at display time and automatically adjust the layout of the clock names and chronogram:
- border="5" will add 5px on every side of the picture
- border="{5 7}" will add 5px to the left and right of the picture, and 7px to the bottom and top
- border="{5 3 7 6}" will add 5px to the left, 3px to the right, 7px to the bottom, and 6px to the top
- border="auto" will add some JavaScript to compute the layout and exact viewBox of the picture at display time
Web browsers will display the picture according to the size of the window. If the SVG picture is very long, it will be scaled down and its display height may become too small. It may even happen that you see nothing in the web page because the height is very small. You can fix this by setting the height attribute of the object to 200 (for instance). This will ensure that the picture is visible. A scrollbar will appear if the resulting display width of the picture is larger than the width of the window.
Ids and classes for CSS and JavaScript
The elements in the SVG pictures have a class and an id so that you can select them for CSS styling and in JavaScript code:
- clockname is the class of the text elements which display the name of the clocks
- clockline is the class of the line elements used for the time line of each clock
- timeline is the class of the line element used for the global time line at the bottom of the picture
- tickhelper is the class of the line elements used for highlighting the alignment of ticks (guiding or helper line)
- tickmark is the class of the line elements used to mark the ticks on the global time line
- clktickmark is the class of the line elements used to mark the ticks on the time line of the clocks
- ticklabel is the class of the text elements used to put labels under the ticks of the global time line
You can look at the CSS styles used for theses classes in the output SVG file.
- c_<clock_number> is the id of the text element which displays the name of a clock. Clocks are numbered from 1 from top to bottom
- l_<clock_number> is the id of the line element used for the time line of a clock.
- timeline is the id of the global time line element
- h_<tag> is the id the line element used for the helper line at a given tag. If the tag is not an integer, the decimal dot is replaced by an underscore.
- m_<tag> is the id of the line element used to mark a tick at a given tag on the global time line (same convention for the decimal point)
- cm_<clock_number>_<tag> is the id of the line element used to mark at a given tag on the time line of a given clock.
- d_<tag> is the id of the text element used to put a label on the global time line at a given tag (d stands for date)
The SVG picture contains two svg elements. The first one has id clocknames and contains the text elements which display the name of the clocks. The second one has id chrono and displays the chronogram.
This can be used to highlight some elements in the pictures. For instance, the following CSS style sheet will highlight the event at date 110 with a red display color:
Assuming you wrote this in a myStyles.css file, you can make the SVG picture use these styles with:
output svg css = "myStyles.css"
If you want to replace the CSS styles completely, you can suppress the default styles which are included in the SVG picture using:
output svg css = "myStyles.css" no-default-css
The following example shows how to modify the SVG picture using JavaScript code. Here, we add a custom label below the labels at dates 110 and 460 to make the picture easier to understand. The viewBox of the picture is enlarged to make the added labels visible:
Assuming you wrote this code in a enhance.js file, you can make the SVG picture use this code with:
output svg javascript = "enhance.js"