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

[spmiller at rockwellcollins.com]

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