diff --git a/README.md b/README.md index 40438f48..4e69e0ef 100755 --- a/README.md +++ b/README.md @@ -1,14 +1,16 @@ -# Electrum +# Electrum Analyzer -This extension to the Alloy Analyzer by the [Institute for Systems and Computer Engineering, Technology and Science](https://www.inesctec.pt/en) and the [French Aerospace Lab](https://www.onera.fr/en) provides an analyzer for Electrum models, a temporal extension to the Alloy modeling language. +This extension to the Alloy Analyzer by [INESC TEC](https://www.inesctec.pt/en) (the Institute for Systems and Computer Engineering, Technology and Science) and [ONERA](https://www.onera.fr/en) (the French aerospace research center) provides an analyzer for Electrum models, a temporal extension to the Alloy modeling language. [Alloy](http://alloy.mit.edu/) is a simple structural modeling language based on first-order logic developed at the [Software Design Group](http://sdg.csail.mit.edu/). Its Analyzer can generate instances of invariants, simulate the execution of operations, and check user-specified properties of a model. -Electrum is open-source and available under the [MIT license](LICENSE), as is the Alloy Analyzer. However, it utilizes several third-party packages whose code may be distributed under a different license (see the various LICENSE files in the distribution for details), including [Kodod](https://github.com/emina/kodkod)'s extension [Pardinus](https://github.com/nmacedo/Pardinus) and its underlying solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose/Syrup](http://www.labri.fr/perso/lsimon/glucose/), [(P)Lingeling](http://fmv.jku.at/lingeling/), and [Yices](http://yices.csl.sri.com)), as well as [CUP](http://www2.cs.tum.edu/projects/cup/) and [JFlex](http://jflex.de/) to generate the parser. Electrum can also perform analyses on an unbounded time horizon: in this case, one needs to install the [Electrod program](https://github.com/grayswandyr/electrod/) too. +Electrum is open-source and available under the [MIT license](LICENSE), as is the Alloy Analyzer. However, it utilizes several third-party packages whose code may be distributed under a different license (see the various LICENSE files in the distribution for details), including [Kodod](https://github.com/emina/kodkod)'s extension [Pardinus](https://github.com/nmacedo/Pardinus) and its underlying solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose/Syrup](http://www.labri.fr/perso/lsimon/glucose/), [(P)Lingeling](http://fmv.jku.at/lingeling/), and [Yices](http://yices.csl.sri.com)), as well as [CUP](http://www2.cs.tum.edu/projects/cup/) and [JFlex](http://jflex.de/) to generate the parser. -## Building Electrum +Electrum can also perform analyses on an unbounded time horizon: in this case, one needs to install the [Electrod](https://github.com/grayswandyr/electrod/) program as well as [NuSMV](http://nusmv.fbk.eu/) or [nuXmv](https://nuxmv.fbk.eu/). -Electrum needs Java 8 and can be built using Maven. The script will also build Kodkod/Pardinus, which uses the [Waf](https://github.com/waf-project/waf) build +## Building Electrum Analyzer + +The Electrum Analyzer requires Java 8 and can be built using Maven. The script will also build Kodkod/Pardinus, which uses the [Waf](https://github.com/waf-project/waf) build system, which requires Python 2.5 or later, and needs a C/C++ compiler for the underlying solvers. * Clone the Electrum repository, as well as Pardinus' as a submodule @@ -20,9 +22,15 @@ system, which requires Python 2.5 or later, and needs a C/C++ compiler for the u `$ mvn clean package -DskipTests` +## Prototype: Electrum with actions + +An [extension of Electrum](https://github.com/haslab/Electrum/releases/tag/v1.0-actions), with actions, is currently under study. + +If you wish to build it, repeat the steps above, just replacing `-b master` in the first line by `-b actions`. + ## Running -[Download](https://github.com/nmacedo/Electrum/releases/tag/v1.0) the executable ``jar`` (or [build](#building-electrum) it) and launch it simply as +[Download](https://github.com/nmacedo/Electrum/releases/tag/v1.0) the executable ``jar`` (or [build](#building-electrum-analyzer) it) and launch it simply as `$ java -jar electrum-1.0.0-gui.jar` @@ -36,9 +44,14 @@ This will launch Electrum's/Alloy Analyzer's simple GUI, which is packaged with - Denis Kuperberg, TU Munich, Germany - Eduardo Pessoa, HASLab, INESC TEC & Universidade do Minho, Portugal +## ERTMS Case Study +ERTMS models developed in response to the ABZ 2018 call for case study submissions: +* Electrum [model](http://haslab.github.io/Electrum/ertms.ele) and [theme](http://haslab.github.io/Electrum/ertms.thm) +* Alloy [model](http://haslab.github.io/Electrum/ertms.als) and [theme](http://haslab.github.io/Electrum/ertms_als.thm) + ## History ### Electrum [1.0.0](https://github.com/nmacedo/Electrum/releases/tag/v1.0) (January 2018) - + - First stable public release - Common interface for temporal relational model finding problems through Pardinus - Bounded and unbounded model checking of Electrum models