From f32ca304be7367ffe711d75db7e6c25750a37ac2 Mon Sep 17 00:00:00 2001 From: Dejan Nickovic Date: Mon, 17 Feb 2025 18:12:40 +0100 Subject: [PATCH 1/4] Addition of the functionality to browse sub-signals + tests. --- .../ltl/discrete_time/explainer.py | 74 +++++++++---------- .../stl/discrete_time/explainer.py | 10 +-- ...tract_discrete_time_offline_interpreter.py | 2 +- ...stract_discrete_time_online_interpreter.py | 5 +- .../semantics/abstract_online_interpreter.py | 7 ++ rtamt/semantics/dense_time_interpreter.py | 1 + .../stl/dense_time/offline/ast_visitor.py | 5 ++ .../stl/dense_time/online/ast_visitor.py | 12 ++- .../dense_time/online/variable_operation.py | 13 ++++ .../stl/discrete_time/offline/ast_visitor.py | 2 +- .../stl/discrete_time/online/ast_visitor.py | 5 ++ .../online/variable_operation.py | 11 +++ rtamt/spec/abstract_specification.py | 14 +++- rtamt/spec/iastl/dense_time/specification.py | 10 ++- .../syntax/ast/parser/abstract_ast_parser.py | 8 +- rtamt/syntax/ast/parser/ltl/parser_visitor.py | 35 ++++++++- rtamt/syntax/ast/parser/stl/parser_visitor.py | 8 ++ .../ast/visitor/abstract_ast_visitor.py | 2 +- setup.py | 2 +- .../api/test_browsing_monitoring_results.py | 70 ++++++++++++++++++ 20 files changed, 241 insertions(+), 55 deletions(-) create mode 100644 rtamt/semantics/stl/dense_time/online/variable_operation.py create mode 100644 rtamt/semantics/stl/discrete_time/online/variable_operation.py create mode 100644 tests/python/api/test_browsing_monitoring_results.py diff --git a/rtamt/explanation/ltl/discrete_time/explainer.py b/rtamt/explanation/ltl/discrete_time/explainer.py index 19ef8dee..85a748e5 100644 --- a/rtamt/explanation/ltl/discrete_time/explainer.py +++ b/rtamt/explanation/ltl/discrete_time/explainer.py @@ -11,7 +11,7 @@ def __init__(self): def explain(self, spec): self.spec = spec for spec in self.spec.specs: - top_signal = self.spec.offline_results[spec] + top_signal = self.spec.results[spec] if top_signal[0] < 0: self.visit(spec, [[[0, 0]], False]) @@ -23,8 +23,8 @@ def visitConstant(self, element, args): def visitPredicate(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] op1_intervals, op2_intervals = explain_predicate(op1_signal, op2_signal, intervals) self.explanations[element.name] = intervals @@ -38,8 +38,8 @@ def visitVariable(self, element, args): def visitAddition(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] op1_intervals, op2_intervals = explain_addition(op1_signal, op2_signal, intervals) self.explanations[element.name] = intervals @@ -49,8 +49,8 @@ def visitAddition(self, element, args): def visitMultiplication(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] op1_intervals, op2_intervals = explain_multiplication(op1_signal, op2_signal, intervals) self.explanations[element.name] = intervals @@ -60,8 +60,8 @@ def visitMultiplication(self, element, args): def visitSubtraction(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] op1_intervals, op2_intervals = explain_subtraction(op1_signal, op2_signal, intervals) self.explanations[element.name] = intervals @@ -71,8 +71,8 @@ def visitSubtraction(self, element, args): def visitDivision(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] op1_intervals, op2_intervals = explain_division(op1_signal, op2_signal, intervals) self.explanations[element.name] = intervals @@ -82,7 +82,7 @@ def visitDivision(self, element, args): def visitAbs(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] op_intervals = explain_abs(op_signal, intervals) self.explanations[element.name] = intervals @@ -91,7 +91,7 @@ def visitAbs(self, element, args): def visitSqrt(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] op_intervals = explain_sqrt(op_signal, intervals) self.explanations[element.name] = intervals @@ -100,7 +100,7 @@ def visitSqrt(self, element, args): def visitExp(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] op_intervals = explain_exp(op_signal, intervals) self.explanations[element.name] = intervals @@ -109,8 +109,8 @@ def visitExp(self, element, args): def visitPow(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] op1_intervals, op2_intervals = explain_pow(op1_signal, op2_signal, intervals) self.explanations[element.name] = intervals @@ -120,7 +120,7 @@ def visitPow(self, element, args): def visitRise(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] op_intervals = explain_rise(op_signal, intervals) self.explanations[element.name] = intervals @@ -129,7 +129,7 @@ def visitRise(self, element, args): def visitFall(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] op_intervals = explain_fall(op_signal, intervals) self.explanations[element.name] = intervals @@ -138,7 +138,7 @@ def visitFall(self, element, args): def visitNot(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_not(op_signal, intervals) else: @@ -150,8 +150,8 @@ def visitNot(self, element, args): def visitAnd(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] if flag: op1_intervals, op2_intervals = explain_sat_and(op1_signal, op2_signal, intervals) else: @@ -164,8 +164,8 @@ def visitAnd(self, element, args): def visitOr(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] if flag: op1_intervals, op2_intervals = explain_sat_or(op1_signal, op2_signal, intervals) else: @@ -178,8 +178,8 @@ def visitOr(self, element, args): def visitImplies(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] if flag: op1_intervals, op2_intervals = explain_sat_implies(op1_signal, op2_signal, intervals) else: @@ -192,8 +192,8 @@ def visitImplies(self, element, args): def visitIff(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] if flag: op1_intervals, op2_intervals = explain_sat_iff(op1_signal, op2_signal, intervals) else: @@ -206,8 +206,8 @@ def visitIff(self, element, args): def visitXor(self, element, args): intervals = args[0] flag = args[1] - op1_signal = self.spec.offline_results[element.children[0]] - op2_signal = self.spec.offline_results[element.children[1]] + op1_signal = self.spec.results[element.children[0]] + op2_signal = self.spec.results[element.children[1]] if flag: op1_intervals, op2_intervals = explain_sat_xor(op1_signal, op2_signal, intervals) else: @@ -220,7 +220,7 @@ def visitXor(self, element, args): def visitEventually(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_eventually(op_signal, intervals) else: @@ -232,7 +232,7 @@ def visitEventually(self, element, args): def visitAlways(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_always(op_signal, intervals) else: @@ -248,7 +248,7 @@ def visitUntil(self, element, args): def visitOnce(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_once(op_signal, intervals) else: @@ -260,7 +260,7 @@ def visitOnce(self, element, args): def visitPrevious(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_prev(op_signal, intervals) else: @@ -272,7 +272,7 @@ def visitPrevious(self, element, args): def visitStrongPrevious(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_prev(op_signal, intervals) else: @@ -284,7 +284,7 @@ def visitStrongPrevious(self, element, args): def visitNext(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_next(op_signal, intervals) else: @@ -296,7 +296,7 @@ def visitNext(self, element, args): def visitStrongNext(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_next(op_signal, intervals) else: @@ -308,7 +308,7 @@ def visitStrongNext(self, element, args): def visitHistorically(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_historically(op_signal, intervals) else: diff --git a/rtamt/explanation/stl/discrete_time/explainer.py b/rtamt/explanation/stl/discrete_time/explainer.py index b7388008..5fb9b64f 100644 --- a/rtamt/explanation/stl/discrete_time/explainer.py +++ b/rtamt/explanation/stl/discrete_time/explainer.py @@ -17,14 +17,14 @@ def visit(self, element, args): def explain(self, spec): self.spec = spec for spec in self.spec.specs: - top_signal = self.spec.offline_results[spec] + top_signal = self.spec.results[spec] if top_signal[0] < 0: self.visit(spec, [[[0,0]], False]) def visitTimedEventually(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_timed_eventually(op_signal, intervals, element.begin, element.end) else: @@ -35,7 +35,7 @@ def visitTimedEventually(self, element, args): def visitTimedAlways(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_timed_always(op_signal, intervals, element.begin, element.end) else: @@ -49,7 +49,7 @@ def visitTimedUntil(self, element, args): def visitTimedOnce(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_timed_once(op_signal, intervals, element.begin, element.end) else: @@ -60,7 +60,7 @@ def visitTimedOnce(self, element, args): def visitTimedHistorically(self, element, args): intervals = args[0] flag = args[1] - op_signal = self.spec.offline_results[element.children[0]] + op_signal = self.spec.results[element.children[0]] if flag: op_intervals = explain_sat_timed_historically(op_signal, intervals, element.begin, element.end) else: diff --git a/rtamt/semantics/abstract_discrete_time_offline_interpreter.py b/rtamt/semantics/abstract_discrete_time_offline_interpreter.py index c4ee770c..8b3ec240 100644 --- a/rtamt/semantics/abstract_discrete_time_offline_interpreter.py +++ b/rtamt/semantics/abstract_discrete_time_offline_interpreter.py @@ -29,7 +29,7 @@ def evaluate(self, dataset): # evaluate spec forest length = len(dataset['time']) - self.ast.offline_results['time'] = dataset['time'] + self.ast.results['time'] = dataset['time'] rob = self.visitAst(self.ast, length) rob = rob[len(rob)-1] diff --git a/rtamt/semantics/abstract_discrete_time_online_interpreter.py b/rtamt/semantics/abstract_discrete_time_online_interpreter.py index 69cd8ff6..cefebd26 100644 --- a/rtamt/semantics/abstract_discrete_time_online_interpreter.py +++ b/rtamt/semantics/abstract_discrete_time_online_interpreter.py @@ -18,7 +18,7 @@ def __init__(self): # inputs - list of [var name, var value] pairs # Example: # update(1, [['a', 2.2], ['b', 3.3]]) - #TODO merge dense and discrete into update AbstractOnlineInterpreter + # TODO merge dense and discrete into update AbstractOnlineInterpreter def update(self, timestamp, dataset): # check ast exists self.exist_ast() @@ -29,6 +29,8 @@ def update(self, timestamp, dataset): # evaluate spec forest rob = self.updateVisitor.visitAst(self.ast, self.online_operator_dict, self.ast.var_object_dict) rob = rob[len(rob) - 1] + self.ast.results = self.updateVisitor.results + out = self.ast.var_object_dict[self.ast.out_var] if self.ast.out_var_field: @@ -60,6 +62,7 @@ def set_variable_to_ast_from_dataset(self, dataset): var_name = data[0] var_value = data[1] self.ast.var_object_dict[var_name] = var_value + self.online_operator_dict[var_name].sample = var_value @property def update_counter(self): diff --git a/rtamt/semantics/abstract_online_interpreter.py b/rtamt/semantics/abstract_online_interpreter.py index fdbe849f..c594eef5 100644 --- a/rtamt/semantics/abstract_online_interpreter.py +++ b/rtamt/semantics/abstract_online_interpreter.py @@ -60,9 +60,13 @@ def visitLeaf(self, node, online_operator_dict): class AbstractOnlineUpdateVisitor(AbstractAstVisitor): + def __init__(self): + self.results = dict() + def visitSpec(self, node, online_operator_dict, var_object_dict): sample_return = self.visit(node, online_operator_dict, var_object_dict) var_object_dict[node] = sample_return #TODO subspec name is necessary as a key for var_object_dict. + self.results[node] = sample_return return sample_return def visitBinary(self, node, online_operator_dict, var_object_dict): @@ -70,12 +74,14 @@ def visitBinary(self, node, online_operator_dict, var_object_dict): sample_right = self.visit(node.children[1], online_operator_dict, var_object_dict) operator = online_operator_dict[node.name] sample_return = operator.update(sample_left, sample_right) + self.results[node] = sample_return return sample_return def visitUnary(self, node, online_operator_dict, var_object_dict): sample = self.visit(node.children[0], online_operator_dict, var_object_dict) op = online_operator_dict[node.name] sample_return = op.update(sample) + self.results[node] = sample_return return sample_return def visitLeaf(self, node, online_operator_dict, var_object_dict): @@ -83,4 +89,5 @@ def visitLeaf(self, node, online_operator_dict, var_object_dict): sample_return = self.visitConstant(node, online_operator_dict, var_object_dict) elif isinstance(node, Variable): sample_return = self.visitVariable(node, online_operator_dict, var_object_dict) + self.results[node] = sample_return return sample_return diff --git a/rtamt/semantics/dense_time_interpreter.py b/rtamt/semantics/dense_time_interpreter.py index d4c51a81..db4caad7 100644 --- a/rtamt/semantics/dense_time_interpreter.py +++ b/rtamt/semantics/dense_time_interpreter.py @@ -20,6 +20,7 @@ def set_variable_to_ast_from_dataset(self, dataset): var_name = data[0] var_object = data[1] self.ast.var_object_dict[var_name] = var_object + self.online_operator_dict[var_name].sample = var_object def time_unit_transformer(self, node): b = node.begin diff --git a/rtamt/semantics/stl/dense_time/offline/ast_visitor.py b/rtamt/semantics/stl/dense_time/offline/ast_visitor.py index d06c6bcb..c6d9414f 100644 --- a/rtamt/semantics/stl/dense_time/offline/ast_visitor.py +++ b/rtamt/semantics/stl/dense_time/offline/ast_visitor.py @@ -283,6 +283,11 @@ def until_timed_operation(sample_left, sample_right, begin, end): class StlDenseTimeOfflineAstVisitor(StlAstVisitor): + def visit(self, node, *args, **kwargs): + result = super(StlDenseTimeOfflineAstVisitor, self).visit(node, *args, **kwargs) + self.ast.results[node] = result + return result + def visitPredicate(self, node, *args, **kwargs): sample_left = self.visit(node.children[0], *args, **kwargs) sample_right = self.visit(node.children[1], *args, **kwargs) diff --git a/rtamt/semantics/stl/dense_time/online/ast_visitor.py b/rtamt/semantics/stl/dense_time/online/ast_visitor.py index f27967ff..35f5c1dc 100644 --- a/rtamt/semantics/stl/dense_time/online/ast_visitor.py +++ b/rtamt/semantics/stl/dense_time/online/ast_visitor.py @@ -1,4 +1,4 @@ - +from rtamt.semantics.stl.dense_time.online.variable_operation import VariableOperation from rtamt.syntax.ast.visitor.stl.ast_visitor import StlAstVisitor from rtamt.semantics.arithmetic.dense_time.online.addition_operation import AdditionOperation @@ -27,6 +27,16 @@ from rtamt.exception.exception import RTAMTException class StlDenseTimeOnlineAstVisitor(StlAstVisitor): + + def visit(self, node, *args, **kwargs): + result = super(StlDenseTimeOnlineAstVisitor, self).visit(node, *args, **kwargs) + self.ast.results[node] = result + return result + + def visitVariable(self, node, *args, **kwargs): + self.visitChildren(node, *args, **kwargs) + self.online_operator_dict[node.name] = VariableOperation(node.operator) + def visitPredicate(self, node, *args, **kwargs): self.visitChildren(node, *args, **kwargs) self.online_operator_dict[node.name] = PredicateOperation(node.operator) diff --git a/rtamt/semantics/stl/dense_time/online/variable_operation.py b/rtamt/semantics/stl/dense_time/online/variable_operation.py new file mode 100644 index 00000000..87cf4a40 --- /dev/null +++ b/rtamt/semantics/stl/dense_time/online/variable_operation.py @@ -0,0 +1,13 @@ + +from rtamt.semantics.abstract_dense_time_online_operation import AbstractDenseTimeOnlineOperation + +class VariableOperation(AbstractDenseTimeOnlineOperation): + def __init__(self): + self.val = None + + def update(self, *args, **kargs): + return self.val + + def update_final(self, *args, **kargs): + out = list() + return diff --git a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py index 963eb3a8..60201e42 100644 --- a/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py +++ b/rtamt/semantics/stl/discrete_time/offline/ast_visitor.py @@ -11,7 +11,7 @@ class StlDiscreteTimeOfflineAstVisitor(StlAstVisitor): def visit(self, node, *args, **kwargs): result = super(StlDiscreteTimeOfflineAstVisitor, self).visit(node, *args, **kwargs) - self.ast.offline_results[node] = result + self.ast.results[node] = result return result def visitPredicate(self, node, *args, **kwargs): diff --git a/rtamt/semantics/stl/discrete_time/online/ast_visitor.py b/rtamt/semantics/stl/discrete_time/online/ast_visitor.py index d670e594..17969271 100644 --- a/rtamt/semantics/stl/discrete_time/online/ast_visitor.py +++ b/rtamt/semantics/stl/discrete_time/online/ast_visitor.py @@ -1,4 +1,5 @@ from rtamt.semantics.stl.discrete_time.online.strong_previous_operation import StrongPreviousOperation +from rtamt.semantics.stl.discrete_time.online.variable_operation import VariableOperation from rtamt.syntax.ast.visitor.stl.ast_visitor import StlAstVisitor from rtamt.semantics.arithmetic.discrete_time.online.addition_operation import AdditionOperation @@ -32,6 +33,10 @@ class StlDiscreteTimeOnlineAstVisitor(StlAstVisitor): + def visitVariable(self, node, *args, **kwargs): + self.visitChildren(node, *args, **kwargs) + self.online_operator_dict[node.name] = VariableOperation() + def visitPredicate(self, node, *args, **kwargs): self.visitChildren(node, *args, **kwargs) self.online_operator_dict[node.name] = PredicateOperation(node.operator) diff --git a/rtamt/semantics/stl/discrete_time/online/variable_operation.py b/rtamt/semantics/stl/discrete_time/online/variable_operation.py new file mode 100644 index 00000000..486ec76e --- /dev/null +++ b/rtamt/semantics/stl/discrete_time/online/variable_operation.py @@ -0,0 +1,11 @@ +from rtamt.semantics.abstract_online_operation import AbstractOnlineOperation + +class VariableOperation(AbstractOnlineOperation): + def __init__(self): + self.sample = None + + def reset(self): + pass + + def update(self): + return self.sample diff --git a/rtamt/spec/abstract_specification.py b/rtamt/spec/abstract_specification.py index b0b8696b..c8463ed8 100644 --- a/rtamt/spec/abstract_specification.py +++ b/rtamt/spec/abstract_specification.py @@ -24,6 +24,7 @@ def __init__(self, ast): self.var_topic_dict = dict() self.free_vars = set() self.var_object_dict = dict() + self.phi_name_to_node_dict = dict() #TODO we need to move it to RTAMT4ROS as wrapper self.modules = dict() @@ -48,8 +49,8 @@ def spec(self, spec): def add_var(self, var): self.ast.vars.add(var) - def get_value(self, var_name): - return self.ast.get_value(var_name) + def get_value(self, phi_name): + return self.ast.get_value(phi_name) def add_sub_spec(self, sub_spec): self.ast.add_sub_spec(sub_spec) @@ -96,6 +97,15 @@ def var_object_dict(self, var_object_dict): self.__var_object_dict = var_object_dict self.ast.var_object_dict = self.var_object_dict + @property + def phi_name_to_node_dict(self): + return self.ast.phi_name_to_node_dict + + @phi_name_to_node_dict.setter + def phi_name_to_node_dict(self, phi_name_to_node_dict): + self.__phi_name_to_node_dict = phi_name_to_node_dict + self.ast.phi_name_to_node_dict = self.phi_name_to_node_dict + @property def free_vars(self): return self.ast.free_vars diff --git a/rtamt/spec/iastl/dense_time/specification.py b/rtamt/spec/iastl/dense_time/specification.py index 4f40743b..85e322bf 100644 --- a/rtamt/spec/iastl/dense_time/specification.py +++ b/rtamt/spec/iastl/dense_time/specification.py @@ -16,33 +16,41 @@ def IAStlOutputRobustnessDenseTimeOfflineSpecification(): spec = AbstractOfflineSpecification(StlAst(), IAStlOutputRobustnessDenseTimeOfflineInterpreter()) return spec + def IAStlInputVacuityDenseTimeOfflineSpecification(): spec = AbstractOfflineSpecification(StlAst(), IAStlInputVacuityDenseTimeOfflineInterpreter()) return spec + def IAStlInputRobustnessDenseTimeOfflineSpecification(): spec = AbstractOfflineSpecification(StlAst(), IAStlInputRobustnessDenseTimeOfflineInterpreter()) return spec + def IAStlOutputVacuityDenseTimeOfflineSpecification(): spec = AbstractOfflineSpecification(StlAst(), IAStlOutputVacuityDenseTimeOfflineInterpreter()) return spec + def IAStlOutputRobustnessDenseTimeOnlineSpecification(): spec = AbstractOnlineSpecification(StlAst(), IAStlOutputRobustnessDenseTimeOnlineInterpreter(), pastifier=StlPastifier()) return spec + def IAStlInputVacuityDenseTimeOnlineSpecification(): spec = AbstractOnlineSpecification(StlAst(), IAStlInputVacuityDenseTimeOnlineInterpreter(), pastifier=StlPastifier()) return spec + def IAStlInputRobustnessDenseTimeOnlineSpecification(): spec = AbstractOnlineSpecification(StlAst(), IAStlInputRobustnessDenseTimeOnlineInterpreter(), pastifier=StlPastifier()) return spec + def IAStlOutputVacuityDenseTimeOnlineSpecification(): - spec = AbstractOnlineSpecification(StlAst(), IAStlOutputVacuityDenseTimeOnlineInterpreter(), pastifier=StlPastifier()) + spec = AbstractOnlineSpecification(StlAst(), IAStlOutputVacuityDenseTimeOnlineInterpreter(), + pastifier=StlPastifier()) return spec diff --git a/rtamt/syntax/ast/parser/abstract_ast_parser.py b/rtamt/syntax/ast/parser/abstract_ast_parser.py index 7ab7ca3b..db5ca1ed 100644 --- a/rtamt/syntax/ast/parser/abstract_ast_parser.py +++ b/rtamt/syntax/ast/parser/abstract_ast_parser.py @@ -65,7 +65,8 @@ def __init__(self, antrlLexerType, antrlParserType, parserErrorListenerType = No self.var_io_dict = dict() self.const_type_dict = dict() self.const_val_dict = dict() - self.offline_results = dict() + self.results = dict() + self.phi_name_to_node_dict = dict() self.modules = dict() @@ -201,8 +202,9 @@ def modules(self, modules): def add_var(self, var): self.vars.add(var) - def get_value(self, var_name): - return self.var_object_dict[var_name] + def get_value(self, phi_name): + node = self.phi_name_to_node_dict[phi_name] + return self.results[node] def add_sub_spec(self, sub_spec): self.modular_spec = self.modular_spec + sub_spec + '\n' diff --git a/rtamt/syntax/ast/parser/ltl/parser_visitor.py b/rtamt/syntax/ast/parser/ltl/parser_visitor.py index cb0d7ceb..7dbaef7f 100644 --- a/rtamt/syntax/ast/parser/ltl/parser_visitor.py +++ b/rtamt/syntax/ast/parser/ltl/parser_visitor.py @@ -46,6 +46,7 @@ def visitExprPredicate(self, ctx): child2 = self.visit(ctx.expression(1)) op_type = self.str_to_op_type(ctx.comparisonOp().getText()) node = Predicate(child1, child2, op_type) + self.phi_name_to_node_dict[node.name] = node return node @@ -56,9 +57,11 @@ def visitExprId(self, ctx): if id in self.const_val_dict: val = self.const_val_dict[id] node = Constant(float(val)) + self.phi_name_to_node_dict[node.name] = node # Identifier is either an input variable or a sub-formula elif id in self.var_subspec_dict: node = self.var_subspec_dict[id] + self.phi_name_to_node_dict[node.name] = node return node else: id_tokens = id.split('.') @@ -91,6 +94,7 @@ def visitExprId(self, ctx): var_io = self.var_io_dict[id_head] node = Variable(id_head, id_tail, var_io) + self.phi_name_to_node_dict[node.name] = node return node @@ -138,141 +142,167 @@ def visitExprAddition(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Addition(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprSubtraction(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Subtraction(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprMultiplication(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Multiplication(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprDivision(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Division(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprAbs(self, ctx): child = self.visit(ctx.expression()) node = Abs(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprSqrt(self, ctx): child = self.visit(ctx.expression()) node = Sqrt(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprExp(self, ctx): child = self.visit(ctx.expression()) node = Exp(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprPow(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Pow(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprNot(self, ctx): child = self.visit(ctx.expression()) node = Neg(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprRise(self, ctx): child = self.visit(ctx.expression()) node = Rise(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprLiteral(self, ctx): val = float(ctx.literal().getText()) node = Constant(val) + self.phi_name_to_node_dict[node.name] = node return node def visitExprFall(self, ctx): child = self.visit(ctx.expression()) node = Fall(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprAnd(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Conjunction(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprOr(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Disjunction(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprImplies(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Implies(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprIff(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Iff(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprXor(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Xor(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprAlways(self, ctx): child = self.visit(ctx.expression()) node = Always(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprEv(self, ctx): child = self.visit(ctx.expression()) node = Eventually(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprPrevious(self, ctx): child = self.visit(ctx.expression()) node = Previous(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprStrongPrevious(self, ctx): child = self.visit(ctx.expression()) node = StrongPrevious(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprNext(self, ctx): child = self.visit(ctx.expression()) node = Next(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprStrongNext(self, ctx): child = self.visit(ctx.expression()) node = StrongNext(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExpreOnce(self, ctx): child = self.visit(ctx.expression()) node = Once(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprHist(self, ctx): child = self.visit(ctx.expression()) node = Historically(child) + self.phi_name_to_node_dict[node.name] = node return node def visitExprSince(self, ctx): child1 = self.visit(ctx.expression(0)) child2 = self.visit(ctx.expression(1)) node = Since(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprUntil(self, ctx): @@ -281,6 +311,7 @@ def visitExprUntil(self, ctx): child2 = self.visit(ctx.expression(1)) node = Until(child1, child2) + self.phi_name_to_node_dict[node.name] = node return node def visitExprUnless(self, ctx): @@ -291,6 +322,7 @@ def visitExprUnless(self, ctx): left = Always(child1, 0, interval.end) right = Until(child1, child2) node = Disjunction(left, right) + self.phi_name_to_node_dict[node.name] = node return node @@ -308,7 +340,8 @@ def visitAssertion(self, ctx): id = 'out' implicit = True else: - id = ctx.Identifier().getText(); + id = ctx.Identifier().getText() + self.phi_name_to_node_dict[id] = out self.var_subspec_dict[id] = out id_tokens = id.split('.') diff --git a/rtamt/syntax/ast/parser/stl/parser_visitor.py b/rtamt/syntax/ast/parser/stl/parser_visitor.py index e7af24ca..9dc966c8 100644 --- a/rtamt/syntax/ast/parser/stl/parser_visitor.py +++ b/rtamt/syntax/ast/parser/stl/parser_visitor.py @@ -35,6 +35,7 @@ def visitExprAlways(self, ctx): else: interval = self.visit(ctx.interval()) node = TimedAlways(child, interval) + self.phi_name_to_node_dict[node.name] = node return node @@ -42,9 +43,11 @@ def visitExprEv(self, ctx): child = self.visit(ctx.expression()) if ctx.interval() == None: node = Eventually(child) + self.phi_name_to_node_dict[node.name] = node else: interval = self.visit(ctx.interval()) node = TimedEventually(child, interval) + self.phi_name_to_node_dict[node.name] = node return node def visitExpreOnce(self, ctx): @@ -54,6 +57,7 @@ def visitExpreOnce(self, ctx): else: interval = self.visit(ctx.interval()) node = TimedOnce(child, interval) + self.phi_name_to_node_dict[node.name] = node return node def visitExprHist(self, ctx): @@ -63,6 +67,7 @@ def visitExprHist(self, ctx): else: interval = self.visit(ctx.interval()) node = TimedHistorically(child, interval) + self.phi_name_to_node_dict[node.name] = node return node def visitExprSince(self, ctx): @@ -73,6 +78,7 @@ def visitExprSince(self, ctx): else: interval = self.visit(ctx.interval()) node = TimedSince(child1, child2, interval) + self.phi_name_to_node_dict[node.name] = node return node def visitExprUntil(self, ctx): @@ -83,6 +89,7 @@ def visitExprUntil(self, ctx): else: interval = self.visit(ctx.interval()) node = TimedUntil(child1, child2, interval) + self.phi_name_to_node_dict[node.name] = node return node def visitExprUnless(self, ctx): @@ -98,6 +105,7 @@ def visitExprUnless(self, ctx): left = TimedAlways(child1, interval_left) right = TimedUntil(child1, child2, interval) node = Disjunction(left, right) + self.phi_name_to_node_dict[node.name] = node return node def visitConstantTimeLiteral(self, ctx): diff --git a/rtamt/syntax/ast/visitor/abstract_ast_visitor.py b/rtamt/syntax/ast/visitor/abstract_ast_visitor.py index 3bb917db..ad5bdcf6 100644 --- a/rtamt/syntax/ast/visitor/abstract_ast_visitor.py +++ b/rtamt/syntax/ast/visitor/abstract_ast_visitor.py @@ -14,7 +14,7 @@ def visitChildren(self, node, *args, **kwargs): result = None for nodeChild in node.children: result = self.visit(nodeChild, *args, **kwargs) - return result # visitChildren reterns only last result + return result # visitChildren returns only last result def visit(self, node, *args, **kwargs): if isinstance(node, BinaryNode): diff --git a/setup.py b/setup.py index 1b5922e2..3ad7db12 100644 --- a/setup.py +++ b/setup.py @@ -9,7 +9,7 @@ setup( name='rtamt', - version='0.4.6', + version='0.4.7', description='Library for specification-based online monitoring.', long_description=long_description, long_description_content_type="text/markdown", diff --git a/tests/python/api/test_browsing_monitoring_results.py b/tests/python/api/test_browsing_monitoring_results.py new file mode 100644 index 00000000..c3cd6dd1 --- /dev/null +++ b/tests/python/api/test_browsing_monitoring_results.py @@ -0,0 +1,70 @@ +import unittest + +from rtamt.spec.stl.discrete_time.specification import StlDiscreteTimeOfflineSpecification +from rtamt.spec.stl.dense_time.specification import StlDenseTimeOfflineSpecification +from rtamt.spec.stl.discrete_time.specification import StlDiscreteTimeOnlineSpecification +from rtamt.spec.stl.dense_time.specification import StlDenseTimeOnlineSpecification + + +class TestBrowsing(unittest.TestCase): + + def __init__(self, *args, **kwargs): + super(TestBrowsing, self).__init__(*args, **kwargs) + + + def test_get_value_offline_dt(self): + spec = StlDiscreteTimeOfflineSpecification() + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.declare_var('d', 'float') + spec.spec = 'c = always(a>=2 and b<=3) d = always(b<=5)' + spec.parse() + + dataset = { + 'time': [0, 1, 2, 3, 4], + 'a': [100, -1, -2, 5, -1], + 'b': [50, 4, 7, 8, 0] + } + spec.evaluate(dataset) + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + d = spec.get_value('d') + conj = spec.get_value('((a)>=(2.0))and((b)<=(3.0))') + pred = spec.get_value('(a)>=(2.0)') + + self.assertListEqual(a, [100, -1, -2, 5, -1]) + self.assertListEqual(b, [50, 4, 7, 8, 0]) + self.assertListEqual(c, [-47, -5, -5, -5, -3]) + self.assertListEqual(d, [-45, -3, -3, -3, 5]) + self.assertListEqual(conj, [-47, -3, -4, -5, -3]) + self.assertListEqual(pred, [98, -3, -4, 3, -3]) + + def test_get_value_online_dt(self): + spec = StlDiscreteTimeOnlineSpecification() + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.declare_var('d', 'float') + spec.spec = 'c = (a>=2 and b<=3) d = (b<=5)' + spec.parse() + + spec.update(0, [('a', 100), ('b', 50)]) + spec.update(1, [('a', -1), ('b', 4)]) + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + d = spec.get_value('d') + conj = spec.get_value('((a)>=(2.0))and((b)<=(3.0))') + pred = spec.get_value('(a)>=(2.0)') + + self.assertEqual(a, -1) + self.assertEqual(b, 4) + self.assertEqual(c, -3) + self.assertEqual(d, 1) + self.assertEqual(conj, -3) + self.assertEqual(pred, -3) + +if __name__ == '__main__': + unittest.main() \ No newline at end of file From 8c2a5680013e3da28cff1a04b6cc81689e5f9b08 Mon Sep 17 00:00:00 2001 From: nickovic Date: Wed, 19 Feb 2025 20:10:30 +0100 Subject: [PATCH 2/4] Completed the browsing functionality. --- .../abstract_dense_time_online_interpreter.py | 9 +++ ...stract_discrete_time_online_interpreter.py | 5 +- rtamt/semantics/dense_time_interpreter.py | 11 +++- .../stl/dense_time/online/ast_visitor.py | 2 +- rtamt/spec/abstract_specification.py | 6 +- .../api/test_browsing_monitoring_results.py | 55 +++++++++++++++++++ .../api/test_stl_sampling_time_units.py | 10 ++-- 7 files changed, 86 insertions(+), 12 deletions(-) diff --git a/rtamt/semantics/abstract_dense_time_online_interpreter.py b/rtamt/semantics/abstract_dense_time_online_interpreter.py index 151a0366..a100f67c 100644 --- a/rtamt/semantics/abstract_dense_time_online_interpreter.py +++ b/rtamt/semantics/abstract_dense_time_online_interpreter.py @@ -35,6 +35,8 @@ def update(self, dataset): rob = self.updateVisitor.visitAst(self.ast, self.online_operator_dict, self.ast.var_object_dict) rob = rob[len(rob) - 1] + self.ast.results = self.updateVisitor.results + out = self.ast.var_object_dict[self.ast.out_var] if self.ast.out_var_field: setattr(out, self.ast.out_var_field, rob) @@ -57,6 +59,13 @@ def update_final(self, dataset): return rob + def set_variable_to_ast_from_dataset(self, dataset): + for data in dataset: + var_name = data[0] + var_object = data[1] + if data[0] in self.ast.free_vars: + self.ast.var_object_dict[var_name] = var_object + self.online_operator_dict[var_name].sample = var_object class DenseTimeOnlineUpdateVisitor(AbstractOnlineUpdateVisitor): def visitVariable(self, node, online_operator_dict, var_object_dict): diff --git a/rtamt/semantics/abstract_discrete_time_online_interpreter.py b/rtamt/semantics/abstract_discrete_time_online_interpreter.py index cefebd26..afa959db 100644 --- a/rtamt/semantics/abstract_discrete_time_online_interpreter.py +++ b/rtamt/semantics/abstract_discrete_time_online_interpreter.py @@ -61,8 +61,9 @@ def set_variable_to_ast_from_dataset(self, dataset): for data in dataset: var_name = data[0] var_value = data[1] - self.ast.var_object_dict[var_name] = var_value - self.online_operator_dict[var_name].sample = var_value + if data[0] in self.ast.free_vars: + self.ast.var_object_dict[var_name] = var_value + self.online_operator_dict[var_name].sample = var_value @property def update_counter(self): diff --git a/rtamt/semantics/dense_time_interpreter.py b/rtamt/semantics/dense_time_interpreter.py index db4caad7..588d396b 100644 --- a/rtamt/semantics/dense_time_interpreter.py +++ b/rtamt/semantics/dense_time_interpreter.py @@ -19,8 +19,15 @@ def set_variable_to_ast_from_dataset(self, dataset): for data in dataset: var_name = data[0] var_object = data[1] - self.ast.var_object_dict[var_name] = var_object - self.online_operator_dict[var_name].sample = var_object + if data[0] in self.ast.free_vars: + self.ast.var_object_dict[var_name] = var_object + + def is_dataset_valid(self, dataset): + dataset_vars = set() + for data in dataset: + dataset_vars.add(data[0]) + valid = dataset_vars == self.ast.free_vars + return valid def time_unit_transformer(self, node): b = node.begin diff --git a/rtamt/semantics/stl/dense_time/online/ast_visitor.py b/rtamt/semantics/stl/dense_time/online/ast_visitor.py index 35f5c1dc..367615da 100644 --- a/rtamt/semantics/stl/dense_time/online/ast_visitor.py +++ b/rtamt/semantics/stl/dense_time/online/ast_visitor.py @@ -35,7 +35,7 @@ def visit(self, node, *args, **kwargs): def visitVariable(self, node, *args, **kwargs): self.visitChildren(node, *args, **kwargs) - self.online_operator_dict[node.name] = VariableOperation(node.operator) + self.online_operator_dict[node.name] = VariableOperation() def visitPredicate(self, node, *args, **kwargs): self.visitChildren(node, *args, **kwargs) diff --git a/rtamt/spec/abstract_specification.py b/rtamt/spec/abstract_specification.py index c8463ed8..e0c3be94 100644 --- a/rtamt/spec/abstract_specification.py +++ b/rtamt/spec/abstract_specification.py @@ -10,6 +10,10 @@ from rtamt.exception.exception import RTAMTException +from antlr4 import * +from antlr4.InputStream import InputStream +from antlr4.error.ErrorListener import ErrorListener + class AbstractSpecification(object): __metaclass__ = ABCMeta @@ -300,8 +304,6 @@ def update(self, *args, **kwargs): i = args[0] dataset = args[1] return self.online_interpreter.update(i, dataset) - else: - pass def final_update(self, *args, **kwargs): if self.set_ast_flag != True: diff --git a/tests/python/api/test_browsing_monitoring_results.py b/tests/python/api/test_browsing_monitoring_results.py index c3cd6dd1..ad67c20c 100644 --- a/tests/python/api/test_browsing_monitoring_results.py +++ b/tests/python/api/test_browsing_monitoring_results.py @@ -66,5 +66,60 @@ def test_get_value_online_dt(self): self.assertEqual(conj, -3) self.assertEqual(pred, -3) + def test_get_value_offline_ct(self): + spec = StlDenseTimeOfflineSpecification() + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.spec = 'c = a and b' + 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]] + + expected = [[0, 1.3], [0.7, 3], [1.3, -1.2], [2.1, -2.2]] + + spec.evaluate(['a', left], ['b', right]) + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + conj = spec.get_value('(a)and(b)') + + self.assertListEqual(a, left) + self.assertListEqual(b, right) + self.assertListEqual(c, expected) + self.assertListEqual(conj, expected) + + def test_get_value_online_ct(self): + spec = StlDenseTimeOnlineSpecification() + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.spec = 'c = a and b' + + spec.parse() + + in_data_1_1 = [[2, 2], [3.3, 3], [5.7, 4]] + in_data_2_1 = [[2.5, 5], [4.7, 6]] + + in_data_1_2 = [] + in_data_2_2 = [[5.7, 1]] + + out_expected_1 = [[2.5, 2], [3.3, 3], [4.7, 3]] + out_expected_2 = [[5.7, 1]] + + spec.update(['a', in_data_1_1], ['b', in_data_2_1]) + spec.update(['a', in_data_1_2], ['b', in_data_2_2]) + + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + conj = spec.get_value('(a)and(b)') + + self.assertListEqual(a, in_data_1_2) + self.assertListEqual(b, in_data_2_2) + self.assertListEqual(c, out_expected_2) + self.assertListEqual(conj, out_expected_2) + if __name__ == '__main__': unittest.main() \ No newline at end of file diff --git a/tests/python/api/test_stl_sampling_time_units.py b/tests/python/api/test_stl_sampling_time_units.py index 582ba1d9..da009d15 100755 --- a/tests/python/api/test_stl_sampling_time_units.py +++ b/tests/python/api/test_stl_sampling_time_units.py @@ -53,11 +53,11 @@ def test_default_unit_default_sampling_unit_greater_tolerance_ok_samples(self): try: spec.parse() - spec.update(0, [['req', 2.2], ['gnt', 1]]) - spec.update(1.11, [['req', 2.2], ['gnt', 1]]) - spec.update(1.99, [['req', 2.2], ['gnt', 1]]) - spec.update(3.38, [['req', 2.2], ['gnt', 1]]) - spec.update(4.39, [['req', 2.2], ['gnt', 1]]) + spec.update(0, [['req', 2.2]]) + spec.update(1.11, [['req', 2.2]]) + spec.update(1.99, [['req', 2.2]]) + spec.update(3.38, [['req', 2.2]]) + spec.update(4.39, [['req', 2.2]]) self.assertEqual(0, spec.sampling_violation_counter, 'Violation counter') except rtamt.RTAMTException as err: From 44593e76e01aa960363502d67f68b430319d5e5a Mon Sep 17 00:00:00 2001 From: nickovic Date: Wed, 19 Feb 2025 20:14:39 +0100 Subject: [PATCH 3/4] Tests with python 3.8 only --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f8d592ab..1325d391 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,7 +8,7 @@ jobs: runs-on: ubuntu-20.04 strategy: matrix: - python-version: [3.7, 3.8] + python-version: [3.8] steps: - uses: actions/checkout@v1 From 5ac3ddf89d481c8c70eb97a620f31ec329a9ac35 Mon Sep 17 00:00:00 2001 From: nickovic Date: Wed, 19 Feb 2025 20:42:48 +0100 Subject: [PATCH 4/4] Added the description of the get_value() method to README and an example to the examples folder. --- README.md | 48 +++++++++++++++++++ .../access_subformulas/access_subformulas.py | 43 +++++++++++++++++ .../syntax/ast/parser/abstract_ast_parser.py | 1 + 3 files changed, 92 insertions(+) create mode 100644 examples/features/access_subformulas/access_subformulas.py diff --git a/README.md b/README.md index 2ac20183..8fa39ca3 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,8 @@ - [Dense-time Offline Monitor](#dense-time-offline-monitor) - [Discrete-time Specifics](#discrete-time-specifics) - [Working with time units and timing assumptions](#working-with-time-units-and-timing-assumptions) +- [Features] + - [Accessing evaluation of sub-formulas] - [References](#references) @@ -517,6 +519,52 @@ Finally, the following program is correct, because the temporal bound is explici spec.parse() ... ``` +# Features + +## Accessing evaluation of sub-formulas + +The following example shows how to use the `get_value` method from the +specification object to access the evaluated values of sub-formulas. This works for both +discrete- and dense-time specifications, as well as for online and offline +monitors. + +```python +def monitor(): + # data + dataset = { + 'time': [0, 1, 2], + 'a': [100.0, -1.0, -2.0], + 'b': [20.0, 2.0, 10.0] + } + + # # stl + spec = rtamt.StlDiscreteTimeSpecification() + spec.name = 'HandMadeMonitor' + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.declare_var('d', 'float') + spec.add_sub_spec('c = a + b') + spec.spec = 'd = c >= - 2' + + try: + spec.parse() + except rtamt.RTAMTException as err: + print('RTAMT Exception: {}'.format(err)) + sys.exit() + + spec.evaluate(dataset) + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + d = spec.get_value('d') + + print('a: ' + str(a)) + print('b: ' + str(b)) + print('c: ' + str(c)) + print('d: ' + str(d)) + +``` # References diff --git a/examples/features/access_subformulas/access_subformulas.py b/examples/features/access_subformulas/access_subformulas.py new file mode 100644 index 00000000..8dc47654 --- /dev/null +++ b/examples/features/access_subformulas/access_subformulas.py @@ -0,0 +1,43 @@ +#!/usr/bin/env python +import sys +import rtamt + +def monitor(): + # data + dataset = { + 'time': [0, 1, 2], + 'a': [100.0, -1.0, -2.0], + 'b': [20.0, 2.0, 10.0] + } + + # # stl + spec = rtamt.StlDiscreteTimeSpecification() + spec.name = 'HandMadeMonitor' + spec.declare_var('a', 'float') + spec.declare_var('b', 'float') + spec.declare_var('c', 'float') + spec.declare_var('d', 'float') + spec.add_sub_spec('c = a + b') + spec.spec = 'd = c >= - 2' + + try: + spec.parse() + except rtamt.RTAMTException as err: + print('RTAMT Exception: {}'.format(err)) + sys.exit() + + spec.evaluate(dataset) + a = spec.get_value('a') + b = spec.get_value('b') + c = spec.get_value('c') + d = spec.get_value('d') + + print('a: ' + str(a)) + print('b: ' + str(b)) + print('c: ' + str(c)) + print('d: ' + str(d)) + +if __name__ == '__main__': + # Process arguments + + monitor() diff --git a/rtamt/syntax/ast/parser/abstract_ast_parser.py b/rtamt/syntax/ast/parser/abstract_ast_parser.py index db5ca1ed..cdd19dcd 100644 --- a/rtamt/syntax/ast/parser/abstract_ast_parser.py +++ b/rtamt/syntax/ast/parser/abstract_ast_parser.py @@ -5,6 +5,7 @@ from antlr4.InputStream import InputStream from antlr4.error.ErrorListener import ErrorListener +from rtamt.syntax.ast.parser.stl.parser_visitor import StlAstParserVisitor from rtamt.exception.exception import RTAMTException class AbstractAst: