[SAL] Assignments/Definitions in SAL

Leonardo de Moura demoura at csl.sri.com
Wed Feb 22 09:46:17 PST 2006


Hi Srihari,

> 1) Does the ";" represent a sequencing of assignments/commands in  
> INITIALIZATION or TRANSITION sections? In A1;A2 is it A2 always  
> performed after A1?

No, A1 and A2 are executed atomically in parallel.

> 2) For a guarded command does the semantics state that all the  
> assignments in "Assignements" are executed atomically? Or can  
> actions from other concurrently composed modules be interleaved  
> with these? eg: if  M1 is "G -> A1 ; A2" and M2 is "A3" can it  
> happen that A3 is executed between A1 and A2 in M1 [] M2?

No, A1 and A2 are executed also atomically in parallel.

Cheers,
Leonardo

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.csl.sri.com/pipermail/sal/attachments/20060222/476b806c/attachment.html


More information about the SAL mailing list