nickovic / rtamt

Specification-based real-time monitoring library
BSD 3-Clause "New" or "Revised" License
50 stars 20 forks source link

ValueError: max() arg is an empty sequence when eventually[time] too long #157

Closed wilhelmw201 closed 2 years ago

wilhelmw201 commented 2 years ago

Hi, I get the above ValueError when I run this code snippet. If I use a shorter time (<20) in the eventually brackets the evaluation goes fine. Is this a feature?

import rtamt
spec = rtamt.STLDiscreteTimeSpecification()
spec.name = 'Example'
spec.declare_var('p1', 'float')
spec.declare_var('p2', 'float')
spec.declare_var('out', 'float')
spec.set_var_io_type('p1', 'input')
spec.set_var_io_type('p2', 'input')
spec.set_var_io_type('out', 'output')
spec.spec = "out = eventually[0, 50] (p1 or p2)"
spec.parse()
data = {'time': range(21), 'p1': [1.0]*21, 'p2': [1.0]*21}
rob = spec.evaluate(data)
print(rob)

Also the following snippet doesn't work unless I set the time in the eventually bracket real low.

import rtamt

spec = rtamt.STLDiscreteTimeSpecification()
spec.name = 'Example'
spec.declare_var('p1', 'float')
spec.declare_var('p2', 'float')
spec.declare_var('out', 'float')
spec.set_var_io_type('p1', 'input')
spec.set_var_io_type('p2', 'input')
spec.set_var_io_type('out', 'output')
spec.spec = "out = eventually[0, 500] (p1 or p2)"
spec.parse()
data = {'time': [0.0, 100.0, 200.0, 300.00000000000006, 400.0, 500.0, 600.0000000000001, 700.0000000000001, 800.0, 900.0, 1000.0, 1100.0, 1200.0000000000002, 1300.0, 1400.0000000000002, 1500.0, 1600.0, 1700.0000000000002, 1800.0, 1900.0000000000002, 2000.0], 'p1': [1.0]*21, 'p2': [1.0]*21}
rob = spec.evaluate(data)
print(rob)

I am using commit da51c815515dfc7cdec1ff592ce463d5b77ff17

nickovic commented 2 years ago

Thanks for pointing this out, it was indeed a bug, that is now fixed.

Note that in the second example, you may want to indicate that each step is 100s, by setting spec.set_sampling_period(100, 's'), otherwise the library will assume that the time step is the default 1s.