Position not reported for specification statement

[pglvdm]

When having a specification statement the run-time error becomes

The specification statement cannot be executed, refine it something explicit if it should be executed at null

The "at null" should be fixed. The model for which this has been tested is:

types
    RANGE = nat inv i == i < 60

channels
    tick, time
    out: RANGE*RANGE    

process AChronometer = begin
state sec: RANGE
      min: RANGE

actions

AInit = [frame wr sec, min pre true and true post sec = 0 and min = 0]

incSec = [frame wr sec pre true post sec = (sec~ + 1) mod 60]     

incMin = [frame wr min pre true post min = (min~ + 1) mod 60]

Run = tick -> incSec(); ([sec = 0] & incMin() [] [sec <> 0] & Skip)
      []
      time -> out!min!sec -> Skip

@ AInit; mu X @ (Run; X)
end

channels inc, minsReq
channels ans: RANGE

process CChronometer = begin
state sec: RANGE
      min: RANGE

actions

SecInit = [frame wr sec pre true post sec = 0]

MinInit = [frame wr min pre true post min = 0]

incSec = [frame wr sec pre true post sec = (sec~ + 1) mod 60]     

incMin = [frame wr min pre true post min = (min~ + 1) mod 60]

RunSec = tick -> incSec(); ([sec = 0] & incMin() [] [sec <> 0] & Skip)
         []
         time -> minsReq -> ans?mins -> out!mins!sec -> Skip

RunMin = inc -> incMin() [] minsReq -> ans!min -> Skip

@ (
    (SecInit(); mu X @ (RunSec; X)) 
        [|{sec}|{|inc, minsReq, ans|}|{min}|]
    (MinInit(); mu X @ (RunMin; X))
)\\{|inc, minsReq, ans|}
end