GAL concepts

GAL Specification

GAL files are simply text files with the extension .gal . For example, foo.gal is a valid GAL filename. Each file defines a single GAL specification that may contain one or more type declarations, a main instance, and properties.

GAL Type Declaration

A GAL type declaration (or just a GAL) is characterized by a name, and contains a sequence of declarations (variables, transitions).

A GAL is declared with the keyword gal, followed by the system name. The name must start with a letter of the alphabet and should be a C-style identifier (only using letters, underscore and numbers).

A good practice is to give a meaningful name to the system created, particularly if it will be reused in a Composite ITS definition.

The body (variable and transitions) of the system name are then placed between a pair of braces.

Here is a declaration of an example GAL system named emptySystem.

gal emptySystem {
        //Variables
        
        // Transitions
}

Variable declarations

A GAL model declares variables. The variables manipulated in GAL can be integers or fixed size arrays of integer. There are no dedicated Boolean or char basic types, nor struct declarations.

There are no dynamic allocation or variable length structures such as lists. To model these using an array is only possible if an upper bound on its size is known a priori.

Integers are C-style signed integers, 32 bit (4 bytes) wide, with the same overflow semantics as in C ( (2³¹ -1) + 1 = - 2³¹).

In this section, we describe how variables of a GAL are declared.

Integer variables

Plain integer variables are introduced with the keyword int followed by the variable name starting with a letter. The variable name may contain alphanumeric characters as well as the “.” character (which may help trace structs from of your source language if you are using GAL as a transformation target).

The name must be unique, and cannot be reused for another variable.

Each variable can be initialized, this is done using the “=” symbol followed by the initial value of this variable. The default initial value for integer variables is 0.

The initial value can be expressed using an integer expression built of constants and/or type parameters, but it cannot refer to other variables. The declaration ends with a semicolon.

Below is an example of a system with two GAL variable declarations :

gal intSystem { 
	// Integer variable declarations...
	int a = 5 ;
	int b = - 2 ;
}

Array declarations

An array declaration allows to declare a fixed size array of integers. Like simple integer variables, each entry in the array needs to be initialized.

A GAL array variable is declared using the keyword array followed by the array size N within square brackets, then the array name.

Each cell of the array needs to be initialized, to this end, a list of N comma separated integers surrounded by parenthesis (or integer expressions of constants and/or type parameters) should be provided. If no initialization is provided, all array cells are set to 0 initially. A semicolon ends the array declaration.

Here is an example of a system with a declaration of an array:

gal intArray {
	 //Variable declarations
	int a = 5 ;
	int b = - 2 ; 
	
	//Array declaration
	array [3] tab = (0, 8, - 6) ;
}

Expressions

GAL expressions can be either integer expressions or Boolean expressions, depending on the context. We give here the syntax of these expressions, which is mostly directly taken from C (or Java).

Usual priorities between operators are observed (e.g. Boolean AND stronger than OR, integer multiplication stronger than addition). If in doubt, parenthesis can be used to force an evaluation order.

Boolean expressions

Boolean expressions are allowed in guards of transitions. It is also possible to write arithmetic expressions, with boolean appearance (as in C), which will be worth 1 or 0 depending on whether they are true or false (see Wrapper)

The basic expressions are true and false.

The usual boolean operators are present in GAL,

Basic Boolean expressions can be any kind of comparison of two integer expressions using one of the comparison operators :

Integer expressions

Binary Operators

The standard linear integer arithmetic operators are provided. Division is integer division.

We also provide multiplications useful in some contexts

Finally, we offer bitwise manipulation operators :

Unary operators

Standard prefix unary operators are provided :

Terminal expressions

Terminal integer expressions are simply :

• a reference to plain integer variables, var
• a reference the cell of an array tab[index],
• or a reference to a parameter $param

When accessing a cell of an array tab[index], the index expression is inductively an arbitrarily complex integer expression.

Wrapper of boolean expressions

Boolean expressions can be raised to integer expressions with the interpretation 1 for true and 0 for false, by surrounding the Boolean expression with parenthesis.

This encapsulation of Boolean expressions as integers enables many (programming/modeling) tricks commonly encountered in C.

Note that the reverse is not possible, in particular, assignments cannot be nested within Boolean conditions, they do not return a value like in C. Hence all Boolean expressions are by construction side-effect free.

Example : myVariable = (a == 0) * 100 ;_//myVariable is 100 or 0_

Transitions

Transition declaration

Transitions allow to step atomically from a source state to a (set of) successor state(s). Transitions are enabled by a guard, which is a Boolean expression and may carry a label that is a string. If the guard is true in the current state, the transition can be fired, executing all the actions it contains in sequence. Actions can be assignments, calls to a label or other statements as described below. Labeled actions cannot be fired if they are not called from another transition or synchronized externally (see ITS composite). Transitions without a label are “private” and can be fired any time their guard is true, with interleaving semantics. A self-contained GAL (not intended for further composition) typically bears no labels on transitions.

Syntactically, a transition is declared with the keyword transition, followed by a unique identifier for the transition. The transition guard (a Boolean expression) is surrounded by brackets (that can be “true” if the transition is always enabled). The transition can optionally be labeled, as introduced with the keyword label followed by double quoted string defining the label. Finally the statements comprising the transition body are placed in a block surrounded by curly braces.

