Merge branch 'siftech:develop' into develop

auxiliary_packages/funman_benchmarks/src/funman_benchmarks/_version.py

@@ -1,4 +1,4 @@
 """Version information."""
 
 # The following line *must* be the last in the module, exactly as formatted:
-__version__ = "1.8.0"
+__version__ = "1.9.1"

auxiliary_packages/funman_demo/src/funman_demo/_version.py

@@ -1,4 +1,4 @@
 """Version information."""
 
 # The following line *must* be the last in the module, exactly as formatted:
-__version__ = "1.8.0"
+__version__ = "1.9.1"

auxiliary_packages/funman_demo/src/funman_demo/box_plotter.py

@@ -209,6 +209,7 @@ def plot_add_patch(self, box: Box, color="r"):
                     linewidth=1,
                     edgecolor=color,
                     facecolor="none",
+                    zorder=box.timestep().lb * box.timestep().lb,
                 )
 
                 # Add the patch to the Axes
@@ -235,6 +236,7 @@ def plot_add_point(self, point: Point, color="r", shape="x", alpha=0.2):
                     marker=shape,
                     alpha=alpha,
                     s=3,
+                    zorder=point.timestep(),
                 )
                 self.fig.canvas.draw()
                 self.fig.canvas.flush_events()
@@ -311,6 +313,7 @@ def plotNDBox(self, box, color="g", alpha=0.2):
                             y_limits.ub,
                             color=color,
                             alpha=alpha,
+                            zorder=box.timestep().lb * box.timestep().lb,
                         )
         plt.show(block=False)
 

auxiliary_packages/funman_demo/src/funman_demo/parameter_space_plotter.py

@@ -1,5 +1,5 @@
 import logging
-from typing import Dict
+from typing import Dict, List
 
 import matplotlib.pyplot as plt
 import numpy as np
