RODIN

Dear Matthias,

Le 9 juin 2011 à 16:59, Matthias Schmalz a écrit :

> I am trying to determine the ISCInvariant corresponding to an 
> IInvariant. My current attempt is
> 
> - get the IMachineRoot of the IInvariant
> - get the ISCMachineRoot
> - search the ISCInvariants of the ISCMachineRoot for one that has the 
> same label as the original IInvariant.
> 
> The attempt fails, because several ISCInvariants may have the label of 
> the original IInvariant (in particular also ISCInvariants inherited from 
> abstract machines).
> So what is the right way to proceed?

ISCInvariant is a subclass of ITraceableElement.  So you should rather use method getSource() to compare with the original invariant.

> My problem would not exist, if Formula.getSourceLocation.getOrigin 
> returned statically checked database elements.

I understand your rant, however the origin of everything is the unchecked element that was entered by the user.  Maybe it was a mistake to flatten these dependencies, but it is unfortunately too late to change it.

Laurent.

Dear Laurent,

Am 09.06.2011 17:15, schrieb Laurent Voisin:
> Dear Matthias,
>
> Le 9 juin 2011 à 16:59, Matthias Schmalz a écrit :
>
>> I am trying to determine the ISCInvariant corresponding to an
>> IInvariant. My current attempt is
>>
>> - get the IMachineRoot of the IInvariant
>> - get the ISCMachineRoot
>> - search the ISCInvariants of the ISCMachineRoot for one that has the
>> same label as the original IInvariant.
>>
>> The attempt fails, because several ISCInvariants may have the label of
>> the original IInvariant (in particular also ISCInvariants inherited from
>> abstract machines).
>> So what is the right way to proceed?
>
> ISCInvariant is a subclass of ITraceableElement.  So you should rather use method getSource() to compare with the original invariant.

Good to know. That solves my issue.

>> My problem would not exist, if Formula.getSourceLocation.getOrigin
>> returned statically checked database elements.
>
> I understand your rant, however the origin of everything is the unchecked element that was entered by the user.  Maybe it was a mistake to flatten these dependencies, but it is unfortunately too late to change it.

I understand that it is too dangerous to change that function. As long 
as we (Gudmund in Edinburgh and me) just do preliminary experiments, 
this is fine. If these experiments are successful and the origin of 
formulae is actually used, a new method with a more meaningful return 
type than object would be useful.

-Matthias