asSet intersection probadorCollection

Context C
invariantCIntersection1 : self.ddec.a->intersection(self.a)->asSet() = self.ddec.a->asSet()
FAIL

Context C
invariantCIntersection2 : self.ddec.a->intersection(self.a)->size()=0
OK

       <details key="invariantCIntersection1" value="self.ddec.a->intersection(self.a)->asSet() = self.ddec.a->asSet()"/>

       <details key="invariantCIntersection2" value="self.ddec.a->intersection(self.a)->size()=0"/>

Genera
 invariant46 = context _C [invariantCIntersection1]
 invariantCIntersection1 self = (((ocl self |.| ddec |.| a''' |->| (intersection (ocl self |.| a'))) |->| asSet)) ||==|| ((ocl self |.| ddec |.| a''' |->| asSet))

 invariant47 = context _C [invariantCIntersection2]
 invariantCIntersection2 self = (((ocl self |.| ddec |.| a''' |->| (intersection (ocl self |.| a'))) |->| size)) |==| (oclInt 0)


Esta retornando una colección vacía