nickovic / rtamt Goto Github PK

View Code? Open in Web Editor NEW

47.0 47.0 20.0 7.05 MB

Specification-based real-time monitoring library

License: BSD 3-Clause "New" or "Revised" License

CMake 1.22% Python 93.77% C++ 3.70% C 0.05% ANTLR 1.21% Dockerfile 0.05%

rtamt's People

Contributors

Stargazers

Watchers

Forkers

bentleyjoakes mehrdad-moradi cirrostratus1 xiaoyaooo yuanzhou-yzhou jaksicstefan sguysc tomyyamy transafeailab beeblebroxvi smallzjuer lawbreaker2022 yuji-date-t mengyuliu0520 sjtuguofei schmidt-embedded-systems-gmbh

rtamt's Issues

cmake -DPythonVersion=3 ../ does not work?

It is master[5366349].
cmake version is v3.17

build$ cmake -DPythonVersion=3 ../
CMake Warning (dev) in CMakeLists.txt:
  No project() command is present.  The top-level CMakeLists.txt file must
  contain a literal, direct call to the project() command.  Add a line of
  code such as

    project(ProjectName)

  near the top of the file, but after cmake_minimum_required().

  CMake is pretending there is a "project(Project)" command on the first
  line.
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Warning at /opt/cmake-3.17.3-Linux-x86_64/share/cmake-3.17/Modules/FindBoost.cmake:2007 (message):
  No header defined for python-py35; skipping header check (note: header-only
  libraries have no designated component)
Call Stack (most recent call first):
  cpplib/stl/rtamt_stl_library_wrapper/CMakeLists.txt:16 (find_package)


CMake Error at /opt/cmake-3.17.3-Linux-x86_64/share/cmake-3.17/Modules/FindPackageHandleStandardArgs.cmake:164 (message):
  Could NOT find Boost (missing: python-py35) (found version "1.65.1")
Call Stack (most recent call first):
  /opt/cmake-3.17.3-Linux-x86_64/share/cmake-3.17/Modules/FindPackageHandleStandardArgs.cmake:445 (_FPHSA_FAILURE_MESSAGE)
  /opt/cmake-3.17.3-Linux-x86_64/share/cmake-3.17/Modules/FindBoost.cmake:2166 (find_package_handle_standard_args)
  cpplib/stl/rtamt_stl_library_wrapper/CMakeLists.txt:16 (find_package)


-- Configuring incomplete, errors occurred!
See also "/mnt/data/repos/rtamt/rtamt/build/CMakeFiles/CMakeOutput.log".

NextOperator and PreviousOperator not supported yet?

Hi @nickovic @TomyYamy,

I tried to parse a specification with next or previous operators but got Syntax errors. I saw here that there are no implementations for token equals the NextOperator or PreviousOperator. Are these two operators not supported yet? Thanks in advance.

get ground truth data from gazebo

Now robot simulator rely on LiDAR data. Probably using ground truth data from gazebo is better.

Probably this info. I can use.
https://answers.ros.org/question/261782/how-to-use-getmodelstate-service-from-gazebo-in-python/
there is no python API for gazebo. we can use just ros API like “$ rosservice call gazebo/get_world_properties”, otherwise C++ API.
http://answers.gazebosim.org/question/924/how-to-use-python-with-gazebo/
It contains useful codes also.
https://github.com/shadow-robot/sr-taco/blob/master/sr_moving_object/src/sr_moving_object/move_objects.py

Documentation update for pypi version

Feature request: Please enhance the README to describe the specific steps used to create the pypi package from this source.

offline STL robustness seems to be different from original STL

I'm not sure why, but semantics of offline STL 'standard' seems to be different from typical STL.

handling interpolation in TL class

I suggested change interpolation function TL.
But now I think it is un-realistic except peace wise constant while implementing continuous time TL.

@nickovic
Do you know whether other TL basic tools support several interpolations or not?
In my experience, no-tool supports it.

Explanation of STLSpecification() and rtamt.STLIOCTSpecification()

