funman package

Subpackages

Submodules

funman.config module

Inheritance diagram of funman.config

This module defines the Funman class, the primary entry point for FUNMAN analysis.

pydantic model funman.config.FUNMANConfig

Bases: BaseModel

Base definition of a configuration object

Show JSON schema
{
   "title": "FUNMANConfig",
   "description": "Base definition of a configuration object",
   "type": "object",
   "properties": {
      "tolerance": {
         "default": 0.001,
         "title": "Tolerance",
         "type": "number"
      },
      "queue_timeout": {
         "default": 1,
         "title": "Queue Timeout",
         "type": "integer"
      },
      "number_of_processes": {
         "default": 1,
         "title": "Number Of Processes",
         "type": "integer"
      },
      "wait_timeout": {
         "anyOf": [
            {
               "type": "integer"
            },
            {
               "type": "null"
            }
         ],
         "default": null,
         "title": "Wait Timeout"
      },
      "wait_action_timeout": {
         "default": 0.05,
         "title": "Wait Action Timeout",
         "type": "number"
      },
      "solver": {
         "default": "dreal",
         "title": "Solver",
         "type": "string"
      },
      "num_steps": {
         "default": 2,
         "title": "Num Steps",
         "type": "integer"
      },
      "step_size": {
         "default": 1,
         "title": "Step Size",
         "type": "integer"
      },
      "num_initial_boxes": {
         "default": 1,
         "title": "Num Initial Boxes",
         "type": "integer"
      },
      "solver_timeout": {
         "anyOf": [
            {
               "type": "integer"
            },
            {
               "type": "null"
            }
         ],
         "default": null,
         "title": "Solver Timeout"
      },
      "initial_state_tolerance": {
         "default": 0.0,
         "title": "Initial State Tolerance",
         "type": "number"
      },
      "save_smtlib": {
         "anyOf": [
            {
               "type": "string"
            },
            {
               "type": "null"
            }
         ],
         "default": null,
         "title": "Save Smtlib"
      },
      "dreal_precision": {
         "default": 0.1,
         "title": "Dreal Precision",
         "type": "number"
      },
      "dreal_log_level": {
         "default": "off",
         "title": "Dreal Log Level",
         "type": "string"
      },
      "constraint_noise": {
         "default": 0.0,
         "title": "Constraint Noise",
         "type": "number"
      },
      "dreal_mcts": {
         "default": true,
         "title": "Dreal Mcts",
         "type": "boolean"
      },
      "substitute_subformulas": {
         "default": false,
         "title": "Substitute Subformulas",
         "type": "boolean"
      },
      "normalization_constant": {
         "anyOf": [
            {
               "type": "number"
            },
            {
               "type": "null"
            }
         ],
         "default": null,
         "title": "Normalization Constant"
      },
      "use_compartmental_constraints": {
         "default": false,
         "title": "Use Compartmental Constraints",
         "type": "boolean"
      },
      "compartmental_constraint_noise": {
         "default": 0.01,
         "title": "Compartmental Constraint Noise",
         "type": "number"
      },
      "normalize": {
         "default": false,
         "title": "Normalize",
         "type": "boolean"
      },
      "simplify_query": {
         "default": false,
         "title": "Simplify Query",
         "type": "boolean"
      },
      "series_approximation_threshold": {
         "anyOf": [
            {
               "type": "number"
            },
            {
               "type": "null"
            }
         ],
         "default": null,
         "title": "Series Approximation Threshold"
      },
      "profile": {
         "default": false,
         "title": "Profile",
         "type": "boolean"
      },
      "taylor_series_order": {
         "anyOf": [
            {
               "type": "integer"
            },
            {
               "type": "null"
            }
         ],
         "default": null,
         "title": "Taylor Series Order"
      },
      "corner_points": {
         "default": false,
         "title": "Corner Points",
         "type": "boolean"
      },
      "verbosity": {
         "default": 40,
         "title": "Verbosity",
         "type": "integer"
      },
      "use_transition_symbols": {
         "default": false,
         "title": "Use Transition Symbols",
         "type": "boolean"
      },
      "uniform_box_splits": {
         "default": false,
         "title": "Uniform Box Splits",
         "type": "boolean"
      },
      "dreal_prefer_parameters": {
         "default": [],
         "items": {
            "type": "string"
         },
         "title": "Dreal Prefer Parameters",
         "type": "array"
      },
      "point_based_evaluation": {
         "default": false,
         "title": "Point Based Evaluation",
         "type": "boolean"
      },
      "prioritize_box_entropy": {
         "default": true,
         "title": "Prioritize Box Entropy",
         "type": "boolean"
      },
      "mode": {
         "default": "mode_smt",
         "enum": [
            "mode_smt",
            "mode_odeint"
         ],
         "title": "Mode",
         "type": "string"
      },
      "random_seed": {
         "default": 0,
         "title": "Random Seed",
         "type": "integer"
      }
   }
}

Config:

  • arbitrary_types_allowed: bool = True

  • validate_default: bool = True

Fields:
Validators:
field compartmental_constraint_noise: float = 0.01

