implies RoyalandLoyal
Contexto Membership
invariant_noEarnings
programs.partners.deliveredServices->forAll(s:Service |s.pointsEarned = 0) implies account->isEmpty()
Falla al generar por el is Empty
programs.partners.deliveredServices->forAll(s:Service |s.pointsEarned = 0) implies self.account->size()>0
Falla al generar codigo
Esto
self.programs.partners.deliveredServices->forAll(s:Service | s.pointsEarned = 0)
Genera
invariant8 = context _Membership [invariant_noEarnings]
invariant_noEarnings self = ((ocl self |.| programs' |.| partners |->| collect(\temp1 -> ocl temp1 |.| deliveredServices)) |->| forAll(\s -> (ocl s |.| pointsEarned) |==| (oclInt 0)))
Esto
0=0 implies 1>0
Genera
invariant8 = context _Membership [invariant_noEarnings]
invariant_noEarnings self = ((oclInt 0) |==| (oclInt 0)) |==>| ((oclInt 1) |>| (oclInt 0))
Esto
self.programs.partners.deliveredServices->forAll(s:Service | s.pointsEarned = 0) implies 1>0
Falla causa desconocida hasta el momento
Edited by Jose Sebastian Sanchez Costa