version, and naming clashes

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.5.2"
+__version__ = "1.8.0"

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.7.0"
+__version__ = "1.8.0"

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.7.0"
+__version__ = "1.8.0"

auxiliary_packages/funman_dreal/test/test_chime_bilayer_solve.py

@@ -30,7 +30,7 @@
 from pysmt.typing import BOOL, INT, REAL
 
 from funman import Funman
-from funman.model import Model, ModelParameter, QueryLE
+from funman.model import FunmanModel, ModelParameter, QueryLE
 from funman.representation.representation import (
     Point,
     ResultCombinedHandler,

auxiliary_packages/pde2petri/src/pde2petri/_version.py

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

docs/source/conf.py

@@ -7,7 +7,7 @@
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information
 
 project = "funman"
-copyright = "2023, SIFT"
+copyright = "2024, SIFT"
 author = "SIFT"
 
 from funman import __version__

docs/source/index.rst

@@ -11,7 +11,6 @@ Welcome to funman's documentation!
    :caption: Contents:
 
    use_cases
-   sw_use_cases
    classes
    packages
    funman

docs/source/use_cases.rst

@@ -291,3 +291,23 @@ query.
     infected_threshold = 130
     assert compare_against_CHIME_bilayer(bilayer_file, infected_threshold)
 
+Climate Use Cases
+======================
+
+.. _pde as petri: https://github.com/ml4ai/funman/tree/main/notebooks/pde_as_petrinet.ipynb
+.. _pde to petri translation: https://github.com/ml4ai/funman/tree/main/auxiliary_packages/pde2petri/doc/discretization/main.pdf
+.. _advection: https://www.uni-muenster.de/imperia/md/content/physik_tp/lectures/ws2016-2017/num_methods_i/advection.pdf
+
+We developed use cases for climate models by translating the climate models into petri nets.  The use cases involve both consistency and parameter synthesis problems.  The notebook `pde to petri`_ demonstrates scenarios for the Halfar ice dome and advection models.  The methodology for translating the PDE models into petri nets is described in the `pde to petri translation`_ documentation.
+
+Identify Parameters for Halfar Ice Model
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+We developed two formulations of the Halfar Ice dome model that used one-sided or centered differential expressions to compare alternative discretization strategies.  We found that the centered differential expressions are able to model the ice dome change symmetrically and the one-sided differentials led to asymmetric change.  This motivates the use of FUNMAN to investigate the stability of different discretization schemes.  
+
+Compare Discretization Methods for PDEs with the Advection Model
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+In the case of the Advection Equation, we are able to observe phenomena that is expected from the literature [`advection`_]. For example, for the equation ∂h/∂t + a * ∂h/∂x = 0 where a > 0, we expect different results depending on the choice of discretization.  Since both the solution and stability behavior is known, our next steps will be to validate FUNMAN’s parameter synthesis by comparing FUNMAN’s calculated valid parameter ranges for the advection equation to what is known in the literature in the forward, centered, and backward difference scheme cases.  FUNMAN was able discover how the forward difference scheme violates the non-negativity constraints we placed upon the model, and that the backward scheme does not.  
+
+The following figure (gif) animates a time series computed by FUNMAN for the two dimensional advection equation where the boundary condition is zero for all locations and times.  The initial state models  a dome-like energy variable “a” over a 5x5 grid.  FUNMAN identifies a parameter value “u” that satisfies several constraints. The constraints are that “u” is in [0.5, 1], and that “a” is non-negative for all time steps and locations.  FUNMAN solves this problem with a petri net encoding of the discretized PDE, using a backward derivative for the spatial dimensions and a forward derivative for the temporal dimension.  The solution animated below assigns u = 0.5 and corresponds to a positive velocity that moves the energy in the positive direction in each dimension and diffusion.  The AMR for this instance is available through the ASKEM Model-Representation repo. 

notebooks/pde_as_petrinet.ipynb

@@ -2,7 +2,7 @@
  "cells": [
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 1,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -4337,18 +4337,22 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [
     {
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "2024-01-25 14:52:43,105 - funman.server.worker - INFO - FunmanWorker running...\n",
-      "[1.00000, 1.00000) has equal lower and upper bounds, so assuming the upper bound is closed.  (I.e., [lb, ub) is actually [lb, ub])\n",
-      "2024-01-25 14:52:43,110 - funman.server.worker - INFO - Starting work on: c6292c45-449a-4496-a514-676c772218af\n",
-      "2024-01-25 14:52:43,112 - funman.scenario.scenario - WARNING - Warning: The scenario is not normalized!\n",
-      "2024-01-25 14:52:45,118 - funman.api.run - INFO - Dumping results to ./out/c6292c45-449a-4496-a514-676c772218af.json\n"
+      "[1.00000, 1.00000) has equal lower and upper bounds, so assuming the upper bound is closed.  (I.e., [lb, ub) is actually [lb, ub])\n"
+     ]
+    },
+    {
+     "name": "stderr",
+     "output_type": "stream",
+     "text": [
+      "2024-01-29 19:34:29,108 - funman.scenario.scenario - WARNING - Warning: The scenario is not normalized!\n",
+      "2024-01-29 19:34:31,116 - funman.api.run - INFO - Dumping results to ./out/99a31f47-d7a4-4579-93f9-4f02eaf6e8f9.json\n"
      ]
     }
    ],

src/funman/_version.py

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

src/funman/api/run.py

@@ -15,7 +15,7 @@
 from funman.api.settings import Settings
 from funman.model.generated_models.petrinet import Model as GeneratedPetriNet
 from funman.model.generated_models.regnet import Model as GeneratedRegnet
-from funman.model.model import Model, _wrap_with_internal_model
+from funman.model.model import FunmanModel, _wrap_with_internal_model
 from funman.server.query import (
     FunmanResults,
     FunmanWorkRequest,
@@ -150,7 +150,7 @@ def elapsed_timer(self):
 
     def run(
         self,
-        model: Union[str, funman.Model, Dict],
+        model: Union[str, funman.FunmanModel, Dict],
         request: Union[str, FunmanWorkRequest, Dict],
         description: str = "",
         case_out_dir: str = ".",
@@ -164,7 +164,7 @@ def run(
 
         Parameters
         ----------
-        model : Union[str, Model, Dict]
+        model : Union[str, GeneratedPetriNet, GeneratedRegNet, Dict]
             Model to analyze
         request : Union[str, FunmanWorkRequest, Dict]
             Request to configure analysis

src/funman/model/__init__.py

@@ -24,4 +24,5 @@
 from .petrinet import *
 from .ensemble import *
 from .regnet import *
-from .generated_models import *
+
+# from .generated_models import *

src/funman/model/bilayer.py

@@ -5,7 +5,7 @@
 from pydantic import BaseModel, ConfigDict
 
 from funman.config import FUNMANConfig
-from funman.model import Model
+from funman.model import FunmanModel
 from funman.representation import Interval
 from funman.representation.parameter import ModelParameter
 
@@ -430,7 +430,7 @@ def to_dot(self, values={}):
         return dot
 
 
-class BilayerModel(Model):
+class BilayerModel(FunmanModel):
     """
     A BilayerModel is a complete specification of a Model that uses a BilayerDynamics graph to represent dynamics. It includes the attributes:
 

src/funman/model/decapode.py

@@ -2,14 +2,14 @@
 
 from pydantic import BaseModel
 
-from .model import Model
+from .model import FunmanModel
 
 
 class DecapodeDynamics(BaseModel):
     json_graph: Dict[str, List[Dict[str, Union[int, str]]]]
 
 
-class DecapodeModel(Model):
+class DecapodeModel(FunmanModel):
     decapode: DecapodeDynamics
 
     def default_encoder(

src/funman/model/encoded.py

@@ -4,11 +4,11 @@
 from pysmt.formula import FNode
 from pysmt.shortcuts import TRUE
 
-from funman.model import Model
+from funman.model.model import FunmanModel
 from funman.representation.parameter import ModelParameter
 
 
-class EncodedModel(Model):
+class EncodedModel(FunmanModel):
     """
     Model that holds an SMT formula encoding a model.  This class is meant to wrap hand-coded SMT formulas.
     """

src/funman/model/ensemble.py

@@ -7,14 +7,14 @@
 from funman.representation.interval import Interval
 from funman.representation.parameter import ModelParameter
 
-from .model import Model
+from .model import FunmanModel
 
 
-class EnsembleModel(Model):
-    models: List[Model]
-    _model_name_map: Dict[str, Model] = None
-    _var_name_map: Dict[str, Tuple[str, Model]] = None
-    _parameter_name_map: Dict[str, Tuple[str, Model]] = None
+class EnsembleModel(FunmanModel):
+    models: List[FunmanModel]
+    _model_name_map: Dict[str, FunmanModel] = None
+    _var_name_map: Dict[str, Tuple[str, FunmanModel]] = None
+    _parameter_name_map: Dict[str, Tuple[str, FunmanModel]] = None
     _parameter_map: Dict[str, ModelParameter] = None
     model_config = ConfigDict()
 

src/funman/model/gromet.py

@@ -4,10 +4,10 @@
 from automates.model_assembly.gromet.model import GrometFNModule
 from automates.program_analysis.JSON2GroMEt.json2gromet import json_to_gromet
 
-from funman.model import Model
+from funman.model import FunmanModel
 
 
-class GrometModel(Model):
+class GrometModel(FunmanModel):
     """
     The GrometModel class is a representation of an executable Gromet model.
     """

src/funman/model/model.py

@@ -49,7 +49,7 @@ def _wrap_with_internal_model(
         return model
 
 
-class Model(ABC, BaseModel):
+class FunmanModel(ABC, BaseModel):
     """
     The abstract base class for Models.
     """

src/funman/model/petrinet.py

@@ -10,10 +10,10 @@
 from ..representation.interval import Interval
 from .generated_models.petrinet import Model as GeneratedPetrinet
 from .generated_models.petrinet import State, Transition
-from .model import Model
+from .model import FunmanModel
 
 
-class AbstractPetriNetModel(Model):
+class AbstractPetriNetModel(FunmanModel):
     def _num_flow_from_state_to_transition(
         self, state_id: Union[str, int], transition_id: Union[str, int]
     ) -> int:
@@ -226,7 +226,7 @@ def _symbols(self):
     def _get_init_value(
         self, var: str, scenario: "AnalysisScenario", config: "FUNMANConfig"
     ):
-        value = Model._get_init_value(self, var, scenario, config)
+        value = FunmanModel._get_init_value(self, var, scenario, config)
         if value is None:
             if hasattr(self.petrinet.semantics, "ode"):
                 initials = self.petrinet.semantics.ode.initials

src/funman/model/query.py

@@ -6,7 +6,7 @@
 from pydantic import BaseModel, ConfigDict
 from pysmt.formula import FNode
 
-from funman.model.model import Model
+from funman.model.model import FunmanModel
 from funman.representation.symbol import ModelSymbol
 
 
@@ -15,7 +15,7 @@ class Query(BaseModel):
     Abstract base class for queries.
     """
 
-    model: Optional[Model] = None
+    model: Optional[FunmanModel] = None
 
     def __str__(self) -> str:
         return self.__class__.__name__

src/funman/model/regnet.py

@@ -7,10 +7,10 @@
 from .generated_models.regnet import Model as GeneratedRegnet
 from .generated_models.regnet import Parameter as GeneratedRegnetParameter
 from .generated_models.regnet import Vertice as GeneratedRegnetVertice
-from .model import Model
+from .model import FunmanModel
 
 
-class AbstractRegnetModel(Model):
+class AbstractRegnetModel(FunmanModel):
     def default_encoder(
         self, config: "FUNMANConfig", scenario: "AnalysisScenario"
     ) -> "Encoder":
@@ -104,7 +104,7 @@ def _transition_rate_constant(self, transitition: GeneratedRegnetEdge):
     def _get_init_value(
         self, var: str, scenario: "AnalysisScenario", config: "FUNMANConfig"
     ):
-        value = Model._get_init_value(self, var, scenario, config)
+        value = FunmanModel._get_init_value(self, var, scenario, config)
         if value is None:
             state_var = next(s for s in self._state_vars() if s.id == var)
             value = state_var.initial
@@ -121,7 +121,7 @@ class RegnetModel(AbstractRegnetModel):
     def _get_init_value(
         self, var: str, scenario: "AnalysisScenario", config: "FUNMANConfig"
     ):
-        value = Model._get_init_value(self, var, scenario, config)
+        value = FunmanModel._get_init_value(self, var, scenario, config)
         if value is None:
             state_var = next(s for s in self._state_vars() if s["id"] == var)
             if "initial" in state_var:

src/funman/model/simulator.py

@@ -3,10 +3,10 @@
 """
 
 
-from funman.model.model import Model
+from funman.model.model import FunmanModel
 
 
-class SimulatorModel(Model):
+class SimulatorModel(FunmanModel):
     main_fn: str = ""
 
     def default_encoder(self) -> "Encoder":

src/funman/representation/constraint.py

@@ -9,7 +9,7 @@
 )
 from typing_extensions import Annotated
 
-from funman.model import Model
+from funman.model import FunmanModel
 from funman.model.query import Query
 
 from .interval import Interval
@@ -52,7 +52,7 @@ def time_dependent(self) -> bool:
 
 class ModelConstraint(Constraint):
     soft: bool = False
-    model: Model
+    model: FunmanModel
 
     model_config = ConfigDict(extra="forbid")
 

src/funman/server/worker.py

@@ -7,7 +7,7 @@
 from enum import Enum
 from typing import Optional
 
-from funman.model.model import Model
+from funman.model.model import FunmanModel
 from funman.scenario.scenario import AnalysisScenario
 from funman.server.exception import FunmanWorkerException
 from funman.server.query import (
@@ -73,7 +73,7 @@ def in_state(self, state: WorkerState) -> bool:
             return self._state == state
 
     def enqueue_work(
-        self, model: Model, request: FunmanWorkRequest
+        self, model: FunmanModel, request: FunmanWorkRequest
     ) -> FunmanWorkUnit:
         if not self.in_state(WorkerState.RUNNING):
             raise FunmanWorkerException(

src/funman/translate/bilayer.py

@@ -31,7 +31,7 @@
     BilayerNode,
     BilayerStateNode,
 )
-from funman.model.model import Model
+from funman.model.model import FunmanModel
 from funman.translate import Encoder, Encoding
 from funman.translate.simplifier import FUNMANSimplifier
 from funman.utils.sympy_utils import to_sympy
@@ -113,14 +113,16 @@ def _encode_untimed_constraints(
             And(untimed_constraints).simplify(), super_untimed_constraints
         )
 
-    def _get_timed_symbols(self, model: Model) -> Set[str]:
+    def _get_timed_symbols(self, model: FunmanModel) -> Set[str]:
         timed_symbols = set([])
         # All state nodes correspond to timed symbols
         for idx, node in model.bilayer._state.items():
             timed_symbols.add(node.parameter)
         return timed_symbols
 
-    def encode_model(self, model: Model, time_dependent_parameters=False):
+    def encode_model(
+        self, model: FunmanModel, time_dependent_parameters=False
+    ):
         """
         Encode the model as an SMTLib formula.