[SAL] Transition with guard commands

[harry huang]

Hi,

Some questions regarding the transition with guard commands. Does the "[]" 
in the  transition block are asynchronous ? The "-->" means wait condition ?

For instance,

=====
       TRANSITION
      [
          x1= 0  --> x'= 0;  pc' = locX                 --(1)
         []
          (x /= 0) AND pc = locX --> pc' = locError    --(2)
         []
          x2= 1 --> x' = 1;  pc' = locY             --(3)
         []
          (x/=1) AND pc = locY --> pc' = locError   --(4)
      ]
=====

x1, x2 are the INPUT and x, pc are the OUTPUT. But the theorem "th1: THEOREM 
data |- G(pc /= locError) " does not hold. The countexample seems system 
asychronously executed (1) when executing the guard condition in (4). So 
(4)'s guard condition was satisfied and "pc' = locError" was reached.  So I 
am wondering what is the execution order in above transitions ? Is the guard 
command condition the wait condition ?

In addition, I noticed before queries said that A1; A2 are performed 
atomically in the gurard command "M1 AND M2 --> A1; A2 ". But how about "M1 
AND M2" ? Is it still atomic ?

Thanks. I hope those questions can be clarified as they are not mentioned 
explictly in the web notes and critical to my program.

Harry