From 4407efe514ce6381e3762270a1becc2931e468cc Mon Sep 17 00:00:00 2001 From: Daniel Bryce Date: Fri, 27 Oct 2023 22:46:06 +0000 Subject: [PATCH] update docs --- README.md | 23 ++++++++++++++---- docs/source/conf.py | 1 + docs/source/index.rst | 5 ++++ requirements-dev.txt | 1 + src/funman/representation/box.py | 2 +- src/funman/search/box_search.py | 40 ++++++++++++++++---------------- 6 files changed, 47 insertions(+), 25 deletions(-) diff --git a/README.md b/README.md index 9ab86f79..c79e7cd5 100644 --- a/README.md +++ b/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**: diff --git a/docs/source/conf.py b/docs/source/conf.py index 5c666bdd..83f68892 100644 --- a/docs/source/conf.py +++ b/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 diff --git a/docs/source/index.rst b/docs/source/index.rst index 5c8cf2ba..c681f3d5 100644 --- a/docs/source/index.rst +++ b/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 ================== diff --git a/requirements-dev.txt b/requirements-dev.txt index d165c18f..1fa27886 100644 --- a/requirements-dev.txt +++ b/requirements-dev.txt @@ -6,4 +6,5 @@ pycln pytest-cov twine autodoc_pydantic +myst-parser parameterized \ No newline at end of file diff --git a/src/funman/representation/box.py b/src/funman/representation/box.py index 61491234..d975944a 100644 --- a/src/funman/representation/box.py +++ b/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 diff --git a/src/funman/search/box_search.py b/src/funman/search/box_search.py index 116cc01e..b872e461 100644 --- a/src/funman/search/box_search.py +++ b/src/funman/search/box_search.py @@ -42,8 +42,8 @@ class FormulaStackFrame(BaseModel): - formulas: List[FNode] = [] - simplified_formulas: List[FNode] = [] + _formulas: List[FNode] = [] + _simplified_formulas: List[FNode] = [] model_config = ConfigDict( arbitrary_types_allowed=True, @@ -51,9 +51,9 @@ class FormulaStackFrame(BaseModel): 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,7 +79,7 @@ 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 @@ -87,7 +87,7 @@ 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])