content: package kodkod.examples.alloy;
  
  import java.util.ArrayList;
  import java.util.List;
  
  import kodkod.ast.Expression;
  import kodkod.ast.Formula;
  import kodkod.ast.Relation;
  import kodkod.ast.Variable;
  import kodkod.engine.Solution;
  import kodkod.engine.Solver;
  import kodkod.engine.config.ConsoleReporter;
  import kodkod.engine.satlab.SATFactory;
  import kodkod.instance.Bounds;
  import kodkod.instance.TupleFactory;
  import kodkod.instance.Universe;
  
  /**
   * KodKod encoding of shakehands.als.
   * 
   * @author Emina Torlak
   */
   public final class Handshake {
  	private final Relation Person, Hilary, Jocelyn, shaken, spouse;
  	
  	public Handshake() {
  		Person = Relation.unary("Person");
  		Hilary = Relation.unary("Hilary");
  		Jocelyn = Relation.unary("Jocelyn");
  		shaken = Relation.binary("shaken");
  		spouse = Relation.binary("spouse");
  	}
  	
  	/**
  	 * Returns the declarations
  	 * @return
  	 * <pre>
  	 * sig Person {spouse: Person, shaken: set Person}
  	 * one sig Jocelyn, Hilary extends Person {}
  	 * </pre>
  	 */
  	public Formula declarations() {
  		final Formula f0 = spouse.function(Person, Person);
  		final Formula f1 = shaken.in(Person.product(Person));
  		final Formula f2 = Hilary.one().and(Jocelyn.one());
  		return f0.and(f1).and(f2);
  	}
  	
  	/**
  	 * Returns the ShakingProtocol fact.
  	 * @return
  	 * <pre>
  	 * fact ShakingProtocol {
  	 *  // nobody shakes own or spouse's hand
  	 *  all p: Person | no (p + p.spouse) & p.shaken
  	 *  // if p shakes q, q shakes p
  	 *  all p, q: Person | p in q.shaken => q in p.shaken
  	 * }
  	 * </pre>
  	 */
  	public Formula shakingProtocol() {
  		final Variable p = Variable.unary("p");
  		final Variable q = Variable.unary("q");
  		final Formula f1 = p.union(p.join(spouse)).intersection(p.join(shaken)).no().forAll(p.oneOf(Person));
  		final Formula f2 = p.in(q.join(shaken)).implies(q.in(p.join(shaken))).forAll(p.oneOf(Person).and(q.oneOf(Person)));
  		return f1.and(f2);
  	}
  	
  	/**
  	 * Returns the Spouses fact.
  	 * @return 
  	 * <pre>
  	 * fact Spouses {
  	 *  all disj p, q: Person {
  	 *   // if q is p's spouse, p is q's spouse
  	 *   p.spouse = q => q.spouse = p
  	 *   // no spouse sharing
  	 *	 p.spouse != q.spouse
  	 *  }
  	 *  all p: Person {
  	 * 	 // a person is his or her spouse's spouse
  	 *	 p.spouse.spouse = p
  	 *	 // nobody is his or her own spouse
  	 *	 p != p.spouse
  	 *	}
  	 * }
  	 * </pre>
  	 */
  	public Formula spouses() {
  		final Variable p = Variable.unary("p");
  		final Variable q = Variable.unary("q");
  		final Formula f1 = p.join(spouse).eq(q).implies(q.join(spouse).eq(p));
  		final Formula f2 = p.join(spouse).eq(q.join(spouse)).not();
  		final Formula f3 = p.intersection(q).no().implies(f1.and(f2)).forAll(p.oneOf(Person).and(q.oneOf(Person)));
  		final Formula f4 = p.join(spouse).join(spouse).eq(p).and(p.eq(p.join(spouse)).not()).forAll(p.oneOf(Person));
  		return f3.and(f4);
  	}
  	
  	/**
  	 * Returns the Puzzle predicate
  	 * @return 
  	 * <pre>
  	 * pred Puzzle() {
  	 *  // everyone but Jocelyn has shaken a different number of hands
  	 *  all disj p,q: Person - Jocelyn | #p.shaken != #q.shaken
  	 *  // Hilary's spouse is Jocelyn
  	 *  Hilary.spouse = Jocelyn
  	 * }
  	 * </pre>
  	 */
  	public Formula puzzle() {
  		final Variable p = Variable.unary("p");
  		final Variable q = Variable.unary("q");
  		final Formula f = p.eq(q).not().implies(p.join(shaken).count().eq(q.join(shaken).count()).not());
  		final Expression e = Person.difference(Jocelyn);
  		return f.forAll(p.oneOf(e).and(q.oneOf(e))).and(Hilary.join(spouse).eq(Jocelyn));
  	}
  	
  	/**
  	 * Returns the conjunction of the facts and the puzzle predicate.
  	 * @return declarations().and(shakingProtocol()).and(spouses()).and(puzzle())
  	 */
  	public Formula runPuzzle() {
  		return declarations().and(shakingProtocol()).and(spouses()).and(puzzle());
  	}
  	
  	/**
  	 * Returns a bounds for the given number of persons.
  	 * @return a bounds for the given number of persons.
  	 */
  	public Bounds bounds(int persons) {
  		final List<String> atoms = new ArrayList<String>(persons);
  		atoms.add("Hilary"); 
  		atoms.add("Jocelyn");
  		for(int i = 2; i < persons; i ++) {
  			atoms.add("Person" + i);
  		}
  		final Universe u = new Universe(atoms);
  		final TupleFactory f = u.factory();
  		final Bounds b = new Bounds(u);
  		b.boundExactly(Person, f.allOf(1));
  		b.boundExactly(Hilary, f.setOf("Hilary"));
  		b.boundExactly(Jocelyn, f.setOf("Jocelyn"));
  		b.bound(spouse, f.allOf(2));
  		b.bound(shaken, f.allOf(2));
  		return b;
  	}
  	
  	private static void usage() {
  		System.out.println("Usage: java examples.Handshake [# persons, must be >= 2]");
  		System.exit(1);
  	}
  	
  	/**
  	 * Usage: java examples.Handshake [# persons, must be >= 2]
  	 */
  	public static void main(String[] args) {
  		if (args.length < 1)
  			usage();
  		
  		final Handshake model =  new Handshake();
  		final Solver solver = new Solver();
  		try {
  			final int persons = Integer.parseInt(args[0]);
  			if (persons<2) usage();
  			solver.options().setBitwidth(6);
  			
  //			solver.options().setSolver(SATFactory.ZChaff);
  			solver.options().setSolver(SATFactory.DEFAULT);
  			
  			solver.options().setSymmetryBreaking(20);
  			solver.options().setBitwidth(32 - Integer.numberOfLeadingZeros(persons));
  			solver.options().setReporter(new ConsoleReporter());
  			final Bounds b = model.bounds(persons);
  			final Formula f = model.runPuzzle();//.and(model.Person.count().eq(IntConstant.constant(persons)));
  			Solution sol = solver.solve(f, b);
  			System.out.println(sol);
  			
  		} catch (NumberFormatException nfe) {
  			usage();
  		} 
  	}
  	
  }
  