Merge remote-tracking branch 'sifttech/develop'

Makefile

@@ -1,4 +1,4 @@
-.PHONY: test
+.PHONY: test docs
 
 # -----------------------------------------------------------------
 # Base Image Construction
@@ -293,7 +293,7 @@ deploy-pages:
  mv docs/build/html www
  touch www/.nojekyll
  rm www/.buildinfo || true
- git checkout --track $(DOCS_REMOTE)/gh-pages
+ git checkout --track $(DOCS_REMOTE)/gh-pages || git checkout $(DOCS_REMOTE)/gh-pages
  rm -r docs || true
  mv www docs
  git add -f docs

README.md

@@ -1,9 +1,24 @@
 # funman
 
-The `funman` package implements multiple simulator model analysis methods.
-Current methods include:
-- Parameter Synthesis
-- Querying a Simulation
+The `funman` package performs Functional Model Analysis by processing a request and model pair that describes an analysis scenario. Funman supports a number of model formats, which correspond to the classes in `funman.models`:
+
+- [GeneratedPetriNet](#funman.model.generated_models.petrinet.Model): AMR model for petri nets generated 
+- [GeneratedRegNet](#funman.model.generated_models.regnet.Model): AMR model for regulatory networks
+- [RegnetModel](#funman.model.regnet.RegnetModel): MIRA model for regulatory networks
+- [PetrinetModel](#funman.model.petrinet.PetrinetModel): MIRA model for petri nets
+- [BilayerModel](#funman.model.bilayer.BilayerModel): ASKE model for bilayer networks
+
+Requests correspond to the class `funman.server.query.FunmanWorkRequest` and specify the following keys:
+- [query](#funman.model.query): a soft constraint that a model must satisfy (legacy support, deprecated)
+- [constraints](#funman.representation.constraint): a list of hard or soft constraints that a model must satisfy
+- parameters: a list of bounded parameters that funman will either synthesize ("label": "all") or satsify ("label": "any"). Funman will check "all" values within the parameter bounds or if "any" within the bounds permit the model to satisfy the query and constraints.
+- [config](#funman.config): A dictionary of funman configuration options. 
+ label regions of the parameter space as satisfying the query and constraints, if synthesized, or find any legal value if asked to satsify. 
+- [structure_parameters](#funman.representation.parameter): parameters shaping the way that funman structures its analysis. Funman requires that either the `num_steps` and `step_size` parameters are specified, or the `schedules` parameter is specified. If all are omitted, then funman defaults to checking one unit-sized step.
+
+## **Running funman**
+
+There are multiple ways to run Funman on a model and request pair. We recommend running funman in Docker, due to some complex dependencies on dReal (and its dependency on ibex). Funman has a Makefile that supports building three Docker use cases: 1) run a development container that mounts the source code, 2) run a container with a jupyter server, and 3) run a container with uvicorn serving a REST API. Examples of running each of these cases are illustrated by the tests (`test/test_api.py`, and `test/test_terarium.py`). It is also possible to pull a pre-generated image that will run the API, as described in `terarium/README.md`.
 
 ## **Use cases**
 ### **Compare Bilayer Model to Simulator**:

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.6.0"
+__version__ = "1.7.0"

auxiliary_packages/funman_demo/src/funman_demo/box_plotter.py

@@ -29,7 +29,7 @@ def __init__(
  "false": "r",
  "unknown": "b",
  },
- shape_map: Dict[str, str] = {"true": "x", "false": "o"},
+ shape_map: Dict[str, str] = {"true": "+", "false": "-"},
  alpha=0.2,
  ) -> None:
  self.parameters = parameters

auxiliary_packages/funman_demo/src/funman_demo/parameter_space_plotter.py

@@ -35,10 +35,12 @@ def __init__(
 
  # TODO this should be easier to access
  values = []
- if len(self.ps.true_points) > 0:
- values = self.ps.true_points[0].values
- elif len(self.ps.false_points) > 0:
- values = self.ps.false_points[0].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.parameters = [k for k in values if parameters and k in parameters]
  self.dim = len(self.parameters)
@@ -107,9 +109,10 @@ def plot(self, show=False):
  for b in self.ps.true_boxes:
  self.plotNDBox(b, self.color_map[t])
  if self.plot_points:
- for p in self.ps.false_points:
+ for p in self.ps.false_points():
  self.plot_add_point(p, self.color_map[f], self.shape_map[f])
- for p in self.ps.true_points:
+ true_points = self.ps.true_points()
+ for p in true_points:
  self.plot_add_point(p, self.color_map[t], self.shape_map[t])
  if show:
  plt.show(block=False)
@@ -128,7 +131,7 @@ def plot_add_point(self, point: Point, color="r", shape="x", alpha=0.9):
  color=color,
  marker=shape,
  alpha=alpha,
- s=4,
+ s=10,
  )
  # self.fig.canvas.draw()
  # self.fig.canvas.flush_events()

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.6.0"
+__version__ = "1.7.0"

auxiliary_packages/funman_dreal/src/funman_dreal/solver.py

@@ -44,7 +44,6 @@
 
 
 l = logging.getLogger(__name__)
-l.setLevel(logging.INFO)
 
 
 # TODO find a better way to determine if solver was successful
@@ -442,6 +441,7 @@ def __init__(
  # self.context.config.use_polytope = True
  # self.context.config.use_worklist_fixpoint = True
  self.model = None
+ self.log_level = dreal.LogLevel.OFF
  if "solver_options" in options:
  if "dreal_precision" in options["solver_options"]:
  self.config.precision = options["solver_options"][
@@ -450,10 +450,13 @@ def __init__(
  if "dreal_log_level" in options["solver_options"]:
  if options["solver_options"]["dreal_log_level"] == "debug":
  dreal.set_log_level(dreal.LogLevel.DEBUG)
+ self.log_level = dreal.LogLevel.DEBUG
  elif options["solver_options"]["dreal_log_level"] == "trace":
  dreal.set_log_level(dreal.LogLevel.TRACE)
+ self.log_level = dreal.LogLevel.TRACE
  elif options["solver_options"]["dreal_log_level"] == "info":
  dreal.set_log_level(dreal.LogLevel.INFO)
+ self.log_level = dreal.LogLevel.INFO
 
  if (
  "dreal_mcts" in options["solver_options"]
@@ -481,13 +484,13 @@ def elapsed_timer(self):
  elapser = None
 
  def __del__(self):
- # print("Exit()")
+ l.trace("Exit()")
  self.context.Exit() # Exit() only logs within dreal
  self.context = None
 
  @clear_pending_pop
  def add_assertion(self, formula, named=None):
- # print(f"Assert({formula.serialize()})")
+ l.trace(f"Assert({formula.serialize()})")
 
  f = self.converter.convert(formula)
 
@@ -514,7 +517,7 @@ def cmd_set_logic(self, cmd):
  pass
 
  def cmd_declare_fun(self, cmd):
- # print(f"DeclareVariable({cmd.args[0]})")
+ l.trace(f"DeclareVariable({cmd.args[0]})")
  if cmd.args[0] in self.converter.symbol_to_decl:
  v = self.converter.symbol_to_decl[cmd.args[0]]
  else:
@@ -529,29 +532,37 @@ def cmd_push(self, cmd):
  self.push(cmd.args[0])
 
  def push(self, levels):
- # print("Push()")
+ l.trace("Push()")
  self.context.Push(levels)
 
  def cmd_pop(self, cmd):
  self.pop(cmd.args[0])
 
  def pop(self, levels):
- # print("Pop()")
+ l.trace("Pop()")
  self.context.Pop(levels)
 
  def cmd_check_sat(self, cmd):
  return self.check_sat()
 
  def check_sat(self):
- # print("CheckSat()")
+ l.trace("CheckSat()")
  with self.elapsed_timer() as t:
+ # FIXME solver is giving wrong results without logging enabled to prime it
+
+ # dreal.set_log_level(dreal.LogLevel.INFO)
+ # self.push(1)
+ # result = self.context.CheckSat()
+ # self.pop(1)
+ dreal.set_log_level(self.log_level)
  result = self.context.CheckSat()
  elapsed_base_dreal = t()
- l.debug(
+ l.trace(
  f"{('delta-sat' if result else 'unsat' )} took {elapsed_base_dreal}s"
  )
  # result = dreal.CheckSatisfiability(self.assertion, 0.001)
  self.model = result
+ l.trace(result)
  return result
 
  def get_unsat_core(self) -> FNode:
@@ -589,8 +600,8 @@ def get_model(self):
  return EagerModel(assignment=assignment, environment=self.environment)
 
  def get_value(self, symbol_pair):
- # print(f"get_value() {item}: {self.model[item]}")
  (symbol, item) = symbol_pair
+ l.trace(f"get_value() {item}: {self.model[item]}")
  if symbol.get_type() == BOOL:
  is_true = self.model[item].lb() == self.model[item].ub() == 1.0
  return Bool(is_true)

docker/dev/user/Dockerfile

@@ -50,8 +50,8 @@ RUN pip install --no-cache-dir build
 RUN pip install --no-cache-dir pylint
 RUN pip install --no-cache-dir black
 RUN pip install --no-cache-dir uvicorn
-RUN pip install --no-cache-dir pydantic==1.10.9
-RUN pip install --no-cache-dir fastapi==0.98.0
+RUN pip install --no-cache-dir pydantic>=2.3.0
+RUN pip install --no-cache-dir fastapi>=0.103.1
 RUN pip install --no-cache-dir pre-commit
 RUN pip install --no-cache-dir pycln
 RUN pip install --no-cache-dir openapi-python-client

docs/source/conf.py

@@ -7,7 +7,7 @@
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information
 
 project = "funman"
-copyright = "2022, SIFT"
+copyright = "2023, SIFT"
 author = "SIFT"
 
 from funman import __version__
@@ -23,6 +23,7 @@
  "sphinx.ext.inheritance_diagram",
  "sphinx.ext.napoleon",
  "sphinxcontrib.autodoc_pydantic",
+ "myst_parser",
 ]
 
 autodoc_pydantic_model_show_json = True

docs/source/index.rst

@@ -16,6 +16,11 @@ Welcome to funman's documentation!
  packages
  funman
 
+README File
+===========
+
+.. include:: ../../README.md
+ :parser: myst_parser.sphinx_
 
 Indices and tables
 ==================