TeSSLa: TeSSLa Standard Library for TeSSLa 1.2.4

module LTL

past-time LTL

ANCHOR historically

historically(a: Events[Bool]): Events[Bool]

Expects a pure input stream which is initialized (has an event at timestamp 0). Returns a stream which gets false the first time the input stream gets false.

It represents the formula H a = !O !a and is equal to !once(!a). (See also once)

Usage example:

in a: Events[Bool]
def d = historically(a)
out d

Trace example:

option timeDomain: [-0.1,6]
stream a: bool
stream d: bool
---
0: a = true
0: d = true
2: a = false
2: d = false
3: a = true

def historically(a: Events[Bool]): Events[Bool] = !once(!a)

ANCHOR once

once(a: Events[Bool]): Events[Bool]

Expects a pure input stream which is initialized (has an event at timestamp 0). Returns a stream which gets true the first time the input stream gets true.

It represents the formula O a = true S a and is equal to since(true, a). (See also since)

Usage example:

in a: Events[Bool]
def d = once(a)
out d

Trace example:

option timeDomain: [-0.1,6]
stream a: bool
stream d: bool
---
0: a = false
0: d = false
2: a = true
2: d = true
3: a = false

def once(a: Events[Bool]): Events[Bool] = since(true, a)

ANCHOR since

since(a: Events[Bool], b: Events[Bool]): Events[Bool]

Expects pure input streams which are initialized (have an event at timestamp 0). Returns a stream which gets true every time both input streams are true. The output stream gets false every time the first input stream gets false.

It represents the formula a S b.

Usage example:

in a: Events[Bool]
in b: Events[Bool]
def d = since(a, b)
out d

Trace example:

option timeDomain: [-0.1,8]
stream a: bool
stream b: bool
stream d: bool
---
0: a = false
0: b = false
0: d = false
1: a = true
2: b = true
2: d = true
3: b = false
4: a = true
5: a = false
5: d = false
6: b = true
7: a = true
7: d = true

def since(a: Events[Bool], b: Events[Bool]): Events[Bool] = MITL.sinceInfinity(0, a, b)