Index of values

add a representant to take into account

Add a mapping cube->v to trie

Add a mapping cube->v to trie

Add a mapping cube->v to trie without checking for subsomption

Add a mapping cube->v to trie without checking for subsomption

Add a node in the trie

all_constructors () returns a list of all the defined constructors.

same as Variable.all_permutations but does not assume elements of l1 to be distinct.

all_permutations l1 l2 returns all possible substitutions from l1 to l2 assuming that the variables of both lists are distinct.

List of all values mapped by the trie

alpha renaming of process variables

ancestor_of a b returns true if a is an ancestor of b

Efficient application of substitution

returns the conjunction in array form of the associated cube

assign_constr s cstr will add the constraint that the constructor cstr must be in the type of s

assign_var x y will add the constraint that the type of y is a subtype of x (use this function when x := y appear in your program

assume id f adds the formula f to the context of the solver with identifier id.

Clears the context and assumes a goal formula

Same as assume_goal but without the solver check

assume_node n a assumes the negation of a node n given in the form of a renaming a; raises Unsat if the context becomes unsatisfiable

Same as assume_node but without the solver check

Backtracking procedure that uses approximated backward reachability (Bwd).

constructs a variable substitution

candidate n c registers a new candidate c emerging from node n

case_split env returns a list of equalities

this takes a system in input and the list of visited nodes, of which the disjunction constitutes an inductive invariant for the system.

check () runs the solver on its context.

check s n raises Unsafe n if the node n is immediately reachable in the system s, i.e.

check s v returns the tags of nodes in v that were used if s implies the disjunction of the nodes in v.

check s v returns the tags of nodes in v that were used if s implies the disjunction of the nodes in v.

check_guard vars s g checks if the guard g is feasible in state s; raises Unsat if it is not the case

Raises ReachedLimit if the limits given in Options have been exceeded

The stragey used for preforming check-sat.

clear () clears the context of the solver.

close () will compute the smallest type possible for each symbol.

compares x y returns 0 if x and y are equal, and is unspecified otherwise but provides a total ordering on hash-consed strings.

compares two atoms.

compare two nodes with a heuristic to find the most general one.

compare two nodes with a heuristic to find the most general one.

compare_list l1 l2 returns 0 if and only if l1 is equal to l2.

compare_nb_common a t1 t2: compares the "level of proximity" with a.

compare_nb_diff a t1 t2: based on the previous measure, this compares the "level" of difference with a

check if an error trace is spurious due to the Crash Failure Model

All values whose keys (cubes) are not inconsistent with the given cube.

constructors ty returns the list of constructors of ty when type is an enumerated data-type, otherwise returns [].

number of delted nodes

given a cube creates a node with a given kind, and a history

create a cube given its existential variables and a conjunction

create a cube in normal form by finding the quantified variables

declare s [arg_1; ... ; arg_n] out declares a new function symbol with type (arg_1, ... , arg_n) -> out

declare n cstrs declares a new enumerated data-type with name n and constructors cstrs., declare n [] declares a new abstract type with name n.

declared x is true if x is already declared.

delete nb registers nb deletions

Delete all values which satisfy the predicate p

Delete from the trie nodes that are subsumed by the first arguments

array form of set difference

returns the dimension of the associated cube (see Cube.dim)

returns the number of exitential distinct variables, i.e.

easy fixpoint test with subset tests

lifts if-then-else constructs and simplify a cube

lifts if-then-else constructs and simplify a conjunction

the empty ("") hash-consed string.

The empty trie.

A dummy empty environment.

A dummy empty state.

Filled by Murphi.mk_encoding_table

entails f returns true if the context of the solver entails the formula f.

equal x y returns true if x and y are the same hash-consed string (constant time).

print an error trace given a faulty node

Same as Instantiation.relevant but does not performs any checks

The formula which represents false

The formula which represents true

Given a list of candidate invariants, returns the first one that seems to be indeed an invariant.

register the result of a successful fixpoint check

fold f to all values mapped to in the trie.

Returns the time in seconds accumulated in the timer.

get_calls () returns the cumulated number of calls to Smt_sig.S.Solver.check.

get_time () returns the cumulated time spent in the solver in seconds.

get_variants s returns a set of constructors, which is the refined type of s.

Returns a good approximation in the form of a candidate invariant if the oracle was able to find one.

full semantic fixpoint test with SMT solver

has_abstract_type x is true if the type of x is abstract.

returns true if one of the ancestor has been set to deleted

has_infinite_type x is true if the type of x is not finite.

has_type_proc x is true if x has the type of a process identifier.

returns true if the atom contains the variable given in argument

returns true if the atom contains one of the variable given in argument

hash x returns the integer (hash) associated to x.

solve r1 r2, solve the equality r1=r2 and return the substitution

hashcons n f hash-cons the value n using function f i.e.

hashcons n f hash-cons the value n using function f i.e.

is the conjunction of c1 and c2 inconsistent knowing that c1 and c2 are consitent on their own.

same as Cube.inconsistent_2 but for arrays

same as Cube.inconsistent_set but for arrays

returns true if the conjunction inconsistent

init l where l is a list of pairs (s, ty) initializes the type (and associated constructors) of each s to its original type ty.

Initialize the oracle on a given system

instantiate transitions with a list of possible parameters

Encoding of a term in the enumerative environment.

Test emptyness of a trie

is_int x is true if the term x has type int

return true if the symbol is owned by the theory

returns true if the variable is a skolem process #i

is_real x is true if the term x has type real

returns true if the substitution is the identity function

iter f iterates f over all elements of the table .

iter f iterates f over all elements of the table .

Apply f to all values mapped to in the trie.

Apply f to all values whose keys (cubes) are subsumed by the given cube.

Give the leaves of a term of the theory

list_assoc x l returns the element associated with x in the list of pairs l.

list_assoc_inv x l returns the first element which is associated to x in the list of pairs l.

list_equal l1 l2 returns true if and only if l1 is equal to l2.

list_mem x l is true if and only if x is equal to an element of l.

Same as Hstring.list_assoc, but simply returns true if a binding exists, and false if no bindings exist for the given key.

list_mem_couple (x,y) l is true if and only if (x,y) is equal to an element of l.

returns the conjunction of litterals of the associated cube

make s builds ans returns a hash-consed string from s.

make cmb [f_1; ...; f_n] creates the formula (f_1 <cmb> ... <cmb> f_n).

Give a representant of a term of the theory

make_app f l creates the application of function symbol f to a list of terms l.

make_arith op t1 t2 creates the term t1 <op> t2.

make_cnf f returns a conjunctive normal form of f under the form: a list (which is a conjunction) of lists (which are disjunctions) of literals.

make_int n creates an integer constant of value n.

make_lit cmp [t1; t2] creates the literal (t1 <cmp> t2).

make_real n creates an real constant of value n.

functional form of transition

Is cube subsumed by some cube in the trie?

Is cube subsumed by some cube in the trie?

Is cube subsumed by some cube in the trie?

mk_env nb sys creates an environment for the enumerative exploration of the transition system sys with a fixed number nb of processes.

Name of the theory

returns the number of differences, i.e.

Returns the number of digits of a positive integer

returns the negation of the atom

register the treatment of a new node

Called by Mulexer

Returns a new uninitialized state from an enumertive environment

Returns the next free integer that is not used for encoding terms.

Prevent the GC from scanning the list of states stored in the environemnt as it is going to be kept in memory all the time.

puts a cube in normal form, so as to have the existential variables contiguous (#1, #2, #3, ...).

transforms a conjunction if the form of a set of atoms to an equivalent representation with an array

returns the origin of the node, i.e.

Pause the time, i.e.

easy fixpoint test including permutations

Pop the last context from the stack and forget what was done since the last push.

pre-image tau n returns the pre-image of n by the transition relation tau as a disjunction of cubes in the form of two lists of new nodes.

Prints a hash-consed strings on a formatter.

print fmt f prints the formula on the formatter fmt.

print () will output the computed refined types on std_err.

prints the conjunction corresponding to the array of atoms

prints a conjunction

prints an atom

prints a term

prints the cube of a node

prints separating double line

prints the trace corresponding to the history of a node

prints a conjunction on a signle line

prints separating line

Prints a list of hash-consed strings on a formatter.

print_list f sep fmt l prints list l whose elements are printed with f, each of them being separated by the separator sep.

prints a complete report.

Printing a state.

print_system p a fmt sys prints the system sys in Murphi's syntax with p processes and infinite types abstracted with the subrange [1;a].

prints section title for stats

predefinied list of skolem variables #1, #2, #3, ...

Same as check but only uses the SMT solver.

Push the current context on a stack.

reached vars s1 s2 raises Unsat if s2 has not been reached

Register the given state as an explored state in the environment.

relevant ~of_cube:a ~to_cube:b returns the list of relevant instantiations of the quantifiers of b for the test exists i1,... b => exists z1,... a.

outputs number of remaining nodes in the queues given a function to count them.

Register bad candidates and try to infer as much inforamtion as possible from the error trace before the restart.

Replays the history of a faulty node and returns (possibly) an error trace

Report location on formatter

Reset the parameters of the GC to its default values.

resisters a backtrack and restart

Runs the SMT solver on its current context

search procs init performs enumerative forward search.

Backward reachability search on a system.

set_arith false deactivates the theory of arithmetic (true by default).

set_cc false deactivates congruence closure algorithm (true by default).

Changes garbage collector parameters limit its effect

set_sum false deactivates the theory of enumerated data types (true by default).

simplify a cube.

simplify a conjunction.

simplify_atoms_base b c simplifies c in the context of b.

returns the size of the associated cube (see Cube.size)

returns the number of atoms in the conjuction

Returns the (heuristically) computed size of tables needed for the exploration.

Given a list of candidate approximations (and their permutations), checks if one is satisfiable on the finite model constructed by search.

check if the history of a node is spurious

check if an error trace is spurious due to the Crash Failure Model

check if an error trace is spurious

Start (or restart) recording user time when this function is called.

Return statistics on the table.

Return statistics on the table.

subset a b returns true if the elements of a are a subsets of the elements contained in b.

returns true if the set of litterals of the cube associated with the first arguement is a subset of the second argument

apply a variable substitution to a variable

Apply the substitution given in argument to the conjunction

Apply the substitution given in argument to the atom.

Apply the substitution given in argument to the term

apply a substitution on a cube

Captures the output of a unix command

Captures the standard and error output of a unix command with its exit status

Types an untyped system and performs subtyping analysis is the flag Options.subtyping is true.

t_false is the boolean term false

t_true is the boolean term true

returns the set of atoms corresponding to the conjuntion encoded in the array

return true if it can be immediately said that the atom in the first argument implies the second

The type of booleans

The type of integers

type_of x returns the type of x.

returns the type of the term as it is known by the SMT solver

The type processes (identifiers)

The type of reals

put a universal guard in disjunctive normal form

in fact concatenation, equivalent to taking the conjunctions of two conjunctinos

Checks if the node is directly reachable on init of the system

return true when the argument is an unsolvable function of the theory

Returns the cube instances that were useful in proving the fixpoint.

returns the existential variables of the given conjunction

returns the existential variables of the given atom

returns the existential variables of the given term

returns the variables of the associated cube

same as variables but only return skolemized variables of the form #i

same as variables but only return skolemized variables of the form #i

same as variables but only return skolemized variables of the form #i

view hs returns the string corresponding to hs.

Width of the virtual terminal (80 if cannot be detected)

returns true if the substitution is well formed, i.e.