loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
13 stars 5 forks source link

Error while instantiating the model for check realizability #35

Closed bcbrusse closed 4 years ago

bcbrusse commented 4 years ago

Using OSATE 2.7.1 with version 2.5.1.202007281151 of AGREE, whenever I try to run the realizability check I get the following messages "Error Instantiating model" and "Error while re-instantiating the model: null"

For reference, I just defined a simple system with an agree annex:

package realizability_test public

with Base_Types;

system S
    features
        Input: in data port Base_Types::Float;
        Output: out data port Base_Types::Float;
    annex agree {**
        assume "" : Input < 2.0;
    **};
end S;

end realizability_test;

kfhoech commented 4 years ago

Confirmed.

This seems to be due to a change internal to the OSATE InstantiateModel API where the instantiation process can no longer retrieve the NoCacheDerivedStateAwareResource generated for the ephemeral component implementation of the component type being checked for realizability.

Since there are caching/flushing side-effects hidden behind the Eclipse resource and resource set API, it seems safest to preserve the interaction of finding the components URI and fetching from that URI. However, we must use the resource set for the transactional editing domain for the ephemeral component implementation rather than the OSATE resource set.

kfhoech commented 4 years ago

Fixed by commit 7bb19ce269ce910c621cacf8a4d573c49498adbd.