funman.translate package¶
Submodules¶
funman.translate.bilayer module¶
This module encodes bilayer models into a SMTLib formula.
- pydantic model funman.translate.bilayer.BilayerEncoder¶
Bases:
EncoderThe BilayerEncoder compiles a BilayerModel into a SMTLib formula. The formula defines a series of steps that update a set of variables each step, as defined by a Bilayer model.
Show JSON schema
{ "title": "BilayerEncoder", "description": "The BilayerEncoder compiles a BilayerModel into a SMTLib formula. The\nformula defines a series of steps that update a set of variables each step,\nas defined by a Bilayer model.", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- can_encode()¶
Return boolean indicating if the scenario can be encoded with the FUNMANConfig
- encode_model(model: FunmanModel, time_dependent_parameters=False)¶
Encode the model as an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
- Returns:
formula encoding the model
- Return type:
FNode
- Raises:
Exception – cannot identify encoding timepoints
Exception – cannot encode model type
- encode_observation(scenario: AnalysisScenario, step: int, substitutions={})¶
- model_post_init(context: Any, /) None¶
We need to both initialize private attributes and call the user-defined model_post_init method.
funman.translate.decapode module¶
- pydantic model funman.translate.decapode.DecapodeEncoder¶
Bases:
EncoderShow JSON schema
{ "title": "DecapodeEncoder", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- encode_model(scenario: AnalysisScenario) Encoding¶
Encode a model into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
- Returns:
formula and symbols for the encoding
- Return type:
- model_post_init(context: Any, /) None¶
We need to both initialize private attributes and call the user-defined model_post_init method.
funman.translate.encoded module¶
This module defines enocoders for already encoded models. (Technically, a pass-through that helps make the encoder abstraction uniform.)
- pydantic model funman.translate.encoded.EncodedEncoder¶
Bases:
EncoderAn EncodedEncoder assumes that a model has already been encoded as an EncodedModel, and acts as a noop to maintain consistency with other encoders.
Show JSON schema
{ "title": "EncodedEncoder", "description": "An EncodedEncoder assumes that a model has already been encoded as an\nEncodedModel, and acts as a noop to maintain consistency with other\nencoders.", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- encode_model(model: FunmanModel)¶
Encode the model by returning the already encoded formula.
- Parameters:
model (FunmanModel) – Encoded model
- Returns:
SMTLib formula encoding the model
- Return type:
FNode
- encode_model_layer(scenario: AnalysisScenario, constraint: ModelConstraint, layer_idx: int, options: EncodingOptions, assumptions: List[Assumption])¶
- encode_model_timed(scenario: AnalysisScenario, num_steps: int, step_size: int) Encoding¶
Encode a model into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
num_steps (int) – number of encoding steps (e.g., time steps)
step_size (int) – size of a step
- Returns:
formula and symbols for the encoding
- Return type:
- model_post_init(context: Any, /) None¶
We need to both initialize private attributes and call the user-defined model_post_init method.
funman.translate.encoding module¶
- pydantic model funman.translate.encoding.Encoding¶
Bases:
BaseModelShow JSON schema
{ "title": "Encoding", "type": "object", "properties": {} }
- 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.
- pydantic model funman.translate.encoding.EncodingOptions¶
Bases:
BaseModelEncodingOptions
Show JSON schema
{ "title": "EncodingOptions", "description": "EncodingOptions", "type": "object", "properties": { "schedule": { "$ref": "#/$defs/EncodingSchedule" }, "normalize": { "default": false, "title": "Normalize", "type": "boolean" }, "normalization_constant": { "anyOf": [ { "type": "number" }, { "type": "null" } ], "default": 1.0, "title": "Normalization Constant" } }, "$defs": { "EncodingSchedule": { "properties": { "timepoints": { "items": { "anyOf": [ { "type": "integer" }, { "type": "number" } ] }, "title": "Timepoints", "type": "array" } }, "required": [ "timepoints" ], "title": "EncodingSchedule", "type": "object" } }, "required": [ "schedule" ] }
- Fields:
- field normalization_constant: float | None = 1.0¶
- field normalize: bool = False¶
- field schedule: EncodingSchedule [Required]¶
- pydantic model funman.translate.encoding.FlatEncoding¶
Bases:
BaseModelAn encoding comprises a formula over a set of symbols.
Show JSON schema
{ "title": "FlatEncoding", "description": "An encoding comprises a formula over a set of symbols.", "type": "object", "properties": {}, "additionalProperties": true }
- Config:
arbitrary_types_allowed: bool = True
extra: str = allow
- assume(assumption: FNode)¶
- encoding()¶
- 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.
- symbols()¶
funman.translate.ensemble module¶
- pydantic model funman.translate.ensemble.EnsembleEncoder¶
Bases:
EncoderShow JSON schema
{ "title": "EnsembleEncoder", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- encode_model(scenario: AnalysisScenario) Encoding¶
Encode a model into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
- Returns:
formula and symbols for the encoding
- Return type:
- encode_observation(scenario: AnalysisScenario, step: int, substitutions={})¶
- model_post_init(context: Any, /) None¶
We need to both initialize private attributes and call the user-defined model_post_init method.
- symbol_values(model_encoding: Encoding, pysmtModel: Model) Dict[str, Dict[str, float]]¶
Get the value assigned to each symbol in the pysmtModel.
- Parameters:
model_encoding (Encoding) – encoding using the symbols
pysmtModel (pysmt.solvers.solver.Model) – assignment to symbols
- Returns:
mapping from symbol and timepoint to value
- Return type:
Dict[str, Dict[str, float]]
funman.translate.gromet module¶
funman.translate.petrinet module¶
- pydantic model funman.translate.petrinet.PetrinetEncoder¶
Bases:
EncoderShow JSON schema
{ "title": "PetrinetEncoder", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- encode_model(model: FunmanModel) Encoding¶
Encode a model into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
- Returns:
formula and symbols for the encoding
- Return type:
- encode_observation(scenario: AnalysisScenario, step: int, substitutions={})¶
- model_post_init(context: Any, /) None¶
We need to both initialize private attributes and call the user-defined model_post_init method.
funman.translate.regnet module¶
- pydantic model funman.translate.regnet.RegnetEncoder¶
Bases:
EncoderShow JSON schema
{ "title": "RegnetEncoder", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- encode_model(model: FunmanModel) Encoding¶
Encode a model into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
- Returns:
formula and symbols for the encoding
- Return type:
- model_post_init(context: Any, /) None¶
We need to both initialize private attributes and call the user-defined model_post_init method.
funman.translate.simplifier module¶
- class funman.translate.simplifier.FUNMANSimplifier(env=None)¶
Bases:
Simplifier- approximate(parameters: List[ModelParameter], threshold=0.0001)¶
- arg_magnitude(lb_values: Dict[str, float], ub_values: Dict[str, float])¶
Get the maximum magnitude of formula given the lb/ub of each parameter. Assume that the formula is a polynomial term. Use the ub for the variables in the numerator, and the lb for the variables in the denominator.
- Parameters:
formula (sympy.Formula) – polynomial term to evaluate
lb_values (Dict[str, float]) – lb values for each variable
ub_values (Dict[str, float]) – ub values for each variable
- sympy_simplify(parameters: List[ModelParameter] = [], substitutions: Dict[FNode, FNode] = {}, threshold: float = 0.0001, taylor_series_order=None)¶
- value_of(subs: Dict[str, float] = {}, _lambdify=False)¶
- walk_pow(formula, args, **kwargs)¶
Default function for a node that is not handled by the Walker.
This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.
funman.translate.translate module¶
This module defines the abstract base classes for the model encoder classes in funman.translate package.
- pydantic model funman.translate.translate.DefaultEncoder¶
Bases:
EncoderThe DefaultEncoder will not actually encode a model as SMT. It is used to provide an Encoder for SimulatorModel objects, but the encoder will not be used.
Show JSON schema
{ "title": "DefaultEncoder", "description": "The DefaultEncoder will not actually encode a model as SMT. It is used to provide an Encoder for SimulatorModel objects, but the encoder will not be used.", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- 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.translate.translate.Encoder¶
Bases:
ABC,BaseModelAn Encoder translates a Model into an SMTLib formula.
Show JSON schema
{ "title": "Encoder", "description": "An Encoder translates a Model into an SMTLib formula.", "type": "object", "properties": { "config": { "$ref": "#/$defs/FUNMANConfig" } }, "$defs": { "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" } }, "required": [ "config" ] }
- Config:
arbitrary_types_allowed: bool = True
- Fields:
- field config: FUNMANConfig [Required]¶
- box_to_smt(box: Box, closed_upper_bound: bool = False, infinity_constraints=False)¶
Compile the interval for each parameter into SMT constraints on the corresponding parameter.
- Parameters:
closed_upper_bound (bool, optional) – use closed upper bounds for each interval, by default False
- Returns:
formula representing the box as a conjunction of interval constraints.
- Return type:
FNode
- can_encode()¶
Return boolean indicating if the scenario can be encoded with the FUNMANConfig
- encode_assumed_constraint(encoded_constraint: Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]], constraint: Constraint, assumptions: List[Assumption], options: EncodingOptions, layer_idx: int = 0) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]]¶
- encode_assumption(assumption: Assumption, options: EncodingOptions, layer_idx: int | None = None) FNode¶
- encode_assumptions(assumptions: List[Assumption], options: EncodingOptions) Dict[Assumption, FNode]¶
- encode_constraint(scenario: AnalysisScenario, constraint: Constraint, options: EncodingOptions, layer_idx: int = 0, assumptions: List[Assumption] = []) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]]¶
- encode_init_layer(scenario: AnalysisScenario) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]]¶
- encode_linear_constraint(scenario: AnalysisScenario, constraint: LinearConstraint, layer_idx: int, options: EncodingOptions, assumptions: List[Assumption]) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]] | None¶
- encode_model_layer(scenario: AnalysisScenario, constraint: ModelConstraint, layer_idx: int, options: EncodingOptions, assumptions: List[Assumption]) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]]¶
- encode_model_timed(scenario: AnalysisScenario, num_steps: int, step_size: int) Encoding¶
Encode a model into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
num_steps (int) – number of encoding steps (e.g., time steps)
step_size (int) – size of a step
- Returns:
formula and symbols for the encoding
- Return type:
- encode_parameter(scenario: AnalysisScenario, constraint: ModelConstraint, layer_idx: int, options: EncodingOptions, assumptions: List[Assumption]) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]] | None¶
- encode_query_layer(scenario: AnalysisScenario, constraint: Constraint, layer_idx: int, options: EncodingOptions, assumptions: List[Assumption])¶
Encode a query into an SMTLib formula.
- Parameters:
model (FunmanModel) – model to encode
- Return type:
formula and symbols for the encoding
- encode_timeseries(scenario: AnalysisScenario, constraint: TimeseriesConstraint, layer_idx: int, options: EncodingOptions, assumptions: List[Assumption]) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]] | None¶
- encode_transition_layer(scenario: AnalysisScenario, layer_idx: int, options: EncodingOptions) Tuple[FNode, List[FNode] | Dict[str, Dict[str, FNode]]]¶
- initialize_encodings(scenario, num_steps)¶
- interval_to_smt(p: str, i: Interval, time: int | None = None, infinity_constraints=False) FNode¶
Convert the interval into contraints on parameter p.
- Parameters:
p (funman.representation.parameter.Parameter) – parameter to constrain
closed_upper_bound (bool, optional) – interpret interval as closed (i.e., p <= ub), by default False
- Returns:
formula constraining p to the interval
- Return type:
FNode
- 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.
- parameter_values(model: FunmanModel, pysmtModel: Model) Dict[str, List[float | None]]¶
Gather values assigned to model parameters.
- Parameters:
model (FunmanModel) – model encoded by self
pysmtModel (pysmt.solvers.solver.Model) – the assignment to symbols
- Returns:
mapping from parameter symbol name to value
- Return type:
Dict[str, List[Union[float, None]]]
- set_step_substitutions(schedule: EncodingSchedule, substitutions: Dict[FNode, FNode])¶
- set_time_step_constraints(layer_idx: int, step_size: int | float, c: FNode)¶
- state_timepoint(schedule: EncodingSchedule, layer_idx: int) int¶
- step_size_index(step_size: int) int¶
- substitutions(schedule: EncodingSchedule) Dict[FNode, FNode]¶
- symbol_timeseries(model_encoding, pysmtModel: Model) Dict[str, List[float | None]]¶
Generate a symbol (str) to timeseries (list) of values
- Parameters:
pysmtModel (pysmt.solvers.solver.Model) – variable assignment
- symbol_values(model_encoding: Encoding, pysmtModel: Model) Dict[str, Dict[str, float]]¶
Get the value assigned to each symbol in the pysmtModel.
- Parameters:
model_encoding (Encoding) – encoding using the symbols
pysmtModel (pysmt.solvers.solver.Model) – assignment to symbols
- Returns:
mapping from symbol and timepoint to value
- Return type:
Dict[str, Dict[str, float]]
- time_step_constraints(timepoint: int | float, stepsize: int | float)¶
- pydantic model funman.translate.translate.LayeredEncoding¶
Bases:
BaseModelAn encoding comprises a formula over a set of symbols.
Show JSON schema
{ "title": "LayeredEncoding", "description": "An encoding comprises a formula over a set of symbols.", "type": "object", "properties": {}, "additionalProperties": true }
- Config:
arbitrary_types_allowed: bool = True
extra: str = allow
- assume(assumption: List[FNode], layers=None)¶
- construct_encoding(scenario: AnalysisScenario, constraint, options: EncodingOptions, layers=None, box: Box = None, assumptions: List[Assumption] | None = None) FNode¶
- 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.
- simplify()¶
- substitute(substitutions: Dict[FNode, FNode])¶
- symbols()¶
Module contents¶
The funman.translate package defines how to translate funman.model models into SMTLib format for different analysis scenarios.