I guess,
STLSpecification(): old version which does not support real-time-stamp.
STLIOCTSpecification():new version
I'm not sure, user need old version. In any case we need to add clear description after cleaning up codes.

Support C++ build on setup.py and pkg version

Support C++ build on setup.py and pkg version.

'not eventually(always(x))' does not work.

Difference between C++ and Python versions

I am trying to run examples/basic/monitor_basic.py and also examples/basic/monitor_basic_cpp.py. It seems they behave differently, even though the difference is just the backend. Is this intentional?

agnishom@agnishomDuncan:~/code/rtamt/examples/basic$ python3 monitor_basic_cpp.py 
time=0 rob=120.0
time=1 rob=1.0
time=2 rob=-12.0
agnishom@agnishomDuncan:~/code/rtamt/examples/basic$ python3 monitor_basic.py 
time=0 rob=122.0
time=1 rob=3.0
time=2 rob=-10.0
agnishom@agnishomDuncan:~/code/rtamt/examples/basic$ diff monitor_basic.py monitor_basic_cpp.py 
13c13
<     spec = rtamt.STLSpecification(1)
---
>     spec = rtamt.STLSpecification(0)

Distributing with docker

My colleague suggests us.
Actually I tried other tools with docker. Its distribution is fantastic. the install is just 5 min! and run!

Handling offline and online stuff

I think we had better to separate class of offline and online method.
My mind of name of eval methods are,
online: stl_instance.update()
offline: stl_instance.eval()

I think we can change
rtamt/operation/abstract_operation.py
to offline and online abstract class.
and only offline can call .update() from eval().
(I mean .update() can not call eval() because of online limitation)

guideline for handling interpolation and extrapolation in TL

When time = [0, inf], then we have time bounded trajectory traj_time = [s-time, e-time], how we handle the start bound = [0, s-time) and the end bound = [e-time, inf]?

I think now we just ignore the start bound = [0, s-time)
For the end bound = [e-time, inf], we expect the extrapolation of the end of trajectory, then calculate [e-time, end of bound of timed operator].
That makes sense, other wise, the robustness trajectory becomes shorten and shorten in every nest of formula.

Returning time series robustness

now spec.update() returns just current one step robustness.

I think we can support to output time series robustness in some way, from a STL debugging perspective.

Dejan thinks we just need a wrapper that will call the update in a loop. BTW, the update function is a function of the input and the internal state of the monitor, so the monitor remembers the past inputs

Bounded Future STL reference in the grammar

Reflect the fact that the grammar is for bounded-future STL and not full STL

README.md for each formal languages

Maybe we can put README.md for each formal languages.
The location is maybe under rtamt/rtamt/grammar/xxx/README.md

Version miss matching between code and runtime

in branch pyt23, when running the evaluator, the warring happens,

ANTLR runtime and generated code versions disagree: 4.8!=4.5.1

It's just a warring and not big effect. I rebuild the code side for sure.
It is because of setup.py setting.
I'm not sure how to match the code and runtime version

How we can handle intermediation in ANTLR

We can reduce valuation of syntax like,
!(p or q) = !p and !q
p->q = !p or q
E(p) = True U p
A(p) = !E(!p)
Regarding current codes, we can do it in node code.
We can make guideline also in RTAMT.

How to call STL formulas recursivly.

I know ROS version could do it while utilizing ROS topics.
How to write it in rtamt native in Python? Those are useful if the formula is long or hierarchical notion.

The image is
''''
spec1.spec = 'always((req>=3) implies (eventually0:5))'
spec2.spec = 'not spec1'
''''

It should relates issue #18 also.

returning robustness options.

Current online evaluate output the latest robustness with time stamp. I think it is good as default option.
However, if we consider synchronized update and evaluation like a ROS environment, the input data will be updated with different subscribers separately and closed loop controller need robustness with time drive that is also not synchronized with update.
Maybe we need following options for that.

output current latest data with out any update
output all robustness trajectories which internally rtamt class has.

Handling vector signal

While discussing with Jyo, Theoretically STL can handle vector signal. Maybe it helps robotics space (x,y.theta).
However almost of all requirement depends on some of “distance“ which is converted from vector to scalar.

