package electrod
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=d89ca19e0c33ca8e2fe19a73eef46a0618387c6c29ddf70789ee61108b4733c7
md5=d0b7fd750762a63cb9e914cbebb972ae
README.md.html
electrod - Formal analysis for the Electrod formal specification language
0.1.6
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.
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.