package electrod

  1. Overview
  2. Docs

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 Source code locations (ranges of positions), used in parsetree.
  • Raw_ident Identifiers in "raw" ASTs.
  • Var Provides fresh identifiers for variables (in formulas) at every stage.
  • Symbol A symbol identifies a constant provided by either:
  • 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.
OCaml

Innovation. Community. Security.