"old" state components are not visible in the debugger

With a CML model like:

values

  N : nat1 = 1

types
  Status = <READY> | <BLOCKED>
  Process :: id: nat
             status : Status

channels
  admit, wakeup, dispatch : nat
  init, timeout, block, terminate

process ProcessManager =
begin
  state
    running : [nat] := nil
    waiting : seq of Process := []
    inv
      ( running <> nil => forall i in set inds waiting @ waiting(i).id <> running )
      and
      ( forall i,j in set inds waiting @ i <> j => waiting(i).id <> waiting(j).id )

  functions
    findPos(q: seq of Process,id: nat) pos : nat
      pre  exists p in set (elems q) @ p.id = id
      post pos in set elems [i | i in set inds q @ q(i).id = id]

    findNext: seq of Process -> nat1
    findNext(q) ==
      hd [i | i in set inds q @ q(i).status = <READY>]
      pre exists p in set elems q @ p.status = <READY>
      post 
        q(RESULT).status = <READY>
        and
        forall i in set {1,...,RESULT-1} @ q(i).status = <READY>

    remove: seq of Process * nat -> seq of Process
    remove(q, pos) ==
      q(1,...,pos-1) ^ q(pos+1,...,len q)
    pre  pos in set inds q
    post RESULT = q(1,...,pos-1) ^ q(pos+1,...,len q)

    NonNil: [nat] -> bool
    NonNil(n) ==
      n <> nil

    PreAdmit: nat * [nat] * seq of Process -> bool
    PreAdmit(i,r,w) ==
      (r <> nil => i <> r)
      and
      forall p in set elems w @ p.id <> i

    PreDispatch: [nat] * seq of Process -> bool
    PreDispatch(r,w) ==
      r = nil
      and
      exists p in set elems w @ p.status = <READY>

  operations
    Init : () ==> ()
    Init() ==
      running := nil ; waiting := []

    Admit: nat ==> ()
    Admit(id) ==
      waiting := waiting ^ [mk_Process(id,<READY>)]
    pre   PreAdmit(id,running,waiting)
    post  waiting = waiting~ ^ [mk_Process(id,<READY>)]    

    Dispatch: nat ==> ()
    Dispatch(id) ==
      running := waiting(findNext(waiting)).id;
      waiting := remove(waiting,findNext(waiting))
    pre   PreDispatch(running,waiting)
    post  running = waiting~(findNext(waiting~)).id
          --and
          --waiting = remove(waiting~,findNext(waiting~))

  actions
    Cycle =
      ( 
        [] s in set {1,...,N} @ 
            [PreAdmit(s,running,waiting)] & admit.s -> Admit(s)
        []
        [PreDispatch(running,waiting)] & dispatch?s -> Dispatch(s)
      ) ; Cycle
@
  init -> Init(); Cycle
end

one can debug it by choosing the initial steps:

[init, admit.1, dispatch.1]

This then yields a run-time error:

Error 4034: Name 'waiting~' not in scope in '/Users/pgl/Documents/SymphonyIDE/Symphony IDE.app/Contents/MacOS/workspace/Test/Test.cml' at line 76:20 at in '/Users/pgl/Documents/SymphonyIDE/Symphony IDE.app/Contents/MacOS/workspace/Test/Test.cml' at line 76:20

which indicates to me that the environment has not been properly adjusted for the reactive part wrt the "old" states used in post-conditions.

symphonytool / symphony

"old" state components are not visible in the debugger #296