package electrod

  1. Overview
  2. Docs
package electrod
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Ast : sig ... end
module Ast_to_elo : sig ... end
module Atom : sig ... end

Atoms (= urelements).

module Domain : sig ... end

The domain represents the set of relation declarations.

module Elo : sig ... end
module Elo_recursor : sig ... end
module Elo_to_ltl1 : sig ... end

Functor that provides a Elo_to_LTL_intf.S converter given an implementation of LTL

module Elo_to_ltl_intf : sig ... end

Abstract type for a converter from Elo models to (abstract) LTL formulas.

module Elo_to_model1 : sig ... end

Provides a converter from Electrod models to (part of) a solver model.

module Elo_to_smv1 : sig ... end

Provides a transformation from Electrod models to SMV models. Uses enumerations when possible.

module Exp_bounds : sig ... end

Computation of bounds for Ast expressions.

module Fmtc : sig ... end
module Gen_goal : sig ... end

Implements the type for concrete (Raw) and abstract (Ast) syntax trees, before inference of De Bruijn indices and simplification into Elo trees.

module Gen_goal_recursor : sig ... end

Implements a recursor over generic goals (necessary for conversion to LTL).

module Instance : sig ... end

An instance is a set of relations whose value is a fixed tuple set.

module Intf : sig ... end

Defines traits and mixins to use about anywhere.

module Invar_computation : sig ... end

Helpers for sorting formulas into invariants, and other types of formulas

module Location : sig ... end

Locations in a file (issued from the parsing phase).

module Msg : sig ... end

Contains all error messages and error handling stuff.

module Name : sig ... end

Names (of relations for instance).

module Outcome : sig ... end

Represents a result trace (or the absence thereof).

module Parser : sig ... end
module Parser_main : sig ... end

Calls the parser and returns the raw AST.

module Raw : sig ... end

Type for "raw" ASTs yielded by the Electrod parser.

module Raw_ident : sig ... end

Identifiers in "raw" ASTs.

module Raw_to_ast : sig ... end

Tranforms raw ASTs into "massaged" ones (conforming to Elo).

module Relation : sig ... end

Type of relations.

module Scanner : sig ... end
module Scope : sig ... end

Relation scopes.

module Scripts : sig ... end
module Shortnames : sig ... end

Rename set/relations and atoms to short names (to reduce the size of generated files).

module Simplify1 : sig ... end

Simplifies Electrod models.

module Simplify2 : sig ... end

Compared to Simplify1, this version maps qualified relations to formulas relying on cardinality arguments.

module Smv : sig ... end

Represents SMV files and how to produce them

module Smv_trace_parser : sig ... end
module Smv_trace_scanner : sig ... end
module Smv_trace_tokens : sig ... end
module Solver : sig ... end

Abstraction of solver-specific LTL and models wrt any concrete implementation in a given model-checker.

module Symbol : sig ... end

Symbols are hash-consed strings

module Symmetry : sig ... end

A symmetry specifies an order over instantiated relations.

module Transfo : sig ... end

Specification of transformations.

module Tuple : sig ... end

Tuples of atoms.

module Tuple_set : sig ... end

Type for sets of tuples.

module Var : sig ... end

Provides fresh identifiers for variables (in formulas) at every stage.