This example system contains two transitions of which one is labeled :

gal transitions { 
	//Variable declarations
	int a = 5 ;
	int b = - 2 ; 
	
	//Array declarations
	array [3] tab = (0, 8, - 6) ;

	transition t1 [a < tab [2]] { //actions...
	}

	transition t2 [true] label "t2_label" { //actions...
	}
}
	

Statements

Statements are operations that generally update the state of the system variables.

Statements are sequentially composed using a semi-column ; within the body of a transition.

The most common type of statement is the assignment of an integer expression on system variables to a system variable.

The call to a label statement introduces non-determinism in the execution by offering several alternatives (any transition bearing the label can be fired).

Other basic statements include an if-then-else control structure, and an *abort instruction.

Other statements such as limited for-loop control structure are provided (see parametric GAL).

Assignment

Assignments are composed of a left-hand side (lhs), that must be a reference to a variable or to the cell of an array, and a right-hand side (rhs) that is an integer expression.

Example : a=3+(b-x);

When the lhs is a reference to an array, the target index within the array can be expressed using an arbitrarily complex integer expression.

Example : tab[a+b]= 42;

GAL also support increment and decrement to a variable, using a += or -= notation. The semantics are the same as in other languages : a+=b is equivalent to a=a+b, a-=b is equivalent to a=a-b, where a is a variable and b an arbitrary integer expression.

Call action

The call action allows to call a label of the current GAL system, i.e. non-deterministically choose any of the enabled transitions that bear this label, and execute its actions.

This powerful mechanism allows to model much more concisely when the transition relation carries non-determinism.

For instance, a transition that non deterministically assigns a value between 0 and N to two variables X and Y can be represented as containing two calls to labels “assignX” and “assignY”. We can then build N transitions tX0, tX1… (resp. tY0, tY1…) bearing label “assignX” (resp. “assignY”), each of them with a [true] guard and a single assignment of a value to the designated variable. We thus accurately represent the transition relation with 2N+1 transitions rather than N^2 transitions.

Calls can also be used to simulate some control structures. For instance, If-Then-Else(cond, actif, actelse) can be simulated by two transitions bearing label “ite”, with guards cond and not cond respectively, and body actif and actelse respectively.

Calling label “ite” in a transition body is like executing an if-then-else block.

Note that the whole ITS semantics is defined using sets, i.e. the successor relation returns a set of successors. Hence if no labeled action is enabled in some states at the point of call, no successors are produced, canceling the effect of the calling the enclosing transition for the concerned states, like an abort action.

Syntactically, a call is introduced by the keyword self, followed by a column ‘.’, followed by a label between double quotes.

This example shows a use of a call to non deterministically update a variable.

gal callExample {
	int variable = 0 ;

	transition invertX [variable == 0 || variable == 1] {
		self."setX" ;
	}

	transition callee1 [true] label "setX" {
		variable = 1 ;
	}

	transition callee2 [true] label "setX" {
		variable = 0 ;
	}
}

If-Then-Else action

To ease modeling, GAL provide the if-then-else alternative control structure. As mentioned above this behavior can also be implemented using calls.

The semantics are those you could expect, if the condition is true the “if” block is executed, otherwise the “else” block is executed (or nothing is done if there is no else block).

The syntax is taken from C or Java, if followed by a Boolean condition between parenthesis, followed by a block between curly braces. Optionally, the statement can be completed by an else followed by a second block of actions.

This example shows a use of an if then else to invert the value of a Boolean variable.

gal iteExample {
	/**
	 * Variable declarations
	 */
	int variable = 0 ;
	/** 
	 * Transitions
	 */

	transition invert [variable == 0 || variable == 1] {
		if (variable == 0) {
			variable = 1;
		} else {
			variable = 0;
		}
	}
}

Abort action

The semantics of GAL (based on ITS definitions) allow a statement to return a set of successors, since GAL natively support non-determinism. The abort statement returns the empty set of successors, hence it interrupts the current transition which then yields no successors.

The abort statement is mainly used to model transition relations where Boolean conditions with side effects need to be represented. It allows to have a transition with a guard, a few statements then typically an if-then-else or a variant using a call, of which some branches may encounter abort and cancel the transition effect for this branch.

The following example shows a use of abort to model the transition relation of a Time Petri net with two places a and b, and a transition t that moves tokens from a to b, with earliest firing time eft and latest firing time lft. Time cannot elapse if an enabled transition has reached its latest firing time, but this test is complex, particularly when there are many transitions. Use of abort allows to concisely represent the semantics.

gal abortExample ($EFT = 1, $LFT = 3) {
	int a = 1 ;
	int b = 0 ;
	int t.clock = 0 ;

	transition t [a >= 1 && t.clock >= $EFT] {
		a = a - 1 ;
		b = b + 1 ;
		t.clock = 0 ;
	}

	transition elapse [true] label "elapse" {
		// is t enabled ?
		if (a >= 1) {
			// is t's clock strictly less than its latest firing time ?
			if (t.clock < $LFT) {
				// if yes increment t clock
				t.clock = t.clock + 1 ;
			} else {
				// otherwise, time cannot elapse, kill exploration
				abort ;
			}
		}
	}
}