fresh

The fresh expression introduces a new copy of a graph/machine scope variable when a node/state is visited.

Syntax

The syntax of a fresh expression is as follows:

 fresh (variable);

The variable here must be (semantically) legal and declared as a graph-scope variable.

Scope

The fresh expression can appear any where inside a node/state section.

Semantics

The fresh expression introduces a new copy of a graph-scope variable. The type and conditions specified with a where clause are retained. Expressions after the fresh expression that are referring to this new copy of graph-scope variable. This can ensure every time a node is visited a different value may be assigned to the fresh variable (depending on the conditions).

An Example

 machine Counting{

      int seconds where seconds>=0 && seconds<=5;

...

      normal state CountDown {

          counter=counter-fresh(seconds);

...

The fresh expression above creates a new copy of variable seconds This freshly created variable retains the type of int and the conditions imposed are also applied. When the state CountDown is visited, the fresh variable seconds will get assigned to a value between 0 and 5.

< Back