StlDenseTimeSpecification semantic bug?

[ANogin]

The following code:

import rtamt

spec = rtamt.StlDenseTimeSpecification()
spec.name = "Bug?"
spec.declare_var("y", "int")
spec.declare_var("x", "int")
spec.set_var_io_type("y", "input")
spec.set_var_io_type("x", "output")
spec.spec = "((historically[0,5] x==1) and y) implies (eventually[0, 1] x==0)"

spec.parse()
spec.pastify()
rob = spec.update(["x", [(0.0, 1)]], ["y", [(0.0, 0)]])
for var, time, val in [
    ("x", 1.0, 1),
    ("y", 7.0, 1),
    ("x", 10.0, 0),
    ("y", 11.0, 0),
]:
    print(f"{var=} {time=} {val=}")
    rob = spec.update([var, [(time, val)]])
    print(f"Robustness @{time}: {rob}")

prints

var='x' time=1.0 val=1
Robustness @1.0: []
var='y' time=7.0 val=1
Robustness @7.0: []
var='x' time=10.0 val=0
Robustness @10.0: []
var='y' time=11.0 val=0
Robustness @11.0: []

with python 3.12 and latest rtamt from github (v 0.4.1).

Am I misunderstanding the intended semantics in some way, or is the specification supposed to be violated at t=7, with the violation caught when the value at t>8 is processed?

[ANogin]

P.S. Of course, if this is just me doing something wrong, or misunderstanding what should happen, I would appreciate any pointers you can provide. Thanks!