Struct biodivine_sketchbook::sketchbook::model::ModelState

pub struct ModelState {
    variables: HashMap<VarId, Variable>,
    regulations: HashSet<Regulation>,
    update_fns: HashMap<VarId, UpdateFn>,
    uninterpreted_fns: HashMap<UninterpretedFnId, UninterpretedFn>,
    layouts: HashMap<LayoutId, Layout>,
    placeholder_variables: HashSet<VarId>,
}

Object representing the state of the model in the Boolean network editor. The model encompasses variables, regulations, uninterpreted functions, update functions, and layout information.

ModelState can be observed/edited using its classical Rust API, as well as through the external events (as it implements the SessionState event).

Fields

variables: HashMap<VarId, Variable>

regulations: HashSet<Regulation>

update_fns: HashMap<VarId, UpdateFn>

uninterpreted_fns: HashMap<UninterpretedFnId, UninterpretedFn>

layouts: HashMap<LayoutId, Layout>

placeholder_variables: HashSet<VarId>

Implementations

impl ModelState

Methods for converting between ModelState and BooleanNetwork (from the lib-param-bn).

fn to_bn_with_options( &self, regulation_types: bool, parameters: bool, update_fns: bool, extra_vars: Option<Vec<String>>, ) -> Result<BooleanNetwork, String>

Internal function to convert the ModelState into a variant of BooleanNetwork with specified information to be included.

By default, all variables and regulations are included. You can choose the following:

• regulation_types: include types of regulations
• parameters: include all parameters for uninterpreted functions
• update_fns: include all update functions
• extra_vars: additional extra variables (with no update fns, no regulations)

It is up to you to make the selection reasonable (e.g., when including update functions that contain parameters, you must also include parameters, and so on…).

pub fn to_empty_bn(&self) -> BooleanNetwork

Convert the ModelState into the corresponding “default” BooleanNetwork object. The resulting BN covers the variables and regulations, but it has empty update functions, and does not cover any parameters.

pub fn to_empty_bn_with_params(&self) -> BooleanNetwork

Convert the ModelState into the corresponding “default” BooleanNetwork object with added parameters. The resulting BN covers the variables, parameters, and regulations, but it has empty update functions.

pub fn to_fake_bn_with_params(&self, num_variables: usize) -> BooleanNetwork

Generate a BooleanNetwork with a only given number of “placeholder” (fake) variables. These variables will be named var0, var1, …

The resulting BN will normally contain all uninterpreted functions (parameters) of this model. There will be no regulations, and update functions will be empty.

This is useful for parsing FnUpdate objects describing syntactic trees of uninterpreted functions.

pub fn to_bn(&self) -> BooleanNetwork

