nickovic / rtamt

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

Until operator showing key error #156

Closed Jaroan closed 2 years ago

Jaroan commented 2 years ago

Hello! I had tried to use the 'until' operator and followed this example as my basis: test_stl_spec_dense_time_offline_evaluation.py

The code was modified to have two clauses before the 'until' operator and I got the following result

def test_until():
    spec = rtamt.STLDenseTimeSpecification();
    spec.declare_var('req', 'float')
    spec.declare_var('gnt', 'float')
    spec.declare_var('out', 'float')
    spec.spec = 'out = (gnt and req) until ( req)'

    spec.parse();
    left = [[0, 1.3], [0.7, 3], [1.3, 0.1], [2.1, -2.2]]
    right = [[0, 2.5], [0.7, 4], [1.3, -1.2], [2.1, 1.7]]

    out = spec.evaluate(['req', left], ['gnt', right])
    print("out", out)
test_until()

out [[0, 1.3], [0.7, 3], [1.3, -1.2], [2.1, -2.2]]

Whereas when I use two clauses after the 'until' operator, I get the following error:

def test_until():
    spec = rtamt.STLDenseTimeSpecification();
    spec.declare_var('req', 'float')
    spec.declare_var('gnt', 'float')
    spec.declare_var('out', 'float')
    spec.spec = 'out = (req) until (gnt and req)'

    spec.parse();
    left = [[0, 1.3], [0.7, 3], [1.3, 0.1], [2.1, -2.2]]
    right = [[0, 2.5], [0.7, 4], [1.3, -1.2], [2.1, 1.7]]

    out = spec.evaluate(['req', left], ['gnt', right])
    print("out", out)
test_until()
Traceback (most recent call last):
  File "stl_check2.py", line 263, in <module>
    test_until()
  File "stl_check2.py", line 261, in test_until
    out = spec.evaluate(['req', left], ['gnt', right])
  File "/site-packages/rtamt/spec/stl/dense_time/specification.py", line 102, in evaluate
    out = self.offline_evaluator.evaluate(self.top, [])
  File "/site-packages/rtamt/evaluator/stl/offline_evaluator.py", line 32, in evaluate
    sample = self.visit(node, args)
  File "/site-packages/rtamt/ast/visitor/stl/ASTVisitor.py", line 64, in visit
    ast = self.visitUntil(element, args)
  File "/site-packages/rtamt/evaluator/stl/offline_evaluator.py", line 284, in visitUntil
    in_sample_2 = self.visit(node.children[1], args)
  File "/site-packages/rtamt/ast/visitor/stl/ASTVisitor.py", line 52, in visit
    ast = self.visitAnd(element, args)
  File "/site-packages/rtamt/evaluator/stl/offline_evaluator.py", line 225, in visitAnd
    monitor = self.node_monitor_dict[node.name]
KeyError: '(gnt)and(req)'

What could be causing this issue? Any help is appreciated, Thanks in advance!

nickovic commented 2 years ago

Thanks for pointing this out. It was indeed a bug - the right branch of the until operator was not properly visited and the unit tests were too simple to catch the fault.

It is fixed now in the master branch.