3  Examples

3.1  Temporal logic

Reglo was developped for programming of synchronous observers. Such an observer checks if a sequence of configurations meets some safety property []. Here are some simple observers:

Once

Let a be a Boolean variable, we want to describe the set of sequences containing at least one configuration where a is true:

Once(a) = [-a]*.a.~~ ;

The preceding equation outlines the first occurence of a. The following definition denotes the same property, but outlines the last occcurence of a:

Once(a) = ~~.a.[-a]* ;

Finally, the following definition outlines “some” occurence, but it is still equivalent:

Once(a) = ~~.a.~~ ;

After

We now want to define the set of traces where a has been true at least once in the past. In order to express the delay, we can use the “true” monomial [], which represents any configuration (do not confuse with the “any sequence” macro ~~= []*):

After(a) = [-a]*.a.[].~~ ;
After(a) = ~~.a.[].~~ ;