package electrod

  1. Overview
  2. Docs
Formal analysis for the Electrod formal specification language

Install

Dune Dependency

Authors

Maintainers

Sources

electrod-0.1.4.tbz
sha256=894ae9e2b88ee853b8ff632d6c93a072e1b10cf46bfc8cd05230b6986ff1532a
md5=7be3cb47a6c3d254a7db2f1aaaeb19b1

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 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.

Copyright and license

(C) 2016-2018 ONERA

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

See LICENSES.md for more information.

Published: 01 Feb 2018

README

electrod - Formal analysis for the Electrod formal specification language

0.1.4

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.

Copyright and license

(C) 2016-2018 ONERA

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

See LICENSES.md for more information.

Dependencies (17)

  1. visitors
  2. sequence >= "0.5"
  3. printbox < "0.6"
  4. ppx_deriving
  5. ppx_blob
  6. mtime
  7. menhir < "20211128"
  8. logs
  9. hashcons
  10. gen
  11. fmt < "0.8.7"
  12. containers >= "2.0" & < "3.0"
  13. cmdliner >= "1.0.2"
  14. ppxfind build
  15. jbuilder >= "1.0+beta9"
  16. ocamlfind build
  17. ocaml >= "4.04"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.