Parametric modeling

One essential task when studying a system consists in analyzing and comparing variants of a system.

For instance, many classic models can be scaled up (e.g. the number of philosophers in a ring), you might want to study the how buffer sizes affect your system, you might want to explore different configurations of your components (ring, star, chain topologies…).

Model-checking as performed in ITS-tools is not parametric, in the sense that it can only check properties for a given value of a parameter. But we do support parametric models, where just changing one declaration is enough to produce a specific instance of a model.

To this end, we introduce GAL parameters, which are prefixed by a $ sign, and are run-time constants. In a specific model instance they have a single value that cannot change as the state of the system evolves.

These parameters can thus be regarded as syntactic sugar, helping the user define his system more easily, but any parametric GAL model can be degeneralized by substituting constant values to parameters in the text.

This conversion is currently performed before invoking the model-checker, inspect the models produced in the “work/” subfolder after using “Run As->ITS Model-check” on a parametric GAL to see the results of this degeneralization.

Parameters with a single value

The first and most basic type of parameters are simply a symbolic alias for a constant.

For instance, you can declare $N=3, then use $N in integer expressions of your specification.

While there is no syntactic constraint, we typically use upper-case names for these constant parameters (e.g. $N rather than $n).

Global parameters

Global parameters are declared at the top level of a GAL file, simply introducing the name of the parameter and its value. The value is just a constant.

Examples :

Suppose you want to configure the size of the system as a parameter N. You can define $N=3;, then use $N to define initial values of variables, size of arrays, maximum value in a range type definition… Updating this $N declaration will update all these dependent declarations to produce the model you need.

// size of buffers
$N=3;

// ...
gal Buffer {
	array [$N] buff;
	int fill=0;
	
	transition put [fill<$N] {
		buff[fill] = 1;
		fill +=1;
	}
	// ...
}
//...

Another use case is simply as symbolic constants, improving readability. In this example, the state of an automaton was encoded onto an integer, using parameters helps read the code.

$IDLE=0;
$RUNNING=1;
// ...
gal Process {
	int state=$IDLE;
	// ...
	transition t1 [state==$IDLE] {
		state=$RUNNING;
		// ...
	}
	// ...
}

Type parameters

A GAL type declaration can optionally declare one or more type parameters. A type parameter essentially declares a symbolic name for an integer constant, that can then be used within the various instructions of the GAL system (including initializations, typedef, guards, statements…).

Parameter names start with a $ sign to avoid any confusion with the variables of the system. Parameters are given a value directly after their declaration.

Note that when instantiating a GAL or composite within the context of composite ITS, parameters can be given a value (different from the value given in the parameter declaration). Thus type parameters can be used to simulate a constructor for the GAL.

Syntactically, type parameters are given as a parenthesized comma separated list, just after the name of the system. Only constant expressions may be used in parameter initializations.

gal paramSystem ($N = 2, $K = 1) {
	int variable = $N ;
	array [2] tab = ($N + $K, $N - 1) ;

	transition t1 [variable > $N && variable < 5+$K] {
		tab [$K] = tab [1] * tab [0] ;
		variable = variable * 5 ;
	}

	transition t2 [variable == $N] label "a" {
		tab [1] = 0 ;
		variable+=1;
	}
}

composite comp {
	paramSystem p1; // default values
	paramSystem p2($N=1,$K=0); // override values
	paramSystem p3($N=1); // $K defaults to 1
	paramSystem p4($K=0); // $N defaults to 2
	
	synchronization allA {
		p1."a";
		p2."a";
		p3."a";
		p4."a";	
	}
}

main comp;

This small example shows a GAL with two type parameters, and how to override the values for these parameters at instantiation. The syntax for Composite type parameters and their instantiation are the same as for GAL.

Parameters over a range of values

The second type of parameter is a bit different; it takes its values from a predefined finite range.

For instance, you can declare typedef indexes=0..3;, then use a parameter $p : indexes that can take any of the values in this range.

This is especially useful when using arrays, and to define similar behaviors in a compact way.

While there is no syntactic constraint, we typically use lower-case names for these parameters over a range (e.g. $p rather than $P).

typedef range declaration

A GAL typedef declaration allows to define a symbolic name for a given range of integers from min to max.

