Verification of QLOCK

If a process/agent is in the critical section then it is at the top of waiting queue.
```
ceq [qinv]:  top(sq(S:Sys)) = I:X$Pid if pc(S:Sys,I:X$Pid) = cs .
```
See qinv.maude for the proof.
Only one agent can be in the critical section at a given moment.
```
 ceq [qgoal]: I:X$Pid  = J:X$Pid if pc(S:Sys,I:X$Pid) = cs /\ pc(S:Sys,J:X$Pid) = cs .
```
See qgoal.maude for the proof.

Back