start alloy

vcs.als

sig Repository {
  file: set File
}

fact {
	all rep: Repository |
		no disj f1, f2: rep.file | f1.path = f2.path
}


sig Local {
  file: set File
}

sig Path {}

sig Content {}

sig File {
  path: Path,
  content: Content
}

fact {
  all l: Local |
    all disj f1, f2: l.file |
      not (f1.path = f2.path)
}

run {}

pred commit (rep, rep': Repository, l: Local, f: File) {
  f in l.file
  rep'.file = rep.file ++ f
}

run commit

pred commitTest (rep, rep': Repository, l: Local, f: File) {
	commit [rep, rep', l, f]
	rep != rep'
}

run commitTest

pred update (rep: Repository, l: Local) {
	l.file = rep.file
}

run update