introduction of sub_specs changes robustness traces

Hi all, I am facing some issues with the use of sub_specs for discrete-time offline monitoring. It would be great if you could check it :)

I set up the following experiment with two specs: 1) a formula with subspecs:

always(premise implies response)
premise = (req >= 3)
response = (eventually[0:5]((gnt>=3) and (gnt<=10)))

2) its equivalent rewriting into a formula without subspecs,

always((req>=3) implies (eventually[0:5]((gnt>=3) and (gnt<=10))))

Expected behavior: I was expecting the two robustness traces to be equal.

Observed behavior: The trace monitoring the unique formula is:

[[0, 3.0], [1, 3.0], [2, 3.0], [3, 3.0], [4, 3.0], [5, 3.0], [6, 3.0], [7, 3.0], [8, 3.0], [9, 3.0], [10, 3.0], [11, 3.0]]

while the trace monitoring the formula with subspecs is:

[[0, -3.0], [1, -3.0], [2, -3.0], [3, 3.0], [4, 3.0], [5, -3.0], [6, -3.0], [7, -3.0], [8, -3.0], [9, -3.0], [10, -3.0], [11, -3.0]]

How to reproduce: See minimal example in python below.

Environment details: I am running it on Ubuntu 20.04, in a virtual env with Python 3.8. RTAMT has installed from the main branch on git, commit 2f2a252f99535d151c3f94033352ce11142afd81

import rtamt

# define data and variables types
data = {
    "time": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11],
    "req": [0.0, 0.0, 0.0, 6.0, 6.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0],
    "gnt": [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 6.0, 6.0, 0.0, 0.0, 0.0],
}

var_types = {
    "req": "float",
    "gnt": "float",
    "premise": "float",
    "response": "float",
}

# example 1: unique stl formula
unique_formula = 'always((req>=3) implies (eventually[0:5]((gnt>=3) and (gnt<=10))))'

spec1 = rtamt.StlDiscreteTimeSpecification()
for var, type in var_types.items():
    spec1.declare_var(var, type)
spec1.spec = unique_formula
spec1.parse()

# example 2: equivalent stl formula with 2 subformulas
premise_formula = 'premise = (req >= 3)'
response_formula = 'response = (eventually[0:5]((gnt>=3) and (gnt<=10)))'
premise_response_formula = 'always(premise implies response)'

spec2 = rtamt.StlDiscreteTimeSpecification()
for var, type in var_types.items():
    spec2.declare_var(var, type)
spec2.add_sub_spec(premise_formula)
spec2.add_sub_spec(response_formula)
spec2.spec = premise_response_formula
spec2.parse()

# evaluate robustness
robustnesses = []
for spec in [spec1, spec2]:
    robustness_trace = spec.evaluate(data)
    robustnesses.append(robustness_trace[0][1])
    print(robustness_trace)

assert robustnesses[0] == robustnesses[1], "the robustness should be equal"

Thanks!

nickovic / rtamt

introduction of sub_specs changes robustness traces #164