funman.search package¶
Submodules¶
funman.search.box_search module¶
This module defines the BoxSearch class and supporting classes.
- class funman.search.box_search.BoxSearch¶
Bases:
Search
Box search algorithm.
- search(problem: AnalysisScenario, config: FUNMANConfig, haltEvent: Event | None = None, resultsCallback: Callable[[ParameterSpace], None] | None = None) ParameterSpace ¶
The BoxSearch.search() creates a BoxSearchEpisode object that stores the search progress. This method is the entry point to the search that spawns several processes to parallelize the evaluation of boxes in the BoxSearch.expand() method. It treats the zeroth process as a special process that is allowed to initialize the search and plot the progress of the search.
- Parameters:
problem (ParameterSynthesisScenario) – Model and parameters to synthesize
config (SearchConfig, optional) – BoxSearch configuration, by default SearchConfig()
- Returns:
Final search results (parameter space) and statistics.
- Return type:
- store_smtlib(episode, box, filename='dbg')¶
- pydantic model funman.search.box_search.BoxSearchEpisode¶
Bases:
SearchEpisode
A BoxSearchEpisode stores the data required to organize a BoxSearch, including intermediate data and results. It takes as input:
config: a SearchConfig object that defines the configuration
problem: a ParameterSynthesisScenario to solve
manager: a SyncManager for coordinating multiple search processes that is used to declare several shared data
A BoxSearchEpisode mainly tracks the true, false, and unknown boxes generated by the BoxSearch, along with statistics on the search.
Show JSON schema
{ "title": "BoxSearchEpisode", "description": "A BoxSearchEpisode stores the data required to organize a BoxSearch, including intermediate data and results. It takes as input:\n\n* config: a SearchConfig object that defines the configuration\n\n* problem: a ParameterSynthesisScenario to solve\n\n* manager: a SyncManager for coordinating multiple search processes that is used to declare several shared data\n\nA BoxSearchEpisode mainly tracks the true, false, and unknown boxes generated by the BoxSearch, along with statistics on the search.", "type": "object", "properties": { "schedule": { "$ref": "#/$defs/EncodingSchedule" }, "problem": { "$ref": "#/$defs/AnalysisScenario" }, "config": { "$ref": "#/$defs/FUNMANConfig" }, "statistics": { "$ref": "#/$defs/SearchStatistics", "default": null } }, "$defs": { "AnalysisScenario": { "additionalProperties": false, "description": "Abstract class for Analysis Scenarios.", "properties": { "parameters": { "items": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Parameter" }, { "$ref": "#/$defs/ModelParameter" }, { "$ref": "#/$defs/StructureParameter" } ] }, "title": "Parameters", "type": "array" }, "normalization_constant": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Normalization Constant" }, "constraints": { "anyOf": [ { "items": { "anyOf": [ { "$ref": "#/$defs/StateVariableConstraint" }, { "$ref": "#/$defs/LinearConstraint" } ] }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Constraints" }, "empty_volume_ok": { "default": false, "title": "Empty Volume Ok", "type": "boolean" }, "model": { "anyOf": [ { "$ref": "#/$defs/GeneratedPetriNetModel" }, { "$ref": "#/$defs/GeneratedRegnetModel" }, { "$ref": "#/$defs/RegnetModel" }, { "$ref": "#/$defs/PetrinetModel" }, { "$ref": "#/$defs/DecapodeModel" }, { "$ref": "#/$defs/BilayerModel" }, { "$ref": "#/$defs/EncodedModel" }, { "$ref": "#/$defs/EnsembleModel" } ], "title": "Model" }, "query": { "anyOf": [ { "$ref": "#/$defs/QueryAnd" }, { "$ref": "#/$defs/QueryGE" }, { "$ref": "#/$defs/QueryLE" }, { "$ref": "#/$defs/QueryEncoded" }, { "$ref": "#/$defs/QueryFunction" }, { "$ref": "#/$defs/QueryTrue" } ], "default": { "model": null }, "title": "Query" } }, "required": [ "parameters", "model" ], "title": "AnalysisScenario", "type": "object" }, "BaseProperties": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "rate_constant": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null } }, "title": "BaseProperties", "type": "object" }, "BilayerDynamics": { "description": "The BilayerDynamics class represents a state update (dynamics) model for a set of variables. The graph consists of:\n\n* state nodes (current state),\n\n* tangent nodes (next state), and\n\n* flux nodes (causal relationships).", "properties": { "json_graph": { "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "BilayerDynamics", "type": "object" }, "BilayerEdge": { "properties": { "src": { "$ref": "#/$defs/BilayerNode" }, "tgt": { "$ref": "#/$defs/BilayerNode" } }, "required": [ "src", "tgt" ], "title": "BilayerEdge", "type": "object" }, "BilayerFluxNode": { "description": "BilayerNode representing a flux.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerFluxNode", "type": "object" }, "BilayerMeasurement": { "description": "The BilayerMeasurement class represents measurements taken on the BilayerNode state nodes of a BilayerDynamics object. The graph consists of:\n\n* state nodes (current state),\n\n* observation nodes, and\n\n* flux nodes (causal relationships).", "properties": { "json_graph": { "title": "Json Graph", "type": "object" }, "state": { "additionalProperties": { "$ref": "#/$defs/BilayerStateNode" }, "default": {}, "title": "State", "type": "object" }, "flux": { "additionalProperties": { "$ref": "#/$defs/BilayerFluxNode" }, "default": {}, "title": "Flux", "type": "object" }, "observable": { "additionalProperties": { "$ref": "#/$defs/BilayerStateNode" }, "default": {}, "title": "Observable", "type": "object" }, "input_edges": { "$ref": "#/$defs/BilayerEdge", "default": [] }, "output_edges": { "$ref": "#/$defs/BilayerEdge", "default": [] } }, "required": [ "json_graph" ], "title": "BilayerMeasurement", "type": "object" }, "BilayerMetadata": { "description": "Metadata for a BilayerNode", "properties": { "ref": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Ref" }, "type": { "anyOf": [ { "enum": [ "float", "int" ], "type": "string" }, { "type": "null" } ], "default": null, "title": "Type" }, "initial_value": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Initial Value" }, "lb": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Lb" }, "ub": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Ub" } }, "title": "BilayerMetadata", "type": "object" }, "BilayerModel": { "description": "A BilayerModel is a complete specification of a Model that uses a BilayerDynamics graph to represent dynamics. It includes the attributes:\n\n* bilayer: the BilayerDynamics graph\n\n* measurements: the BilayerMeasurement graph (used to derive additional variables from the state nodes)\n\n* init_values: a dict mapping from state variables and flux parameters to initial value\n\n* identical_parameters: a list of lists of flux parameters that have identical values\n\n* parameter_bounds: a list of lower and upper bounds on parameters", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "bilayer": { "$ref": "#/$defs/BilayerDynamics" }, "measurements": { "$ref": "#/$defs/BilayerMeasurement", "default": null }, "identical_parameters": { "default": [], "items": { "items": { "type": "string" }, "type": "array" }, "title": "Identical Parameters", "type": "array" } }, "required": [ "bilayer" ], "title": "BilayerModel", "type": "object" }, "BilayerNode": { "description": "Node in a BilayerGraph.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerNode", "type": "object" }, "BilayerStateNode": { "description": "BilayerNode representing a state variable.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerStateNode", "type": "object" }, "DecapodeDynamics": { "properties": { "json_graph": { "additionalProperties": { "items": { "additionalProperties": { "anyOf": [ { "type": "integer" }, { "type": "string" } ] }, "type": "object" }, "type": "array" }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "DecapodeDynamics", "type": "object" }, "DecapodeModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "decapode": { "$ref": "#/$defs/DecapodeDynamics" } }, "required": [ "decapode" ], "title": "DecapodeModel", "type": "object" }, "Edge": { "properties": { "id": { "title": "Id", "type": "string" }, "sign": { "title": "Sign", "type": "boolean" }, "source": { "title": "Source", "type": "string" }, "target": { "title": "Target", "type": "string" }, "properties": { "anyOf": [ { "$ref": "#/$defs/BaseProperties" }, { "type": "null" } ], "default": null } }, "required": [ "id", "sign", "source", "target" ], "title": "Edge", "type": "object" }, "EncodedModel": { "description": "Model that holds an SMT formula encoding a model. This class is meant to wrap hand-coded SMT formulas.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/ModelParameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" } }, "title": "EncodedModel", "type": "object" }, "EncodingSchedule": { "properties": { "timepoints": { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "title": "Timepoints", "type": "array" } }, "required": [ "timepoints" ], "title": "EncodingSchedule", "type": "object" }, "EnsembleModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "models": { "items": { "$ref": "#/$defs/FunmanModel" }, "title": "Models", "type": "array" } }, "required": [ "models" ], "title": "EnsembleModel", "type": "object" }, "FUNMANConfig": { "description": "Base definition of a configuration 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" } }, "title": "FUNMANConfig", "type": "object" }, "FunmanModel": { "description": "The abstract base class for Models.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" } }, "title": "FunmanModel", "type": "object" }, "GeneratedPetriNetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "petrinet": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model" } }, "required": [ "petrinet" ], "title": "GeneratedPetriNetModel", "type": "object" }, "GeneratedRegnetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "regnet": { "$ref": "#/$defs/funman__model__generated_models__regnet__Model" } }, "required": [ "regnet" ], "title": "GeneratedRegnetModel", "type": "object" }, "Header": { "properties": { "name": { "title": "Name", "type": "string" }, "schema": { "format": "uri", "minLength": 1, "title": "Schema", "type": "string" }, "schema_name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Schema Name" }, "description": { "title": "Description", "type": "string" }, "model_version": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Model Version" } }, "required": [ "name", "schema", "description" ], "title": "Header", "type": "object" }, "Initial": { "properties": { "target": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Target" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Initial", "type": "object" }, "Interval": { "description": "An interval is a pair [lb, ub) that is open (i.e., an interval specifies all points x where lb <= x and ub < x).", "properties": { "lb": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": -1.7976931348623157e+308, "title": "Lb" }, "ub": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": 1.7976931348623157e+308, "title": "Ub" }, "closed_upper_bound": { "default": false, "title": "Closed Upper Bound", "type": "boolean" }, "original_width": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Original Width" }, "normalized": { "default": false, "title": "Normalized", "type": "boolean" }, "unnormalized_lb": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Unnormalized Lb" }, "unnormalized_ub": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Unnormalized Ub" } }, "title": "Interval", "type": "object" }, "LinearConstraint": { "additionalProperties": false, "properties": { "soft": { "default": true, "title": "Soft", "type": "boolean" }, "name": { "title": "Name", "type": "string" }, "timepoints": { "anyOf": [ { "$ref": "#/$defs/Interval" }, { "type": "null" } ], "default": null }, "additive_bounds": { "$ref": "#/$defs/Interval" }, "variables": { "items": { "type": "string" }, "title": "Variables", "type": "array" }, "weights": { "anyOf": [ { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Weights" }, "derivative": { "default": false, "title": "Derivative", "type": "boolean" } }, "required": [ "name", "additive_bounds", "variables" ], "title": "LinearConstraint", "type": "object" }, "ModelParameter": { "additionalProperties": false, "description": "A parameter is a free variable for a Model. It has the following attributes:\n\n* lb: lower bound\n\n* ub: upper bound\n\n* symbol: a pysmt FNode corresponding to the parameter variable", "properties": { "name": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Name" }, "interval": { "$ref": "#/$defs/Interval", "default": { "lb": -1.7976931348623157e+308, "ub": 1.7976931348623157e+308, "closed_upper_bound": false, "original_width": Infinity, "normalized": false, "unnormalized_lb": null, "unnormalized_ub": null } }, "label": { "default": "any", "enum": [ "any", "all" ], "title": "Label", "type": "string" } }, "required": [ "name" ], "title": "ModelParameter", "type": "object" }, "ModelSymbol": { "properties": { "name": { "title": "Name", "type": "string" }, "model": { "title": "Model", "type": "string" } }, "required": [ "name", "model" ], "title": "ModelSymbol", "type": "object" }, "Observable": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "required": [ "id" ], "title": "Observable", "type": "object" }, "OdeSemantics": { "properties": { "rates": { "anyOf": [ { "items": { "$ref": "#/$defs/Rate" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Rates" }, "initials": { "anyOf": [ { "items": { "$ref": "#/$defs/Initial" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Initials" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Parameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" }, "observables": { "anyOf": [ { "items": { "$ref": "#/$defs/Observable" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Observables" }, "time": { "anyOf": [ { "$ref": "#/$defs/Time" }, { "type": "null" } ], "default": null } }, "title": "OdeSemantics", "type": "object" }, "ParamOrNumber": { "anyOf": [ { "type": "number" }, { "type": "string" } ], "title": "ParamOrNumber" }, "PetrinetDynamics": { "properties": { "json_graph": { "additionalProperties": { "items": { "additionalProperties": { "anyOf": [ { "additionalProperties": { "anyOf": [ { "type": "string" }, { "type": "boolean" }, { "type": "number" }, { "type": "null" } ] }, "type": "object" }, { "type": "integer" }, { "type": "string" }, { "type": "number" }, { "type": "null" } ] }, "type": "object" }, "type": "array" }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "PetrinetDynamics", "type": "object" }, "PetrinetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "petrinet": { "$ref": "#/$defs/PetrinetDynamics" } }, "required": [ "petrinet" ], "title": "PetrinetModel", "type": "object" }, "Properties": { "additionalProperties": true, "properties": { "name": { "title": "Name", "type": "string" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null } }, "required": [ "name" ], "title": "Properties", "type": "object" }, "Query": { "description": "Abstract base class for queries.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "Query", "type": "object" }, "QueryAnd": { "description": "Conjunction of queries.\n\nParameters\n----------\nqueries : List[Query]\n queries to conjoin.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "queries": { "items": { "anyOf": [ { "$ref": "#/$defs/QueryLE" }, { "$ref": "#/$defs/QueryGE" }, { "$ref": "#/$defs/QueryEquals" }, { "$ref": "#/$defs/Query" } ] }, "title": "Queries", "type": "array" } }, "required": [ "queries" ], "title": "QueryAnd", "type": "object" }, "QueryEncoded": { "description": "Class to contain a formula that is already encoded by a pysmt FNode.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "QueryEncoded", "type": "object" }, "QueryEquals": { "description": "Class to represent a query of the form: var == value, where var is a variable, and value is a constant.\n\nParameters\n----------\nvariable : str\n model variable name\nvalue : float\n value\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "value": { "title": "Value", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "value" ], "title": "QueryEquals", "type": "object" }, "QueryFunction": { "description": "This query uses a Python function passed to the constructor to evaluate a query on the results of a scenario.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "function": { "title": "Function", "type": "string" } }, "required": [ "function" ], "title": "QueryFunction", "type": "object" }, "QueryGE": { "description": "Class to represent a query of the form: var >= lb, where var is a variable, and lb is a constant lower bound.\n\nParameters\n----------\nvariable : str\n model variable name\nlb : float\n lower bound constant\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "lb": { "title": "Lb", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "lb" ], "title": "QueryGE", "type": "object" }, "QueryLE": { "description": "Class to represent a query of the form: var <= ub, where var is a variable, and ub is a constant upper bound.\n\nParameters\n----------\nvariable : str\n model variable name\nub : float\n upper bound constant\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "ub": { "title": "Ub", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "ub" ], "title": "QueryLE", "type": "object" }, "QueryTrue": { "additionalProperties": false, "description": "Query that represents logical true. I.e., this query does not place any additional constraints upon a model.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "QueryTrue", "type": "object" }, "Rate": { "properties": { "target": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Target" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Rate", "type": "object" }, "RegnetDynamics": { "properties": { "json_graph": { "additionalProperties": { "anyOf": [ { "type": "string" }, { "additionalProperties": { "items": { "type": "object" }, "type": "array" }, "type": "object" } ] }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "RegnetDynamics", "type": "object" }, "RegnetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "regnet": { "$ref": "#/$defs/RegnetDynamics" } }, "required": [ "regnet" ], "title": "RegnetModel", "type": "object" }, "SearchStatistics": { "properties": {}, "title": "SearchStatistics", "type": "object" }, "Semantics": { "properties": { "ode": { "anyOf": [ { "$ref": "#/$defs/OdeSemantics" }, { "type": "null" } ], "default": null }, "typing": { "anyOf": [ { "$ref": "#/$defs/TypingSemantics" }, { "type": "null" } ], "default": null, "description": "(Optional) Information for aligning models for stratification" }, "span": { "anyOf": [ { "items": { "$ref": "#/$defs/TypingSemantics" }, "type": "array" }, { "type": "null" } ], "default": null, "description": "(Optional) Legs of a span, each of which are a full ASKEM Petri Net", "title": "Span" } }, "title": "Semantics", "type": "object" }, "State": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "State", "type": "object" }, "StateVariableConstraint": { "additionalProperties": false, "properties": { "soft": { "default": true, "title": "Soft", "type": "boolean" }, "name": { "title": "Name", "type": "string" }, "timepoints": { "anyOf": [ { "$ref": "#/$defs/Interval" }, { "type": "null" } ], "default": null }, "variable": { "title": "Variable", "type": "string" }, "interval": { "$ref": "#/$defs/Interval", "default": null } }, "required": [ "name", "variable" ], "title": "StateVariableConstraint", "type": "object" }, "States": { "items": { "$ref": "#/$defs/State" }, "title": "States", "type": "array" }, "StructureParameter": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Name" }, "interval": { "$ref": "#/$defs/Interval", "default": { "lb": -1.7976931348623157e+308, "ub": 1.7976931348623157e+308, "closed_upper_bound": false, "original_width": Infinity, "normalized": false, "unnormalized_lb": null, "unnormalized_ub": null } }, "label": { "default": "any", "enum": [ "any", "all" ], "title": "Label", "type": "string" } }, "required": [ "name" ], "title": "StructureParameter", "type": "object" }, "Time": { "properties": { "id": { "title": "Id", "type": "string" }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Time", "type": "object" }, "Transition": { "properties": { "id": { "title": "Id", "type": "string" }, "input": { "items": { "type": "string" }, "title": "Input", "type": "array" }, "output": { "items": { "type": "string" }, "title": "Output", "type": "array" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "properties": { "anyOf": [ { "$ref": "#/$defs/Properties" }, { "type": "null" } ], "default": null } }, "required": [ "id", "input", "output" ], "title": "Transition", "type": "object" }, "Transitions": { "items": { "$ref": "#/$defs/Transition" }, "title": "Transitions", "type": "array" }, "TypingSemantics": { "properties": { "system": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model", "description": "A Petri net representing the 'type system' that is necessary to align states and transitions across different models during stratification." }, "map": { "description": "A map between the (state and transition) nodes of the model and the (state and transition) nodes of the type system", "items": { "items": { "type": "string" }, "type": "array" }, "title": "Map", "type": "array" } }, "required": [ "system", "map" ], "title": "TypingSemantics", "type": "object" }, "Unit": { "additionalProperties": true, "properties": { "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Unit", "type": "object" }, "Vertice": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "rate_constant": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null }, "id": { "title": "Id", "type": "string" }, "sign": { "title": "Sign", "type": "boolean" }, "initial": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null } }, "required": [ "id", "sign" ], "title": "Vertice", "type": "object" }, "funman__model__generated_models__petrinet__Distribution": { "additionalProperties": true, "properties": { "type": { "title": "Type", "type": "string" }, "parameters": { "title": "Parameters", "type": "object" } }, "required": [ "type", "parameters" ], "title": "Distribution", "type": "object" }, "funman__model__generated_models__petrinet__Grounding": { "additionalProperties": false, "properties": { "identifiers": { "title": "Identifiers", "type": "object" }, "modifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Modifiers" } }, "required": [ "identifiers" ], "title": "Grounding", "type": "object" }, "funman__model__generated_models__petrinet__Model": { "additionalProperties": true, "properties": { "header": { "$ref": "#/$defs/Header" }, "properties": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Properties" }, "model": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model1" }, "semantics": { "anyOf": [ { "$ref": "#/$defs/Semantics" }, { "type": "null" } ], "default": null, "description": "Information specific to a given semantics (e.g., ODEs) associated with a model." }, "metadata": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "description": "(Optional) Information not useful for execution of the model, but that may be useful to some consumer in the future. E.g. creation timestamp or source paper's author.", "title": "Metadata" } }, "required": [ "header", "model" ], "title": "Model", "type": "object" }, "funman__model__generated_models__petrinet__Model1": { "additionalProperties": false, "properties": { "states": { "$ref": "#/$defs/States" }, "transitions": { "$ref": "#/$defs/Transitions" } }, "required": [ "states", "transitions" ], "title": "Model1", "type": "object" }, "funman__model__generated_models__petrinet__Parameter": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "value": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Value" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "distribution": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Distribution" }, { "type": "null" } ], "default": null }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Parameter", "type": "object" }, "funman__model__generated_models__regnet__Distribution": { "properties": { "type": { "title": "Type", "type": "string" }, "parameters": { "title": "Parameters", "type": "object" } }, "required": [ "type", "parameters" ], "title": "Distribution", "type": "object" }, "funman__model__generated_models__regnet__Grounding": { "additionalProperties": false, "properties": { "identifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Identifiers" }, "modifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Modifiers" } }, "title": "Grounding", "type": "object" }, "funman__model__generated_models__regnet__Model": { "properties": { "header": { "$ref": "#/$defs/Header" }, "properties": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Properties" }, "model": { "$ref": "#/$defs/funman__model__generated_models__regnet__Model1" }, "metadata": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "description": "(Optional) Information not useful for execution of the model, but that may be useful to some consumer in the future. E.g. creation timestamp or source paper's author.", "title": "Metadata" } }, "required": [ "header", "model" ], "title": "Model", "type": "object" }, "funman__model__generated_models__regnet__Model1": { "additionalProperties": false, "properties": { "vertices": { "items": { "$ref": "#/$defs/Vertice" }, "title": "Vertices", "type": "array" }, "edges": { "items": { "$ref": "#/$defs/Edge" }, "title": "Edges", "type": "array" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/funman__model__generated_models__regnet__Parameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" } }, "required": [ "vertices", "edges" ], "title": "Model1", "type": "object" }, "funman__model__generated_models__regnet__Parameter": { "properties": { "id": { "title": "Id", "type": "string" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "value": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Value" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "distribution": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Distribution" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Parameter", "type": "object" } }, "required": [ "schedule", "problem", "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field schedule: EncodingSchedule [Required]¶
- field statistics: SearchStatistics = None¶
- model_post_init(context: Any, /) None ¶
We need to both initialize private attributes and call the user-defined model_post_init method.
- pydantic model funman.search.box_search.BoxSearchEpisodeMP¶
Bases:
BoxSearchEpisode
Show JSON schema
{ "title": "BoxSearchEpisodeMP", "type": "object", "properties": { "schedule": { "$ref": "#/$defs/EncodingSchedule" }, "problem": { "$ref": "#/$defs/AnalysisScenario" }, "config": { "$ref": "#/$defs/FUNMANConfig" }, "statistics": { "$ref": "#/$defs/SearchStaticsMP", "default": null } }, "$defs": { "AnalysisScenario": { "additionalProperties": false, "description": "Abstract class for Analysis Scenarios.", "properties": { "parameters": { "items": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Parameter" }, { "$ref": "#/$defs/ModelParameter" }, { "$ref": "#/$defs/StructureParameter" } ] }, "title": "Parameters", "type": "array" }, "normalization_constant": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Normalization Constant" }, "constraints": { "anyOf": [ { "items": { "anyOf": [ { "$ref": "#/$defs/StateVariableConstraint" }, { "$ref": "#/$defs/LinearConstraint" } ] }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Constraints" }, "empty_volume_ok": { "default": false, "title": "Empty Volume Ok", "type": "boolean" }, "model": { "anyOf": [ { "$ref": "#/$defs/GeneratedPetriNetModel" }, { "$ref": "#/$defs/GeneratedRegnetModel" }, { "$ref": "#/$defs/RegnetModel" }, { "$ref": "#/$defs/PetrinetModel" }, { "$ref": "#/$defs/DecapodeModel" }, { "$ref": "#/$defs/BilayerModel" }, { "$ref": "#/$defs/EncodedModel" }, { "$ref": "#/$defs/EnsembleModel" } ], "title": "Model" }, "query": { "anyOf": [ { "$ref": "#/$defs/QueryAnd" }, { "$ref": "#/$defs/QueryGE" }, { "$ref": "#/$defs/QueryLE" }, { "$ref": "#/$defs/QueryEncoded" }, { "$ref": "#/$defs/QueryFunction" }, { "$ref": "#/$defs/QueryTrue" } ], "default": { "model": null }, "title": "Query" } }, "required": [ "parameters", "model" ], "title": "AnalysisScenario", "type": "object" }, "BaseProperties": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "rate_constant": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null } }, "title": "BaseProperties", "type": "object" }, "BilayerDynamics": { "description": "The BilayerDynamics class represents a state update (dynamics) model for a set of variables. The graph consists of:\n\n* state nodes (current state),\n\n* tangent nodes (next state), and\n\n* flux nodes (causal relationships).", "properties": { "json_graph": { "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "BilayerDynamics", "type": "object" }, "BilayerEdge": { "properties": { "src": { "$ref": "#/$defs/BilayerNode" }, "tgt": { "$ref": "#/$defs/BilayerNode" } }, "required": [ "src", "tgt" ], "title": "BilayerEdge", "type": "object" }, "BilayerFluxNode": { "description": "BilayerNode representing a flux.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerFluxNode", "type": "object" }, "BilayerMeasurement": { "description": "The BilayerMeasurement class represents measurements taken on the BilayerNode state nodes of a BilayerDynamics object. The graph consists of:\n\n* state nodes (current state),\n\n* observation nodes, and\n\n* flux nodes (causal relationships).", "properties": { "json_graph": { "title": "Json Graph", "type": "object" }, "state": { "additionalProperties": { "$ref": "#/$defs/BilayerStateNode" }, "default": {}, "title": "State", "type": "object" }, "flux": { "additionalProperties": { "$ref": "#/$defs/BilayerFluxNode" }, "default": {}, "title": "Flux", "type": "object" }, "observable": { "additionalProperties": { "$ref": "#/$defs/BilayerStateNode" }, "default": {}, "title": "Observable", "type": "object" }, "input_edges": { "$ref": "#/$defs/BilayerEdge", "default": [] }, "output_edges": { "$ref": "#/$defs/BilayerEdge", "default": [] } }, "required": [ "json_graph" ], "title": "BilayerMeasurement", "type": "object" }, "BilayerMetadata": { "description": "Metadata for a BilayerNode", "properties": { "ref": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Ref" }, "type": { "anyOf": [ { "enum": [ "float", "int" ], "type": "string" }, { "type": "null" } ], "default": null, "title": "Type" }, "initial_value": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Initial Value" }, "lb": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Lb" }, "ub": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Ub" } }, "title": "BilayerMetadata", "type": "object" }, "BilayerModel": { "description": "A BilayerModel is a complete specification of a Model that uses a BilayerDynamics graph to represent dynamics. It includes the attributes:\n\n* bilayer: the BilayerDynamics graph\n\n* measurements: the BilayerMeasurement graph (used to derive additional variables from the state nodes)\n\n* init_values: a dict mapping from state variables and flux parameters to initial value\n\n* identical_parameters: a list of lists of flux parameters that have identical values\n\n* parameter_bounds: a list of lower and upper bounds on parameters", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "bilayer": { "$ref": "#/$defs/BilayerDynamics" }, "measurements": { "$ref": "#/$defs/BilayerMeasurement", "default": null }, "identical_parameters": { "default": [], "items": { "items": { "type": "string" }, "type": "array" }, "title": "Identical Parameters", "type": "array" } }, "required": [ "bilayer" ], "title": "BilayerModel", "type": "object" }, "BilayerNode": { "description": "Node in a BilayerGraph.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerNode", "type": "object" }, "BilayerStateNode": { "description": "BilayerNode representing a state variable.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerStateNode", "type": "object" }, "DecapodeDynamics": { "properties": { "json_graph": { "additionalProperties": { "items": { "additionalProperties": { "anyOf": [ { "type": "integer" }, { "type": "string" } ] }, "type": "object" }, "type": "array" }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "DecapodeDynamics", "type": "object" }, "DecapodeModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "decapode": { "$ref": "#/$defs/DecapodeDynamics" } }, "required": [ "decapode" ], "title": "DecapodeModel", "type": "object" }, "Edge": { "properties": { "id": { "title": "Id", "type": "string" }, "sign": { "title": "Sign", "type": "boolean" }, "source": { "title": "Source", "type": "string" }, "target": { "title": "Target", "type": "string" }, "properties": { "anyOf": [ { "$ref": "#/$defs/BaseProperties" }, { "type": "null" } ], "default": null } }, "required": [ "id", "sign", "source", "target" ], "title": "Edge", "type": "object" }, "EncodedModel": { "description": "Model that holds an SMT formula encoding a model. This class is meant to wrap hand-coded SMT formulas.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/ModelParameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" } }, "title": "EncodedModel", "type": "object" }, "EncodingSchedule": { "properties": { "timepoints": { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "title": "Timepoints", "type": "array" } }, "required": [ "timepoints" ], "title": "EncodingSchedule", "type": "object" }, "EnsembleModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "models": { "items": { "$ref": "#/$defs/FunmanModel" }, "title": "Models", "type": "array" } }, "required": [ "models" ], "title": "EnsembleModel", "type": "object" }, "FUNMANConfig": { "description": "Base definition of a configuration 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" } }, "title": "FUNMANConfig", "type": "object" }, "FunmanModel": { "description": "The abstract base class for Models.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" } }, "title": "FunmanModel", "type": "object" }, "GeneratedPetriNetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "petrinet": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model" } }, "required": [ "petrinet" ], "title": "GeneratedPetriNetModel", "type": "object" }, "GeneratedRegnetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "regnet": { "$ref": "#/$defs/funman__model__generated_models__regnet__Model" } }, "required": [ "regnet" ], "title": "GeneratedRegnetModel", "type": "object" }, "Header": { "properties": { "name": { "title": "Name", "type": "string" }, "schema": { "format": "uri", "minLength": 1, "title": "Schema", "type": "string" }, "schema_name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Schema Name" }, "description": { "title": "Description", "type": "string" }, "model_version": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Model Version" } }, "required": [ "name", "schema", "description" ], "title": "Header", "type": "object" }, "Initial": { "properties": { "target": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Target" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Initial", "type": "object" }, "Interval": { "description": "An interval is a pair [lb, ub) that is open (i.e., an interval specifies all points x where lb <= x and ub < x).", "properties": { "lb": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": -1.7976931348623157e+308, "title": "Lb" }, "ub": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": 1.7976931348623157e+308, "title": "Ub" }, "closed_upper_bound": { "default": false, "title": "Closed Upper Bound", "type": "boolean" }, "original_width": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Original Width" }, "normalized": { "default": false, "title": "Normalized", "type": "boolean" }, "unnormalized_lb": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Unnormalized Lb" }, "unnormalized_ub": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Unnormalized Ub" } }, "title": "Interval", "type": "object" }, "LinearConstraint": { "additionalProperties": false, "properties": { "soft": { "default": true, "title": "Soft", "type": "boolean" }, "name": { "title": "Name", "type": "string" }, "timepoints": { "anyOf": [ { "$ref": "#/$defs/Interval" }, { "type": "null" } ], "default": null }, "additive_bounds": { "$ref": "#/$defs/Interval" }, "variables": { "items": { "type": "string" }, "title": "Variables", "type": "array" }, "weights": { "anyOf": [ { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Weights" }, "derivative": { "default": false, "title": "Derivative", "type": "boolean" } }, "required": [ "name", "additive_bounds", "variables" ], "title": "LinearConstraint", "type": "object" }, "ModelParameter": { "additionalProperties": false, "description": "A parameter is a free variable for a Model. It has the following attributes:\n\n* lb: lower bound\n\n* ub: upper bound\n\n* symbol: a pysmt FNode corresponding to the parameter variable", "properties": { "name": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Name" }, "interval": { "$ref": "#/$defs/Interval", "default": { "lb": -1.7976931348623157e+308, "ub": 1.7976931348623157e+308, "closed_upper_bound": false, "original_width": Infinity, "normalized": false, "unnormalized_lb": null, "unnormalized_ub": null } }, "label": { "default": "any", "enum": [ "any", "all" ], "title": "Label", "type": "string" } }, "required": [ "name" ], "title": "ModelParameter", "type": "object" }, "ModelSymbol": { "properties": { "name": { "title": "Name", "type": "string" }, "model": { "title": "Model", "type": "string" } }, "required": [ "name", "model" ], "title": "ModelSymbol", "type": "object" }, "Observable": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "required": [ "id" ], "title": "Observable", "type": "object" }, "OdeSemantics": { "properties": { "rates": { "anyOf": [ { "items": { "$ref": "#/$defs/Rate" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Rates" }, "initials": { "anyOf": [ { "items": { "$ref": "#/$defs/Initial" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Initials" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Parameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" }, "observables": { "anyOf": [ { "items": { "$ref": "#/$defs/Observable" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Observables" }, "time": { "anyOf": [ { "$ref": "#/$defs/Time" }, { "type": "null" } ], "default": null } }, "title": "OdeSemantics", "type": "object" }, "ParamOrNumber": { "anyOf": [ { "type": "number" }, { "type": "string" } ], "title": "ParamOrNumber" }, "PetrinetDynamics": { "properties": { "json_graph": { "additionalProperties": { "items": { "additionalProperties": { "anyOf": [ { "additionalProperties": { "anyOf": [ { "type": "string" }, { "type": "boolean" }, { "type": "number" }, { "type": "null" } ] }, "type": "object" }, { "type": "integer" }, { "type": "string" }, { "type": "number" }, { "type": "null" } ] }, "type": "object" }, "type": "array" }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "PetrinetDynamics", "type": "object" }, "PetrinetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "petrinet": { "$ref": "#/$defs/PetrinetDynamics" } }, "required": [ "petrinet" ], "title": "PetrinetModel", "type": "object" }, "Properties": { "additionalProperties": true, "properties": { "name": { "title": "Name", "type": "string" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null } }, "required": [ "name" ], "title": "Properties", "type": "object" }, "Query": { "description": "Abstract base class for queries.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "Query", "type": "object" }, "QueryAnd": { "description": "Conjunction of queries.\n\nParameters\n----------\nqueries : List[Query]\n queries to conjoin.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "queries": { "items": { "anyOf": [ { "$ref": "#/$defs/QueryLE" }, { "$ref": "#/$defs/QueryGE" }, { "$ref": "#/$defs/QueryEquals" }, { "$ref": "#/$defs/Query" } ] }, "title": "Queries", "type": "array" } }, "required": [ "queries" ], "title": "QueryAnd", "type": "object" }, "QueryEncoded": { "description": "Class to contain a formula that is already encoded by a pysmt FNode.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "QueryEncoded", "type": "object" }, "QueryEquals": { "description": "Class to represent a query of the form: var == value, where var is a variable, and value is a constant.\n\nParameters\n----------\nvariable : str\n model variable name\nvalue : float\n value\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "value": { "title": "Value", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "value" ], "title": "QueryEquals", "type": "object" }, "QueryFunction": { "description": "This query uses a Python function passed to the constructor to evaluate a query on the results of a scenario.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "function": { "title": "Function", "type": "string" } }, "required": [ "function" ], "title": "QueryFunction", "type": "object" }, "QueryGE": { "description": "Class to represent a query of the form: var >= lb, where var is a variable, and lb is a constant lower bound.\n\nParameters\n----------\nvariable : str\n model variable name\nlb : float\n lower bound constant\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "lb": { "title": "Lb", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "lb" ], "title": "QueryGE", "type": "object" }, "QueryLE": { "description": "Class to represent a query of the form: var <= ub, where var is a variable, and ub is a constant upper bound.\n\nParameters\n----------\nvariable : str\n model variable name\nub : float\n upper bound constant\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "ub": { "title": "Ub", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "ub" ], "title": "QueryLE", "type": "object" }, "QueryTrue": { "additionalProperties": false, "description": "Query that represents logical true. I.e., this query does not place any additional constraints upon a model.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "QueryTrue", "type": "object" }, "Rate": { "properties": { "target": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Target" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Rate", "type": "object" }, "RegnetDynamics": { "properties": { "json_graph": { "additionalProperties": { "anyOf": [ { "type": "string" }, { "additionalProperties": { "items": { "type": "object" }, "type": "array" }, "type": "object" } ] }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "RegnetDynamics", "type": "object" }, "RegnetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "regnet": { "$ref": "#/$defs/RegnetDynamics" } }, "required": [ "regnet" ], "title": "RegnetModel", "type": "object" }, "SearchStaticsMP": { "properties": {}, "title": "SearchStaticsMP", "type": "object" }, "Semantics": { "properties": { "ode": { "anyOf": [ { "$ref": "#/$defs/OdeSemantics" }, { "type": "null" } ], "default": null }, "typing": { "anyOf": [ { "$ref": "#/$defs/TypingSemantics" }, { "type": "null" } ], "default": null, "description": "(Optional) Information for aligning models for stratification" }, "span": { "anyOf": [ { "items": { "$ref": "#/$defs/TypingSemantics" }, "type": "array" }, { "type": "null" } ], "default": null, "description": "(Optional) Legs of a span, each of which are a full ASKEM Petri Net", "title": "Span" } }, "title": "Semantics", "type": "object" }, "State": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "State", "type": "object" }, "StateVariableConstraint": { "additionalProperties": false, "properties": { "soft": { "default": true, "title": "Soft", "type": "boolean" }, "name": { "title": "Name", "type": "string" }, "timepoints": { "anyOf": [ { "$ref": "#/$defs/Interval" }, { "type": "null" } ], "default": null }, "variable": { "title": "Variable", "type": "string" }, "interval": { "$ref": "#/$defs/Interval", "default": null } }, "required": [ "name", "variable" ], "title": "StateVariableConstraint", "type": "object" }, "States": { "items": { "$ref": "#/$defs/State" }, "title": "States", "type": "array" }, "StructureParameter": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Name" }, "interval": { "$ref": "#/$defs/Interval", "default": { "lb": -1.7976931348623157e+308, "ub": 1.7976931348623157e+308, "closed_upper_bound": false, "original_width": Infinity, "normalized": false, "unnormalized_lb": null, "unnormalized_ub": null } }, "label": { "default": "any", "enum": [ "any", "all" ], "title": "Label", "type": "string" } }, "required": [ "name" ], "title": "StructureParameter", "type": "object" }, "Time": { "properties": { "id": { "title": "Id", "type": "string" }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Time", "type": "object" }, "Transition": { "properties": { "id": { "title": "Id", "type": "string" }, "input": { "items": { "type": "string" }, "title": "Input", "type": "array" }, "output": { "items": { "type": "string" }, "title": "Output", "type": "array" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "properties": { "anyOf": [ { "$ref": "#/$defs/Properties" }, { "type": "null" } ], "default": null } }, "required": [ "id", "input", "output" ], "title": "Transition", "type": "object" }, "Transitions": { "items": { "$ref": "#/$defs/Transition" }, "title": "Transitions", "type": "array" }, "TypingSemantics": { "properties": { "system": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model", "description": "A Petri net representing the 'type system' that is necessary to align states and transitions across different models during stratification." }, "map": { "description": "A map between the (state and transition) nodes of the model and the (state and transition) nodes of the type system", "items": { "items": { "type": "string" }, "type": "array" }, "title": "Map", "type": "array" } }, "required": [ "system", "map" ], "title": "TypingSemantics", "type": "object" }, "Unit": { "additionalProperties": true, "properties": { "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Unit", "type": "object" }, "Vertice": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "rate_constant": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null }, "id": { "title": "Id", "type": "string" }, "sign": { "title": "Sign", "type": "boolean" }, "initial": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null } }, "required": [ "id", "sign" ], "title": "Vertice", "type": "object" }, "funman__model__generated_models__petrinet__Distribution": { "additionalProperties": true, "properties": { "type": { "title": "Type", "type": "string" }, "parameters": { "title": "Parameters", "type": "object" } }, "required": [ "type", "parameters" ], "title": "Distribution", "type": "object" }, "funman__model__generated_models__petrinet__Grounding": { "additionalProperties": false, "properties": { "identifiers": { "title": "Identifiers", "type": "object" }, "modifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Modifiers" } }, "required": [ "identifiers" ], "title": "Grounding", "type": "object" }, "funman__model__generated_models__petrinet__Model": { "additionalProperties": true, "properties": { "header": { "$ref": "#/$defs/Header" }, "properties": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Properties" }, "model": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model1" }, "semantics": { "anyOf": [ { "$ref": "#/$defs/Semantics" }, { "type": "null" } ], "default": null, "description": "Information specific to a given semantics (e.g., ODEs) associated with a model." }, "metadata": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "description": "(Optional) Information not useful for execution of the model, but that may be useful to some consumer in the future. E.g. creation timestamp or source paper's author.", "title": "Metadata" } }, "required": [ "header", "model" ], "title": "Model", "type": "object" }, "funman__model__generated_models__petrinet__Model1": { "additionalProperties": false, "properties": { "states": { "$ref": "#/$defs/States" }, "transitions": { "$ref": "#/$defs/Transitions" } }, "required": [ "states", "transitions" ], "title": "Model1", "type": "object" }, "funman__model__generated_models__petrinet__Parameter": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "value": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Value" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "distribution": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Distribution" }, { "type": "null" } ], "default": null }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Parameter", "type": "object" }, "funman__model__generated_models__regnet__Distribution": { "properties": { "type": { "title": "Type", "type": "string" }, "parameters": { "title": "Parameters", "type": "object" } }, "required": [ "type", "parameters" ], "title": "Distribution", "type": "object" }, "funman__model__generated_models__regnet__Grounding": { "additionalProperties": false, "properties": { "identifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Identifiers" }, "modifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Modifiers" } }, "title": "Grounding", "type": "object" }, "funman__model__generated_models__regnet__Model": { "properties": { "header": { "$ref": "#/$defs/Header" }, "properties": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Properties" }, "model": { "$ref": "#/$defs/funman__model__generated_models__regnet__Model1" }, "metadata": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "description": "(Optional) Information not useful for execution of the model, but that may be useful to some consumer in the future. E.g. creation timestamp or source paper's author.", "title": "Metadata" } }, "required": [ "header", "model" ], "title": "Model", "type": "object" }, "funman__model__generated_models__regnet__Model1": { "additionalProperties": false, "properties": { "vertices": { "items": { "$ref": "#/$defs/Vertice" }, "title": "Vertices", "type": "array" }, "edges": { "items": { "$ref": "#/$defs/Edge" }, "title": "Edges", "type": "array" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/funman__model__generated_models__regnet__Parameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" } }, "required": [ "vertices", "edges" ], "title": "Model1", "type": "object" }, "funman__model__generated_models__regnet__Parameter": { "properties": { "id": { "title": "Id", "type": "string" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "value": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Value" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "distribution": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Distribution" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Parameter", "type": "object" } }, "required": [ "schedule", "problem", "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field statistics: SearchStaticsMP = None¶
- model_post_init(context: Any, /) None ¶
We need to both initialize private attributes and call the user-defined model_post_init method.
- pydantic model funman.search.box_search.FormulaStack¶
Bases:
BaseModel
Show JSON schema
{ "title": "FormulaStack", "type": "object", "properties": { "formula_stack": { "default": [], "items": { "$ref": "#/$defs/FormulaStackFrame" }, "title": "Formula Stack", "type": "array" }, "time": { "default": -2, "title": "Time", "type": "integer" } }, "$defs": { "FormulaStackFrame": { "properties": {}, "title": "FormulaStackFrame", "type": "object" } } }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field formula_stack: List[FormulaStackFrame] = []¶
- field time: int = -2¶
- add_assertion(formula)¶
- compute_assignment(episode: SearchEpisode, _smtlib_save_fn: Callable | None = None) Model ¶
- 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.
- pop(levels: int = 1, pop_solver: bool = True)¶
- push(levels: int = 1, push_solver: bool = True)¶
- to_list(simplified=False) List[FNode] ¶
- pydantic model funman.search.box_search.FormulaStackFrame¶
Bases:
BaseModel
Show JSON schema
{ "title": "FormulaStackFrame", "type": "object", "properties": {} }
- Config:
arbitrary_types_allowed: bool = True
- add_assertion(formula, is_simplified=False)¶
- 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.search.search module¶
- class funman.search.search.Search¶
Bases:
ABC
- invoke_solver(s: Solver, timeout: int | None = None) Model | BoxExplanation ¶
- abstract search(problem: AnalysisScenario, config: FUNMANConfig | None = None, haltEvent: Event | None = None, resultsCallback: Callable[[ParameterSpace], None] | None = None) SearchEpisode ¶
- pydantic model funman.search.search.SearchEpisode¶
Bases:
BaseModel
Show JSON schema
{ "title": "SearchEpisode", "type": "object", "properties": { "schedule": { "$ref": "#/$defs/EncodingSchedule" }, "problem": { "$ref": "#/$defs/AnalysisScenario" }, "config": { "$ref": "#/$defs/FUNMANConfig" }, "statistics": { "$ref": "#/$defs/SearchStatistics", "default": null } }, "$defs": { "AnalysisScenario": { "additionalProperties": false, "description": "Abstract class for Analysis Scenarios.", "properties": { "parameters": { "items": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Parameter" }, { "$ref": "#/$defs/ModelParameter" }, { "$ref": "#/$defs/StructureParameter" } ] }, "title": "Parameters", "type": "array" }, "normalization_constant": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Normalization Constant" }, "constraints": { "anyOf": [ { "items": { "anyOf": [ { "$ref": "#/$defs/StateVariableConstraint" }, { "$ref": "#/$defs/LinearConstraint" } ] }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Constraints" }, "empty_volume_ok": { "default": false, "title": "Empty Volume Ok", "type": "boolean" }, "model": { "anyOf": [ { "$ref": "#/$defs/GeneratedPetriNetModel" }, { "$ref": "#/$defs/GeneratedRegnetModel" }, { "$ref": "#/$defs/RegnetModel" }, { "$ref": "#/$defs/PetrinetModel" }, { "$ref": "#/$defs/DecapodeModel" }, { "$ref": "#/$defs/BilayerModel" }, { "$ref": "#/$defs/EncodedModel" }, { "$ref": "#/$defs/EnsembleModel" } ], "title": "Model" }, "query": { "anyOf": [ { "$ref": "#/$defs/QueryAnd" }, { "$ref": "#/$defs/QueryGE" }, { "$ref": "#/$defs/QueryLE" }, { "$ref": "#/$defs/QueryEncoded" }, { "$ref": "#/$defs/QueryFunction" }, { "$ref": "#/$defs/QueryTrue" } ], "default": { "model": null }, "title": "Query" } }, "required": [ "parameters", "model" ], "title": "AnalysisScenario", "type": "object" }, "BaseProperties": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "rate_constant": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null } }, "title": "BaseProperties", "type": "object" }, "BilayerDynamics": { "description": "The BilayerDynamics class represents a state update (dynamics) model for a set of variables. The graph consists of:\n\n* state nodes (current state),\n\n* tangent nodes (next state), and\n\n* flux nodes (causal relationships).", "properties": { "json_graph": { "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "BilayerDynamics", "type": "object" }, "BilayerEdge": { "properties": { "src": { "$ref": "#/$defs/BilayerNode" }, "tgt": { "$ref": "#/$defs/BilayerNode" } }, "required": [ "src", "tgt" ], "title": "BilayerEdge", "type": "object" }, "BilayerFluxNode": { "description": "BilayerNode representing a flux.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerFluxNode", "type": "object" }, "BilayerMeasurement": { "description": "The BilayerMeasurement class represents measurements taken on the BilayerNode state nodes of a BilayerDynamics object. The graph consists of:\n\n* state nodes (current state),\n\n* observation nodes, and\n\n* flux nodes (causal relationships).", "properties": { "json_graph": { "title": "Json Graph", "type": "object" }, "state": { "additionalProperties": { "$ref": "#/$defs/BilayerStateNode" }, "default": {}, "title": "State", "type": "object" }, "flux": { "additionalProperties": { "$ref": "#/$defs/BilayerFluxNode" }, "default": {}, "title": "Flux", "type": "object" }, "observable": { "additionalProperties": { "$ref": "#/$defs/BilayerStateNode" }, "default": {}, "title": "Observable", "type": "object" }, "input_edges": { "$ref": "#/$defs/BilayerEdge", "default": [] }, "output_edges": { "$ref": "#/$defs/BilayerEdge", "default": [] } }, "required": [ "json_graph" ], "title": "BilayerMeasurement", "type": "object" }, "BilayerMetadata": { "description": "Metadata for a BilayerNode", "properties": { "ref": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Ref" }, "type": { "anyOf": [ { "enum": [ "float", "int" ], "type": "string" }, { "type": "null" } ], "default": null, "title": "Type" }, "initial_value": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Initial Value" }, "lb": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Lb" }, "ub": { "anyOf": [ { "type": "number" }, { "type": "integer" }, { "type": "null" } ], "default": null, "title": "Ub" } }, "title": "BilayerMetadata", "type": "object" }, "BilayerModel": { "description": "A BilayerModel is a complete specification of a Model that uses a BilayerDynamics graph to represent dynamics. It includes the attributes:\n\n* bilayer: the BilayerDynamics graph\n\n* measurements: the BilayerMeasurement graph (used to derive additional variables from the state nodes)\n\n* init_values: a dict mapping from state variables and flux parameters to initial value\n\n* identical_parameters: a list of lists of flux parameters that have identical values\n\n* parameter_bounds: a list of lower and upper bounds on parameters", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "bilayer": { "$ref": "#/$defs/BilayerDynamics" }, "measurements": { "$ref": "#/$defs/BilayerMeasurement", "default": null }, "identical_parameters": { "default": [], "items": { "items": { "type": "string" }, "type": "array" }, "title": "Identical Parameters", "type": "array" } }, "required": [ "bilayer" ], "title": "BilayerModel", "type": "object" }, "BilayerNode": { "description": "Node in a BilayerGraph.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerNode", "type": "object" }, "BilayerStateNode": { "description": "BilayerNode representing a state variable.", "properties": { "index": { "title": "Index", "type": "integer" }, "parameter": { "title": "Parameter", "type": "string" }, "metadata": { "anyOf": [ { "$ref": "#/$defs/BilayerMetadata" }, { "type": "null" } ], "default": null } }, "required": [ "index", "parameter" ], "title": "BilayerStateNode", "type": "object" }, "DecapodeDynamics": { "properties": { "json_graph": { "additionalProperties": { "items": { "additionalProperties": { "anyOf": [ { "type": "integer" }, { "type": "string" } ] }, "type": "object" }, "type": "array" }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "DecapodeDynamics", "type": "object" }, "DecapodeModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "decapode": { "$ref": "#/$defs/DecapodeDynamics" } }, "required": [ "decapode" ], "title": "DecapodeModel", "type": "object" }, "Edge": { "properties": { "id": { "title": "Id", "type": "string" }, "sign": { "title": "Sign", "type": "boolean" }, "source": { "title": "Source", "type": "string" }, "target": { "title": "Target", "type": "string" }, "properties": { "anyOf": [ { "$ref": "#/$defs/BaseProperties" }, { "type": "null" } ], "default": null } }, "required": [ "id", "sign", "source", "target" ], "title": "Edge", "type": "object" }, "EncodedModel": { "description": "Model that holds an SMT formula encoding a model. This class is meant to wrap hand-coded SMT formulas.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/ModelParameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" } }, "title": "EncodedModel", "type": "object" }, "EncodingSchedule": { "properties": { "timepoints": { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "title": "Timepoints", "type": "array" } }, "required": [ "timepoints" ], "title": "EncodingSchedule", "type": "object" }, "EnsembleModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "models": { "items": { "$ref": "#/$defs/FunmanModel" }, "title": "Models", "type": "array" } }, "required": [ "models" ], "title": "EnsembleModel", "type": "object" }, "FUNMANConfig": { "description": "Base definition of a configuration 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" } }, "title": "FUNMANConfig", "type": "object" }, "FunmanModel": { "description": "The abstract base class for Models.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" } }, "title": "FunmanModel", "type": "object" }, "GeneratedPetriNetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "petrinet": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model" } }, "required": [ "petrinet" ], "title": "GeneratedPetriNetModel", "type": "object" }, "GeneratedRegnetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "regnet": { "$ref": "#/$defs/funman__model__generated_models__regnet__Model" } }, "required": [ "regnet" ], "title": "GeneratedRegnetModel", "type": "object" }, "Header": { "properties": { "name": { "title": "Name", "type": "string" }, "schema": { "format": "uri", "minLength": 1, "title": "Schema", "type": "string" }, "schema_name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Schema Name" }, "description": { "title": "Description", "type": "string" }, "model_version": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Model Version" } }, "required": [ "name", "schema", "description" ], "title": "Header", "type": "object" }, "Initial": { "properties": { "target": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Target" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Initial", "type": "object" }, "Interval": { "description": "An interval is a pair [lb, ub) that is open (i.e., an interval specifies all points x where lb <= x and ub < x).", "properties": { "lb": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": -1.7976931348623157e+308, "title": "Lb" }, "ub": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": 1.7976931348623157e+308, "title": "Ub" }, "closed_upper_bound": { "default": false, "title": "Closed Upper Bound", "type": "boolean" }, "original_width": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Original Width" }, "normalized": { "default": false, "title": "Normalized", "type": "boolean" }, "unnormalized_lb": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Unnormalized Lb" }, "unnormalized_ub": { "anyOf": [ { "type": "number" }, { "type": "string" }, { "type": "null" } ], "default": null, "title": "Unnormalized Ub" } }, "title": "Interval", "type": "object" }, "LinearConstraint": { "additionalProperties": false, "properties": { "soft": { "default": true, "title": "Soft", "type": "boolean" }, "name": { "title": "Name", "type": "string" }, "timepoints": { "anyOf": [ { "$ref": "#/$defs/Interval" }, { "type": "null" } ], "default": null }, "additive_bounds": { "$ref": "#/$defs/Interval" }, "variables": { "items": { "type": "string" }, "title": "Variables", "type": "array" }, "weights": { "anyOf": [ { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Weights" }, "derivative": { "default": false, "title": "Derivative", "type": "boolean" } }, "required": [ "name", "additive_bounds", "variables" ], "title": "LinearConstraint", "type": "object" }, "ModelParameter": { "additionalProperties": false, "description": "A parameter is a free variable for a Model. It has the following attributes:\n\n* lb: lower bound\n\n* ub: upper bound\n\n* symbol: a pysmt FNode corresponding to the parameter variable", "properties": { "name": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Name" }, "interval": { "$ref": "#/$defs/Interval", "default": { "lb": -1.7976931348623157e+308, "ub": 1.7976931348623157e+308, "closed_upper_bound": false, "original_width": Infinity, "normalized": false, "unnormalized_lb": null, "unnormalized_ub": null } }, "label": { "default": "any", "enum": [ "any", "all" ], "title": "Label", "type": "string" } }, "required": [ "name" ], "title": "ModelParameter", "type": "object" }, "ModelSymbol": { "properties": { "name": { "title": "Name", "type": "string" }, "model": { "title": "Model", "type": "string" } }, "required": [ "name", "model" ], "title": "ModelSymbol", "type": "object" }, "Observable": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "required": [ "id" ], "title": "Observable", "type": "object" }, "OdeSemantics": { "properties": { "rates": { "anyOf": [ { "items": { "$ref": "#/$defs/Rate" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Rates" }, "initials": { "anyOf": [ { "items": { "$ref": "#/$defs/Initial" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Initials" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Parameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" }, "observables": { "anyOf": [ { "items": { "$ref": "#/$defs/Observable" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Observables" }, "time": { "anyOf": [ { "$ref": "#/$defs/Time" }, { "type": "null" } ], "default": null } }, "title": "OdeSemantics", "type": "object" }, "ParamOrNumber": { "anyOf": [ { "type": "number" }, { "type": "string" } ], "title": "ParamOrNumber" }, "PetrinetDynamics": { "properties": { "json_graph": { "additionalProperties": { "items": { "additionalProperties": { "anyOf": [ { "additionalProperties": { "anyOf": [ { "type": "string" }, { "type": "boolean" }, { "type": "number" }, { "type": "null" } ] }, "type": "object" }, { "type": "integer" }, { "type": "string" }, { "type": "number" }, { "type": "null" } ] }, "type": "object" }, "type": "array" }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "PetrinetDynamics", "type": "object" }, "PetrinetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "petrinet": { "$ref": "#/$defs/PetrinetDynamics" } }, "required": [ "petrinet" ], "title": "PetrinetModel", "type": "object" }, "Properties": { "additionalProperties": true, "properties": { "name": { "title": "Name", "type": "string" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null } }, "required": [ "name" ], "title": "Properties", "type": "object" }, "Query": { "description": "Abstract base class for queries.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "Query", "type": "object" }, "QueryAnd": { "description": "Conjunction of queries.\n\nParameters\n----------\nqueries : List[Query]\n queries to conjoin.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "queries": { "items": { "anyOf": [ { "$ref": "#/$defs/QueryLE" }, { "$ref": "#/$defs/QueryGE" }, { "$ref": "#/$defs/QueryEquals" }, { "$ref": "#/$defs/Query" } ] }, "title": "Queries", "type": "array" } }, "required": [ "queries" ], "title": "QueryAnd", "type": "object" }, "QueryEncoded": { "description": "Class to contain a formula that is already encoded by a pysmt FNode.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "QueryEncoded", "type": "object" }, "QueryEquals": { "description": "Class to represent a query of the form: var == value, where var is a variable, and value is a constant.\n\nParameters\n----------\nvariable : str\n model variable name\nvalue : float\n value\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "value": { "title": "Value", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "value" ], "title": "QueryEquals", "type": "object" }, "QueryFunction": { "description": "This query uses a Python function passed to the constructor to evaluate a query on the results of a scenario.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "function": { "title": "Function", "type": "string" } }, "required": [ "function" ], "title": "QueryFunction", "type": "object" }, "QueryGE": { "description": "Class to represent a query of the form: var >= lb, where var is a variable, and lb is a constant lower bound.\n\nParameters\n----------\nvariable : str\n model variable name\nlb : float\n lower bound constant\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "lb": { "title": "Lb", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "lb" ], "title": "QueryGE", "type": "object" }, "QueryLE": { "description": "Class to represent a query of the form: var <= ub, where var is a variable, and ub is a constant upper bound.\n\nParameters\n----------\nvariable : str\n model variable name\nub : float\n upper bound constant\nat_end : bool, optional\n apply the constraint to the last timepoint of a scenario only, by default False", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null }, "variable": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Variable" }, "ub": { "title": "Ub", "type": "number" }, "at_end": { "default": false, "title": "At End", "type": "boolean" } }, "required": [ "variable", "ub" ], "title": "QueryLE", "type": "object" }, "QueryTrue": { "additionalProperties": false, "description": "Query that represents logical true. I.e., this query does not place any additional constraints upon a model.", "properties": { "model": { "anyOf": [ { "$ref": "#/$defs/FunmanModel" }, { "type": "null" } ], "default": null } }, "title": "QueryTrue", "type": "object" }, "Rate": { "properties": { "target": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Target" }, "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Rate", "type": "object" }, "RegnetDynamics": { "properties": { "json_graph": { "additionalProperties": { "anyOf": [ { "type": "string" }, { "additionalProperties": { "items": { "type": "object" }, "type": "array" }, "type": "object" } ] }, "title": "Json Graph", "type": "object" } }, "required": [ "json_graph" ], "title": "RegnetDynamics", "type": "object" }, "RegnetModel": { "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" }, "regnet": { "$ref": "#/$defs/RegnetDynamics" } }, "required": [ "regnet" ], "title": "RegnetModel", "type": "object" }, "SearchStatistics": { "properties": {}, "title": "SearchStatistics", "type": "object" }, "Semantics": { "properties": { "ode": { "anyOf": [ { "$ref": "#/$defs/OdeSemantics" }, { "type": "null" } ], "default": null }, "typing": { "anyOf": [ { "$ref": "#/$defs/TypingSemantics" }, { "type": "null" } ], "default": null, "description": "(Optional) Information for aligning models for stratification" }, "span": { "anyOf": [ { "items": { "$ref": "#/$defs/TypingSemantics" }, "type": "array" }, { "type": "null" } ], "default": null, "description": "(Optional) Legs of a span, each of which are a full ASKEM Petri Net", "title": "Span" } }, "title": "Semantics", "type": "object" }, "State": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "State", "type": "object" }, "StateVariableConstraint": { "additionalProperties": false, "properties": { "soft": { "default": true, "title": "Soft", "type": "boolean" }, "name": { "title": "Name", "type": "string" }, "timepoints": { "anyOf": [ { "$ref": "#/$defs/Interval" }, { "type": "null" } ], "default": null }, "variable": { "title": "Variable", "type": "string" }, "interval": { "$ref": "#/$defs/Interval", "default": null } }, "required": [ "name", "variable" ], "title": "StateVariableConstraint", "type": "object" }, "States": { "items": { "$ref": "#/$defs/State" }, "title": "States", "type": "array" }, "StructureParameter": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "$ref": "#/$defs/ModelSymbol" } ], "title": "Name" }, "interval": { "$ref": "#/$defs/Interval", "default": { "lb": -1.7976931348623157e+308, "ub": 1.7976931348623157e+308, "closed_upper_bound": false, "original_width": Infinity, "normalized": false, "unnormalized_lb": null, "unnormalized_ub": null } }, "label": { "default": "any", "enum": [ "any", "all" ], "title": "Label", "type": "string" } }, "required": [ "name" ], "title": "StructureParameter", "type": "object" }, "Time": { "properties": { "id": { "title": "Id", "type": "string" }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Time", "type": "object" }, "Transition": { "properties": { "id": { "title": "Id", "type": "string" }, "input": { "items": { "type": "string" }, "title": "Input", "type": "array" }, "output": { "items": { "type": "string" }, "title": "Output", "type": "array" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "properties": { "anyOf": [ { "$ref": "#/$defs/Properties" }, { "type": "null" } ], "default": null } }, "required": [ "id", "input", "output" ], "title": "Transition", "type": "object" }, "Transitions": { "items": { "$ref": "#/$defs/Transition" }, "title": "Transitions", "type": "array" }, "TypingSemantics": { "properties": { "system": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model", "description": "A Petri net representing the 'type system' that is necessary to align states and transitions across different models during stratification." }, "map": { "description": "A map between the (state and transition) nodes of the model and the (state and transition) nodes of the type system", "items": { "items": { "type": "string" }, "type": "array" }, "title": "Map", "type": "array" } }, "required": [ "system", "map" ], "title": "TypingSemantics", "type": "object" }, "Unit": { "additionalProperties": true, "properties": { "expression": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression" }, "expression_mathml": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Expression Mathml" } }, "title": "Unit", "type": "object" }, "Vertice": { "properties": { "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "rate_constant": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null }, "id": { "title": "Id", "type": "string" }, "sign": { "title": "Sign", "type": "boolean" }, "initial": { "anyOf": [ { "$ref": "#/$defs/ParamOrNumber" }, { "type": "null" } ], "default": null } }, "required": [ "id", "sign" ], "title": "Vertice", "type": "object" }, "funman__model__generated_models__petrinet__Distribution": { "additionalProperties": true, "properties": { "type": { "title": "Type", "type": "string" }, "parameters": { "title": "Parameters", "type": "object" } }, "required": [ "type", "parameters" ], "title": "Distribution", "type": "object" }, "funman__model__generated_models__petrinet__Grounding": { "additionalProperties": false, "properties": { "identifiers": { "title": "Identifiers", "type": "object" }, "modifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Modifiers" } }, "required": [ "identifiers" ], "title": "Grounding", "type": "object" }, "funman__model__generated_models__petrinet__Model": { "additionalProperties": true, "properties": { "header": { "$ref": "#/$defs/Header" }, "properties": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Properties" }, "model": { "$ref": "#/$defs/funman__model__generated_models__petrinet__Model1" }, "semantics": { "anyOf": [ { "$ref": "#/$defs/Semantics" }, { "type": "null" } ], "default": null, "description": "Information specific to a given semantics (e.g., ODEs) associated with a model." }, "metadata": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "description": "(Optional) Information not useful for execution of the model, but that may be useful to some consumer in the future. E.g. creation timestamp or source paper's author.", "title": "Metadata" } }, "required": [ "header", "model" ], "title": "Model", "type": "object" }, "funman__model__generated_models__petrinet__Model1": { "additionalProperties": false, "properties": { "states": { "$ref": "#/$defs/States" }, "transitions": { "$ref": "#/$defs/Transitions" } }, "required": [ "states", "transitions" ], "title": "Model1", "type": "object" }, "funman__model__generated_models__petrinet__Parameter": { "properties": { "id": { "title": "Id", "type": "string" }, "name": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Name" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "value": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Value" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Grounding" }, { "type": "null" } ], "default": null }, "distribution": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__petrinet__Distribution" }, { "type": "null" } ], "default": null }, "units": { "anyOf": [ { "$ref": "#/$defs/Unit" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Parameter", "type": "object" }, "funman__model__generated_models__regnet__Distribution": { "properties": { "type": { "title": "Type", "type": "string" }, "parameters": { "title": "Parameters", "type": "object" } }, "required": [ "type", "parameters" ], "title": "Distribution", "type": "object" }, "funman__model__generated_models__regnet__Grounding": { "additionalProperties": false, "properties": { "identifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Identifiers" }, "modifiers": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Modifiers" } }, "title": "Grounding", "type": "object" }, "funman__model__generated_models__regnet__Model": { "properties": { "header": { "$ref": "#/$defs/Header" }, "properties": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "title": "Properties" }, "model": { "$ref": "#/$defs/funman__model__generated_models__regnet__Model1" }, "metadata": { "anyOf": [ { "type": "object" }, { "type": "null" } ], "default": null, "description": "(Optional) Information not useful for execution of the model, but that may be useful to some consumer in the future. E.g. creation timestamp or source paper's author.", "title": "Metadata" } }, "required": [ "header", "model" ], "title": "Model", "type": "object" }, "funman__model__generated_models__regnet__Model1": { "additionalProperties": false, "properties": { "vertices": { "items": { "$ref": "#/$defs/Vertice" }, "title": "Vertices", "type": "array" }, "edges": { "items": { "$ref": "#/$defs/Edge" }, "title": "Edges", "type": "array" }, "parameters": { "anyOf": [ { "items": { "$ref": "#/$defs/funman__model__generated_models__regnet__Parameter" }, "type": "array" }, { "type": "null" } ], "default": null, "title": "Parameters" } }, "required": [ "vertices", "edges" ], "title": "Model1", "type": "object" }, "funman__model__generated_models__regnet__Parameter": { "properties": { "id": { "title": "Id", "type": "string" }, "description": { "anyOf": [ { "type": "string" }, { "type": "null" } ], "default": null, "title": "Description" }, "value": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": null, "title": "Value" }, "grounding": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Grounding" }, { "type": "null" } ], "default": null }, "distribution": { "anyOf": [ { "$ref": "#/$defs/funman__model__generated_models__regnet__Distribution" }, { "type": "null" } ], "default": null } }, "required": [ "id" ], "title": "Parameter", "type": "object" } }, "required": [ "schedule", "problem", "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- field problem: AnalysisScenario [Required]¶
- field schedule: EncodingSchedule [Required]¶
- field statistics: SearchStatistics = None¶
- 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.
- num_parameters()¶
- pydantic model funman.search.search.SearchStaticsMP¶
Bases:
SearchStatistics
Show JSON schema
{ "title": "SearchStaticsMP", "type": "object", "properties": {} }
- Config:
arbitrary_types_allowed: bool = True
- model_post_init(context: Any, /) None ¶
We need to both initialize private attributes and call the user-defined model_post_init method.
- pydantic model funman.search.search.SearchStatistics¶
Bases:
BaseModel
Show JSON schema
{ "title": "SearchStatistics", "type": "object", "properties": {} }
- Config:
arbitrary_types_allowed: bool = True
- 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.search.search.run_with_limited_time(func, args, kwargs, time)¶
funman.search.simulate module¶
- pydantic model funman.search.simulate.Simulator¶
Bases:
BaseModel
Show JSON schema
{ "title": "Simulator", "type": "object", "properties": { "model": { "$ref": "#/$defs/FunmanModel" }, "init": { "additionalProperties": { "anyOf": [ { "type": "number" }, { "type": "string" } ] }, "title": "Init", "type": "object" }, "parameters": { "additionalProperties": { "type": "number" }, "title": "Parameters", "type": "object" }, "tvect": { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "title": "Tvect", "type": "array" } }, "$defs": { "FunmanModel": { "description": "The abstract base class for Models.", "properties": { "name": { "default": "model_a6f04917-34c0-45e0-a42c-128947736090", "title": "Name", "type": "string" }, "init_values": { "additionalProperties": { "type": "number" }, "default": {}, "title": "Init Values", "type": "object" }, "parameter_bounds": { "additionalProperties": { "items": { "type": "number" }, "type": "array" }, "default": {}, "title": "Parameter Bounds", "type": "object" } }, "title": "FunmanModel", "type": "object" } }, "required": [ "model", "init", "parameters", "tvect" ] }
- Fields:
- field init: Dict[str, float | str] [Required]¶
- field model: FunmanModel [Required]¶
- field parameters: Dict[str, float] [Required]¶
- field tvect: List[int | float] [Required]¶
- initial_state() List[float] ¶
- model_args() List[float] ¶
- sim() Timeseries | None ¶
funman.search.simulator_check module¶
- class funman.search.simulator_check.SimulatorCheck¶
Bases:
Search
- build_formula(episode: SearchEpisode, schedule: EncodingSchedule, options: EncodingOptions) Tuple[FNode, FNode] ¶
- eval_point(beta_val, gamma_val, query_condition=True, plot=False, rtol=1, atol=1, mxstep=10, mxordn=1, mxords=1, hmin=1)¶
- expand(problem, episode, options: EncodingOptions, parameter_space, schedule: EncodingSchedule)¶
- ps(parameter_space, num_dim_points=10)¶
- search(problem, config: FUNMANConfig | None = None, haltEvent: Event | None = None, resultsCallback: Callable[[ParameterSpace], None] | None = None) SearchEpisode ¶
- solve_formula(s: Solver, formula: FNode, episode) Model | Explanation ¶
- store_smtlib(formula, filename='dbg.smt2')¶
funman.search.smt_check module¶
- class funman.search.smt_check.SMTCheck¶
Bases:
Search
- build_formula(episode: SearchEpisode, schedule: EncodingSchedule, options: EncodingOptions) Tuple[FNode, FNode] ¶
- expand(problem, episode, options: EncodingOptions, parameter_space, schedule: EncodingSchedule)¶
- search(problem, config: FUNMANConfig | None = None, haltEvent: Event | None = None, resultsCallback: Callable[[ParameterSpace], None] | None = None) SearchEpisode ¶
- solve_formula(s: Solver, formula: FNode, episode) Model | Explanation ¶
- store_smtlib(formula, filename='dbg.smt2')¶
Module contents¶
This subpackage contains the search algorithms used to run FUNMAN. It also defines the representations for episodes (single executions) of one of the search algorithms supported by FUNMAN.