search

nickovic / rtamt

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

RFE: should there be a more obvious error message when the value at t=0 is not provided? #169

Open ANogin opened 11 months ago

ANogin commented 11 months ago 
import rtamt

spec = rtamt.StlDenseTimeSpecification()
spec.name = "Bug?"
spec.declare_var("y", "int")
spec.declare_var("x", "int")
spec.set_var_io_type("y", "input")
spec.set_var_io_type("x", "output")
spec.spec = "((historically[0,5] x==1) and y) implies (eventually[0, 0.02] x==0)"

spec.parse()
spec.pastify()
rob = spec.update(["x", [(0.0, 1)]])

results in 

    rob = spec.update(["x", [(0.0, 1)]])
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/spec/abstract_specification.py", line 288, in update
    return self.online_interpreter.update(dataset)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/semantics/abstract_dense_time_online_interpreter.py", line 35, in update
    rob = self.updateVisitor.visitAst(self.ast, self.online_operator_dict, self.ast.var_object_dict)
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/syntax/ast/visitor/abstract_ast_visitor.py", line 33, in visitAst
    out.append(self.visit(spec, *args, **kwargs))
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/syntax/ast/visitor/abstract_ast_visitor.py", line 21, in visit
    result = self.visitBinary(node, *args, **kwargs)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/semantics/abstract_online_interpreter.py", line 69, in visitBinary
    sample_left  = self.visit(node.children[0], online_operator_dict, var_object_dict)
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/syntax/ast/visitor/abstract_ast_visitor.py", line 21, in visit
    result = self.visitBinary(node, *args, **kwargs)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/semantics/abstract_online_interpreter.py", line 70, in visitBinary
    sample_right = self.visit(node.children[1], online_operator_dict, var_object_dict)
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/syntax/ast/visitor/abstract_ast_visitor.py", line 23, in visit
    result = self.visitUnary(node, *args, **kwargs)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/semantics/abstract_online_interpreter.py", line 78, in visitUnary
    sample_return = op.update(sample)
                    ^^^^^^^^^^^^^^^^^
  File "/Users/aleksey/python-venv/3.12/lib/python3.12/site-packages/rtamt/semantics/stl/dense_time/online/once_timed_operation.py", line 36, in update
    while len(sample) >= i:
          ^^^^^^^^^^^
TypeError: object of type 'int' has no len()

If I add print(node.name, sample) just before line 78 in abstract_online_interpreter.py, it prints

once[1/50,1/50](x) [(0.0, 1)]
historically[0,5]((once[1/50,1/50](x))==(1.0)) []
once[1/50,1/50](y) 0

before it dies. I am guessing the issue is that I did not provide the value of y at time 0? If so, it would be good to catch it and provide an explicit error message about that.