package electrod

  1. Overview
  2. Docs

Abstraction of solver-specific LTL and models wrt any concrete implementation in a given model-checker.

module type ATOMIC_PROPOSITION = sig ... end

Abstract type for atomic propositions of LTL.

module type LTL = sig ... end

Abstract type of LTL (contains past connectives as well as basic counting capabilities).

module LTL_from_Atomic (At : ATOMIC_PROPOSITION) : LTL with module Atomic = At

Builds an LTL implementation out of an implementation of atomicic propositions.

type script_type =
  1. | Default of string
  2. | File of string
module type MODEL = sig ... end
OCaml

Innovation. Community. Security.