package lutin

You can search for identifiers within the package.

in-package search v0.2.0

Lutin: modeling stochastic reactive systems

Install

Dune Dependency

www-verimag.imag.fr Edit opam file Versions (4)

Authors

Maintainers

E

erwan.jahier@univ-grenoble-alpes.fr

Sources

lutin.v2.71.15.tgz

md5=a7da42464f4ad0619bc4e759f2defca3

sha512=2142fe82b22c10f1baaf8591d177f2497c00b93e4f9d92b50e4ff24b34ecbc9d5dc8537efa21c94c09623501a1ef26292cfad36fa12fdde5cbe0add716b9c7cb

doc/lutin/Formula_to_bdd/index.html

Module `Formula_to_bdd`Source

Encoding formula and expressions into bdds.

Sourcetype t

Sourceval init : unit -> t

Sourceval tbl_to_string : t -> string

Sourceval f : t -> Var.env_in -> Var.env -> string -> int -> Exp.formula -> t * Bdd.t

Formula_to_bdd.f input memory ctx_msg verbosity_level f returns the bdd of f where input and pre variables have been repaced by their values. ctx_msg is used for printing source information in case of errors.

ZZZ this function fills in local tables that are used later on during the random toss (e.g., via index_to_linear_constraint). Hence bdd should be build by this module.

Source

val num_to_gne : 
  t ->
  Var.env_in ->
  Var.env ->
  string ->
  int ->
  Exp.num ->
  t * Gne.t

Source

val eval_int_expr : 
  t ->
  Exp.num ->
  string ->
  Var.env_in ->
  Var.env ->
  int ->
  int option

Sourceval clear_all : t -> t

Clean-up all the internal tables that migth have been filled by (non-regression) assertions.

Sourceval clear_step : t -> t

Clean-up the cache tables that contain information that depends on input or pre. Indeed, this information is very likely to change (especially because floats) at each step, therefore we do not keep that information to avoid memory problems.

Sourceval index_to_linear_constraint : t -> int -> Constraint.t

Sourceval get_index_from_linear_constraint : t -> Constraint.t -> int