Additional factor used to relax compartmental constraint (needed due to floating point imprecision)

Validated by:
field constraint_noise: float = 0.0

Use MCTS in dreal

Validated by:
field corner_points: bool = False

Compute Corner points of each box

Validated by:
field dreal_log_level: str = 'off'

Constraint noise term to relax constraints

Validated by:
field dreal_mcts: bool = True

Substitute subformulas to simplify overall encoding

Validated by:
field dreal_precision: float = 0.1

Precision delta for dreal solver

Validated by:
field dreal_prefer_parameters: List[str] = []

Prefer to split the listed parameters in dreal

Validated by:
field initial_state_tolerance: float = 0.0

Factor used to relax initial state values bounds

Validated by:
field mode: Literal['mode_smt', 'mode_odeint'] = 'mode_smt'

Mode to run FUNMAN, either funman.constants.MODE_ODEINT or funman.constants.MODE_SMT

Validated by:
field normalization_constant: float | None = None

Simplify query by propagating substutions

Validated by:
field normalize: bool = False

Normalization constant to use for normalization (attempt to compute if None)

Validated by:
field num_initial_boxes: int = 1

Number of initial boxes for BoxSearch

Validated by:
field num_steps: int = 2

Number of timesteps to encode

Validated by:
field number_of_processes: int = 1

Number of BoxSearch processes

Validated by:
field point_based_evaluation: bool = False

Evaluate parameters using point-based simulation over interval-based SMT encoding

Validated by:
field prioritize_box_entropy: bool = True

When comparing boxes, prefer those with low entropy

Validated by:
field profile: bool = False

Generate profiling output

Validated by:
field queue_timeout: int = 1

Multiprocessing queue timeout, used by BoxSearch

Validated by:
field random_seed: int = 0

Random seed

Validated by:
field save_smtlib: str | None = None

Whether to save each smt invocation as an SMTLib file

Validated by:
field series_approximation_threshold: float | None = None

Series approximation threshold for dropping series terms

Validated by:
field simplify_query: bool = False

Convert query object to a single formula based only on the parameters (deprecated)

Validated by:
field solver: str = 'dreal'

Name of pysmt solver to use

Validated by:
field solver_timeout: int | None = None

Number of seconds to allow each call to SMT solver

Validated by:
field step_size: int = 1

Step size for encoding

Validated by:
field substitute_subformulas: bool = False

Enforce compartmental variable constraints

Validated by:
field taylor_series_order: int | None = None

Use Taylor series of given order to approximate transition function, if None, then do not compute series

Validated by:
field tolerance: float = 0.001

Algorithm-specific tolerance for approximation, used by BoxSearch

Validated by:
field uniform_box_splits: bool = False

Uniformly split boxes in box search, instead of separating points in boxes

Validated by:
field use_compartmental_constraints: bool = False

Normalize scenarios prior to solving

Validated by:
field use_transition_symbols: bool = False

Use transition symbols in encoding transition functions

Validated by:
field verbosity: int = 40

Verbosity (INFO, DEBUG, TRACE, WARN, ERROR)

Validated by:
field wait_action_timeout: float = 0.05

Time to sleep proceses waiting for work

Validated by:
field wait_timeout: int | None = None

Timeout for BoxSearch procesess to wait for boxes to evaluate

Validated by:
validator check_use_compartmental_constraints  »  all fields
validator import_dreal  »  solver
model_post_init(context: Any, /) → None

This function is meant to behave like a BaseModel method to initialise private attributes.

It takes context as an argument since that’s what pydantic-core passes when calling it.

Parameters:

  • self – The BaseModel instance.

  • context – The context.

funman.constants module

This module contains defintions of constants used within FUNMAN

funman.funman module

Inheritance diagram of funman.funman

This module defines the Funman class, the primary entry point for FUNMAN analysis.

class funman.funman.Funman

Bases: object

The Funman FUNctional Model ANalysis class is the main entry point for performing analysis on models. The main entry point Funman.solve() performs analysis of an funman.scenario.AnalysisScenario, subject to a set of configuration options in the funman.search.SearchConfig class.

solve(problem: AnalysisScenario, config: FUNMANConfig = None, haltEvent: Event | None = None, resultsCallback: Callable[[ParameterSpace], None] | None = None) → AnalysisScenarioResult

This method is the main entry point for Funman analysis. Its inputs describe an AnalysisScenario and SearchConfig that setup the problem and analysis technique. The return value is an AnalysisScenarioResult, which comprises all relevant output pertaining to the AnalysisScenario.

Parameters:

  • problem (AnalysisScenario) – The problem is a description of the analysis to be performed, and typically describes a Model and a Query.

  • config (SearchConfig, optional) – The configuration for the search algorithm applied to analyze the problem, by default SearchConfig()

Returns:

The resulting data, statistics, and other relevant information produced by the analysis.

Return type:

AnalysisScenarioResult

Module contents

The funman package implements multiple simulator model analysis methods. Current methods include:

  • Simulation: running original simulator and querying the results.

  • Parameter Synthesis: Generating feasible values for model parameters.

  • Consistency: Check that a parameterized model is self-consistent.