diff --git a/Dockerfile b/Dockerfile index 8dfaa47..4d2465a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -10,6 +10,8 @@ RUN pip3 install bs4 COPY src /app +RUN sed -i 's/min_valdInf/min_val/g' ../usr/local/lib/python3.10/site-packages/monitors/mtl.py + ENV FLASK_APP=main.py EXPOSE 5000 diff --git a/src/logic_endpoints.py b/src/logic_endpoints.py index 277f437..5957fe6 100644 --- a/src/logic_endpoints.py +++ b/src/logic_endpoints.py @@ -71,7 +71,8 @@ def _formula_info_from_request() -> dict: return formula_info -def _data_from_formula_info(formula_info: dict, options: dict): +def _data_from_formula_info(formula_info: dict): + options: dict = formula_info.get('options', {}) source = formula_info["measurement_source"] if source == "influx": @@ -115,8 +116,7 @@ def _data_from_formula_info(formula_info: dict, options: dict): def start_evaluation(formula, params_string, formula_info): - options: dict = formula_info.get('options', {}) - points_names, multi_dim_array = _data_from_formula_info(formula_info, options) + points_names, multi_dim_array = _data_from_formula_info(formula_info) # if the formula is in future-MTL the trace is reversed and the results also reverse = False @@ -125,6 +125,7 @@ def start_evaluation(formula, params_string, formula_info): array.reverse() reverse = True + options: dict = formula_info.get('options', {}) mtl_eval_output, intervals = MTLEvaluator(formula, params_string).evaluate( points_names, multi_dim_array, diff --git a/src/mtl_evaluation/mtl_refinement.py b/src/mtl_evaluation/mtl_refinement.py index 3f7a560..a596b36 100644 --- a/src/mtl_evaluation/mtl_refinement.py +++ b/src/mtl_evaluation/mtl_refinement.py @@ -94,9 +94,9 @@ def _refine_bounds_two_sided(self, is_satisfied: bool, current_bounds: Interval) :return: Whether the timebound has been refined. """ if self._refined_bounds.lower < 0: - if not is_satisfied: + if not is_satisfied and not current_bounds.lower == 0: # found lower bound if the formula is not satisfied and the previous one was - current_bounds.lower -= 1 + current_bounds.lower = current_bounds.lower - 1 self._refined_bounds.lower = current_bounds.upper = current_bounds.lower else: current_bounds.lower += 1 @@ -120,7 +120,7 @@ def _refine_bounds_one_sided(self, is_satisfied: bool, current_bounds: Interval) :return: Whether the timebound has been refined. """ if self._refined_bounds.upper < 0: - if not is_satisfied: + if not is_satisfied and not current_bounds.upper == 0: self._refined_bounds.upper = current_bounds.upper - 1 return True elif current_bounds.upper == self._max_index: