[SAL] Transition with guard commands
harryh23 at hotmail.com
Thu Jun 29 08:49:15 PDT 2006
Some questions regarding the transition with guard commands. Does the ""
in the transition block are asynchronous ? The "-->" means wait condition ?
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.
More information about the SAL