spec cpp does not support float time

Hi there,

While trying the provided example in examples/basic/monitor_basic_cpp.py, I've found out that if I changed the times in the signals to float number, i.e.:

dataSet = {
         'a': [(0., 100.0), (1., -1.0), (2., -2.0)],
         'b': [(0., 20.0), (1., 2.0), (2., -10.0)]
    }

I would get the following error:

Boost.Python.ArgumentError: Python argument types in
    None.None(Sample, float)
did not match C++ signature:
    None(stl_library::Sample {lvalue}, int)

This does not happen for the Python version of rtamt.STLSpecification. Is this a bug of the cpp version?

Parser error

Hi there,

I got Syntax Error for specification "c = always((a>=3) and eventually(b>4) -> (b>=3))". It would work if I add a time boundary for the eventually operator. Since I couldn't find any documentation about the syntax that is allowed by rtamt, could you please help me understand this error? Thanks in advance.

The simplest example.

I feel we can simplify the example code more. like eliminating import as many as possible.
I also think your examples are implemented with deep concern.
I come up with we can make the simplest example in addition for beginner.

Separate install_requires=[] for python2 and python3 in setup.py

abbreviated form in formula

Just it is useful when formula becomes long.
always := G
eventually := F
imply := ->
and := &
and so on.

It is not urgent.

Parser Error - AttributeError: 'Eventually' object has no attribute 'node'

Thank you for this useful project.

When I try to use the eventually operator, I get the following error. This is with an rtamt installation from today.

Traceback (most recent call last):
  File "mwe.py", line 70, in <module>
    p.prove([spec], var_types, var_types)
  File "mwe.py", line 32, in prove
    rob = spec.offline(self.data)
  File "/home/boakes/Software/miniconda3/lib/python3.7/site-packages/rtamt-0.0.11-py3.7.egg/rtamt/spec/stl/specification.py", line 240, in offline
  File "/home/boakes/Software/miniconda3/lib/python3.7/site-packages/rtamt-0.0.11-py3.7.egg/rtamt/spec/stl/specification.py", line 92, in update
  File "/home/boakes/Software/miniconda3/lib/python3.7/site-packages/rtamt-0.0.11-py3.7.egg/rtamt/spec/stl/evaluator.py", line 23, in evaluate
  File "/home/boakes/Software/miniconda3/lib/python3.7/site-packages/rtamt-0.0.11-py3.7.egg/rtamt/spec/stl/visitor.py", line 52, in visit
  File "/home/boakes/Software/miniconda3/lib/python3.7/site-packages/rtamt-0.0.11-py3.7.egg/rtamt/spec/stl/evaluator.py", line 145, in visitEventually
AttributeError: 'Eventually' object has no attribute 'node'

Here is an example of the failing specification. If the first eventually is changed to always, the specification succeeds in parsing.
out = eventually((AmbientTemperatureSignal1>0) implies eventually[0:5](AmbientTemperatureSignal1==1))

The attached mwe.py and mwe.csv are a minimum working example.

Please let me know any other information you need.
mwe.zip

How long time the STL takes to evaluate?

It’s Kawamura-san’s question. It’s depend on, but we can make some nasty test case.
Maybe we can compare some of evaporators even the purposes are not same.

comparison of evaluation speed

Perhaps we need to confirm how much it is fast.

supporting STL formula nest.

I'm not sure how much rtamt handle it.
To easy to handle complex STL

'Interval' call error

I'm trying [f0c6720] at pyt23.
I find a issue related to 'Interval'. I think some of wrapper setting has issue...

