package electrod

You can search for identifiers within the package.

in-package search v0.2.0

package electrod

electrod
- Library electrod.libelectrod
  - Libelectrod
    
    Ast
    
    Ast_to_elo
    
    E
    
    Atom
    
    Domain
    
    Elo
    
    map
    
    fold
    
    Elo_recursor
    
    recursor
    
    Elo_to_ltl1
    
    G
    
    TS
    
    Make
    
    environment
    
    converter
    
    Elo_to_ltl_intf
    
    S
    
    Elo_to_model1
    
    S
    
    Make
    
    Elo_to_smv1
    
    SMV_atom
    
    SMV_LTL
    
    Atomic
    
    Infix
    
    SMV_file_format
    
    Elo_to_SMV_LTL
    
    environment
    
    converter
    
    Elo_to_SMV_model
    
    Exp_bounds
    
    Fmtc
    
    Dump
    
    Gen_goal
    
    map
    
    fold
    
    Gen_goal_recursor
    
    recursor
    
    Instance
    
    Intf
    
    Print
    
    S
    
    Mixin
    
    COMPARE
    
    Invar_computation
    
    Location
    
    Msg
    
    Location
    
    LoggingSetup
    
    M
    
    Extract
    
    Fatal
    
    Warn
    
    Name
    
    Map
    
    Outcome
    
    Parser
    
    Parser_main
    
    Raw
    
    Raw_ident
    
    Raw_to_ast
    
    Relation
    
    Scanner
    
    Scope
    
    Scripts
    
    Shortnames
    
    Simplify1
    
    TS
    
    L
    
    simplify
    
    Simplify2
    
    TS
    
    simplify
    
    Smv
    
    Make_SMV_LTL
    
    Atomic
    
    Infix
    
    Make_SMV_file_format
    
    Smv_trace_parser
    
    Make
    
    Smv_trace_scanner
    
    Smv_trace_tokens
    
    Solver
    
    ATOMIC_PROPOSITION
    
    LTL
    
    Atomic
    
    Infix
    
    LTL_from_Atomic
    
    Atomic
    
    Infix
    
    MODEL
    
    Symbol
    
    Symmetry
    
    Transfo
    
    Tuple
    
    Set
    
    Tuple_set
    
    Var
- Sources
  - electrod.libelectrod
    
    Ast.ml
    
    Ast_to_elo.ml
    
    Atom.ml
    
    Domain.ml
    
    Elo.ml
    
    Elo_recursor.ml
    
    Elo_to_ltl1.ml
    
    Elo_to_ltl_intf.ml
    
    Elo_to_model1.ml
    
    Elo_to_smv1.ml
    
    Exp_bounds.ml
    
    Fmtc.ml
    
    Gen_goal.ml
    
    Gen_goal_recursor.ml
    
    Instance.ml
    
    Intf.ml
    
    Invar_computation.ml
    
    Location.ml
    
    Msg.ml
    
    Name.ml
    
    Outcome.ml
    
    Parser.ml
    
    Parser_main.ml
    
    Raw.ml
    
    Raw_ident.ml
    
    Raw_to_ast.ml
    
    Relation.ml
    
    Scanner.ml
    
    Scope.ml
    
    Scripts.ml
    
    Shortnames.ml
    
    Simplify1.ml
    
    Simplify2.ml
    
    Smv.ml
    
    Smv_trace_parser.ml
    
    Smv_trace_scanner.ml
    
    Smv_trace_tokens.ml
    
    Solver.ml
    
    Symbol.ml
    
    Symmetry.ml
    
    Transfo.ml
    
    Tuple.ml
    
    Tuple_set.ml
    
    Var.ml
    
    libelectrod.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Libelectrod.Smv`Source

Represents SMV files and how to produce them

Sourceval nuXmv_default_script : string

Sourceval nuSMV_default_script : string

Sourceval nuXmv_default_bmc_script : string

Sourceval nuSMV_default_bmc_script : string

Source

module Make_SMV_LTL
  (At : Solver.ATOMIC_PROPOSITION) : 
  Solver.LTL with module Atomic = At

Given an implementation for atoms, provides a LTL implementation with a pretty printing function for Solver formulas.

Source

module Make_SMV_file_format
  (Ltl : Solver.LTL) : 
  Solver.MODEL with type ltl = Ltl.t and type atomic = Ltl.Atomic.t

TODO: implement abstract file format functions

package electrod

Module Libelectrod.SmvSource

Module `Libelectrod.Smv`Source