[SAL] Simulates a concurrent program

[harry huang]

Hi,

I am just wondering about how to simulate a procedure concurrent program and 
its wait condition. For instance, the pseudo-code of a concurrent program  :

===
class A
Begin
    wait until A.1 = true
     ....
     A.2
    wait untile A.3 = true
End
===

I thought about simulating this code into SAL tansition. Is it possible to 
transform it  into  the below transition :

======
TRANSITION
[
  Firstwait:
     pc = locX and A.1 = true --> pc' = locY    -- (HHH)
  []
  Processingcode:
     pc = locY --> A.2 ; pc' = locZ                  -- (FFF)
  []
  Secondwait:
     pc = locZ and A.3 = true  --> pc' = locV
  []
  ELSE -->
]
=====

I have 3 questions for the above transition.

(1). Does it correctly behave the pseudo-code version of the procedure 
language ?

(2).Is the guard in the SAL transition a wait condition ? In other words,  
the guard " pc = locX and A.1" waits until it becomes true ?  However, since 
there is "ELSE" transition indicating in the above transition,, so if  the 
guard " pc = locX and A.1" is unsatisfied , does the transition jump to 
execute "ELSE" part , which is not we want to see because "ELSE" part 
represents the end of our procedure program.

(3). For the FFF and HHH mark in the above transition, I am wondering the  
"pc = locX and A.1 = true"  and "A.2 ; pc' = locZ " are atomic ?

Thanks.
Harry