package electrod

Not available on OCaml 5.5
  1. Overview
  2. Docs
Formal analysis for the Electrod formal pivot language

Install 

dune-project
 Dependency

github.com Readme Changelog MPL-2.0 License Edit opam file Versions (3)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2

Description

Electrod is a model finder inspired by Kodkod. It takes as input a model expressed in a mixture of relational first-order logic (RFOL) over bounded domains and linear temporal logic (LTL) over an unbounded time horizon. Then it compiles the model to a problem for a solver (currently the NuSMV and nuXmv tools) to produce example or counter-example traces. Electrod is primarily meant to be used as a backend for the Electrum formal method and tool.

Added to opam-repository:

README

electrod - Formal analysis for the Electrod formal specification language

Electrod is a model finder inspired by Kodkod. It takes as input a model expressed in a mixture of relational first-order logic (RFOL) over bounded domains and linear temporal logic (LTL) over an unbounded time horizon. Then it compiles the model to a problem for a solver (currently the NuSMV and nuXmv model-checkers). Electrod is mainly meant to be used as a backend for the Electrum Analyzer.

Github homepage

ONERA homepage

Installation instructions

Installation has only been tested on GNU/Linux and Mac OS X. It may not work on MS Windows.

The easiest way to install Electrod is to rely on the Opam OCaml package manager.

opam update
opam upgrade 
opam install electrod

After installation, you will see a program called "electrod" in your PATH.

External dependencies

As of now, Electrod relies on NuSMV (2.6+) or nuXmv (2.0+), so you must at least install one of them.

Running

Electrod is primarily aimed at being called by external tools such as the Electrum Analyzer.

However, it can also be run as a standalone tool by calling the electrod program. Type electrod --help to get some help on options.

(C) 2016-2020 ONERA

electrod is distributed under the terms of the Mozilla Public License v2.0.

See LICENSE.md for more information.

Dev Dependencies (2)

  1. odoc with-doc
  2. mdx with-test

Optional Dependencies

None

Used by

None

Conflicts

None

Build status

Results of building electrod with each compiler on check.ci.ocaml.org, run of against opam-repository 8a77e58. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
1.0.0 (this version) good n/a n/a n/a n/a
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure