Module `Libelectrod`Source

Sourcemodule Ast : sig ... end

Sourcemodule Ast_to_elo : sig ... end

Sourcemodule Atom : sig ... end

Atoms (= urelements).

Sourcemodule Domain : sig ... end

The domain represents the set of relation declarations.

Sourcemodule Elo : sig ... end

Sourcemodule Elo_recursor : sig ... end

Sourcemodule Elo_to_ltl1 : sig ... end

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

Sourcemodule Elo_to_ltl_intf : sig ... end

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

Sourcemodule Elo_to_model1 : sig ... end

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

Sourcemodule Elo_to_smv1 : sig ... end

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

Sourcemodule Exp_bounds : sig ... end

Computation of bounds for Ast expressions.

Sourcemodule Fmtc : sig ... end

Sourcemodule 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.

Sourcemodule Gen_goal_recursor : sig ... end

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

Sourcemodule Instance : sig ... end

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

Sourcemodule Intf : sig ... end

Defines traits and mixins to use about anywhere.

Sourcemodule Invar_computation : sig ... end

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

Sourcemodule Location : sig ... end

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

Sourcemodule Msg : sig ... end

Contains all error messages and error handling stuff.

Sourcemodule Name : sig ... end

Names (of relations for instance).

Sourcemodule Outcome : sig ... end

Represents a result trace (or the absence thereof).

Sourcemodule Parser : sig ... end

Sourcemodule Parser_main : sig ... end

Calls the parser and returns the raw AST.

Sourcemodule Raw : sig ... end

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

Sourcemodule Raw_ident : sig ... end

Identifiers in "raw" ASTs.

Sourcemodule Raw_to_ast : sig ... end

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

Sourcemodule Relation : sig ... end

Type of relations.

Sourcemodule Scanner : sig ... end

Sourcemodule Scope : sig ... end

Relation scopes.

Sourcemodule Scripts : sig ... end

Sourcemodule Shortnames : sig ... end

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

Sourcemodule Simplify1 : sig ... end

Simplifies Electrod models.

Sourcemodule Simplify2 : sig ... end

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

Sourcemodule Smv : sig ... end

Represents SMV files and how to produce them

Sourcemodule Smv_trace_parser : sig ... end

Sourcemodule Smv_trace_scanner : sig ... end

Sourcemodule Smv_trace_tokens : sig ... end

Sourcemodule Solver : sig ... end

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

Sourcemodule Symbol : sig ... end

Symbols are hash-consed strings

Sourcemodule Symmetry : sig ... end

A symmetry specifies an order over instantiated relations.

Sourcemodule Transfo : sig ... end

Specification of transformations.

Sourcemodule Tuple : sig ... end

Tuples of atoms.

Sourcemodule Tuple_set : sig ... end

Type for sets of tuples.

Sourcemodule Var : sig ... end

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/index.html

Module `Libelectrod`Source

package electrod

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/index.html

Module LibelectrodSource

Module `Libelectrod`Source