Skip to content
This repository has been archived by the owner. It is now read-only.

AGREE enum issue #81

Closed
janetlj opened this issue Feb 22, 2018 · 2 comments
Closed

AGREE enum issue #81

janetlj opened this issue Feb 22, 2018 · 2 comments
Assignees
Labels

Comments

@janetlj
Copy link

@janetlj janetlj commented Feb 22, 2018

When trying to use AGREE enum type in the AGREE contracts, I found the following things:

  1. enum type can only be defined in an AGREE annex associated with an AADL packages, not with an AADL system.

  2. When I placed the following enum definition in the AGREE annex for an AADL package named "Constants:
    annex agree{**
    enum Status_Type = {DOES_NOT_EXIST, BUILDING, COMPLETE};
    **};

Then add the following AGREE contracts in an AGREE annex for an AADL system named "A_Sys" in another package:
eq status: Constants.Status_Type;
eq transition: bool = (status = Constants.COMPLETE);

Trying to run realizability analysis on the above AADL system returned the following error:

Variable 'Constants.COMPLETE' appears in an assertion, lemma or equation statement in component 'A_Sys_wrapper_Instance' but subcomponent 'Constants' does not contain an AGREE annex

@kfhoech
Copy link
Contributor

@kfhoech kfhoech commented Feb 23, 2018

Duplicated in develop branch hash 2af6b96.

The problem lies in the relatively new implementation of the sanity check for the existence of an annex for all identifiers. The problem is that there is some mismatch as enumerations are lifted to Lustre global types and in some circumstances enumerator expression ids are not.

There are two possible work-arounds which will likely be effective:

  1. Add a 'renames Constants::all;' to your A_Sys package and drop the package name from your enumerators, or

  2. Add a constant for each enumerator to package annexes as follows:

    enum Status_Type = {DOES_NOT_EXIST, BUILDING, COMPLETE};
    const c_DOES_NOT_EXIST : Status_Type = DOES_NOT_EXIST;
    const c_BUILDING : Status_Type = BUILDING;
    const c_COMPLETE : Status_Type = COMPLETE:

and then use the constants rather than the enumerators. That's ugly, I know, but it gives an opportunity for a comment to fix the code once AGREE gets fixed.

@kfhoech kfhoech self-assigned this Feb 23, 2018
@kfhoech kfhoech added bug AGREE labels Feb 23, 2018
@kfhoech
Copy link
Contributor

@kfhoech kfhoech commented Mar 6, 2018

Fixed in pull request 82.

@kfhoech kfhoech closed this Mar 6, 2018
@kfhoech kfhoech added the v2.3.3 label Jul 11, 2018
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants