Merge branch 'siftech:develop' into develop

docker/base/Dockerfile

@@ -38,11 +38,11 @@ ARG AUTOMATES_COMMIT_TAG
 #     && git checkout ${AUTOMATES_COMMIT_TAG}
 # RUN pip install -e automates
 
-RUN pip install --no-cache-dir z3-solver
+RUN pip install --no-cache-dir z3-solver==4.12.6
 RUN pip install --no-cache-dir graphviz
-RUN pip install --no-cache-dir pydantic>=2.3.0
+RUN pip install --no-cache-dir pydantic
 RUN pip install --no-cache-dir pydantic-settings
-RUN pip install --no-cache-dir fastapi>=0.103.1
+RUN pip install --no-cache-dir fastapi
 
 RUN pip install --no-cache-dir --upgrade setuptools pip
 RUN pip install --no-cache-dir wheel

docker/deploy/Dockerfile.deploy

@@ -34,7 +34,7 @@ RUN git clone --depth=1 https://github.com/danbryce/automates.git automates \
     && git checkout e5fb635757aa57007615a75371f55dd4a24851e0
 RUN pip install -e automates
 
-RUN pip install --no-cache-dir z3-solver
+RUN pip install --no-cache-dir z3-solver==4.12.6
 RUN pip install --no-cache-dir graphviz
 
 # Install funman dev packages

docker/dev/root/Dockerfile.root

@@ -59,7 +59,7 @@ WORKDIR /root
 #     && git checkout e5fb635757aa57007615a75371f55dd4a24851e0
 # RUN pip install -e automates
 
-RUN pip install --no-cache-dir z3-solver
+RUN pip install --no-cache-dir z3-solver==4.12.6
 RUN pip install --no-cache-dir graphviz
 
 RUN pip install /dreal4/dreal-*.whl

docker/dev/user/Dockerfile

@@ -67,7 +67,7 @@ WORKDIR /home/$UNAME
 #     && git checkout e5fb635757aa57007615a75371f55dd4a24851e0
 # RUN pip install -e automates
 
-RUN pip install --no-cache-dir z3-solver
+RUN pip install --no-cache-dir z3-solver==4.12.6
 RUN pip install --no-cache-dir graphviz
 
 RUN pip install /dreal4/dreal-*.whl

docker/dreal4/Dockerfile.dreal4

@@ -75,7 +75,7 @@ RUN cd /dreal4 \
       && pip3 install --upgrade setuptools \
       && pip3 install --upgrade pip \
       && python3 setup.py bdist_wheel \
-      && DREAL_WHEEL=dreal-$(python setup.py --version)-cp310-none-manylinux_$(ldd --version | grep '^ldd' | sed -E 's/^ldd.*([0-9]+)\.([0-9]+)$/\1_\2/')_$(arch).whl \
+      && DREAL_WHEEL=dreal-$(python setup.py --version)-cp38-none-manylinux_$(ldd --version | grep '^ldd' | sed -E 's/^ldd.*([0-9]+)\.([0-9]+)$/\1_\2/')_$(arch).whl \
       && cp ./dist/$DREAL_WHEEL /tmp/$DREAL_WHEEL \
       && pip3 install ./dist/$DREAL_WHEEL \
       && bazel clean --expunge \

docker/ibex/Dockerfile

@@ -1,10 +1,8 @@
-FROM ubuntu:22.04
+FROM ubuntu:20.04
 ARG IBEX_BRANCH
 
 ARG ENABLE_DEBUG=no
 
-ARG ENABLE_DEBUG=no
-
 ARG DEBIAN_FRONTEND=noninteractive
 # Install base dependencies
 RUN apt update && apt install -y --no-install-recommends \

src/funman/api/run.py

@@ -482,7 +482,7 @@ def get_args():
         help=f"Create parameter space plot with only the last timestep.",
     )
 
-    parser.set_defaults(plot=False)
+    parser.set_defaults(plot=None)
     return parser.parse_args()
 
 

src/funman/representation/interval.py

@@ -1,10 +1,12 @@
 import logging
 from decimal import Decimal