These bounds are inclusive, with the constraint that min ≤ max, so that there is at least one element in any range definition.

These type definitions are used when declaring transition parameters, or within a for loop. They allow to define a set of similar transitions in a compact and readable manner.

Syntactically, a type definition is introduced with the keyword typedef followed by a unique name for this type, followed by the actual range specification in the form “= min..max;”. min and max are integer expressions built from constant parameters and constants only.

Here is an example of a system with some range definitions:

$N=2;

typedef paramType1 = 1..$N; // $N values

typedef paramType3 = 0..3; // 4 values

gal paramDef {
	
	// scope is the enclosing GAL
	typedef paramType2 = 2..4;  // 3 values
	int variable = 0;
	
	// a transition compactly modeling $N*3 (card(pt1)=$N, card(pt2)=3) basic transitions
	transition trans (paramType1 $p1, paramType2 $p2) [$p1 <$p2] {
		variable = $p1 + $p2;
	}
}

Transition parameters

Transitions can optionally define one or more parameters that allow a more concise and readable representation of a complex transition relation.

Transition parameters iterate over a given range of integers, defined using a typedef.

Semantically, each parameter can be replaced in the transition effects by each of the possible values in its range. Thus a parametric transition compactly represents many alternative transitions, that differ by the substitution value used for their parameters.

Transition parameters have the transition body as scope, and thus do not name clash with parameters of other transitions.

Syntactically, transition parameters are declared in a parenthesized comma separated list just after the transition name, with a syntax reminiscent of arguments for a function or method.

Each parameter is defined by giving its type followed by the parameter name which must start with a $ sign and cannot shadow another parameter already in scope.

In this small example, we use two parameters. In such a case, the cross product of the ranges of the parameters is explored.

gal paramDef ($N=2) {
	typedef paramType = 0..$N;
	typedef paramType2 = 0..1;
	int variable = 0;
	
	// a transition compactly modeling ($N+1)*2 (card(pt1)=$N+1, card(pt2)=2) basic transitions
	transition trans (paramType $p1, paramType2 $p2) [$p1 != $p2] {
		variable = $p1 + $p2;
	}
}

This example is equivalent to this version that does not use parameter definitions. :

gal paramDef_inst {
	int variable = 0 ;

	// not that only 4 transitions (out of 6 possible) were produced due to guard $p1!=$p2
	// since transitions with false guard have no effect, they are suppressed here.

	transition trans_0_1 [true] {
		variable = 1 ;
	}

	transition trans_1_0 [true] {
		variable = 1 ;
	}

	transition trans_2_0 [true] {
		variable = 2 ;
	}

	transition trans_2_1 [true] {
		variable = 3 ;
	}
}

Transition parameters can be seen as a way of expressing a (parametric) set of alternative behaviors. If the transition label does not use parameters, any one of these variants can be non-deterministically chosen for firing. This makes this mechanism a dual of the for loop, that offers (parametric) sequential composition of behaviors.

For loop action

To ease modeling, GAL provide a constrained For loop iterative control structure. This mechanism is close to macro expansion, the loop is unrolled before analysis is performed.

A for loop defines a local parameter which has as scope the body of the loop. Since the domain of the parameter is is both known and finite, the loop can be simply unrolled.

The syntax is reminiscent of Java foreach loop, for ($forparam : paramType) { body; }. The body is an arbitrary sequence of statements.

This example shows a use of a for loop to set values in an array.

gal forLoop  {
	typedef Dom = 0..2;

	array [3] tab  = (0,0,0);
	
	transition forExample [true] {
		for ($i : Dom) {
			tab[$i] = $i;
		}
	}
}

It is strictly equivalent to this version.

gal forLoop_inst {
	array [3] tab = (0, 0, 0) ;

	transition forExample [true] {
		tab [0] = 0 ;
		tab [1] = 1 ;
		tab [2] = 2 ;
	}
}

Parameters in Labels

Parameters can be used in labels, helping to define a finite set of labels sharing some characteristics. Labels can define a set of arguments which must have a fixed value at runtime (i.e. the set of labels does not evolve with the state).

The values for these arguments can be given or computed using the transition parameters when declaring a label. Similarly, when calling a label all arguments must have a fixed value.

