From b42b49fac038ad93d9d8c261783c36743c9dc8cf Mon Sep 17 00:00:00 2001 From: David Chemouil Date: Wed, 7 Feb 2018 17:30:51 +0100 Subject: [PATCH 1/3] Update README.md Change name for ONERA. Add instructions for the version with actions. --- README.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 40438f48..fa99b8cc 100755 --- a/README.md +++ b/README.md @@ -1,14 +1,16 @@ # Electrum -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 the [Institute for Systems and Computer Engineering, Technology and Science](https://www.inesctec.pt/en) 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. + +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/). ## Building Electrum -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 +Electrum 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,6 +22,12 @@ 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 From d73a4c6fd5891d5151e1c3f168d02d29f3b7daef Mon Sep 17 00:00:00 2001 From: Nuno Macedo Date: Wed, 7 Feb 2018 22:45:48 +0000 Subject: [PATCH 2/3] Update README.md --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index fa99b8cc..a9fed300 100755 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -# 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 [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. +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. @@ -8,9 +8,9 @@ Electrum is open-source and available under the [MIT license](LICENSE), as is th 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/). -## Building Electrum +## Building Electrum Analyzer -Electrum 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 +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 @@ -30,7 +30,7 @@ If you wish to build it, repeat the steps above, just replacing `-b master` in t ## 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` @@ -46,7 +46,7 @@ This will launch Electrum's/Alloy Analyzer's simple GUI, which is packaged with ## 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 From 99a2b8e5b47f696ea8481baa30c4b1e73c81a3f4 Mon Sep 17 00:00:00 2001 From: Nuno Macedo Date: Thu, 8 Feb 2018 09:33:19 +0000 Subject: [PATCH 3/3] Update README.md --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index a9fed300..4e69e0ef 100755 --- a/README.md +++ b/README.md @@ -44,6 +44,11 @@ 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)