Previous Up Next

4  Examples

4.1  Temporal logic

Reglo was developped for programming of synchronous observers. Such an observer checks if a sequence of configurations meets some safety property [2]. 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.[].~~ ;

Previous Up Next