Convert the ModelState into the corresponding BooleanNetwork object (that will contain all of the variables, regulations, update functions, and uninterpreted functions.

Note that currently the BooleanNetwork class does not support all features of the ModelState (such as various regulation types or details of uninterpreted functions) – these will be lost during the conversion.

pub fn to_bn_with_plain_regulations( &self, extra_vars: Option<Vec<String>>, ) -> BooleanNetwork

Convert the ModelState into the corresponding BooleanNetwork object (that will contain all of the variables, (plain) regulations, update functions, and uninterpreted functions). However, the types of regulations (both monotonicity and essentiality) are ignored, and instead used as unspecified.

This might be useful if we want to process regulation types later via static properties.

You can add optional extra variables (extra_vars). These will have no update fns or regulations.

impl ModelState

pub fn from_bn(bn: &BooleanNetwork) -> Result<Self, String>

Convert the ModelState into the corresponding BooleanNetwork object (that will contain all of the variables, regulations, update functions, and uninterpreted functions).

Annotations for both variables and functions are let empty. See ModelState::from_reg_graph for details on how regulations and variables are handled.

A name of parameters used in BooleanNetwork (which should be unique) is used as both its ID and name in the resulting ModelState.

impl ModelState

Methods for converting between ModelState and RegulatoryGraph (from the lib-param-bn).

pub fn to_reg_graph(&self, extra_vars: Option<Vec<String>>) -> RegulatoryGraph

Extract the regulatory graph (RegulatoryGraph object) from the ModelState. Sorted variable IDs of the ModelState are used for variable names in RegulatoryGraph.

The conversion might loose some information, as the RegulatoryGraph does not support all the variants of Monotonicity and Essentiality. See also bn_utils::sign_to_monotonicity.

Note that we can convert the resulting RegulatoryGraph back, but the conversion loses some information, like the original variable names and layout information. Also, all of the other model components, such as update functions or uninterpreted functions are not part of the RegulatoryGraph.

You can add optional extra variables (extra_vars).

pub fn to_reg_graph_with_unspecified_regs( &self, extra_vars: Option<Vec<String>>, ) -> RegulatoryGraph

Extract the regulatory graph (RegulatoryGraph object) from the ModelState. Sorted variable IDs of the ModelState are used for variable names in RegulatoryGraph.

The types of regulations (their essentiality and monotonicity) are ignored, and unspecified versions are used instead.

This might be useful in inference, if we want to process regulation types later via static properties.

You can add optional extra variables (extra_vars).

fn _to_reg_graph( &self, include_reg_types: bool, extra_vars: Option<Vec<String>>, ) -> RegulatoryGraph

Internal utility to extract the regulatory graph (RegulatoryGraph object) from the ModelState. Sorted variable IDs of the ModelState are used for variable names in RegulatoryGraph.

There are two modes based on include_reg_types argument. If it is set to true, the types of regulations (their essentiality and monotonicity) are preserved. If it is set to false, they are ignored, and unspecified versions are used instead.

You can add optional extra variables (extra_vars).

pub fn from_reg_graph(reg_graph: &RegulatoryGraph) -> Result<ModelState, String>

Convert the RegulatoryGraph into the corresponding ModelState instance. A name of the variable used in RegulatoryGraph (which should be unique) is used as both its ID and name in the resulting ModelState.

Note that only the default layout (all nodes at 0,0) is created for the ModelState. Variables’ annotations are left empty.

impl ModelState

Methods for safely constructing or mutating instances of ModelState.

These methods focus on general manipulation with variables/regulations. See below for API focusing on layout manipulation.

pub fn new_empty() -> ModelState

Create a new ModelState that does not contain any Variables, Uninterpreted Functions, or Regulations yet. It contains a single empty default Layout.

pub fn new_from_model_data(model_data: &ModelData) -> Result<ModelState, String>

Create a new ModelState given a corresponding ModelData instance.

pub fn new_from_vars(variables: Vec<(&str, &str)>) -> Result<ModelState, String>

Create new ModelState using provided variable ID-name pairs, both strings. All variables have default (empty) update functions. Result will contain no UninterpretedFns or Regulations, and a single default Layout.

The IDs must be unique valid identifiers. The names might be same as the IDs. It also might be empty or non-unique. The variable annotations are left empty.

Return Err in case the IDs are not unique.

pub fn add_var( &mut self, var_id: VarId, name: &str, annot: &str, ) -> Result<(), String>

Add a new variable with given var_id and name to this ModelState. The variable will receive a default “empty” update function.

The ID must be valid identifier that is not already used by some other variable. The names might be same as the ID. It also might be empty or non-unique.

Returns Err in case the id is already being used.

pub fn add_var_by_str( &mut self, id: &str, name: &str, annot: &str, ) -> Result<(), String>

Add a new variable with given id and name to this ModelState. The variable will receive a default “empty” update function.

The ID must be valid identifier that is not already used by some other variable. The names might be same as the ID. It also might be empty or non-unique.

Returns Err in case the id is not a valid identifier or if it is already being used.

pub fn add_multiple_variables( &mut self, id_name_pairs: Vec<(&str, &str)>, ) -> Result<(), String>

Shorthand to add a list of new variables with given string IDs and names to this ModelState.

Each ID must be valid identifier that is not already used by some other variable. The names might be same as the ID. It also might be empty or non-unique. Variable annotations are left empty.

Returns Err in case some id is already being used.

pub fn add_uninterpreted_fn( &mut self, fn_id: UninterpretedFnId, name: &str, arguments: Vec<FnArgument>, expression: &str, annot: &str, ) -> Result<(), String>

Add a new uninterpreted fn given by its components.

pub fn add_empty_uninterpreted_fn( &mut self, fn_id: UninterpretedFnId, name: &str, arity: usize, ) -> Result<(), String>

Add a new uninterpreted fn with given id, name and arity to this ModelState. Note that constraints regarding monotonicity or essentiality must be added separately.

The ID must be valid identifier that is not already used by some other uninterpreted fn. Returns Err in case the id is already being used.

pub fn add_empty_uninterpreted_fn_by_str( &mut self, id: &str, name: &str, arity: usize, ) -> Result<(), String>

Add a new uninterpreted fn with given string id, name, and arity to this ModelState.

The ID must be valid identifier that is not already used by some other uninterpreted fn. Returns Err in case the id is already being used.

pub fn add_multiple_uninterpreted_fns( &mut self, id_name_arity_tuples: Vec<(&str, &str, usize)>, ) -> Result<(), String>

Shorthand to add a list of new uninterpreted fns, each with a string ID, name, and arity, to this ModelState. Details (incl. annotations) for these functions are left empty.

Each ID must be valid identifier that is not already used by some other uninterpreted fns. Returns Err in case the id is already being used.

pub fn add_regulation( &mut self, regulator: VarId, target: VarId, essential: Essentiality, regulation_sign: Monotonicity, ) -> Result<(), String>

Add a new Regulation to this ModelState.

Returns Err when one of the variables is invalid, or the regulation between the two variables already exists.

pub fn add_regulation_by_str( &mut self, regulation_str: &str, ) -> Result<(), String>

Add a new Regulation to this ModelState using a string representation. The variables in the given string must be valid ID strings for this ModelState.

Returns Err when the string does not encode a valid regulation, if the provided variables are not valid variable IDs, or when the regulation between the two variables already exists.

pub fn add_multiple_regulations( &mut self, regulations: Vec<&str>, ) -> Result<(), String>

Shorthand to add a list of new Regulations given by their string encoding to this ModelState. The variables in the given string must be valid ID strings for this ModelState.

Returns Err when the string does not encode a valid regulation, if the provided variables are not valid variable IDs, or when the regulation between the two variables already exists.

pub fn set_raw_var( &mut self, var_id: &VarId, var_data: Variable, ) -> Result<(), String>

Set the raw variable data for a variable var_id.

pub fn set_raw_function( &mut self, fn_id: &UninterpretedFnId, fn_data: UninterpretedFn, ) -> Result<(), String>

Set the raw uninterpreted function data for a function fn_id.

pub fn set_var_name(&mut self, var_id: &VarId, name: &str) -> Result<(), String>

Set the name of a network variable given by id var_id. The name does not have to be unique, as multiple variables might share a name.

Note that you don’t have to rename anything else in the network, since all other structures reference variables with ids.

pub fn set_var_name_by_str( &mut self, id: &str, name: &str, ) -> Result<(), String>

Set the name of a network variable given by string id.

The name does not have to be unique, as multiple variables might share a name.

pub fn set_var_annot( &mut self, var_id: &VarId, annot: &str, ) -> Result<(), String>

Set the annotation of a network variable given by id var_id.

pub fn set_var_annot_by_str( &mut self, id: &str, annot: &str, ) -> Result<(), String>

Set the annotation of a network variable given by id var_id.

pub fn set_var_id( &mut self, original_id: &VarId, new_id: VarId, ) -> Result<(), String>

Set the id of variable with original_id to new_id.

Note that this operation may be costly as it affects several components of the state.

pub fn set_var_id_by_str( &mut self, original_id: &str, new_id: &str, ) -> Result<(), String>

Set the id of variable given by string original_id to new_id.

Note that this operation may be costly as it affects several components.

pub fn remove_var(&mut self, var_id: &VarId) -> Result<(), String>

Remove the network variable with given var_id from this ModelState. This also removes the variable from all Layouts, removes its UpdateFn and all Regulations where this variable figures.

Returns Err in case the var_id is not a valid variable’s identifier, or if some update function depends on it.

pub fn remove_var_by_str(&mut self, id: &str) -> Result<(), String>

Remove the network variable with given var_id from this ModelState. This also removes the variable from all Layouts, removes its UpdateFn and all Regulations where this variable figures.

Returns Err in case the var_id is not a valid variable’s identifier.

pub fn set_uninterpreted_fn_name( &mut self, fn_id: &UninterpretedFnId, name: &str, ) -> Result<(), String>

Set the name of an uninterpreted fn given by id fn_id.

pub fn set_uninterpreted_fn_name_by_str( &mut self, id: &str, name: &str, ) -> Result<(), String>

Set the name of an uninterpreted fn given by string id.

pub fn set_fn_annot( &mut self, fn_id: &UninterpretedFnId, annot: &str, ) -> Result<(), String>

Set annotation of an uninterpreted fn given by id fn_id.

pub fn set_fn_annot_by_str( &mut self, id: &str, annot: &str, ) -> Result<(), String>

Set annotation of an uninterpreted fn given by string id.

pub fn set_uninterpreted_fn_arity( &mut self, fn_id: &UninterpretedFnId, arity: usize, ) -> Result<(), String>

Set arity of an uninterpreted fn given by id fn_id.

In order to change arity of a function symbol, it must not currently be used in any update/uninterpreted function’s expression (because in expressions, it is used on a fixed number of arguments).

pub fn set_uninterpreted_fn_arity_by_str( &mut self, id: &str, arity: usize, ) -> Result<(), String>

Set the arity of an uninterpreted fn given by string id.

pub fn increment_fn_arity( &mut self, fn_id: &UninterpretedFnId, ) -> Result<(), String>

Increment the arity of an uninterpreted fn given by id fn_id. Basically adds a defualt argument (with unknown monotonicity/essentiality) at the end of the function’s arg list.

pub fn decrement_fn_arity( &mut self, fn_id: &UninterpretedFnId, ) -> Result<(), String>

Decrement the arity of an uninterpreted fn given by id fn_id. Basically drops the last argument of the function. The last argument must not be used in function’s expression.

pub fn set_uninterpreted_fn_expression( &mut self, fn_id: &UninterpretedFnId, expression: &str, ) -> Result<(), String>

Set expression of an uninterpreted fn given by id fn_id.

pub fn set_uninterpreted_fn_expression_by_str( &mut self, id: &str, expression: &str, ) -> Result<(), String>

Set expression of an uninterpreted fn given by string id.

pub fn set_uninterpreted_fn_essentiality( &mut self, fn_id: &UninterpretedFnId, essentiality: Essentiality, index: usize, ) -> Result<(), String>

Set essentiality of an argument of given uninterpreted fn (on provided index).

pub fn set_uninterpreted_fn_essentiality_by_str( &mut self, id: &str, essentiality: Essentiality, index: usize, ) -> Result<(), String>

Set essentiality of an argument of given uninterpreted fn (on provided index).

pub fn set_uninterpreted_fn_monotonicity( &mut self, fn_id: &UninterpretedFnId, monotonicity: Monotonicity, index: usize, ) -> Result<(), String>

Set monotonicity of an argument of given uninterpreted fn (on provided index).

pub fn set_uninterpreted_fn_monotonicity_by_str( &mut self, id: &str, monotonicity: Monotonicity, index: usize, ) -> Result<(), String>

Set monotonicity of an argument of given uninterpreted fn (on provided index).

pub fn set_uninterpreted_fn_all_args( &mut self, fn_id: &UninterpretedFnId, fn_arguments: Vec<FnArgument>, ) -> Result<(), String>

Set constraints on all arguments of given uninterpreted fn.

pub fn set_uninterpreted_fn_all_args_by_str( &mut self, id: &str, fn_arguments: Vec<FnArgument>, ) -> Result<(), String>

Set constraints on all arguments of given uninterpreted fn.

pub fn set_uninterpreted_fn_id( &mut self, original_id: &UninterpretedFnId, new_id: UninterpretedFnId, ) -> Result<(), String>

Set the id of an uninterpreted fn with original_id to new_id.

Note that this operation may be costly as it affects several components of the state.

pub fn set_uninterpreted_fn_id_by_str( &mut self, original_id: &str, new_id: &str, ) -> Result<(), String>

Set the id of an uninterpreted fn given by string original_id to new_id.

pub fn remove_uninterpreted_fn( &mut self, fn_id: &UninterpretedFnId, ) -> Result<(), String>

Remove the uninterpreted fn with given fn_id from this ModelState. Note that this uninterpreted fn must not be used in any update fn.

Also returns Err in case the fn_id is not a valid uninterpreted fn’s identifier or if some update/uninterpreted function depends on it.

pub fn remove_uninterpreted_fn_by_str(&mut self, id: &str) -> Result<(), String>

Remove the uninterpreted_fn with given string id from this ModelState. Note that this uninterpreted_fn must not be used in any update fn.

Also returns Err in case the fn_id is not a valid uninterpreted_fn’s identifier.

pub fn remove_regulation( &mut self, regulator: &VarId, target: &VarId, ) -> Result<(), String>

Remove a Regulation pointing from regulator to target from this ModelState.

Returns Err when one of the variables is invalid, or the regulation between the two variables does not exist.

pub fn remove_regulation_by_str( &mut self, regulation_str: &str, ) -> Result<(), String>

Remove a Regulation given by regulation_str from this ModelState. The variables in the regulation_str must be valid ID strings for this ModelState.

Returns Err when one of the variables is invalid, or the regulation between the two variables does not exist.

pub fn change_regulation_sign( &mut self, regulator: &VarId, target: &VarId, new_sign: &Monotonicity, ) -> Result<(), String>

Shorthand to change sign of a Regulation pointing from regulator to target. Currently it basically removes the regulation, and adds a new one with the new sign.

Returns Err when one of the variables is invalid

pub fn change_regulation_essentiality( &mut self, regulator: &VarId, target: &VarId, new_essentiality: &Essentiality, ) -> Result<(), String>

Shorthand to change essentiality of a Regulation pointing from regulator to target. Currently it basically removes the regulation, and adds a new one with the new essentiality value.

Returns Err when one of the variables is invalid

pub fn set_update_fn( &mut self, var_id: &VarId, expression: &str, ) -> Result<(), String>

Set update function for a given variable to a provided expression.

pub fn set_multiple_update_fns( &mut self, update_functions: Vec<(&str, &str)>, ) -> Result<(), String>

Set update functions for multiple variables (given ID-function pairs). The IDs must be unique valid identifiers.

fn add_placeholder_vars_if_needed(&mut self, arity: usize)

(internal) Utility method to add as many placeholder variables as is required by an addition (or update) of an uninterpreted fn of given arity.

fn remove_placeholder_vars_if_needed(&mut self)

(internal) Utility method to remove as many placeholder variables as is required after a removal (or update) of an uninterpreted fn.

fn add_default_update_fn(&mut self, var_id: VarId) -> Result<(), String>

(internal) Utility method to add a default update fn for a given variable.

fn remove_all_regulations_var(&mut self, variable: &VarId) -> Result<(), String>

(internal) Remove all Regulations where variable figures (as either regulator or target) from this ModelState. Returns Err when the variable is invalid.

impl ModelState

Several utility methods to manipulate with layouts.

pub fn add_layout_simple( &mut self, layout_id: LayoutId, name: &str, ) -> Result<(), String>

Add a new Layout with given layout_id and name to this ModelState. The layout will contain nodes for all model’s variables, all of them located at a default position.

Returns Err if layout_id is already being used for some other Layout.

pub fn add_or_update_layout_raw( &mut self, id: LayoutId, layout: Layout, ) -> Result<(), String>

Add a new (pre-generated) Layout with given id to this ModelState, or update existing if the id is already used. The layout must contain nodes for exactly all model’s variables.

pub fn add_layout_copy( &mut self, layout_id: LayoutId, name: &str, template_layout_id: &LayoutId, ) -> Result<(), String>

Add a new Layout with given layout_id and name to this ModelState. The layout will be a direct copy of another existing layout given by id template_layout_id.

Returns Err if layout_id is already being used for some other Layout in this ModelState, or if template_layout_id does not exist.

pub fn remove_layout(&mut self, layout_id: &LayoutId) -> Result<(), String>

Remove a Layout with given layout_id from this ModelState. Default layout can not be deleted.

Returns Err in case the id is not a valid identifier in this ModelState.

pub fn remove_layout_by_str(&mut self, id: &str) -> Result<(), String>

Remove a Layout with given id from this ModelState.

Returns Err in case the id is not a valid identifier in this ModelState.

pub fn update_position( &mut self, layout_id: &LayoutId, var_id: &VarId, px: f32, py: f32, ) -> Result<(), String>

Update position of a node for variable var_id in layout layout_id.

Returns Err in case one of the ids is not a valid for this ModelState.

fn insert_to_layout( &mut self, var_id: VarId, layout_id: &LayoutId, ) -> Result<(), String>

(internal) Utility method to add a variable node to a given layout. The node is inserted to a default position x=0,y=0.

fn insert_to_default_layout(&mut self, var_id: VarId) -> Result<(), String>

(internal) Shorthand method for adding a variable node to a default layout. The node is inserted to a default position x=0,y=0.

fn insert_to_all_layouts(&mut self, var_id: VarId) -> Result<(), String>

(internal) Shorthand method for adding a variable node to all layouts. The node is always inserted to a default position x=0,y=0.

fn remove_from_all_layouts(&mut self, var_id: &VarId) -> Result<(), String>

(internal) Utility method to remove a variable node from all layouts.

impl ModelState

Several utility methods to assert (non-)existence of variables/regulations/layouts in the current state.

fn assert_no_regulation( &self, regulator: &VarId, target: &VarId, ) -> Result<(), String>

(internal) Utility method to ensure there is no regulation between the two variables yet.

fn assert_no_variable(&self, var_id: &VarId) -> Result<(), String>

(internal) Utility method to ensure there is no variable with given Id yet.

fn assert_valid_variable(&self, var_id: &VarId) -> Result<(), String>

(internal) Utility method to ensure there is a variable with given Id.

fn assert_no_uninterpreted_fn( &self, fn_id: &UninterpretedFnId, ) -> Result<(), String>

(internal) Utility method to ensure there is no uninterpreted_fn with given Id yet.

fn assert_valid_uninterpreted_fn( &self, fn_id: &UninterpretedFnId, ) -> Result<(), String>

(internal) Utility method to ensure there is a uninterpreted fn with given Id.

fn assert_no_layout(&self, layout_id: &LayoutId) -> Result<(), String>

(internal) Utility method to ensure there is no layout with given Id yet.

fn assert_valid_layout(&self, layout_id: &LayoutId) -> Result<(), String>

(internal) Utility method to ensure there is a layout with given Id.

fn assert_fn_not_used_in_expressions( &self, fn_id: &UninterpretedFnId, ) -> Result<(), String>

(internal) Utility method to ensure that an uninterpreted function is not used in any expressions (corresponding to any update function or any uninterpreted function).

impl ModelState

Methods for safely generating valid instances of identifiers for the current ModelState.

pub fn generate_var_id( &self, ideal_id: &str, start_index: Option<usize>, ) -> VarId

Generate valid VarId that’s currently not used by any variable in this ModelState.

First, the given ideal_id or its transformation by replacing invalid characters are tried. If they are both invalid (non-unique), a numerical identifier is added at the end. By specifying start_index, the index search starts directly at that number (e.g., when ideal ID is “var” and start index is 3, search for ID starts with “var_3”, “var_4”, …)

Warning: Do not use this to pre-generate more than one id at a time, as the process is deterministic and might generate the same IDs. Always generate an Id, add that variable to the model, and then repeat for other variables.

pub fn generate_layout_id( &self, ideal_id: &str, start_index: Option<usize>, ) -> LayoutId

Generate valid LayoutId that’s currently not used by layouts in this ModelState.

First, the given ideal_id or its transformation by replacing invalid characters are tried. If they are both invalid (non-unique), a numerical identifier is added at the end. By specifying start_index, the index search starts directly at that number (e.g., when ideal ID is “l” and start index is 3, search for ID starts with “l_3”, “l_4”, …)

Warning: Do not use this to pre-generate more than one id at a time, as the process is deterministic and might generate the same IDs. Always generate an Id, add that layout to the model, and then repeat for other layouts.

pub fn generate_uninterpreted_fn_id( &self, ideal_id: &str, start_index: Option<usize>, ) -> UninterpretedFnId

Generate valid UninterpretedFnId that’s currently not used by uninterpreted_fns in this ModelState.

First, the given ideal_id or its transformation by replacing invalid characters are tried. If they are both invalid (non-unique), a numerical identifier is added at the end. By specifying start_index, the index search starts directly at that number (e.g., when ideal ID is “fn” and start index is 3, search for ID starts with “fn_3”, “fn_4”, …)

Warning: Do not use this to pre-generate more than one id at a time, as the process is deterministic and might generate the same IDs. Always generate an Id, add that fn to the model, and then repeat for other fns.

impl ModelState

Some basic utility methods for inspecting the ModelState.

pub fn num_vars(&self) -> usize

The number of variables in this ModelState.

pub fn num_uninterpreted_fns(&self) -> usize

The number of uninterpreted_fns in this ModelState.

pub fn num_layouts(&self) -> usize

The number of layouts in this ModelState.

pub fn num_regulations(&self) -> usize

The number of regulations in this ModelState.

pub(crate) fn num_placeholder_vars(&self) -> usize

The number of placeholder variables in this ModelState.

pub fn is_valid_var_id(&self, var_id: &VarId) -> bool

Check if there is a variable with given Id.

pub(crate) fn is_valid_placeholder_var_id(&self, var_id: &VarId) -> bool

Check if there is a placeholder variable with given Id.

pub fn is_valid_var_id_str(&self, id: &str) -> bool

Check if the given id corresponds to some variable’s valid Id.

pub fn is_valid_uninterpreted_fn_id(&self, fn_id: &UninterpretedFnId) -> bool

Check if there is a uninterpreted fn with given Id.

pub fn is_valid_uninterpreted_fn_id_str(&self, id: &str) -> bool

Check if the given id corresponds to some uninterpreted fn’s valid Id.

pub fn is_valid_layout_id(&self, layout_id: &LayoutId) -> bool

Check if there is a layout with given Id.

pub fn is_valid_layout_id_str(&self, id: &str) -> bool

Check if the given id corresponds to some layout’s valid Id.

pub fn get_var_id(&self, id: &str) -> Result<VarId, String>

Return a valid variable’s VarId corresponding to the given str id.

Return Err if such variable does not exist (and the ID is invalid).

pub(crate) fn get_placeholder_var_id(&self, id: &str) -> Result<VarId, String>

Return a valid placeholder variable’s VarId corresponding to the given str id.

Return Err if such variable does not exist (and the ID is invalid).

pub fn get_variable(&self, var_id: &VarId) -> Result<&Variable, String>

Return a Variable corresponding to a given VarId.

Return Err if such variable does not exist (the ID is invalid in this context).

pub fn get_uninterpreted_fn_id( &self, id: &str, ) -> Result<UninterpretedFnId, String>

Return a valid uninterpreted fn’s UninterpretedFnId corresponding to the given str id.

Return Err if no such uninterpreted fn exists (and the ID is invalid).

pub fn get_uninterpreted_fn( &self, fn_id: &UninterpretedFnId, ) -> Result<&UninterpretedFn, String>

Return a UninterpretedFn corresponding to a given UninterpretedFnId.

Return Err if no such uninterpreted fn exists (the ID is invalid in this context).

pub fn get_uninterpreted_fn_arity( &self, fn_id: &UninterpretedFnId, ) -> Result<usize, String>

Return arity of a UninterpretedFn corresponding to a given UninterpretedFnId.

Return Err if no such uninterpreted fn exists (the ID is invalid in this context).

pub fn get_uninterpreted_fn_annot( &self, fn_id: &UninterpretedFnId, ) -> Result<&str, String>

Return annotation of a UninterpretedFn corresponding to a given UninterpretedFnId.

Return Err if no such uninterpreted fn exists (the ID is invalid in this context).

pub fn get_var_name(&self, var_id: &VarId) -> Result<&str, String>

Shortcut to return a name of the variable corresponding to a given VarId.

Return Err if such variable does not exist (the ID is invalid in this context).

pub fn get_var_annotation(&self, var_id: &VarId) -> Result<&str, String>

Shortcut to return an annotation of the variable corresponding to a given VarId.

Return Err if such variable does not exist (the ID is invalid in this context).

pub fn get_regulation( &self, regulator: &VarId, target: &VarId, ) -> Result<&Regulation, String>

Find a Regulation between two variables if it exists.

Return Err if one of variable ids is invalid or the regulation does not exist.

pub fn get_regulation_by_str( &self, reg: &str, target: &str, ) -> Result<&Regulation, String>

Shorthand to find a Regulation between two variables (specified by strings) if it exists.

Return Err if one of variable ids is invalid or the regulation does not exist.

pub fn get_layout(&self, id: &LayoutId) -> Result<&Layout, String>

Return a Layout corresponding to the given LayoutId.

Return Err if the LayoutId is invalid.

pub fn get_default_layout(&self) -> &Layout

Return a default Layout.

pub fn get_layout_id(&self, id: &str) -> Result<LayoutId, String>

Return a valid layout’s LayoutId corresponding to the Id given by a String.

Return Err if such variable does not exist (and the ID is invalid).

pub fn get_layout_name(&self, id: &LayoutId) -> Result<&String, String>

Shorthand for getting a string name of a layout.

pub fn get_node_position( &self, layout_id: &LayoutId, var_id: &VarId, ) -> Result<&NodePosition, String>

Shorthand for getting a position of a node for given variable in a given layout.

pub fn regulators(&self, target: &VarId) -> Result<Vec<&VarId>, String>

Return a sorted list of variables that regulate the given target variable.

pub fn targets(&self, regulator: &VarId) -> Result<Vec<&VarId>, String>

Return a sorted list of variables that are regulated by the given regulator variable.

pub fn get_update_fn(&self, var_id: &VarId) -> Result<&UpdateFn, String>

Get an update function for the given variable.

pub fn get_update_fn_string(&self, var_id: &VarId) -> Result<&str, String>

Get an update function’s expression for the given variable.

pub fn get_vars_with_empty_update(&self) -> Vec<&str>

Get a list of variables with “empty” update function. Returned list contains string ID of each such variable

pub fn is_var_contained_in_updates(&self, var_id: &VarId) -> bool

Check whether variable is used in any update function’s expressions. This is important in case we want to safely delete it.

We expect valid var id here.

pub fn variables(&self) -> VariableIterator<'_>

Return an iterator over all variables (with IDs) of this model.

pub fn update_fns(&self) -> UpdateFnIterator<'_>

Return an iterator over all update functions (with corresponding var IDs) of this model.

pub fn uninterpreted_fns(&self) -> UninterpretedFnIterator<'_>

Return an iterator over all uninterpreted_fns (with IDs) of this model.

pub fn regulations(&self) -> RegulationIterator<'_>

Return an iterator over all regulations of this model.

pub fn layouts(&self) -> LayoutIterator<'_>

Return an iterator over all layouts (with IDs) of this model.

pub fn get_default_layout_id() -> LayoutId

Static fn to get LayoutId of the default layout (same for all ModelStates).

pub fn get_default_layout_name() -> &'static str

Static fn to get name of the default layout (same for all ModelStates).

impl ModelState

Implementation for events related to layouts of the model.

pub(super) fn perform_layout_event( &mut self, event: &Event, at_path: &[&str], ) -> Result<Consumed, DynError>

Perform events related to layouts component of this ModelState.

pub(super) fn event_add_layout( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new layout component to this ModelState.

pub(super) fn event_modify_layout( &mut self, event: &Event, at_path: &[&str], layout_id: LayoutId, ) -> Result<Consumed, DynError>

Perform event of modifying or removing existing layout component of this ModelState.

impl ModelState

Implementation for events related to regulations of the model.

pub(super) fn perform_regulation_event( &mut self, event: &Event, at_path: &[&str], ) -> Result<Consumed, DynError>

Perform events related to regulations component of this ModelState.

pub(super) fn event_add_regulation( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new regulation component to this ModelState.

This breaks the event down into two of them, one to make corresponding property, and the other to make the regulation itself.

pub(super) fn event_add_regulation_raw( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new regulation component to this ModelState.

This version is only adding the raw regulation, and not the corresponding static property. It is expected that event_add_regulation is called first, handling the actual division into this event + event for adding the property.

pub(super) fn event_modify_regulation( &mut self, event: &Event, at_path: &[&str], regulator_id: VarId, target_id: VarId, ) -> Result<Consumed, DynError>

Perform event of modifying or removing existing regulation component of this ModelState.

impl ModelState

Implementation for events related to uninterpreted functions of the model.

pub(super) fn perform_uninterpreted_fn_event( &mut self, event: &Event, at_path: &[&str], ) -> Result<Consumed, DynError>

Perform events related to uninterpreted fns component of this ModelState.

pub(super) fn event_add_uninterpreted_fn( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new uninterpreted fn component to this ModelState. This variant assumes that ID, arity (and so on) were already given.

For now, it is assumed that new functions have no constraints (monotonicity, essentiality, or expression).

pub(super) fn event_add_default_uninterpreted_fn( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new “default” uninterpreted fn component to this ModelState.

The field values will be newly generated or predefined (“default”) constants will be used. Particularly, new ID will be generated, the same string will be used for its name, and arity will be zero. Default function symbols also have no constraints (monotonicity, essentiality, or expression).

pub(super) fn event_modify_uninterpreted_fn( &mut self, event: &Event, at_path: &[&str], fn_id: UninterpretedFnId, ) -> Result<Consumed, DynError>

Perform event of modifying or removing existing uninterpreted fn component of this ModelState.

impl ModelState

Implementation for events related to variables of the model.

pub(super) fn perform_variable_event( &mut self, event: &Event, at_path: &[&str], ) -> Result<Consumed, DynError>

Perform events related to variables component of this ModelState.

pub(super) fn event_add_variable( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new variable component to this ModelState. This expects that the variable was already defined elsewhere (i.e., its ID and other fields are already known).

This event will be broken into sub-events (raw addition of the variable, and re-positioning).

pub(super) fn event_add_default_variable( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new variable component to this ModelState.

The field values will be generated or predefined (“default”) constants will be used. New ID will be generated, the same string will be used for its name, and variable will have empty update function.

This event will be broken into sub-events (raw addition of the variable, and re-positioning).

pub(super) fn event_add_variable_raw( &mut self, event: &Event, ) -> Result<Consumed, DynError>

Perform event of adding a new variable component to this ModelState. This is an atomic event (only adds variable, already expects layout positioning to happen elsewhere).

pub(super) fn event_modify_variable( &mut self, event: &Event, at_path: &[&str], var_id: VarId, ) -> Result<Consumed, DynError>

Perform event of modifying or removing existing variable component of this ModelState.

impl ModelState

Implementation for refresh (getter) events.

pub(super) fn refresh_whole_model( &self, full_path: &[String], ) -> Result<Event, DynError>

Get a whole model.

pub(super) fn refresh_variables( &self, full_path: &[String], ) -> Result<Event, DynError>

Get a list of all variables.

pub(super) fn refresh_uninterpreted_fns( &self, full_path: &[String], ) -> Result<Event, DynError>

Get a list of all uninterpreted fns.

pub(super) fn refresh_regulations( &self, full_path: &[String], ) -> Result<Event, DynError>

Get a list of all regulations.

pub(super) fn refresh_layouts( &self, full_path: &[String], ) -> Result<Event, DynError>

Get a list of all layouts (just basic information like IDs and names).

pub(super) fn refresh_layout_nodes( &self, full_path: &[String], at_path: &[&str], ) -> Result<Event, DynError>

Get a list with all nodes in a specified layout.

Trait Implementations

impl Clone for ModelState

fn clone(&self) -> ModelState

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ModelState

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ModelState

fn default() -> ModelState

Default model object with no Variables, Uninterpreted Functions, or Regulations yet. It contains a single empty default Layout.

impl Manager for ModelState

fn generate_id<T>( &self, ideal_id: &str, is_taken: &dyn Fn(&Self, &T) -> bool, num_indices: usize, start_index: Option<usize>, ) -> T

where T: FromStr, <T as FromStr>::Err: Debug,

Generate an ID of type T for a certain component of a manager (e.g., generate a VariableId for a Variable in a ModelState).

fn assert_ids_unique_and_used<T>( &self, id_list: &Vec<&str>, assert_id_is_managed: &dyn Fn(&Self, &T) -> Result<(), String>, ) -> Result<(), String>

where T: Eq + Hash + Debug + FromStr, <T as FromStr>::Err: Debug,

Check that the list of (typesafe or string) IDs contains only unique IDs (no duplicates), and check that all of the IDs are already managed by the manager instance (this is important, for instance, when we need to change already existing elements).

fn assert_ids_unique_and_new<T>( &self, id_list: &Vec<&str>, assert_id_is_new: &dyn Fn(&Self, &T) -> Result<(), String>, ) -> Result<(), String>

where T: Eq + Hash + Debug + FromStr, <T as FromStr>::Err: Debug,

Check that the list of (typesafe or string) IDs contains only unique IDs (no duplicates), and check that all of the IDs are NOT yet managed by the manager instance, i.e., they are fresh new values (this is important, for instance, when we need to add several new elements).

impl PartialEq for ModelState

fn eq(&self, other: &ModelState) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl SessionHelper for ModelState

fn starts_with<'a, 'b>( prefix: &str, at_path: &'a [&'b str], ) -> Option<&'a [&'b str]>

A utility function which checks if at_path starts with a specific first segment. If yes, returns the remaining part of the path.

fn matches(expected: &[&str], at_path: &[&str]) -> bool

A utility function which checks if at_path is exactly

fn invalid_path_error_generic<T>(at_path: &[&str]) -> Result<T, DynError>

A utility function which emits a generic “invalid path” error.

fn invalid_path_error_specific<T>( path: &[&str], component: &str, ) -> Result<T, DynError>

A utility function which emits a “invalid path” error mentioning specific state’s component.

fn clone_payload_str(event: &Event, component: &str) -> Result<String, DynError>

A utility function to get and clone a payload of an event. Errors if payload is empty.

fn assert_path_length( path: &[&str], length: usize, component: &str, ) -> Result<(), DynError>

A utility function to assert that path has a given length, or emit a DynError otherwise.

fn assert_payload_empty(event: &Event, component: &str) -> Result<(), DynError>

A utility function to assert that payload is empty - otherwise, DynError is emitted.

impl SessionState for ModelState

fn perform_event( &mut self, event: &Event, at_path: &[&str], ) -> Result<Consumed, DynError>

Modify the session state using the provided event. The possible outcomes are described by Consumed.

fn refresh( &self, full_path: &[String], at_path: &[&str], ) -> Result<Event, DynError>

“Read” session state into an event without modifying it.

impl StructuralPartialEq for ModelState