This example shows a (lossy) buffer containing a data. For external synchronization the buffer exports a set of labels, one pair send(d),receive(d),for each data d it can contain.

We also declare a bounded counter, which can be incremented by calling it’s inc(d) label. The value passed to the label controls how much the counter is incremented.

But if the value passed to this buggy counter is inc(1), an alternative available is to not increment the counter. This inc2 transition shows how to define label parameters even if the transition itself is not parametric.

The overall composite just assembles these pieces into a scenario, where a counter is used to both count and limit the number of sent messages in the buffer.

Two more counters are used to compute respectively how many messages were received, and the sum of their contents.

This scenario is not particularly meaningful, but it is chosen to exhibit all the syntax related to both declaring parameters on labels and calling such labels.

$MAX=3;
typedef data=0..$MAX-1;

// A lossy buffer, with a single cell, that can hold a data.
gal Buffer {
	// MAX models an empty buffer
	int value=$MAX;
	
	/** Allows to write to the buffer, if it is empty */
	transition put (data $d) [value==$MAX] label "send"($d) {
		value = $d;
	}
	/** allows to read the value held by the buffer */
	transition get (data $d) [value==$d] label "receive"($d) {
		value = $MAX;
	}
	/** This buffer is lossy, at any time (no label) the data can be lost. */
	transition lose [value!=$MAX] {
		value = $MAX;
	}		
}
// An example (buggy) counter ; can be incremented up to a bound.
gal BoundedCounter($BOUND=5) {
	int count=0;
	
	/** The quantity to increment by is passed through the label.	 */
	transition inc (data $d) [count < $BOUND] label "inc"($d) {
		count+=$d;
	}
	/** incrementing by one should increment by one. 
	*   But it could also not increment because this counter is buggy. */
	transition inc2 [count < $BOUND] label "inc"(1) {
		count+=2;
	}
}

composite Channel {
	// the sender sends at most three messages
	BoundedCounter sender($BOUND=3);
	Buffer buff;
	// to count the sum of all data values in actually received packets
	BoundedCounter summer($BOUND=20);
	// to count the number of received messages
	BoundedCounter receiver;
	
	// our sender sends a random packet, and increments its send counter by one
	synchronization sendData (data $d) {
		sender."inc"(1);
		buff."send"($d);
	}
	// at reception, we read the data from the buffer
	synchronization receiveData (data $d) {
		buff."receive"($d);		
		// increment "summer" by the value in the packet
		summer."inc"($d);
		// increment received message counter by 1 : a constant value
		receiver."inc"(1);
	}	
}

main Channel;

Parameters in Composite

Within composite types, there are no variables, only nested instances. Parameters can however be used to define parametric synchronizations, to iterate on arrays of instances using a for loop, and to define complex synchronization rules in combining if-then-else (where the condition is over parameters) and abort statements.

These control structures for,if-then-else and abort statements are the same as in GAL, within the limits of not having variables in scope.

This means all their condition reduces to true or false after parameter instantiation, hence this is again syntactic sugar degeneralized away prior to model-checking. Look in the “work/” subfolder created after you execute “Run As-> ITS model-check” to see the target model.

This example shows some use of these features to model some classic synchronization patterns :

• start : A choose one from a set with event that gives the token to a single random participant
• passToken : A circular synchronization using a modulo to chain participants in a logical ring
• reset : A broadcast synchronization, that all the participants receive
• passFast : A more complex synchronization, featuring a condition and an abort. The condition modeled here is completely arbitrary, it gives fast channels from participant at index 0 to all other participants and allows some participants to skip their immediate successor. The abort avoids creating a self loop with no effect on all states, otherwise passFast instantiated for any ($i,$j) that do not meet the condition would produce an empty synchronization.

$N=10;
typedef index=0..$N-1;

