Module Model

module Model: sig .. end
Term or lambda expression

module MIL: Map.S  with type key = int list
type value = 
| Term of Term.t
| Lambda of Term.lambda
| Map of Term.t MIL.t
Term or lambda expression
type t = value Var.VarHashtbl.t 
A model is a list of variables and assignemnts
type path = value list StateVar.StateVarHashtbl.t 
A path is a map of state variables to assignments
val equal_value : value -> value -> bool
Equality over values of model
val path_offset : Numeral.t
Offset of the variables at each step of a path.
val pp_print_value : ?as_type:Type.t -> Format.formatter -> value -> unit
Pretty-print a value
val pp_print_value_xml : ?as_type:Type.t -> Format.formatter -> value -> unit
Pretty-print a value in xml format
val pp_print_model : Format.formatter -> t -> unit
Pretty-print a model
val pp_print_path : Format.formatter -> path -> unit
Pretty-print a path
val create : int -> t
Create a model of the given size
val create_path : int -> path
Create a path of the given size
val import_value : value -> value
Import a variable assignment from a different instance
val of_list : (Var.t * value) list -> t
Create a model of an association list
val to_list : t -> (Var.t * value) list
Return an association list with the assignments in the model
val path_to_list : path -> (StateVar.t * value list) list
Return an association list with the assignments in the model
val path_of_list : (StateVar.t * value list) list -> path
Create a model of an association list
val path_of_term_list : (StateVar.t * Term.t list) list -> path
Create a model of an association list
val path_from_model : StateVar.t list -> t -> Numeral.t -> path
Convert a model to a path

path_from_model s m k extracts from the model m a path of values for each of the state variables in s from the offset zero up to k. The lists of values for each state variable are of equal length. Values that are not defined in the model are filled with TermLib.default_of_type.

val path_length : path -> int
Return the length of the value paths

All value paths are of equal lengths.

val model_at_k_of_path : path -> Numeral.t -> t
Extract values at instant k from the path and return a model
val models_of_path : path -> t list
Return a list of models, one for each step on the path
val exists_on_path : (t -> bool) -> path -> bool
Return true if the predicate p applies at one step of the path
val for_all_on_path : (t -> bool) -> path -> bool
Return true if the predicate p applies at each step of the path
val bump_var : Numeral.t -> t -> t
Add k to offset of all variables in model
val set_var_offset : Numeral.t -> t -> t
Set offset of all variables in model to k
val merge : t -> t -> t
Combine assignments of two models into one. If a variable has an assignment in both models, it gets the assignment in the second model.
val bump_and_merge : Numeral.t -> t -> t -> t
Combine assignments of two models into one as in Model.merge, but bump the variables in the second model by the given offset before merging.
val dimension_of_map : Term.t MIL.t -> int list
Returns the bounds / dimension of the array value represented by the map in the model