Computing leap years in TESL

Table of contents

There are several ways of computing leap years in TESL, which illustrate different coding styles.

A year is leap is it is a multiple of 4, but not a multiple of 100, unless it is a multiple of 400.

Using pure clocks and filteringWith pure clocks

This specification of leap years relies on pure clocks and filtered by implications.

int-clock year periodic 1 // compute year numbers

unit-clock year4  // ticks for each year which is a multiple of 4
year filtered by 0,1 (3,1)* implies year4

unit-clock year100  // ticks for each year which is a multiple of 100
year filtered by 0,1 (99,1)* implies year100

unit-clock year400  // ticks for each year which is a multiple of 400
year filtered by 0,1 (399,1)* implies year400

unit-clock leap  // ticks for leap years
// A year is leap if it is divisible by 4 but not by 100
year4 sustained immediately from year4 to year100 weakly implies leap
// However, a year divisible by 400 is leap
year400 implies leap

@maxstep 2200

This specification can be made more readable using every and when not:

int-clock year periodic 1

unit-clock year4
year every 4 implies year4

unit-clock year100
year every 100 implies year100

unit-clock year400
year every 400 implies year400

unit-clock leap

year4 when not year100 implies leap
year400 implies leap

@maxstep 2200

Using integer periodic clocksWith integer clocks

Instead of filtering the ticks on clock year, we can rely on tags and periodic clocks:

int-clock year periodic 1 // count years

int-clock year4 periodic 4 // build a clock with period 4 on the same time same as year
tag relation year4 = year

int-clock year100 periodic 100 // build a clock with period 100 on the same time same as year
tag relation year100 = year

int-clock year400 periodic 400 // build a clock with period 400 on the same time same as year
tag relation year400 = year

unit-clock leap
// A year is leap if it is divisible by 4 but not by 100
year4 when not year100 implies leap
// However, a year divisible by 400 is leap
year400 implies leap

@maxstep 2200

Using pure clocks and filteringWith pure clocks

Using integer periodic clocksWith integer clocks

The result