electrod

AuthorsDavid Chemouil and Julien Brunel
LicenseMPL-2.0
Homepagehttps://github.com/grayswandyr/electrod/
Issue Trackerhttps://github.com/grayswandyr/electrod/issues
MaintainerDavid Chemouil <david.chemouil+git@onera.fr>
Dependencies
&cmdliner>= 1.0.2
containers>= 2.0
fmt
gen
hashcons
jbuilder>= 1.0+beta20
logs
menhir
mtime
ppx_expect
ppx_inline_test
ppxfind
printbox
sequence
visitors>= 20180513
Availableocaml-version >= "4.04"
PublishedMay 23, 2018
Source [http] https://github.com/grayswandyr/electrod/releases/download/0.1.7/electrod-0.1.7.tbz
4a88e818d658569b86577905c8e9d97d
StatisticsInstalled 2 times last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/electrod/electrod.0.1.7/opam

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 Electrod compiles the model to a problem for a solver (currently the NuSMV and nuXmv tools) to produce example or counter-example traces.

Electrod is mainly meant to be used as a backend for the Electrum Analyzer.

See the file INSTALL.md for building and installation instructions.

Home page

External dependencies

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

Running

Electrod is primarily aimed at being called by external, more abstract 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-2018 ONERA

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

See LICENSES.md for more information.

No package is dependent