$ python3 monitor_stl_ct.py
Traceback (most recent call last):
  File "monitor_stl_ct.py", line 3, in <module>
    import rtamt
  File "/usr/local/lib/python3.6/dist-packages/rtamt/__init__.py", line 1, in <module>
    from rtamt.spec.stl.specification import STLSpecification
  File "/usr/local/lib/python3.6/dist-packages/rtamt/spec/stl/specification.py", line 17, in <module>
    from rtamt.parser.stl.StlLexer import StlLexer
  File "/usr/local/lib/python3.6/dist-packages/rtamt/parser/stl/StlLexer.py", line 316, in <module>
    class StlLexer(Lexer):
  File "/usr/local/lib/python3.6/dist-packages/rtamt/parser/stl/StlLexer.py", line 318, in StlLexer
    atn = ATNDeserializer().deserialize(serializedATN())
  File "/usr/local/lib/python3.6/dist-packages/antlr4/atn/ATNDeserializer.py", line 87, in deserialize
    sets = self.readSets(atn)
  File "/usr/local/lib/python3.6/dist-packages/antlr4/atn/ATNDeserializer.py", line 211, in readSets
    iset.addRange(Interval(i1, i2 + 1)) # range upper limit is exclusive
NameError: name 'Interval' is not defined

Temporally I'm using 18.04 on Windows 10 (windows power shell). Maybe it does not matter.

Python vs. C++ backend

I'm trying to understand some of the implementation details of this library. There seems to be both a C++ and Python backend, but it's not clear what the relationship between these is. Could you provide some extra information about this? A few questions come to mind:

Does the Python backend call into C++ code, or is it completely standalone? I think it's the latter, but then is there also a variant of the Python backend which calls into C++?
Is there any major difference in functionality, performance, etc. between the backends?
Does the PyPI package include the C++ backend, or is that in the longer-term plan for the package?
If we have the option, should we prefer one backend over the other?

Naming of ct and dt

I think you use ct (continuous time) as dense time.
However many guys misunderstand it as continuous on value space.
I think we can change the name also.

support Offline-STL semantically

I understood current rtamt.STLIOCTSpecification.offline() run online-STL semantics in offline fashion.
Is that possible to implement just typical STL semantically?
I think it is good for debugging the stl formula for biggner. Like once confirm with offline-STL then shift to online-STL, because online-STL has some limitation theoretically.

About output of formula setting

Regarding example,
'''
spec = rtamt.STLIOSpecification(1)
spec.name = 'Example 1'
spec.declare_var('req', 'float')
spec.declare_var('gnt', 'float')
spec.declare_var('out', 'float')
spec.set_var_io_type('req', 'input')
spec.set_var_io_type('gnt', 'output')
spec.spec = 'out = always((req>=3) implies (eventually0:5))'
spec.iosem = 'standard'
'''
Even "out" is not default setting, it does not work when "out" setting is removed.
I think this setting comes from ROS support to output the robustness to the topic.

I think purely python user will not need "out" variable. Further more, I'm sure, how the robustness output is handling on either "out" variable on spec or "spec" instance itself.

I think "out" setting should be option or encapsulated internal of rtamt.STLIOSpecification class.

online_monitor_ct.py does not work on python2

master [5366349]
online_monitor_ct.py does not work on python2. (in python3 case, it works)

