sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
electrod 1.0.0
Libraries
This package provides the following libraries (via dune):
electrod.libelectrod
Documentation:
Libelectrod.Ast
Libelectrod.Ast_to_elo
Libelectrod.Atom
Atoms (= urelements).Libelectrod.Domain
The domain represents the set of relation declarations.Libelectrod.Elo
Libelectrod.Elo_recursor
Libelectrod.Elo_to_ltl1
Functor that provides aElo_to_LTL_intf
.S converter given an implementation of LTLLibelectrod.Elo_to_ltl_intf
Abstract type for a converter from Elo models to (abstract) LTL formulas.Libelectrod.Elo_to_model1
Provides a converter from Electrod models to (part of) a solver model.Libelectrod.Elo_to_smv1
Provides a transformation from Electrod models to SMV models. Uses enumerations when possible.Libelectrod.Exp_bounds
Computation of bounds for Ast expressions.Libelectrod.Fmtc
Libelectrod.Gen_goal
Implements the type for concrete (Raw
) and abstract (Ast
) syntax trees, before inference of De Bruijn indices and simplification intoElo
trees.Libelectrod.Gen_goal_recursor
Implements a recursor over generic goals (necessary for conversion to LTL).Libelectrod.Instance
An instance is a set of relations whose value is a fixed tuple set.Libelectrod.Intf
Defines traits and mixins to use about anywhere.Libelectrod.Invar_computation
Helpers for sorting formulas into invariants, and other types of formulasLibelectrod.Location
Locations in a file (issued from the parsing phase).Libelectrod.Msg
Contains all error messages and error handling stuff.Libelectrod.Name
Names (of relations for instance).Libelectrod.Outcome
Represents a result trace (or the absence thereof).Libelectrod.Parser
Libelectrod.Parser_main
Calls the parser and returns the raw AST.Libelectrod.Raw
Type for "raw" ASTs yielded by the Electrod parser.Libelectrod.Raw_ident
Identifiers in "raw" ASTs.Libelectrod.Raw_to_ast
Tranforms raw ASTs into "massaged" ones (conforming to Elo).Libelectrod.Relation
Type of relations.Libelectrod.Scanner
Libelectrod.Scope
Relation scopes.Libelectrod.Scripts
Libelectrod.Shortnames
Rename set/relations and atoms to short names (to reduce the size of generated files).Libelectrod.Simplify1
Simplifies Electrod models.Libelectrod.Simplify2
Compared to Simplify1, this version maps qualified relations to formulas relying on cardinality arguments.Libelectrod.Smv
Represents SMV files and how to produce themLibelectrod.Smv_trace_parser
Libelectrod.Smv_trace_scanner
Libelectrod.Smv_trace_tokens
Libelectrod.Solver
Abstraction of solver-specific LTL and models wrt any concrete implementation in a given model-checker.Libelectrod.Symbol
Symbols are hash-consed stringsLibelectrod.Symmetry
A symmetry specifies an order over instantiated relations.Libelectrod.Transfo
Specification of transformations.Libelectrod.Tuple
Tuples of atoms.Libelectrod.Tuple_set
Type for sets of tuples.Libelectrod.Var
Provides fresh identifiers for variables (in formulas) at every stage.
Dependencies: containers, containers-data, containers.unix, fmt, fmt.tty, gen, hashcons, logs.fmt, mtime.clock.os, printbox, iter, stdcompat, stdlib-shims, ppx_deriving.runtime, visitors.runtime
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page