search

nickovic / rtamt4ros

Real-time monitoring tool for ROS applications that uses the rtamt library
BSD 3-Clause "New" or "Revised" License
5 stars 2 forks source link

Always / eventually operator error #20

Open apalapramanik opened 1 year ago

apalapramanik commented 1 year ago

Running RTAMT4ROS for a simple specification (always(value>1)) raises this exception:

"raise LTLNotImplementedException('Always operator is not implemented in the STL online monitor.') rtamt.exception.ltl.exception.LTLNotImplementedException: Always operator is not implemented in the STL online monitor."

Ubuntu 20 ROS Noetic

nickovic commented 1 year ago

The unbounded future temporal operators (i.e. always, eventually and until) without bounds, are not supported by the runtime monitoring library, as they would need an unbounded horizon to determine the outcome. They are though supported for the offline evaluation (because the entire trace is available, and hence the "future" is determined).

If you have a formula always (phi), you may want either to monitor phi in an online fashion (determining at every point in time the robustness degree of phi at that time) or historically(phi) (which remebers what has been the worst robustness degree pf phi so far).

I hope this helps.

apalapramanik commented 1 year ago

How can I enable online monitoring? Specification phi gets value in terms of ros msg. In the paper how have you used the specification "out.value = always(abs(cmd.linear.x - robot.twist.twist.linear.x ) <= 0.5)" ? I want to do something similar but I am unable to figure out.