Issue: When an AGREE statement in a component type references a property value defined at a higher level, running realizability on that component type does not work (see the first error message image below.) This is understandable since the property value is not defined. However, toggling the setting the error message points to ("Analyze unspecified AADL properties as inputs") also produces an error (see the second error message image below).
I understand this is not straightforward to "fix" since treating unspecified AADL properties as inputs may produce false negative realizability results. Suggestions/options:
1) At a minimum, the second error message should be cleaned up, even if it simply says "Realizability does not support statements that reference unspecified AADL properties"
2) Maybe we want to support treating the AADL properties as inputs for realizability, but we need to inform the user that they might get a false negative depending on the actual values of those AADL properties.
3) Maybe the tool automatically ignores AGREE statements that refer to unspecified AADL property values, warns the user, and runs realizability on the rest of the statements.
4) Maybe the user should have two choices for realizability -- no. 2 or no. 3 above. This seems ideal from my perspective.
Issue: When an AGREE statement in a component type references a property value defined at a higher level, running realizability on that component type does not work (see the first error message image below.) This is understandable since the property value is not defined. However, toggling the setting the error message points to ("Analyze unspecified AADL properties as inputs") also produces an error (see the second error message image below).
I understand this is not straightforward to "fix" since treating unspecified AADL properties as inputs may produce false negative realizability results. Suggestions/options: 1) At a minimum, the second error message should be cleaned up, even if it simply says "Realizability does not support statements that reference unspecified AADL properties" 2) Maybe we want to support treating the AADL properties as inputs for realizability, but we need to inform the user that they might get a false negative depending on the actual values of those AADL properties. 3) Maybe the tool automatically ignores AGREE statements that refer to unspecified AADL property values, warns the user, and runs realizability on the rest of the statements. 4) Maybe the user should have two choices for realizability -- no. 2 or no. 3 above. This seems ideal from my perspective.
I've checked in a small example that exhibits this behavior when running realizability on ComponentA. It is located here: https://github.com/loonwerks/formal-methods-workbench/tree/master/models/agree/property_set_ex
Finally, for reference, I am using OSATE and Agree version 2.4.0.v20190205-2225 (a release Thomas Logan provided to me).