@@ -15,6 +15,7 @@ class ParameterSpacePlotter:
     def __init__(
         self,
         parameter_space: ParameterSpace,
+        boxes: List[Box] = None,
         plot_bounds: Box = None,
         title: str = "Feasible Regions",
         color_map: Dict[str, str] = {
@@ -35,16 +36,10 @@ def __init__(
             # FIXME this is a hack to accept ParameterSpace objects from the openapi client
             self.ps = ParameterSpace.model_validate(parameter_space.to_dict())
 
-        # TODO this should be easier to access
-        values = []
-        true_points = self.ps.true_points()
-        false_points = self.ps.false_points()
-        if len(true_points) > 0:
-            values = true_points[0].values
-        elif len(false_points) > 0:
-            values = false_points[0].values
+        self.boxes = boxes
 
-        self.parameters = [k for k in values if parameters and k in parameters]
+        # Expect that parameters are available in the parameter space
+        self.parameters = parameters  # [k for k in scenario_parameters if parameters and k in parameters]
         self.synthesized_parameters = (
             synthesized_parameters if synthesized_parameters else None
         )
@@ -126,28 +121,44 @@ def initialize_figure(self, plot_diagonal):
         plt.legend(self.custom_lines, ["true", "false"])
 
     def plot(self, show=False, plot_diagonal=False):
-        self.initialize_figure(plot_diagonal)
+        self.initialize_figure((plot_diagonal or len(self.parameters) == 1))
         t = "true"
         f = "false"
-        for b in self.ps.false_boxes:
-            self.plotNDBox(b, self.color_map[f], plot_diagonal=plot_diagonal)
-        for b in self.ps.true_boxes:
-            self.plotNDBox(b, self.color_map[t], plot_diagonal=plot_diagonal)
+        if self.boxes:
+            for b in self.boxes:
+                self.plotNDBox(
+                    b,
+                    self.color_map[b.label],
+                    plot_diagonal=(plot_diagonal or len(self.parameters) == 1),
+                )
+        else:
+            for b in self.ps.false_boxes:
+                self.plotNDBox(
+                    b,
+                    self.color_map[f],
+                    plot_diagonal=(plot_diagonal or len(self.parameters) == 1),
+                )
+            for b in self.ps.true_boxes:
+                self.plotNDBox(
+                    b,
+                    self.color_map[t],
+                    plot_diagonal=(plot_diagonal or len(self.parameters) == 1),
+                )
         if self.plot_points:
             for p in self.ps.false_points():
                 self.plot_add_point(
                     p,
                     self.color_map[f],
                     self.shape_map[f],
-                    plot_diagonal=plot_diagonal,
+                    plot_diagonal=(plot_diagonal or len(self.parameters) == 1),
                 )
             true_points = self.ps.true_points()
             for p in true_points:
                 self.plot_add_point(
                     p,
                     self.color_map[t],
                     self.shape_map[t],
-                    plot_diagonal=plot_diagonal,
+                    plot_diagonal=(plot_diagonal or len(self.parameters) == 1),
                 )
         if show:
             plt.show(block=False)
@@ -179,11 +190,14 @@ def plot_add_point(
                     marker=shape,
                     alpha=alpha,
                     s=10,
+                    zorder=point.timestep(),
                 )
                 # self.fig.canvas.draw()
                 # self.fig.canvas.flush_events()
 
-    def plotNDBox(self, box, color="g", alpha=0.2, plot_diagonal=False):
+    def plotNDBox(
+        self, box, color="g", alpha=0.2, plot_diagonal=False, max_width=100000
+    ):
         for i in range(self.dim):
             for j in range(self.dim):
                 i_coord, j_coord = self.map_param_idx_to_plot_loc(
@@ -215,16 +229,27 @@ def plotNDBox(self, box, color="g", alpha=0.2, plot_diagonal=False):
                 else:
                     # Plot a box
                     if (
-                        abs(float(x_limits.lb)) < 1000
-                        and abs(float(x_limits.ub)) < 1000
+                        abs(float(x_limits.lb)) < max_width
+                        and abs(float(x_limits.ub)) < max_width
                     ):
                         x = np.linspace(
-                            float(x_limits.lb), float(x_limits.ub), 1000
+                            float(x_limits.lb), float(x_limits.ub), max_width
                         )
                         self.axs[i_coord, j_coord].fill_between(
                             x,
                             y_limits.lb,
                             y_limits.ub,
                             color=color,
                             alpha=alpha,
+                            zorder=box.timestep().lb,
+                        )
+                        self.axs[i_coord, j_coord].text(
+                            (x_limits.lb + x_limits.ub) / 2,
+                            (y_limits.lb + y_limits.ub) / 2,
+                            # f"[{box.timestep().lb}, {box.timestep().ub}]",
+                            f"{box.timestep().lb}",
+                            ha="center",
+                            va="center",
+                            fontsize=8,
+                            color="blue",
                         )

auxiliary_packages/funman_demo/src/funman_demo/plot.py

@@ -76,6 +76,7 @@ def summarize_results(
     parameters_to_plot=None,
     label_color={"true": "g", "false": "r"},
     synthesized_parameters=None,
+    print_last_time=False,
 ) -> str:
     points = results.points()
     boxes = results.parameter_space.boxes()
@@ -104,9 +105,16 @@ def summarize_results(
         {json.dumps(box.explain(), indent=4)}
         """
 
-    boxes = results.parameter_space.boxes()
+    boxes = (
+        results.parameter_space.boxes()
+        if not print_last_time
+        else results.parameter_space.last_boxes()
+    )
+
     if parameters_to_plot is None:
-        parameters_to_plot = results.model._parameter_names() + ["timestep"]
+        parameters_to_plot = results.model._parameter_names()
+        if not print_last_time:
+            parameters_to_plot += ["timestep"]
     if len(boxes) > 0 and len(parameters_to_plot) > 1:
         ParameterSpacePlotter(
             results.parameter_space,

auxiliary_packages/funman_dreal/setup.py

@@ -23,7 +23,7 @@
     packages=find_packages("src"),
     package_dir={"": "src"},
     install_requires=["funman", "docker", "tenacity", "pyparsing"],
-    extras_require={"dreal": ["dreal"]},
+    # extras_require={"dreal": ["dreal"]},
     tests_require=["unittest"],
     zip_safe=False,
 )

auxiliary_packages/funman_dreal/src/funman_dreal/_version.py

@@ -1,4 +1,4 @@
 """Version information."""
 
 # The following line *must* be the last in the module, exactly as formatted:
-__version__ = "1.8.0"
+__version__ = "1.9.1"

auxiliary_packages/funman_dreal/src/funman_dreal/solver.py

@@ -20,7 +20,7 @@
 )
 from pysmt.formula import FNode
 from pysmt.logics import QF_NRA
-from pysmt.shortcuts import BOOL, Bool, Real, get_env
+from pysmt.shortcuts import BOOL, TRUE, Bool, Real, get_env
 from pysmt.smtlib.parser import SmtLibParser
 from pysmt.smtlib.script import SmtLibCommand
 from pysmt.smtlib.solver import SmtLibOptions, SmtLibSolver
@@ -443,6 +443,11 @@ def __init__(
         self.model = None
         self.log_level = dreal.LogLevel.OFF
         if "solver_options" in options:
+            if (
+                "preferred" in options["solver_options"]
+                and len(options["solver_options"]["preferred"]) > 0
+            ):
+                self.config.preferred = options["solver_options"]["preferred"]
             if "dreal_precision" in options["solver_options"]:
                 self.config.precision = options["solver_options"][
                     "dreal_precision"
@@ -595,8 +600,11 @@ def get_model(self):
         for sn in self.symbols:
             s = self.symbols[sn][0]
             if s.is_term():
-                v = self.get_value(self.symbols[sn])
-                assignment[s] = v
+                try:
+                    v = self.get_value(self.symbols[sn])
+                    assignment[s] = v
+                except ValueError as e:
+                    l.error(f"DRealNative.get_model(): {e}")
         return EagerModel(assignment=assignment, environment=self.environment)
 
     def get_value(self, symbol_pair):
@@ -610,7 +618,11 @@ def get_value(self, symbol_pair):
             lb = self.model[item].lb()
             mid = (ub - lb) / 2.0
             mid = mid + lb
-            if not isinstance(mid, int) and (
+
+            if math.isnan(lb) and math.isnan(ub):
+                # Value was not assigned
+                return None
+            elif not isinstance(mid, int) and (
                 isinstance(ub, int) or isinstance(lb, int)
             ):
                 return Real(lb) if isinstance(lb, int) else Real(ub)

auxiliary_packages/pde2petri/src/pde2petri/_version.py

@@ -1 +1 @@
-__version__ = "1.8.0"
+__version__ = "1.9.1"

docker/dev/root/Dockerfile.root

@@ -36,7 +36,8 @@ RUN pip install --no-cache-dir wheel
 
 RUN pip install --no-cache-dir pytest==7.1.2
 RUN pip install --no-cache-dir sphinx==5.2.2
-RUN pip install --no-cache-dir sphinx-rtd-theme==1.0.0
+RUN pip install --no-cache-dir myst-parser
+RUN pip install --no-cache-dir autodoc-pydantic
 RUN pip install --no-cache-dir twine
 RUN pip install --no-cache-dir build
 RUN pip install --no-cache-dir pylint

docker/dev/user/Dockerfile

@@ -44,7 +44,8 @@ RUN pip install --no-cache-dir wheel
 
 RUN pip install --no-cache-dir pytest==7.1.2
 RUN pip install --no-cache-dir sphinx==5.2.2
-RUN pip install --no-cache-dir sphinx-rtd-theme==1.0.0
+RUN pip install --no-cache-dir myst-parser
+RUN pip install --no-cache-dir autodoc-pydantic
 RUN pip install --no-cache-dir twine
 RUN pip install --no-cache-dir build
 RUN pip install --no-cache-dir pylint

docker/docker-bake.hcl

@@ -23,7 +23,7 @@ variable "DREAL_REPO_URL" {
   default = "https://github.com/danbryce/dreal4.git"
 }
 variable "DREAL_COMMIT_TAG" {
-  default = "b46e45dbd38f739889a629168851e6d050448275"
+  default = "844d64fd7427d5d2ce3b01a2f83231cefc8709a4"
 }
 variable "AUTOMATES_COMMIT_TAG" {
   default = "e5fb635757aa57007615a75371f55dd4a24851e0"

docker/dreal4/Dockerfile.dreal4

@@ -71,10 +71,11 @@ RUN cd /dreal4 \
       && bazel build //:archive \
       && tar xfz bazel-bin/archive.tar.gz --strip-components 3 -C /usr \
 # Install Python3 Binding
-      && pip3 install wheel \
+      && pip3 install --upgrade wheel \
+      && pip3 install --upgrade setuptools \
       && pip3 install --upgrade pip \
       && python3 setup.py bdist_wheel \
-      && DREAL_WHEEL=dreal-*-cp38-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)-cp310-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,4 +1,4 @@
-FROM ubuntu:20.04
+FROM ubuntu:22.04
 ARG IBEX_BRANCH
 
 ARG ENABLE_DEBUG=no

docs/source/conf.py

@@ -45,7 +45,7 @@
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output
 
 # html_theme = 'pydata_sphinx_theme'
-html_theme = "sphinx_rtd_theme"
+html_theme = "classic"
 html_static_path = ["_static"]
 
 # Napoleon configuration for handling numpy docstrings