// A participant : can hold the token. Other behavior is not modeled.
gal Participant($TOKEN=0) {
	int hasToken=$TOKEN;
	
	transition get [hasToken==1] label "get" {
		hasToken = 0;
	}
	transition put [hasToken==0] label "put" {
		hasToken = 1;
	}
	transition reset [true] label "reset" {
		hasToken = 0;
	}		
}
composite Collaboration {
	// the leader starts and ends cycles
	Participant leader($TOKEN=1);
	// A ring of participants
	Participant [$N] ring;

	// our leader gives the token to a random participant
	synchronization start (index $i) {
		ring[$i]."put";
		leader."get";
	}
	
	// There is a topological ring of participants
	synchronization passToken (index $i) {
		ring[$i]."get";
		ring[($i+1)% $N]."put";		
	}
	
	// The reset is a broadcast : the leader gets the token back forcefully
	synchronization reset {
		leader."put";
		for ($i : index) {
			ring[$i]."reset";
		}
	}
	// the condition used is random/meaningless ;
	// this example shows if/abort used to make complex synchronization
	synchronization passFast (index $i, index $j) {
		if ( $i!=$j && ( $i==0 || $j == $i + 2)) {
			ring[$i]."get";
			ring[$j]."put";
		} else {
			abort;
		}		
	} 
	
}

main Collaboration;

Parameter Instantiation

This section gives an overview of the algorithms used when instantiating parameters. Most end-users do not need to be fully aware of the mechanics, so feel free to skip this section, provided mostly for documentation.

The main points relevant for the end-user are :

• During parameter instantiation, we also do a number of simplifications, that may remove variables (if they are constant), may remove transitions (if they are labelled and not called), may remove statements (if they have no tangible effect) and may remove type declarations (if they are not used in the main instance)
• Some identical behaviors can be fused if they are redundant
• Transitions and synchronizations with several parameters may be translated to a more compact form by decomposing the transition

Parameter Instantiation

Parameter instantiation consists in applying the following steps, in this order:

1. All type level parameters (symbolic constants) are replaced by their value in all expressions.
2. “For” loops are unrolled, i.e. the statement is replaced by n occurrences of the body statement, where the loop variable is replaced by its value in each of these occurrences. The unrolling of loops is done first on nested statements.
3. Transition parameters are then instantiated. Each transition that has parameters can produce several transitions. Suppose transition has parameters $p1,..$pk in domains D1,..DK (see typedef keyword). We first instantiate $p1 giving |D1| transitions, in which $p1 is substituted by one of the values in D1. More precisely, any occurrence of $p1 is replaced by its numeric value, in the guard, label, and in the transition body (where the parameter $p1 may occur in calls to a label). Each occurrence of the transition has a new name allowing traceability. On the fly, the guard of the newly created transitions is simplified, and no transition is produced if it happens to be false. This can skip construction of many transitions in some examples. Because we do this iteratively and test after each parameter instantiation if the transition is false, the number of “skipped transitions” reported in the verbose trace can thus be smaller than the difference between the Cartesian product of domain sizes and the number of transitions actually produced.

We then apply simplifications, currently we do the following rather trivial simplifications:

1. Arithmetic and Boolean simplifications, on all constant expressions. Thus we replace (2 + 2) by (4), we also apply basic absorbing (0 * x -> 0, false && x -> false, true || x -> true) and neutral element (1 * x -> x, false || x -> x, true && x-> x) simplifications.
2. We replace calls to non existing labels by an abort statement. These can occur as a result of other transition simplifications.
3. We replace any sequence of statements containing an abort by a single abort statement. We destroy any transition with abort as body.
4. Transitions with a false guard are destroyed.
5. if (c) { s1 } else { s2 } is replaced by s1 if c can be reduced to true or to s2 if c can be reduced to false.
6. Constant variables are identified and simplified away. To do this, we first track all write accesses to variables or arrays. Initially, all variables and array cells are supposed constant. We then scan all write access (assignments) in the specification. If a variable is assigned to, it isn’t a constant. A write access to a single cell of an array (tab[3]) means this cell is not constant. A write access to an array using an index expression (tab[i]) discards the whole array. Variables that are actually constant can then be replaced by their intial values in the whole specification. Simple constant variables and arrays that are entirely constant are then removed from the state signature, i.e. they are totally discarded. Because of the fact some variables disappear, this can lead to some confusion from the user, please look closely at the traces to understand what was simplified away.
7. If we can find within a sequence of statements increments and/or decrements of a variable, and that they are commutative with statements that separate them, we fuse their effects. If the total effect is to leave the variable unchanged, the idle statement x=x+0 is removed. This can occur for instance with test-arc behavior in Petri nets.
8. If two transitions that bear a label called only once and are identical in effects up to renaming of self, label and parameters, they are fused and only one of them is kept. This makes the specification slightly more compact, but is redundant with simplifications that occur in the model-checking engine. This reduction is called “fusion of isomorphic effects”.

