Context t: Tournament
inv: matches- >forall(m:Match | m.start.after(t.start) and m.end.before(t.end))
It means we have a tournament called t. And every match e belongs to the tournament has to be held within it.
Say if the tournament will be held for the whole April, then all the related matches has be held within April.
1 comment:
You write very well.
Post a Comment