You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hello, it seems like I'm running into a few issues when using "top-level" (non-nested) until operators.
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
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)
The text was updated successfully, but these errors were encountered:
Hello, it seems like I'm running into a few issues when using "top-level" (non-nested) until operators.
add_sample
, if the last sample I added was exactly at theget_online_rob
function segfaultsrobs
) takes on the value of RoSI upper, which is incorrect (1 instead of -4 in the example provided)robs
are the sameHere's a script to reproduce the issues I'm seeing:
The text was updated successfully, but these errors were encountered: