search

loonwerks / Resolute

BSD 3-Clause "New" or "Revised" License
2 stars 1 forks source link

Support of property record in resolute #1

Closed kfhoech closed 1 year ago

kfhoech commented 4 years ago

Issue by juli1 Monday Nov 02, 2015 at 18:11 GMT Originally opened as https://github.com/smaccm/smaccm/issues/40

We would need to support property record when analyzing property. Right now, record are not used/managed. See https://github.com/osate/examples/blob/master/core-examples/resolute/property-record.aadl for an example of a model and https://github.com/osate/examples/blob/master/core-examples/resolute/property-record-theorem.aadl for the associated theorem.

The function property_member does not exist, it should be a function specific to property record.

The goal is to be able to parse the following code and get resolute able to analyze the model.

iamundson commented 1 year ago

property_member was implemented a while ago so the property-record example is working. However, no 'record' type is defined in Resolute, so the following still isn't possible:

test (c : component) <=
    ** "test" **
    -- The Record_Test::Record_List property is a list of records
    let records : [record] = property(c, Record_Test::Record_List);
    forall(r : as_set(records)) . check_record(r)

It looks like adding a 'record' type to the xtext grammar should do the trick, as the other necessary infrastructure to support this has already been implemented.

kfhoech commented 1 year ago

There is also the ResoluteRecordValue which is not first class as it does not have a corresponding type in the Resolute grammar.

If possible, it would be nice to unify the property records with the added record type and have ResoluteRecordValue instances be of record type.