Interpreter: Breakpoints in functions used in guards are ignorred by the interpreter

[pglvdm]

So if one for example insert a breakpoint in the PreRecordLanding function here it never stops at the breakpoint:

types
  Aircraft = token

channels
  init, success, failure
  givePermission, recordLanding, recordTakeOff : Aircraft
  getLanded, getPermission : set of Aircraft
  numberWaiting : nat

process Airport =
begin

 functions  
    permitted: Aircraft -> bool
    permitted(a) ==
      true

    down: Aircraft -> bool
    down(a) ==
      false

    PreRecordLanding: Aircraft -> bool
    PreRecordLanding(a) ==
      permitted(a) and not down(a)

  operations

    GivePermission : Aircraft ==> ()
    GivePermission(a) ==
      return 
    pre not permitted(a)

  actions
    Cycle =
       givePermission?a -> 
          ( [not permitted(a)] & success -> GivePermission(a)
            []
            [permitted(a)] & failure -> Cycle)
  @
    init -> Cycle
end

[lausdahl]

The problem reported above can be ignored since the function isn't called at all. However it exposes a different issue where the location of the breakpoints is wrong. This is because the breakpoints is set in the top-most executing behavior and there fore binary constructs that generates new behaviors will report the breakpoints in the wrong place and wrong behavior.

Should be represented by something like:

channels
  c

process P =
begin

 functions  
    permitted: nat -> bool
    permitted(a) ==
      true

  @
    c-> 
     (
       [not permitted(2)] & c->Skip
       []
      [permitted(1)] & c-> Skip
      )
end