electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
Module Libelectrod . Solver
module type ATOMIC_PROPOSITION = sig ... end

Abstract type for atomic propositions of LTL.

module type LTL = sig ... end

Abstract type of LTL (contains pElo 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 =
| Default of string
| File of string
module type MODEL = sig ... end