mtl package:copilot-libraries

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.