signUpGroup(ident uid, ident id, ident studentId, ident groupId) {
  assume exists /exercise[id] && /exercise[id]/open && 
         exists /account[uid]/student && /account[uid]/student/id = studentId
      || exists /account[uid]/assistant[id];
 
  assume exists /exercise[id]/student[studentId]; # implies the existence of the exercise
  assume exists /exercise[id]/group[groupId]; # also implies it, but once is really enough
 
  assume not exists /exercise[id]/student[studentId]/group;
  assume /exercise[id]/group[groupId]/curSize < /exercise[id]/group[groupId]/maxSize;
 
  insert /exercise[id]/student[studentId]/group groupId;
  update /exercise[id]/group[groupId]/curSize (/exercise[id]/group[groupId]/curSize + 1);
}