electrod 0.4.1

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 a Elo_to_LTL_intf.S converter given an implementation of LTL
• Libelectrod.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 into Elo 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 formulas
• Libelectrod.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 them
• Libelectrod.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 strings
• Libelectrod.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, ppx_inline_test.config, ppx_inline_test.runtime-lib