[SAL] Re: I need help for modeling in SAL
bruno at csl.sri.com
Mon Jun 18 11:13:08 PDT 2007
ranjan mandal wrote:
> Dear Sir,
> I am modeling the Welch-Lynch clock synchronization algorithm in SAL. I
> 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
> Thanking you,
> Ranjan Mandal
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
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 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 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.
More information about the SAL