The type system treats ENFORCE and RULE differently.

[stefjoosten]

What happened

I am trying to compile the following program:

CONTEXT "Issue1397"

CLASSIFY Application ISA MaintainedItem

RELATION deployed[MaintainedItem*Platform]
RELATION loaded[Application*Platform]

ENFORCE loaded >: deployed

ENDCONTEXT

This produces an error message:

% ampersand check Issue1397.adl
Issue1397.adl:8:1 error:
  Type error, cannot match:
    the concept MaintainedItem (Src of deployed [MaintainedItem*Platform])
    and concept Application (Src of RELATION loaded [Application*Platform]  )
ExitFailure 10

The following script contains the workaround:

CONTEXT "Issue1397"

CLASSIFY Application ISA MaintainedItem

RELATION deployed[MaintainedItem*Platform]
RELATION loaded[Application*Platform]

ENFORCE loaded >: I[Application];deployed

ENDCONTEXT

This compiles flawlessly.

What I expected

I expected that the statement

ENFORCE loaded >: deployed

would be type checked identically to:

RULE loaded >: deployed

Version of ampersand that was used

Ampersand-v4.7.1

[hanjoosten]

Please use the latest generator. Does it happen with release 4.7.6 as well?

[hanjoosten]

I can confirm that it is in release 4.7.6 as well. Hopefully @sjcjoosten can take a look. Of course, you can use a workaround:

CONTEXT Issue1397

CLASSIFY Application ISA MaintainedItem

RELATION deployed[MaintainedItem*Platform]
RELATION loaded[Application*Platform]

ENFORCE loaded >: I[Application];deployed

ENDCONTEXT

[stefjoosten]

It is a bug

I tried to generate a prototype from the following script:

CONTEXT "Issue1397-1"

    CLASSIFY Application ISA MaintainedItem

    RELATION deployed[MaintainedItem*Platform]
    RELATION loaded[Application*Platform]
    RELATION flv[Application*Discipline] [UNI]

    ENFORCE deployed >: flv#"FLV" - loaded

ENDCONTEXT

This was the response (some intermediate lines have been left out)

% ampersand proto model/Issue1398.adl --verbose
2023-03-10 11:17:10.961347: [debug] Ampersand-v4.7.1 [Conceptual-Analysis:5903bb784] runs with the following settings:
2023-03-10 11:17:10.965070: [debug] --[no-]backend True

...

2023-03-10 11:17:11.189162: [info] Generating frontend...
2023-03-10 11:17:11.190095: [debug] Start copy templates
2023-03-10 11:17:11.190158: [debug]   From: ./templates
2023-03-10 11:17:11.191100: [debug]   To:   .proto/templates
2023-03-10 11:17:11.191247: [debug] No project specific templates are copied (there is no such directory ./templates)
!             Ampersand-v4.7.1 [Conceptual-Analysis:5903bb784]
Cannot unite (with operator "\/") term l of type [Application*Platform]
   ECpl (EDif (EPrd (EDcD flv[Application*Discipline],EMp1 "FLV" Platform),EDcD loaded[Application*Platform]))
   with term r of type [MaintainedItem*Platform]
   EDcD deployed[MaintainedItem*Platform]
CallStack (from HasCallStack):
  fatal, called at src/Ampersand/Core/AbstractSyntaxTree.hs:1096:10 in ampersand-4.7.1-Evu2DMMq1n0JnK2WkVlrg5:Ampersand.Core.AbstractSyntaxTree
2023-03-10 11:17:11.205840: [error] ExitFailure 2

I expected that fatals never occur. This proves that this is a bug (and not a feature).

[stefjoosten]

Analysis

I hypothesize that the operator >: in the ENFORCE rules is treated differently from the operator |- in RULE. Let's gather some evidence for that...

[stefjoosten]

I will add the programd Issue1397.adl and Issue1397-1.adl to Ampersand/testing/Travis/testcases/Bugs/Current/Other. I will also add a command to testinfo.yaml in that same directory (Currently, it is empty):

testCmds:
  - command: ampersand validate --verbose
    exitcode: 0
  - command: ampersand proto --verbose
    exitcode: 0