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
Edited by Jose Sebastian Sanchez Costa