Parameter Separation

Parameter separation consists in rewriting conjunction of choices (as expressed by transitions with several parameters) to sequence of choices where possible.

De-generalizing parametric transitions that bear a large number of parameters can produce very large GAL specifications. In general, degeneralization produces as many transitions as the size of the cartesian product of the domains of the formal parameters. But in many case, the full combinatorial unfolding can be avoided, allowing a compact transition representation while preserving semantics.

A transition has two independent parameters if it contains no statement that uses both parameters. Such a transition can be split into two labelled sub-transitions, one for each parameter, the semantics being preserved by calling the labels of these two sub-transitions. Statements are moved to the appropriate sub-transitions depending on the parameter they rely on.

We thus obtain three transitions: the modified original one, that calls the sub-transitions and has no more parameter, and the sub-transitions, each of which has a single parameter. If the domain sizes of both parameters are called r1 and r2, we obtain after the instantiation of the parameters r1 + r2 + 1 transitions instead of r1 * r_2. Thanks to the sequence and call statements, the semantics is preserved.

More generally, the detection of the parameters to be separated in a given transition is done by building an hypergraph, whose nodes are parameters and where an hyperedge is added for each statement, connecting together all the parameters used in it. We then consider the connectivity graph between parameters induced by this hypergraph.

If a parameter $p has no neighbor, it can be separated: a new transition with parameter $p and a new label “lp” is built, whose body is the sequence of statements that depend on $p.

These statements are replaced in the original transition by a call the label “lp”.

Similarly, a parameter $p1 that has a single neighbor $p2 can also be separated. We similarly build a transition with the statements depending upon $p1 alone or on both $p1 and $p2. This transition bears both parameters $p1 and $p2, and is labelled with a new label “lp2”. Parameter $p1 can then be removed from the original transition, and the relevant statements be replaced by a call to label “lp2”. The procedure can be iterated on the simplified original transition, where $p2 may now be separable too. Instantiation will also instantiate $p2 in “lp2”, so as to ensure consistency for the values of $p2 across the separated transitions.

This procedure has low complexity, depending on the size of the parametric GAL. It is applied before instantiation of the parameters. Relying on the distributivity between sequential and parallel composition, it helps producing transition relation expressed as sequences of parallel compositions, yielding much more compact representations than an expanded parallel composition of sequences (such as used by LTSmin).

This factored representation would not be efficient without the ability of symbolic operations to deal with parallel composition natively. One may see this transform as a manner of delaying the computation of the combinatorial number of instantiations until symbolic evaluation time, where the symbolic data structures help with the combinatorics.

This example transition of a colored Petri net taken from this VendingMachine example of the Model checking contest at Petri nets shows how this reduction works in practice.

This is an extract of the full model. Before separation, we have many independent parameters. In fact here all parameters are independent, since no statement simultaneously uses two parameters. Furthermore parameters $o1 $o2 and $o3 play a very symmetric role.

gal Document {
	typedef Options = 0 .. 1 ;
	typedef Quality = 0 .. 7 ;
	typedef Products = 0 .. 1 ;
	array [8] ready = (0, 0, 0, 0, 0, 0, 0, 0) ;
	array [8] wait = (1, 1, 1, 1, 1, 1, 1, 1) ;
	array [2] theProducts = (1, 1) ;
	array [2] productSlots = (0, 0) ;
	array [2] theOptions = (1, 1) ;
	array [2] optionSlots = (0, 0) ;

	transition elaborate3 (Options $o2, Options $o3, Options $o1, Quality $x, Products $p) [$x > 5 && $x <= 7 &&
	theProducts [$p] >= 1 && theOptions [$o3] >= 1 && theOptions [$o2] >= 1 && theOptions [$o1] >= 1 && wait [$x] >= 1] {
		theProducts [$p] = theProducts [$p] - 1 ;
		theOptions [$o3] = theOptions [$o3] - 1 ;
		theOptions [$o2] = theOptions [$o2] - 1 ;
		theOptions [$o1] = theOptions [$o1] - 1 ;
		wait [$x] = wait [$x] - 1 ;
		ready [$x] = ready [$x] + 1 ;
		optionSlots [$o2] = optionSlots [$o2] + 1 ;
		optionSlots [$o1] = optionSlots [$o1] + 1 ;
		optionSlots [$o3] = optionSlots [$o3] + 1 ;
		productSlots [$p] = productSlots [$p] + 1 ;
	}

}

