search

symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

State invariant shall only hold at the end of atomic #223

Closed pglvdm closed 10 years ago

pglvdm commented 10 years ago

For an example such as:

process Test =
begin

state 
  n : nat := 0
  m : nat := 0
inv n = m 

operations

Op: nat ==> () 
Op(a) ==
  atomic (
    n := n + a;
    m := m + a)

@ Skip

end

one should only get one PO for the 2 assignments inside Op. The invariant should only hold after the atomic statement is finished (not inside it).

ldcouto commented 10 years ago

This has been fixed as part of the implementation of statement composition in the POG.

Work is still ongoing wrt to Invariant obligations but atomic statements in particular are correctly processed.