[SAL] Simulates a concurrent program
harryh23 at hotmail.com
Mon Jun 26 07:04:23 PDT 2006
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 :
wait until A.1 = true
wait untile A.3 = true
I thought about simulating this code into SAL tansition. Is it possible to
transform it into the below transition :
pc = locX and A.1 = true --> pc' = locY -- (HHH)
pc = locY --> A.2 ; pc' = locZ -- (FFF)
pc = locZ and A.3 = true --> pc' = locV
I have 3 questions for the above transition.
(1). Does it correctly behave the pseudo-code version of the procedure
(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 ?
More information about the SAL