Merge pull request #6 from Cambio-Project/add_time_refinement

Various fixes

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

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,

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: