Dynamic Behavior Specification

This page is about the specification of dynamic behaviors for blocks.

What is a dynamic behaviors

Regarding the specificaiton of blocks, it can happend that the semantics of the block might vary according to the value taken by the input during the execution. If we take the axample of a block computing the absolute value of the input, the executed code will be different if the input is positive (or null) or if the input is negative. We provide here such specification:

library ConstTest {
	typeDef realDouble myDouble
	blockType Abs {
		variant Abs_Root isDynamic {
			out S1 : myDouble
			in E1 : myDouble
		}
		mode BM1 implements Abs_Root {
			struct inv in matlab : "E1 < 0";
			compute : post in matlab : "S1 = - E1";
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
		mode BM2 implements Abs_Root {
			struct inv in matlab : "E1 >= 0";
			compute : post in matlab : "S1 = E1";
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
	}
}

This kind of dynamic behavior appears when we specify constraints (struct construct in the specification listing) on the parts of a block that cannot be gessed outside of the execution of the block (constraints depending on the inputs and memories of a block ?)

How to handle this in the specification

  • Is the condition sufficient ? (constraints depending on the values of inputs and memories of a block)
  • Maybe it is interesting to handle this by adding a isDynamic attribute on a BlockVariant. If this attribute is set to true then the sub-tree (of the specification) with this BlockVariant as root, is consideered to describe a dynamic behavior.

One dimension linear interpolator

Lets imagine a block computing a linear interpolation of a function \(f\). A block computing a linear interpolation of the functiowill take an input \(x\) and provide as input the interpolated value \(f(x)\).

Such computation relies on control points (known images of the \(f\) function). So we imagine that the interpolator block will have a \(H1\) parameter containing such values.

We provide here a specification for this block:

library Simulink_Basic {
	typeDef realDouble double
	typeDef enum onOff {ON, OFF}
	typeDef array h1Type of double [16,2]
	blockType OneDInter{
		variant OneDInter_Root {
			out s1 : double
			in e1 : double
			parameter exth1 : onOff
		}
		variant H1asParameter extends OneDInter_Root {
			parameter h1 : h1Type {
				struct pre in al : "forall i:int. (0 <= i < 15) -> h1[i][0] <. h1[i+1][0]";
			}
			struct inv in matlab : "exth1 = OFF" ;
		}
		variant H1asInput extends OneDInter_Root {
			in h1 : h1Type {
				struct pre in al : "forall i:int. (0 <= i < 15) -> h1[i][0] <. h1[i+1][0]";
			}
			struct inv in matlab : "exth1 = ON" ;
		}
		mode OneDInter_inf implements uxor H1asInput, H1asParameter {
			struct inv in matlab : "e1 <. h1[0][0]";
			compute : inv in matlab : "s1 = h1[0][1]" ;
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
		mode OneDInter_sup implements uxor H1asInput, H1asParameter {
			struct inv in matlab : "e1 >=. h1[15][0] /\\ e1 >=. h1[0][0]";
			compute : inv in matlab : "s1 = h1[15][1]" ;
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
		mode OneDInter_mid implements uxor H1asInput, H1asParameter {
			struct 
				inv in matlab : "e1 <. h1[15][0] /\\ e1 >=. h1[0][0]";
				inv in al : "exists i:int. 0 <= i <= 14 -> h1[i][0] <=. e1 <. h1[i+1][0]";
			compute : inv in matlab : "s1 = h1[i][1] +. ((e1-h1[i][0])*.((h1[i+1][1]-.h1[i][1])/.(h1[i+1][0]-.h1[i][0])))" ;
			backTyping : inv in matlab : "" ;
			forwardTyping : inv in matlab : "" ;
		}
	}
}

And the expected generated code with annotations:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
typedef struct {
	double H1[16][2];
	double E1;
	double S1;
}OneDInter_struct;

OneDInter_struct data;

//@	ghost int it_final;

/*@ 	requires \forall integer n; 0 <= n < 15 ==> data.H1[n][0] < data.H1[n+1][0];
	assigns data.S1, it_final;
	behavior inf:
		assumes data.E1 < data.H1[0][0];
		ensures data.S1 == data.H1[0][1];
	behavior sup:
		assumes data.E1 >= data.H1[15][0] && data.E1 >= data.H1[0][0];
		ensures data.S1 == data.H1[15][1];
	behavior mid:
		assumes data.E1 < data.H1[15][0] && data.E1 >= data.H1[0][0];
		ensures data.H1[it_final][0] <= data.E1 < data.H1[it_final+1][0];
		ensures data.S1 ==  data.H1[it_final][1] + ((data.E1 - data.H1[it_final][0]) *
			((data.H1[it_final+1][1] - data.H1[it_final][1]) /
  			(data.H1[it_final+1][0] - data.H1[it_final][0])));
	complete behaviors;
	disjoint behaviors;
*/
void compute(void){
	if (data.E1 < data.H1[0][0]){
		data.S1 = data.H1[0][1];
	}else if (data.E1 >= data.H1[15][0]){
		data.S1 = data.H1[15][1];
	}else {	
		int it=0;
		/*@	loop invariant 0 <= it < 15;
 			loop invariant \forall integer n; 0 <= n < it ==> !(data.E1 < data.H1[n+1][0]);
			loop invariant data.E1 >= data.H1[it][0];
			loop assigns it;
			loop variant 15-it;
		*/
		while(data.E1 >= data.H1[it+1][0]){
			it++;
		}
		//@	ghost it_final = it;
		data.S1 = data.H1[it][1] + ((data.E1 - data.H1[it][0]) * 
			((data.H1[it+1][1] - data.H1[it][1]) /
			 (data.H1[it+1][0] - data.H1[it][0])));
	}
}

Example interpretation

According to the input value, the OneDInterpolator block will search for the interval in wich is included this value. Then according to this, the value of OneDInterpolator(E1) is computed. Here are the three possible behaviors for this computation:

  • \(E1 < H1[0][0]\)

    \(OneDInterpolator(E1) = H1[0][1]\)

  • \(E1 >= H1[15][0]\)

    \(OneDInterpolator(E1) = H1[15][1]\)

  • \(\exists ! i \in [0,15[, H1[i][0] <= E1 < H1[i+1][0]\)

    \(OneDInterpolator(E1) = H1[i+1][1] + (E1 - H1[i][0])\times\frac{H1[i+1][1] - H1[i][1]}{H1[i+1][0] - H1[i][0]}\)

Complete/Disjoint behaviors

In the code of the linear interpolator function, we wrote some annotations. The most specific annotations in the function contract are the defined inf, mid and sup behaviors. For each behavior, Pre-Conditions (assumes clauses called Ainf, Amid and Asup) and Post-Conditions (ensures clauses called Einf, Emid and Esup) are specified. After these behaviors specification, we wrote complete behaviors and disjoint behaviors. Here is the meaning of these annotations:

  • Complete behaviors

    This means that in all the previously specified behaviors, all the possible cases are specified, in mathematical terms we will have:

    \(R \Rightarrow (Ainf \lor Amid \lor Asup)\)

    Where R is the set of Pre-Conditions for the full specification (in our example: line 11).

  • Disjoint behaviors

    This means that in all the previously specified behaviors, each behaviors is disjoint from an other one. In mathematical terms we will have:

    \(R \Rightarrow \lnot(Ainf \land Amid \land Asup)\)

    Where R is the set of Pre-Conditions for the full specification (in our example: line 11).

Adding complete and disjoint behaviors notation is not mandatory but it might be interesting to prove such properties on a contract.