OCaml logo

lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module Exp
type ext_func_name = string
type ext_func_type = Type.t list
type ext_lib_name = string
type t =
| Formu of formula
| Numer of num
| Liste of simple_tbl(*

struct and arrays are flattened in such a list

*)
and formula =
| And of formula * formula
| Or of formula * formula
| Xor of formula * formula
| NXor of formula list
| Nor of formula list
| Diese of formula list
| Impl of formula * formula
| IteB of formula * formula * formula
| Not of formula
| EqB of formula * formula
| True
| False
| Bvar of var
| Eq of num * num
| Sup of num * num
| SupEq of num * num
| Inf of num * num
| InfEq of num * num
and var = t Var.t
and func_call_arg = string * Ezdl.cfunc * ext_func_type * ext_lib_name * t list
and num =
| Sum of num * num
| Diff of num * num
| Prod of num * num
| Quot of num * num
| Mod of num * num
| Div of num * num
| Uminus of num
| Inf_int
| Ival of Num.num
| Fval of float
| Ivar of var
| Fvar of var
| FFC of func_call_arg
| IFC of func_call_arg
| Gcont of num * num * num
| Gstop of num * num * num
| Icont of num * num * num
| Istop of num * num * num
| Ite of formula * num * num
and simple =
| Fo of formula
| Nu of num
and simple_tbl = simple Util.StringMap.t
val ext_func_tbl_to_string : ext_func_tbl -> string
type weight =
| Wint of int
| Wexpr of num
| Infinity

A weight can be an integer, or a integer expression that depends only on inputs and memories.

val weight_to_string : weight -> string
type var_tbl = var Util.StringMap.t
val add_value : string -> simple -> simple_tbl -> simple_tbl
val add_var : string -> var -> var_tbl -> var_tbl
val empty_var_tbl : var Util.StringMap.t
val empty_simple_tbl : simple Util.StringMap.t
val remove_prefix : string -> string -> string -> string

remove from a string everything that is before the first "." or the first "". This is useful to go to var_tbl indexes (which depends on the var name) to simple_tbl indexes (which depend only on the type).