electrod 0.1.4

Libraries

This package provides the following libraries (via ocamlobjinfo):

electrod.libelectrod

Documentation:

• Fmtc Contains pretty-printing facilities. Note: same licence as Fmt.
• Intf Defines traits and mixins to use about anywhere.
• Location Locations in a file (issued from the parsing phase).
• Raw_ident Identifiers in "raw" ASTs.
• Var Provides fresh identifiers for variables (in formulas) at every stage.
• Symbol Symbols are hash-consed strings
• Atom Atoms (= urelements).
• Tuple Tuples of atoms.
• TupleSet Type for sets of tuples.
• Transfo Specification of transformations.
• Name Names (of relations for instance).
• Symmetry
• Instance An instance is a set of relations whose value is a fixed tuple set.
• Scope Relation scopes.
• Relation Type of relations.
• Domain The domain represents the set of relation declarations.
• GenGoal
• Elo Definition of the type for Electrod models.
• Outcome Represents a result trace (or the absence thereof).
• Solver Abstraction of solver-specific LTL and models wrt any concrete implementation in a given model-checker.
• Msg Contains all error messages and error handling stuff.
• Simplify1 Simplifies Electrod models.
• Simplify2 Compared to Simplify1, this version maps qualified relations to formulas relying on cardinality arguments.
• Raw Type for "raw" ASTs yielded by the Electrod parser.
• Parser
• Scanner
• SMV_trace_tokens
• SMV_trace_scanner
• SMV_trace_parser
• SMV Represents SMV files and how to produce them
• Raw_to_elo Tranforms raw ASTs into "massaged" ones (conforming to Elo).
• Parser_main Calls the parser and returns the raw AST.
• Invar_computation
• GenGoalRecursor Implements a recursor over generic goals (necessary for conversion to LTL).
• Exp_bounds Computation of bounds for Elo expressions.
• Elo_to_LTL_intf Abstract type for a converter from Elo models to (abstract) LTL formulas.
• Elo_to_model1 Provides a converter from Electrod models to (part of) a solver model.
• Elo_to_LTL1 Functor that provides a Elo_to_LTL_intf.S converter given an implementation of LTL
• Elo_to_SMV1 Provides a transformation from Electrod models to SMV models. Uses enumerations when possible.