electrod
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.
sha256=e5d2278c99128621110cd015dafcbcae9792bbf2c8bb09d7b02c57d50fa28075
sha512=e08ecf720d35b6ee72f37d780cc3da22f61e22314ffd093ff3314fb89684b863b5c96c97375d48bcb4ba2838ec8f61a495105c989f292c5dbcd095e14f52bdba
>= "20190513"
< "0.6"
with-test
>= "0.8.7"
>= "2.8" & < "3.0"
>= "2.0"
>= "4.05.0"