Tutorial

Introduction

This brief tutorial to Electrum is aimed at users already fluent in Alloy.

We also suppose that Electrum Analyzer is already installed.

What is Electrum?

In a nutshell, Electrum is an extension of Alloy with:

1. A keyword ("var") to declare some fields and signature as mutable (i.e. their valuation may vary along time);
2. Connectives from Linear Temporal Logic with Past (PLTL) to express properties of traces;
3. Primed expressions that represent the value of the said expressions in the next instant (so the prime sign is not a valid character for identifiers anymore);
4. Bounded and unbounded model-checking procedures to analyze the resulting specifications.

If you are used to modelling Alloy specifications using the "local state idiom", then the shift is very easy:

1. Relations that were indexed by Time will usually be just tagged var;
2. You need not join variable expression with an expression denoting an instant;
3. You must replace quantifications over time by the corresponding, classic LTL operators (e.g. always, eventually...);
4. Traces are now always infinite sequences of states, hence there is no hypothetical last state of a trace to consider (but it also means that if your specification models a system that may terminate, you must still ensure traces are infinite, otherwise your specification may be inconsistent: we shall see later how to achieve this).

To be continued...