[SAL-HELP] Making non-deterministic choices in guarded commands

[Leonardo de Moura]

Hi Steve,

You need to use a multi-command. It is exactly what you want, a non- 
deterministic
choice whose scope is the whole command (guard + assignment). Your  
transition can
be rewritten in the following way using a multi-command:

...
[]
([] (t : TASK) :  current_task = idle AND assignment(t) = p AND  
can_progress(t, progress[t] + 1, switch)
                          -->
                          current_task' = t;
                          switch' = update_switch(current_task',  
progress[t] + 1, switch)
)
[]
...

Cheers,
Leonardo.


On Aug 14, 2006, at 6:27 AM, <spmiller at rockwellcollins.com> wrote:

> Greetings,
>
> I'm working on a small SAL example and am having trouble making a
> non-deterministic choice that will apply to all the definitions in a
> guarded command.  More specifically, I'd like to write something like
>
>                 ...
>       [] resume_another_task:
>                   current_task = Idle AND
>                         (EXISTS (t: TASK): assignment(t) = p AND
> can_progress(t, progress[t] + 1, switch))
>                   --> current_task' IN
>                         {t: TASK | assignment(t) = p AND  
> can_progress(t,
> progress[t] + 1, switch)};
>                         switch' = update_switch(current_task',
> progress[current_task'] + 1, switch)
>                 []
>
> The guard ensures that the set to choose current_task' from is not  
> empty,
> and setting current_task' in this way seems to work.  However, I  
> need to be
> able to refer to the same selection when updating the switch in the  
> last
> line and SAL doesn't seem to like the use of current_task' in the  
> rhs of
> the assignment.  It doesn't complain, but sal-inf-bmc goes into an  
> infinite
> loop during model checking unless the last line is commented out.
>
> I can't figure out how to use a Let statement so that the  
> nondeterminsitic
> choice can be applied to both definitions in the guarded command  
> and am
> wondering if there is any way to do this.  I'll be happy to share  
> the full
> example with an individual, but am reluctant to post it on the general
> forum.
>
> Thanks,
>
> Steve Miller
> Rockwell Collins