TeSSLa: TeSSLa Standard Library for TeSSLa 2.0.0

module LTL

past-time LTL

Imports

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)
Imported from StreamFunctions

average, boolFilter, bursts, burstsSince, const, constIf, count, default, defaultFrom, defined, delay, falling, filter, first, firstEvent, fold, isFirst, last, lift, lift1, lift2, lift3, lift4, lift5, maximum, merge, merge2, merge3, merge4, merge5, merge6, merge7, merge8, mergeUnit, mergeUnit2, mergeUnit3, mergeUnit4, minimum, nil, noEvent, on, period, prev, pure, reduce, resetCount, rising, runtime, sample, slift, slift1, slift2, slift3, slift4, slift5, sum, time, unitIf, zip, zip2, zip3, zip4, zip5

Imported from Types

Bool, Events, Float, Int, String, Unit, raw