After separation (and fusion of isomorphic effects on $o1 $o2 and $o3) we obtain the following model :

gal Document_sep {
	typedef Options = 0 .. 1 ;
	typedef Quality = 0 .. 7 ;
	typedef Products = 0 .. 1 ;
	array [8] ready = (0, 0, 0, 0, 0, 0, 0, 0) ;
	array [8] wait = (1, 1, 1, 1, 1, 1, 1, 1) ;
	array [2] theProducts = (1, 1) ;
	array [2] productSlots = (0, 0) ;
	array [2] theOptions = (1, 1) ;
	array [2] optionSlots = (0, 0) ;
	transition elaborate3 [true] {
		self."elaborate3o2" ;
		self."elaborate3o2" ;
		self."elaborate3o2" ;
		self."elaborate3x" ;
		self."elaborate3p" ;
	}
	transition elaborate3o2 (Options $o2) [theOptions [$o2] >= 1] label "elaborate3o2" {
		theOptions [$o2] = theOptions [$o2] - 1 ;
		optionSlots [$o2] = optionSlots [$o2] + 1 ;
	}
	transition elaborate3x (Quality $x) [wait [$x] >= 1 && $x > 5 && $x <= 7] label "elaborate3x" {
		wait [$x] = wait [$x] - 1 ;
		ready [$x] = ready [$x] + 1 ;
	}
	transition elaborate3p (Products $p) [theProducts [$p] >= 1] label "elaborate3p" {
		theProducts [$p] = theProducts [$p] - 1 ;
		productSlots [$p] = productSlots [$p] + 1 ;
	}
}

This model when instantiated is still compact as shown here. Compare to what a plain instantiation obtains; obviously when applicable this approach helps to scale as it can avoid polynomial (with degree the number of independent parameters) blowups in specification size.

gal Document_flat {
	array [8] ready = (0, 0, 0, 0, 0, 0, 0, 0) ;
	array [8] wait = (1, 1, 1, 1, 1, 1, 1, 1) ;
	array [2] theProducts = (1, 1) ;
	array [2] productSlots = (0, 0) ;
	array [2] theOptions = (1, 1) ;
	array [2] optionSlots = (0, 0) ;
	transition elaborate3 [true] {
		self."elaborate3o2" ;
		self."elaborate3o2" ;
		self."elaborate3o2" ;
		self."elaborate3x" ;
		self."elaborate3p" ;
	}
	transition elaborate3o2_0 [theOptions [0] >= 1] label "elaborate3o2" {
		theOptions [0] = theOptions [0] - 1 ;
		optionSlots [0] = optionSlots [0] + 1 ;
	}
	transition elaborate3o2_1 [theOptions [1] >= 1] label "elaborate3o2" {
		theOptions [1] = theOptions [1] - 1 ;
		optionSlots [1] = optionSlots [1] + 1 ;
	}
	transition elaborate3x_6 [wait [6] >= 1] label "elaborate3x" {
		wait [6] = wait [6] - 1 ;
		ready [6] = ready [6] + 1 ;
	}
	transition elaborate3x_7 [wait [7] >= 1] label "elaborate3x" {
		wait [7] = wait [7] - 1 ;
		ready [7] = ready [7] + 1 ;
	}
	transition elaborate3p_0 [theProducts [0] >= 1] label "elaborate3p" {
		productSlots [0] = productSlots [0] + 1 ;
		theProducts [0] = theProducts [0] - 1 ;
	}
	transition elaborate3p_1 [theProducts [1] >= 1] label "elaborate3p" {
		productSlots [1] = productSlots [1] + 1 ;
		theProducts [1] = theProducts [1] - 1 ;
	}
}