[SAL-HELP] Re: [SAL] functions with random output

[Lee Pike]

Peter,

> Non-deterministic assignment is supported in the transition  
> language of SAL: “Lhs IN Expression”.
>
> Do you know if it is possible to define _functions_ with non- 
> deterministic output?
>
> My approach was this one: SAL functions are defined by the  
> expression language. Arbitrary variables in a function can be  
> defined via the “LET” statement. However, I didn’t find any  
> construct to define random assignments within “LET”.
>
> Of course, I can implement the functionality via SAL transitions  
> but for model readability I’m looking for a function-based solution.

What I believe you want to do is to write a function that returns a  
set.  Then, you can place that function on the right hand side of an  
"IN" statement.

Here's a simple example derived from some work I did with Geoffrey  
Brown:

timeout( min : REAL, max : REAL) : [REAL -> BOOLEAN] =
   {x : REAL | min <= x AND x <= max};

m : MODULE =
BEGIN
   OUTPUT t : REAL
   TRANSITION
   [  TRUE --> t’ IN timeout(1, 2);
   ]
END;

By the way, I mentioned this "trick" and some others in a paper I  
wrote recently giving some of my experiences about how to use SAL  
effectively that I gave at the AFM workshop: http:// 
www.cs.indiana.edu/~lepike/pub_pages/afm07.html

Lee

--
Galois <http://www.galois.com/>

Phone: +1 503.626.6616 ext. 135
Fax: +1 503.350.0833