Electrum

Electrum mode extends Forge with temporal operators to ease specification and checking of dynamic systems. This mode draws heavily on the Electrum work by INESC TEC and ONERA, but there are differences.

To enable Electrum mode, pass option problem_type temporal to Forge. This will cause a number of changes in how Forge processes your models, the largest one being that it will now always search for lasso traces (see below) rather than arbitrary instances. The maximum length of the trace is given by option max_tracelength <k> and defaults to 5.

Variable state

Electrum mode allows var annotations to be placed on sig and field definitions. Such an annotation indicates that the contents of the corresponding relation may vary over time. For instance, saying sig Vertex { var edges: set Vertex } defines a directed graph whose edge relation may vary. Writing var sig Student {} denotes that the set of students need not remain constant.

A Note on Meaning

From the point of view of the constraints you're about to write, a trace is an infinite object. However, the solver underlying Forge needs to finitize the problem in order to solve it. The solution to this, given a finite state-space, is to invoke the Pigeonhole Principle and seek traces that end in a loop: "lassos".

However, this abstraction choice is not without a cost. If your system takes a great deal of steps before it loops back (e.g., an integer counter that overflows), Forge may tell you that there are no traces. Always pay attention to your max_tracelength option, and be convinced that it is sufficient to include the lassos you're interested in.

Added relational operators

Electrum mode adds one relational operator: priming ('). Any relational expression that is primed implicitly means "this expression in the next state". Thus, you can use priming to easily phrase transition effects. E.g., cookies' in cookies would mean that in every transition, the set of cookies never grows over time (will either shrink or remain the same).

Added formula operators

Electrum mode adds a number of formula operators, corresponding to those present in Linear Temporal Logic (LTL) and Past-Time Linear Temporal Logic.

• next_state <fmla> is true in a state i if and only if: fmla holds in state i+1.
• always <fmla> is true in a state i if and only if: fmla holds in every state >=i.
• eventually <fmla> is true in a state i if and only if: fmla holds in some state >=i.

Standard LTL Operators

• <fmla-a> until <fmla-b> is true in a state i if and only if: fmla-b holds in some state j>=i and fmla-a holds in all states k where i <= k < j. Note that the obligation to see fmla-a ceases in the state where fmla-b holds.

A natural question to ask is: what happens if fmla-b holds at multiple points in the future? However, this turns out not to matter: the definition says that the until formula is true in the current state if fmla-b holds at some point in the future (and fmla-a holds until then).

• <fmla-a> releases <fmla-b> is true in a state i if and only if: fmla-a holds in some state j>=i and fmla-b holds in all states k where i <= k <= j, or fmla-a never occurs in a later state and fmla-b holds forever after. Note that the intuitive role of the two formulas is reversed between until and releases, and that, unlike until, the obligation extends to the state where fmla-a holds.

Past-time LTL Operators

• prev_state <fmla> is true in a state i if and only if: fmla holds in state i-1. prev_state <fmla> is canonically false if i=0, since there is no prior state.
• historically <fmla> is true in a state i if and only if: fmla holds in every state <=i.
• once <fmla> is true in a state i if and only if: fmla holds in some state <=i.

Historical Note for Alloy Users

Alloy 6 and Electrum use the keywords after and before where Forge uses next_state and prev_state. We changed Forge to use these (admittedly more verbose) keywords in the hopes they are more clear. For example, after sounds like it could be a binary operator; in English, we might say "turn left after 3 stops". Also, next_state is definitely a formula about the following state whereas after does not communicate the same sense of immediacy.