Parametric temporal logic for "model measuring"