/rtamt/examples/online_monitors$ python2 online_monitor_ct.py 
Robustness offline: [[2.0, 3.0], [3.5, 1.0], [4.3, -0.10000000000000009], [8.9, -0.10000000000000009]]
Traceback (most recent call last):
  File "online_monitor_ct.py", line 99, in <module>
    monitor()
  File "online_monitor_ct.py", line 64, in monitor
    rob = spec.update(['req', req_1], ['gnt', gnt_1])
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl_ct/specification.py", line 41, in update
    out = self.evaluator.evaluate(self.top, ['update'])
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl_ct/evaluator.py", line 13, in evaluate
    sample = self.visit(element, args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl/visitor.py", line 54, in visit
    out = self.visitAlways(element, args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl_ct/evaluator.py", line 167, in visitAlways
    in_sample = self.visit(element.children[0], args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl/visitor.py", line 46, in visit
    out = self.visitImplies(element, args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl_ct/evaluator.py", line 128, in visitImplies
    in_sample_1 = self.visit(element.children[0], args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl/visitor.py", line 58, in visit
    out = self.visitOnce(element, args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl_ct/evaluator.py", line 186, in visitOnce
    in_sample = self.visit(element.children[0], args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl/visitor.py", line 36, in visit
    out = self.visitPredicate(element, args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/io_stl_ct/evaluator.py", line 11, in visitPredicate
    out_sample = super(STLIOCTEvaluator, self).visitPredicate(element, args)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/spec/stl_ct/evaluator.py", line 26, in visitPredicate
    out_sample = element.node.update(in_sample_1, in_sample_2)
  File "/usr/local/lib/python2.7/dist-packages/rtamt/operation/stl_ct/predicate_operation.py", line 27, in update
    out_val = in_sample[1] - self.threshold
AttributeError: 'PredicateOperation' object has no attribute 'threshold'

I don't have enough confidence about installing... If it is because of that I'm sorry.

The location or path setting of /tests

Now we need to run

$ sudo pip install . --upgrade

Before run test. However it is annoying.
I guess we don't need to run test after installation usually. we need to check it before installation or debugging.

Why cmake version 3.12 or higher version is needed?

I'm using Ubuntu 18.04. the cmake version is v3.10 in default.
And we can consider Ubuntu 16.04 user also as ROS user.

Why does the latest version need cmake v3.12 or higher version?

STL interval parameter does not allow decimal point.

like
'''
spec.spec = 'out = always[0:1.5](a<0.0)'
'''
The error is
'''
$ python issue_no27.py
Traceback (most recent call last):
File "issue_no27.py", line 17, in
spec.parse()
File "/xxx/python2.7/site-packages/rtamt/spec/io_stl_ct/specification.py", line 34, in parse
super(STLIOCTSpecification, self).parse()
File "/xxx/python2.7/site-packages/rtamt/spec/stl_ct/specification.py", line 27, in parse
super(STLCTSpecification, self).parse()
File "/xxx/python2.7/site-packages/rtamt/spec/stl/specification.py", line 64, in parse
ctx = parser.stlfile()
File "/xxx/python2.7/site-packages/rtamt/parser/stl/StlParser.py", line 298, in stlfile
self.stlSpecification()
File "/xxx/python2.7/site-packages/rtamt/parser/stl/StlParser.py", line 403, in stlSpecification
self.assertion()
File "/xxx/python2.7/site-packages/rtamt/parser/stl/StlParser.py", line 568, in assertion
self.expression(0)
File "/xxx/python2.7/site-packages/rtamt/parser/stl/StlParser.py", line 1599, in expression
self.interval()
File "/xxx/python2.7/site-packages/rtamt/parser/stl/StlParser.py", line 1051, in interval
self.intervalTime()
File "/xxx/python2.7/site-packages/rtamt/parser/stl/StlParser.py", line 1117, in intervalTime
self._errHandler.reportError(self, re)
File "/usr/local/lib/python2.7/dist-packages/antlr4/error/ErrorStrategy.py", line 146, in reportError
self.reportInputMismatch(recognizer, e)
File "/usr/local/lib/python2.7/dist-packages/antlr4/error/ErrorStrategy.py", line 287, in reportInputMismatch
recognizer.notifyErrorListeners(msg, e.offendingToken, e)
File "/usr/local/lib/python2.7/dist-packages/antlr4/Parser.py", line 318, in notifyErrorListeners
listener.syntaxError(self, offendingToken, line, column, msg, e)
File "/usr/local/lib/python2.7/dist-packages/antlr4/error/ErrorListener.py", line 85, in syntaxError
delegate.syntaxError(recognizer, offendingSymbol, line, column, msg, e)
File "/xxx/python2.7/site-packages/rtamt/parser/stl/error/parser_error_listener.py", line 6, in syntaxError
raise STLParseException (str(line) + ":" + str(column) + ": Syntax ERROR, " + str(msg))
rtamt.exception.stl.exception.STLParseException: 1:15: Syntax ERROR, mismatched input '1.5' expecting IntegerLiteral
'''
The example is branch issue_no27

Supporting four arithmetic operations

I know it is cosmetic. Perhaps it is useful.

The priority is low

camke update

Ubuntu 16.04, 18.04 does not support package cmake ver 3.12. Thus, user need to upgrade cmake.
The problem is some auto-remove of ros packages happens.

tar xvf cmake-3.12.0-Linux-x86_64.tar.gz

sudo mv cmake-3.12.0-Linux-x86_64 /opt
sudo apt-get install ros-kinetic-desktop-full

sudo apt-get install ros-kinetic-tmc-desktop-full
sudo ln -s /opt/cmake-3.12.0-c3-Linux-x86_64/bin/* /usr/bin

We can provide additional documents for that.

guideline for bound of timed operators

maybe we can consider I=[stime, etime].
However generally it should be I=[stime, etime).

For temporal logic designer, I guess we can suggest some guideline.

bounded and unbounded operator can be abstract class methods.

I have already understand the benefit of separating bounded and unbounded operator.
We can implement faster operator in specific unbounded cases.

My intention in here is, we can provide well defined class architecture as much as possible.

Possibly, unbounded operator can inherit bounded operator, and programmer skip to implement unbounded operator, even it is slow and complicated in early prototyping.

WeakUntil Operator

Thanks for the tool.

Is it possible for the WeakUntil operator to be added to RTAMT? My research utilizes a mapping of specification patterns to STL (from [1]), and this mapping uses WeakUntil for quite a few patterns.

For example, Before R, Existence of P -> ¬R W (P ∧ ¬R)

Of course, the WeakUntil transforms as: A W B -> Always(A) or A Until B, so this is semantic sugar. But it would be preferable on my side to move this complexity down into the RTAMT library.

Thanks for your time.
Bentley

[1] M. Autili, L. Grunske, M. Lumpe, P. Pelliccione, and A. Tang, “Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar,” IEEE Transactions on Software Engineering, vol. 41, no. 7, pp. 620–638, 2015.

Edit: Fixed Always(B) to Always(A)

Supporting python3

I know current ROS1 works on python 2.7. However STL independent use-case is also considerable. In that sense, python 2.7 is old and python3 is common. I know it is low priority.

FYI, I found the error below even antr4 is set up.

 python3 simple_STLeval.py 
Traceback (most recent call last):
  File "simple_STLeval.py", line 5, in <module>
    from rtamt_stl_pymon.spec.stl_specification import STLSpecification
  File "/mnt/data/repos/mondiro/code/catkin_ws/src/rtamt_stl_pymon/src/rtamt_stl_pymon/spec/stl_specification.py", line 13, in <module>
    from antlr4 import *
  File "/usr/local/lib/python3.5/dist-packages/antlr4/__init__.py", line 3, in <module>
    from antlr4.BufferedTokenStream import TokenStream
  File "/usr/local/lib/python3.5/dist-packages/antlr4/BufferedTokenStream.py", line 43, in <module>
    from antlr4.error.Errors import IllegalStateException
  File "/usr/local/lib/python3.5/dist-packages/antlr4/error/Errors.py", line 30, in <module>
    from antlr4.atn.Transition import PredicateTransition
  File "/usr/local/lib/python3.5/dist-packages/antlr4/atn/Transition.py", line 44, in <module>
    from __builtin__ import unicode
ImportError: No module named '__builtin__'

I remember VerifAI needs python 3.5

Parser issue

The sentence 'c = always(abs(a1) > 0)' returns syntax error.

STL Parse Exception: 1:19: Syntax ERROR, mismatched input '>' expecting {'-', '+', '*', '/', ')', 'or', 'and', , , 'xor', 'until', 'since'}

Full C++ support

In our project, we're in a position where we may need to convert all of our code to C++, for performance reasons. It's my understanding that some portions of the Python interface aren't directly accessible from C++ -- primarily, the STL specification parsing and update functionality. Is there any plan to expose this functionality to C++? Our goal is to access the same functionality that we currently do, but without touching the Python interface at all.

Probably, problem is explanation. we will provide several sample ceases.

add new operation to online-STL in python
How to make C++ wrapper At first prototype, in python is enough. It is for when developer needs a faster code.
Build a completly new language. Propbably a simple language is good.