-from typing import List, Optional, Union
+from math import isinf
+from typing import Any, List, Optional, Union
 
 from numpy import average, finfo, nextafter
 from pydantic import (
     BaseModel,
+    ConfigDict,
     Field,
     SerializerFunctionWrapHandler,
     field_serializer,
@@ -24,6 +26,7 @@ class Interval(BaseModel):
     An interval is a pair [lb, ub) that is open (i.e., an interval specifies all points x where lb <= x and ub < x).
     """
 
+    model_config = ConfigDict(ser_json_inf_nan="constants")
     lb: Optional[Union[float, str]] = NEG_INFINITY
     ub: Optional[Union[float, str]] = POS_INFINITY
     closed_upper_bound: bool = False
@@ -403,6 +406,17 @@ def _denormalize(self):
         self.ub = self.ub if not self.unnormalized_ub else self.unnormalized_ub
         self.unnormalized_ub = None
 
+    @model_validator(mode="before")
+    @classmethod
+    def check_original_width_inf(cls, data: Any) -> Any:
+        if (
+            "original_width" in data
+            and isinstance(data["original_width"], float)
+            and isinf(data["original_width"])
+        ):
+            data["original_width"] = None
+        return data
+
     @model_validator(mode="after")
     def check_interval(self) -> str:
         if self.lb is None:

src/funman/search/box_search.py

@@ -1221,15 +1221,15 @@ def _expand(
                                 l.trace(f"+++ True:\n{box}")
 
                                 if episode.config.corner_points:
-                                    corner_points: List[
-                                        Point
-                                    ] = self.get_box_corners(
-                                        solver,
-                                        episode,
-                                        curr_step_box,
-                                        rval,
-                                        options,
-                                        my_solver,
+                                    corner_points: List[Point] = (
+                                        self.get_box_corners(
+                                            solver,
+                                            episode,
+                                            curr_step_box,
+                                            rval,
+                                            options,
+                                            my_solver,
+                                        )
                                     )
 
                                 # Advance a true box to be considered for later timesteps
@@ -1275,15 +1275,15 @@ def _expand(
                             l.debug(f"False @ {box.timestep().lb}")
                             l.trace(f"--- False:\n{box}")
                             if episode.config.corner_points:
-                                corner_points: List[
-                                    Point
-                                ] = self.get_box_corners(
-                                    solver,
-                                    episode,
-                                    box,
-                                    rval,
-                                    options,
-                                    my_solver,
+                                corner_points: List[Point] = (
+                                    self.get_box_corners(
+                                        solver,
+                                        episode,
+                                        box,
+                                        rval,
+                                        options,
+                                        my_solver,
+                                    )
                                 )
                             rval.put(box.model_dump())
                         else:  # Timeout FIXME copy of split code

src/funman/server/query.py

@@ -195,7 +195,12 @@ def update_progress(
 
     def finalize(self):
         """Calculate total time"""
-        self.total_time = self.end_time - self.start_time
+        try:
+            self.total_time = self.end_time - self.start_time
+        except Exception as e:
+            l.exception(
+                f"Exception in FunmanResultsTiming:finalize() start_time: {self.start_time} end_time: {self.end_time}"
+            )
 
 
 class FunmanResults(BaseModel):
@@ -278,7 +283,11 @@ def update_parameter_space(
         self.progress.progress = coverage_of_search_space
         self.progress.coverage_of_search_space = coverage_of_search_space
         self.progress.coverage_of_representable_space = coverage_of_repr_space
-        self.timing.update_progress(self.progress.coverage_of_search_space)
+
+        try:
+            self.timing.update_progress(self.progress.coverage_of_search_space)
+        except Exception as e:
+            l.exception(f"Unable to update progress due to exception: {e}")
 
         self.contract_model()
 
@@ -544,7 +553,9 @@ def plot(
                         **kwargs,
                     )
                 else:
+                    # data = [state_vars[c].tolist() for c in state_vars.columns]
                     ax = plt.plot(
+                        # data, #
                         state_vars,
                         label=label,
                         marker=label_marker[label],

tools/update-dreal.user

@@ -10,7 +10,7 @@ if [ ! -d $DREAL_ROOT ] ; then
   exit 1
 fi
 
-DREAL_WHEEL=dreal-$(python ${DREAL_ROOT}/setup.py --version)-cp310-none-manylinux_$(ldd --version | grep '^ldd' | sed -E 's/^ldd.*([0-9]+)\.([0-9]+)$/\1_\2/')_$(arch).whl \
+DREAL_WHEEL=dreal-$(python ${DREAL_ROOT}/setup.py --version)-cp38-none-manylinux_$(ldd --version | grep '^ldd' | sed -E 's/^ldd.*([0-9]+)\.([0-9]+)$/\1_\2/')_$(arch).whl \
 
 FUNMAN_ENV_PATH=$HOME/funman_venv
 FUNMAN_PYTHON=${FUNMAN_ENV_PATH}/bin/python