package electrod
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=b2263601350f2ffe3cb1671d8bdd256729986b248c1ec39e84ec76a2f2b8408c
sha512=f4c0e7a196c7a14fff51e7f0cc6f91ed8b3df965523d878ab507320f9771ec69efddb31252ff9763ed2f92bc8c369cea73ca20edebbc3c9ff327fe500f33bdf0
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.
Published: 05 Dec 2020
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.
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.
Copyright and license
(C) 2016-2020 ONERA
electrod is distributed under the terms of the Mozilla Public License v2.0.
See LICENSE.md for more information.
Dependencies (18)
-
visitors
>= "20190513"
- stdlib-shims
- stdcompat
- iter
-
printbox
< "0.6"
- ppx_deriving
-
mtime
< "2.0.0"
- menhir
- logs
- hashcons
- gen
-
fmt
>= "0.8.7"
- containers-data
-
containers
>= "3.0"
- cmdliner
- dune-build-info
-
dune
>= "2.0"
-
ocaml
>= "4.11.0"
Dev Dependencies (1)
-
mdx
with-test
Used by
None
Conflicts
None