Interpreter: Scope rules for calling functions from other functions used in guards messed up

[pglvdm]

I have tried to cut it down to a small model but failed. So I can say that it fails for a CML model like:

types
  Aircraft = token

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

process Airport =
begin
  state
    permission : set of Aircraft := {}
    landed     : set of Aircraft := {}
    inv landed subset permission

 functions  
    permitted: Aircraft * set of Aircraft -> bool
    permitted(a,perm) ==
      a in set perm

    down: Aircraft * set of Aircraft -> bool
    down(a,land) ==
      a in set land

    PreRecordLanding: Aircraft * set of Aircraft * set of Aircraft -> bool
    PreRecordLanding(a,p,l) ==
      permitted(a,p) and not down(a,l)

  operations

    Init : () ==> ()
    Init() ==
      permission := {} ; landed := {}

    GivePermission : Aircraft ==> ()
    GivePermission(a) ==
      permission := permission union {a}
    pre not permitted(a,permission)

    RecordLanding : Aircraft ==> ()
    RecordLanding(a) ==
      landed := landed union {a}
    pre PreRecordLanding(a,landed,permission)

    RecordTakeOff : Aircraft ==> ()
    RecordTakeOff(a) ==
      atomic (
      landed := landed \ {a};
      permission := permission \ {a} )
    pre down(a,landed)

    NumberWaiting : () ==> nat
    NumberWaiting() ==
      return card (permission \ landed)

  actions
    Cycle =
      ( givePermission?a -> 
          ( [not permitted(a,permission)] & success -> GivePermission(a)
            []
            [permitted(a,permission)] & failure -> Skip )
        []
        recordLanding?a ->
          ( [PreRecordLanding(a,permission,landed)] & success -> RecordLanding(a)
            []
            [not PreRecordLanding(a,permission,landed)] & failure -> Skip )
        []
        recordTakeOff?a ->
          ( [down(a,landed)] & success -> RecordTakeOff(a)
            []
            [not down(a,landed)] & failure -> Skip )
        []
        getLanded!landed -> Skip
        []
        getPermission!permission -> Skip
        []
        (dcl w : nat @ w := NumberWaiting(); numberWaiting!w -> Skip )) ; Cycle
  @
    init -> Init(); Cycle
end

With a trace like: [init, recordLanding.mk_token(7)] one gets:

Error 4034: Name 'permitted(Aircraft, set of (Aircraft))' not in scope in '/Users/pgl/Documents/svn/compass/Common/PublicLiveCMLCaseStudies/Airport/Airport.cml' at line 28:6 at in '/Users/pgl/Documents/svn/compass/Common/PublicLiveCMLCaseStudies/Airport/Airport.cml' at line 28:6

which to me indicate that the scope rules are not r´correctly handled when functions in guards call other functions...

[pglvdm]

Sorry I found a smaller model where I can reproduce this issue:

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 PreRecordLanding(a)] & success -> GivePermission(a)
            []
            [permitted(a)] & failure -> Cycle)
  @
    init -> Cycle
end

[lausdahl]

What is the issue that this bug is suppose to represent? scope rules? What function is or should not be in scope where?

[pglvdm]

The error report I get is that the "permitted" function is not in scope when the "PreRecordLanding" function is invoked.

[joey-coleman]

Minimised this further:

process P =
begin
  functions  
    nested: () -> bool
    nested() == true

    outer: () -> bool
    outer() == nested()
  @
    [outer()] & Skip
    -- This is ok:
    -- [nested()] & Skip
end

error at end of trace <c,c> is:

Error 4034: Name 'nested()' not in scope in '/Users/jwc/Development/symphony/ide/product/target/products/eu.compassresearch.ide.product/macosx/cocoa/x86_64/SymphonyIDE/Symphony IDE.app/Contents/MacOS/workspace/a/a.cml' at line 11:15 at in '/Users/jwc/Development/symphony/ide/product/target/products/eu.compassresearch.ide.product/macosx/cocoa/x86_64/SymphonyIDE/Symphony IDE.app/Contents/MacOS/workspace/a/a.cml' at line 11:15