For the POG, given a state invariant and atomic assignment, the assignments show up in the antecedent of the PO predicate. For example:
process Test = begin
state
x :int
y :int
inv
x = y
operations
op : () ==> ()
op()== atomic(x:=1; y:=1)
@Skip
end
Will yield 1=1 => 1 =1. The cause is that the list of assignments in the atomic is being traversed and context information is collected for all of them. This must be changed and the POG must process the entire atomic in one go.
For the POG, given a state invariant and atomic assignment, the assignments show up in the antecedent of the PO predicate. For example:
Will yield
1=1 => 1 =1
. The cause is that the list of assignments in the atomic is being traversed and context information is collected for all of them. This must be changed and the POG must process the entire atomic in one go.