[SAL] Re: I need help for modeling in SAL

[Bruno Dutertre]

ranjan mandal wrote:
> Dear Sir,
> I am modeling the Welch-Lynch clock synchronization algorithm in SAL. I 
> have
> encountered some problems. I am trying to solve them for the last 2 months,
> but I could not come up with the solutions.
> The problems are:
> 1. How to pass an array to a module? I am storing the deviation values 
> in an
> array and the want to calculate the fault tolerant mid point average of it.
> 2. How to remove the first element of the array?
> 
> I have looked at the examples that are given in sal-2.3 and your manuals
> from SRI International(Timed Systems in SAL).
> Please spare some of your valuable time and reply to me at your earliest
> convenience.
> Thanking you,
> Ranjan Mandal
> 

Hi,

Arrays are like other types. You can declare a module variable with
array types and that should work. If you have N modules, that produce
one output each and you want to collect the N outputs in an array,
you have to use a WITH/RENAME construct.

Example: if N modules share a global array V, where V[i] is the
output X from module i. Then you have to use something like

   ID: TYPE = [1 .. N];

   P[i: ID]: MODULE =
    OUTPUT X: INT
    ...
   END;

   global: MODULE =
     WITH OUTPUT V: ARRAY ID OF INT
       ([] (i: ID): (RENAME  X TO V[i] IN P[i]));

global is the composition of P[1] to P[N], with the output
X of P[i] renamed to V[i].

I'm not sure what you mean by removing the first element
of an array. You get the first element of array V as V[1] in
the usual way. If you want to construct a new array W that's
equal to V[2.. N], you can write that as

  W: ARRAY [2..N] OF INT = [[i:[2..N]] A[i]]

in general, [[i:type] expr] is an array expression. It's similar
to (lamdba (i:type) expr) for function. In particular expr may
depend on i.

Bruno