gistfile1.txt

open util/ordering[Date]

sig Organizer {
  members : set Player,
}

fun games[o : Organizer] : set Tournament {
  Tournament <: organizer.o
}

sig Tournament {
  organizer : Organizer,
  period : Period,
  players : set Player,
  fee : Int
} {
  players in organizer.members
  fee > 0
}

fact {
  all t1, t2 : Tournament {
    t1.organizer = t2.organizer implies
      ((t1 = t2) or not overlap[t1.period, t2.period])
  }
}

sig Date {}
sig Period {
  start : Date,
  end : Date
} {
  lt[start, end]
}

pred overlap[p1, p2 : Period] {
  not (lt[p1.end, p2.start] or lt[p2.end, p1.start])
}

sig Player {
  purse : Int
} {
  not no organizers
  purse >= 0
}

fun games[p : Player] : set Tournament {
  Tournament <: players.p
}

fun organizers[p : Player] : set Organizer {
  Organizer <: members.p
}

//--------------------------------------------------------------------

OverlapShouldDetectOverlap : check {
  all p1, p2 : Period {
    (p1.end   = next[next[p1.start]] and
     p2.start = next[p1.start] and
     p2.end   = next[next[next[p1.start]]]) implies overlap[p1, p2]
  }
  all p1, p2 : Period {
    (p1.end   = next[next[next[p1.start]]] and
     p2.start = next[p1.start] and
     p2.end   = next[next[p1.start]]) implies overlap[p1, p2]
  }
} for 0 but exactly 4 Date, exactly 2 Period

PeriodShouldHaveValidTimeInterval : check {
  all p : Period | lt[p.start, p.end]
}

EveryTournamentsHeldByAnOrganizerShouldNotOverlap : check {
  all o : Organizer | all g1, g2 : o.games {
    (g1 = g2) or not overlap[g1.period, g2.period]
  }
}

AllPlayersInATournamentShouldBeMemberOfTheOrganizer : check {
  all t : Tournament {
    t.players in t.organizer.members
  }
}

EveryPlayerShouldBelongSomeOrganizer : check {
  all p : Player {
    some p.organizers
  }
}

EveryParticipatedGamesShouldBeHeldByOneOfJoinedOrganizer : check {
  all p : Player {
    p.games.organizer in p.organizers
  }
}

ShouldGenerateConsistentInstance : run {
  #Organizer = 1
  #Tournament = 2
  #Period = 2
  #Date = 4
  #Player = 4
} for 4

//--------------------------------------------------------------------

pred entry[t, t' : Tournament, p, p' : Player] {
  // Pre-condition
  p not in t.players
  p.purse >= t.fee
  p in t.organizer.members

  // Post-condition
  p'.purse = minus[p.purse, t.fee]
  p'.games = p.games + t'
  t'.players = t.players + p'

  // Frame condition
  t.organizer.members = t'.organizer.members
  t.period = t'.period
  t.fee = t'.fee

  // Separation condition
  not (t' in p.games) and not (t in p'.games)
}

PlayerShouldBeAbleToJoinATournament : run {
  some t, t' : Tournament, p, p' : Player {
    entry[t, t', p, p']
  }
}