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/Bddd/index.html

Module `Bddd`Source

Bdd Drawer.

Machinery to perform a draw in a bdd.

ZZZ : To be used by Solver only !!

Sourcetype t

Sourceval tbl_to_string : t -> string

Sourceexception No_numeric_solution of t

Source

val draw_in_bdd : 
  t ->
  Var.env_in ->
  Var.env ->
  int ->
  string ->
  Exp.var list ->
  Bdd.t ->
  Bdd.t ->
  t * Var.env * Store.t' * Store.p

draw_in_bdd memory verbose_level ctx_msg state vars bdd comb returns a draw of the Boolean variables as well as a range based and a polyhedron based representation of numeric constraints (cf. the Store module).

Side effect: this is where the solution number tables is filled in.

Raises No_numeric_solution.

Source

val formula_to_bdd : 
  t ->
  Var.env_in ->
  Var.env ->
  string ->
  int ->
  Exp.formula ->
  t * Bdd.t

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

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

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 : t -> t

Sourceval sol_number : t -> Bdd.t -> Sol_nb.sol_nb * Sol_nb.sol_nb

sol_number bdd returns the solution number in the then and else branches of bdd.

package lutin

Install

Dune Dependency

Authors

Maintainers

Sources

doc/lutin/Bddd/index.html

Module BdddSource

Module `Bddd`Source