Skip to content

collect RoyalandLoyal

contexto

LoyaltyProgram

       <details key="invariant_minServices" value="(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) >= 0"/> 
       <details key="invariant_minServices2" value="(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) >= 1"/> 
       <details key="invariant_minServices3" value="(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) >= 2"/>
       <details key="invariant_minServices4" value="(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) = 0"/> 
       <details key="invariant_minServices5" value="(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) = 1"/> 
       <details key="invariant_minServices6" value="(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) = 2"/>

Genera OK

invariant1 = context _LoyaltyProgram [invariant_minServices]
 invariant_minServices self = (((ocl self |.| partners |->| collect(\i_ProgramPartner -> ocl          i_ProgramPartner |.| deliveredServices)) |->| size)) |>=| (oclInt 0)
 
 invariant2 = context _LoyaltyProgram [invariant_minServices2]
 invariant_minServices2 self = (((ocl self |.| partners |->| collect(\i_ProgramPartner -> ocl         i_ProgramPartner |.| deliveredServices)) |->| size)) |>=| (oclInt 1)
 
 invariant3 = context _LoyaltyProgram [invariant_minServices3]
 invariant_minServices3 self = (((ocl self |.| partners |->| collect(\i_ProgramPartner -> ocl         i_ProgramPartner |.| deliveredServices)) |->| size)) |>=| (oclInt 2)
 
 invariant4 = context _LoyaltyProgram [invariant_minServices4]
 invariant_minServices4 self = (((ocl self |.| partners |->| collect(\i_ProgramPartner -> ocl         i_ProgramPartner |.| deliveredServices)) |->| size)) |==| (oclInt 0)
 
 invariant5 = context _LoyaltyProgram [invariant_minServices5]
 invariant_minServices5 self = (((ocl self |.| partners |->| collect(\i_ProgramPartner -> ocl         i_ProgramPartner |.| deliveredServices)) |->| size)) |==| (oclInt 1)
 
 invariant6 = context _LoyaltyProgram [invariant_minServices6]
 invariant_minServices6 self = (((ocl self |.| partners |->| collect(\i_ProgramPartner -> ocl         i_ProgramPartner |.| deliveredServices)) |->| size)) |==| (oclInt 2)

No debería dar true en size 2

Edited by Jose Sebastian Sanchez Costa