Bugs in the until operator

[rolizzlefoshizzle]

Hello, it seems like I'm running into a few issues when using "top-level" (non-nested) until operators.

1. When I use add_sample, if the last sample I added was exactly at the $a$ bound of $\phi_1 U_{[a,b]} \phi_2$, the get_online_rob function segfaults

• doesn't segfault if I add more samples after that

2. The robustness values don't seem correct

• before the window $[a,b]$ it seems like the robustness (element 0 of robs) takes on the value of RoSI upper, which is incorrect (1 instead of -4 in the example provided)
• in the interval, all elements of robs are the same
  • All values are the RoSI lower
    • before the satisfying sample is added, all elements of robs are negative (afterwards $\rightarrow$ positive, respectively)
  • RoSI upper not actually bounding upper bound (should be limited by $\min_{t \in [0,t_{sample}]}\rho(\phi_1,t)$ until a sample after $b$ is added (1, in the example provided)

Here's a script to reproduce the issues I'm seeing:

import stlrom

driver = stlrom.STLDriver()
driver.parse_string("signal x,y\nphi:=(x[t]>0) until_[3,5] (y[t] > 5)")

print("driver received:")
driver.disp()

signal = [[0, 1, 1],  # 0
          [0.5, 1, 1],  # 0.5
          [1, 1, 1],  # 1
          [1.5, 1, 1],  # 1.5
          [2, 1, 1],  # 2
          [2.5, 1, 1],  # 2.5
          [3, 1, 1],  # 3, changing this to 3.00001 stops the seg fault
          [3.5, 1, 1],  # 3.5
          [4, 5.5, 5.5],  # 4
          [4.5, 5.5, 1],  # 4.5
          [5, 5.5, 1]]  # 5

# use this variable to skip accessing robustness at that time:
skip3 = False

for i in range(len(signal)):
    driver.add_sample(signal[i])
    if (signal[i][0] == 3) & skip3:
        print("skipping 3!")
    else:
        robs = driver.get_online_rob("phi")
        print("\n\n time:")
        print(signal[i][0])
        print("\n sample:")
        print(signal[i][1:3])
        print("\n robustness:")
        print(robs)