package electrod
Formal analysis for the Electrod formal pivot language
Install
Authors
Maintainers
Sources
electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2
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: 11 Jan 2021
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.7"
-
ocaml
>= "4.11.0"
Used by
Conflicts
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page