Develop trajectory and duration logic

[roberthsheng]

Definition 2. A state valuation σ is a mapping of signal names x ∈ Var to real values, i.e., a function σ : Var → R. The set of all state valuations is denoted by Σ. A (discrete time) trajectory τ : N → Σ is a mapping from time instants, where time is identified with the natural numbers N, to state valuations.

Satisfaction of an STL formula φ by a (discrete-time) trajectory τ at time instant t ∈ N, denoted as τ, t |= φ, is defined recursively as τ , t |= ⊤ holds, τ, t |= g ≥ c iff G(τ(t)) ≥ c, where G is the linear function defined by expression g, τ , t |= ¬ φ iff τ,t̸|=φ, τ , t |= φ ∨ ψ iff τ,t|=φ or τ,t|=ψ, τ, t |= φU[t1,t2]ψ iff ∃k ∈ {t+t1,...,t+t2} : (τ,k |= ψ)∧∀l ∈ {t,...,k−1} : (τ,l |= φ).

Note that the truth value of an STL formula φ over a trajectory τ at time t thus can be decided at time t + duration(φ) if the values τ(k)(x) are known for all time instants k ∈ {t, . . . , t + duration(φ)} and all variable names x occurring in φ, where duration(φ) is defined as follows: duration(⊤) = 0, duration(g ≥ c) = 0, duration(¬φ) = duration(φ), duration(φ ∨ ψ) = max(duration(φ), duration(ψ)), duration(φU[t1 ,t2 ] ψ) = max(t2 − 1 + duration(φ), t2 + duration(ψ)).

[roberthsheng]

unneeded by implementation of measures.py