mtl is:module

Metric Temporal Logic (MTL) over a discrete time domain consisting of sampled time values. The operators in this module receive two additional arguments: a clock stream clk, indicating the current time, and a distance between samples dist. For the purposes of explaining the MTL aspects, we ignore those arguments. If you are using streams for which you can treat time as a discrete increasing number, you can safely assume that the clock is a counter (i.e., [0, 1, 2,...], which can be defined by the stream counter = [0] ++ counter) and the distance between samples is 1.

Reexports of most definitions from "mtl" and "transformers". For details check out the source.

This module defines operations for producing SMTLib2-compatible queries useful for interfacing with solvers that accecpt SMTLib2 as an input language.