update docs

Author: danbryce

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**:

docs/source/conf.py

@@ -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
 ==================

requirements-dev.txt

@@ -6,4 +6,5 @@ pycln
 pytest-cov
 twine
 autodoc_pydantic
+myst-parser
 parameterized

src/funman/representation/box.py

@@ -114,7 +114,7 @@ def project(self, vars: Union[List[ModelParameter], List[str]]) -> "Box":
 
         Parameters
         ----------
-        vars : Union[List[Parameter], List[str]]
+        vars : Union[List[ModelParameter], List[str]]
             variables to project onto
 
         Returns

src/funman/search/box_search.py

@@ -42,18 +42,18 @@
 
 
 class FormulaStackFrame(BaseModel):
-    formulas: List[FNode] = []
-    simplified_formulas: List[FNode] = []
+    _formulas: List[FNode] = []
+    _simplified_formulas: List[FNode] = []
 
     model_config = ConfigDict(
         arbitrary_types_allowed=True,
     )
 
     def add_assertion(self, formula, is_simplified=False):
         if is_simplified:
-            self.simplified_formulas.append(formula)
+            self._simplified_formulas.append(formula)
         else:
-            self.formulas.append(formula)
+            self._formulas.append(formula)
 
     # def __str__(self) -> str:
     #     s_formulas = [f.serialize() for f in self.formulas]
@@ -65,8 +65,8 @@ def add_assertion(self, formula, is_simplified=False):
 class FormulaStack(BaseModel):
     formula_stack: List[FormulaStackFrame] = []
     time: int = -2
-    solver: Optional[Solver] = None
-    substitutions: Dict[FNode, FNode] = None
+    _solver: Optional[Solver] = None
+    _substitutions: Dict[FNode, FNode] = None
 
     model_config = ConfigDict(
         arbitrary_types_allowed=True,
@@ -79,15 +79,15 @@ def __init__(self, *args, **kwargs):
     def pop(self, levels: int = 1, pop_solver: bool = True):
         for i in range(levels):
             if pop_solver:
-                self.solver.pop(1)
+                self._solver.pop(1)
             self.formula_stack.pop()
             self.time -= 1
 
     def push(self, levels: int = 1, push_solver: bool = True):
         for i in range(levels):
             self.formula_stack.append(FormulaStackFrame())
             if push_solver:
-                self.solver.push(1)
+                self._solver.push(1)
             self.time += 1
 
     # def __str__(self)-> str:
@@ -99,24 +99,24 @@ def add_assertion(self, formula):
             formula, is_simplified=False
         )
 
-        if self.substitutions is not None:
+        if self._substitutions is not None:
             simplified_formula = formula.substitute(
-                self.substitutions
+                self._substitutions
             ).simplify()
             self.formula_stack[self.time + 1].add_assertion(
                 simplified_formula, is_simplified=True
             )
-            self.solver.add_assertion(simplified_formula)
+            self._solver.add_assertion(simplified_formula)
         else:
-            self.solver.add_assertion(formula)
+            self._solver.add_assertion(formula)
 
     def to_list(self, simplified=False) -> List[FNode]:
         if simplified:
             return [
-                f for sf in self.formula_stack for f in sf.simplified_formulas
+                f for sf in self.formula_stack for f in sf._simplified_formulas
             ]
         else:
-            return [f for sf in self.formula_stack for f in sf.formulas]
+            return [f for sf in self.formula_stack for f in sf._formulas]
 
     def compute_assignment(
         self, episode: SearchEpisode, _smtlib_save_fn: Callable = None
@@ -125,21 +125,21 @@ def compute_assignment(
         original_formulas = [
             formula
             for frame in self.formula_stack
-            for formula in frame.formulas
+            for formula in frame._formulas
         ]
         for formula in original_formulas:
-            self.solver.add_assertion(formula)
+            self._solver.add_assertion(formula)
             self.formula_stack[-1].add_assertion(
                 formula, is_simplified=True
             )  # formula is not simplified but want to layer on top of simplified formulas to compute state variables
         if _smtlib_save_fn:
             _smtlib_save_fn(filename=f"box_search_{episode._iteration}")
 
-        if not self.solver.solve():
+        if not self._solver.solve():
             raise Exception(
                 f"Could not compute Assignment from simplified formulas"
             )
-        result = self.solver.get_model()
+        result = self._solver.get_model()
         self.pop()
         return result
 
@@ -176,7 +176,7 @@ def __init__(self, **kwargs):
         self._unknown_boxes = QueueSP()
         self.statistics = SearchStatistics()
         if self.config.substitute_subformulas and self.config.simplify_query:
-            self._formula_stack.substitutions = self.problem._encodings[
+            self._formula_stack._substitutions = self.problem._encodings[
                 self.schedule
             ]._encoder.substitutions(self.schedule)
 
@@ -941,7 +941,7 @@ def _expand(
             )
 
             with my_solver() as solver:
-                episode._formula_stack.solver = solver
+                episode._formula_stack._solver = solver
                 l.info(f"{process_name} entering process loop")
                 # print("Starting initializing dynamics of model")
                 # self._initialize_encoding(solver, episode, [0])