import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Calls lookup(decls) and returns the cached value, if any. If a
 * replacement has not been cached, visits each of the children's variable
 * and expression. If nothing changes, the argument is cached and returned,
 * otherwise a replacement Decls object is cached and returned.
 * 
 * @return { d: Decls | d.size = decls.size && all i: [0..d.size) |
 *         d.declarations[i] = decls.declarations[i].accept(delegate) }
 */
public Decls visit(Decls decls) {
	Decls ret = lookup(decls);
	if (ret != null)
		return ret;

	Decls visitedDecls = null;
	boolean allSame = true;
	for (Decl decl : decls) {
		Decls newDecl = visit(decl);
		if (newDecl != decl)
			allSame = false;
		visitedDecls = (visitedDecls == null) ? newDecl : visitedDecls.and(newDecl);
	}
	ret = allSame ? decls : visitedDecls;
	return cache(decls, ret);
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * @see kodkod.ast.visitor.AbstractReplacer#visit(kodkod.ast.Comprehension)
 */
@Override
public final Expression visit(Comprehension expr) {
	Expression ret = lookup(expr);
	if (ret != null)
		return ret;
	final Environment<Expression,Expression> oldRepEnv = repEnv; // skolemDepth
																	// < 0
																	// at
																	// this
																	// point
	final Decls decls = visit((Decls) expr.decls());
	final Formula formula = expr.formula().accept(this);
	ret = (decls == expr.decls() && formula == expr.formula()) ? expr : formula.comprehension(decls);
	repEnv = oldRepEnv;
	return cache(expr, ret);
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Returns a formula that properly constrains the given skolem's domain.
 * 
 * @requires !nonSkolems.isEmpty()
 * @return a formula that properly constrains the given skolem's domain.
 */
private Formula domainConstraint(Decl skolemDecl, Relation skolem) {
	final Iterator<DeclInfo> itr = nonSkolems.iterator();
	Decls rangeDecls = null;
	while (itr.hasNext()) {
		Decl d = itr.next().decl;
		Decl dd = d.variable().oneOf(d.expression());
		rangeDecls = rangeDecls != null ? rangeDecls.and(dd) : dd;
	}
	// System.out.println(skolemDecl.expression());
	Expression skolemDomain = skolem;
	for (int i = 0, max = skolemDecl.variable().arity(); i < max; i++) {
		skolemDomain = skolemDomain.join(Expression.UNIV);
	}
	return skolemDomain.in(Formula.TRUE.comprehension(rangeDecls));
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows (where A_0...A_|A| stand
 * for boolean variables that represent the tuples of the expression A,
 * etc.): let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }"
 * | { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b,
 * ..., x) }.
 * 
 * @param decls the declarations comprehension
 * @param param formula the body of the comprehension
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations;
 *            should be Boolean.TRUE intially
 * @param partialIndex partial index into the provided matrix; should be 0
 *            initially
 * @param matrix boolean matrix that will retain the final results; should
 *            be an empty matrix of dimensions universe.size^decls.length
 *            initially
 * @ensures the given matrix contains the translation of the comprehension
 *          "{ decls | formula }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints,
		int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl == decls.size()) {
		// TODO: what about this and overflow???
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int) StrictMath.pow(interpreter.universe().size(), decls.size() - currentDecl - 1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for (IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl + 1, factory.and(entry.value(), declConstraints),
				partialIndex + entry.index() * position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);
	}
	env = env.parent();
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows (where A_0...A_|A| stand
 * for boolean variables that represent the tuples of the expression A,
 * etc.): let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " | sum a:
 * A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b,
 * ..., x) else 0 }.
 * 
 * @param decls intexpr declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations;
 *            should be Boolean.TRUE intially
 * @param values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size() == currentDecl) {
		Int intExpr = expr.accept(this);
		Int newInt = intExpr.choice(declConstraints, factory.integer(0));
		values.add(newInt);
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for (IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl + 1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);
	}
	env = env.parent();
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Visits the given comprehension, quantified formula, or sum
 * expression. The method returns TRUE if the creator body contains any
 * variable not bound by the decls; otherwise returns FALSE.
 */
private Boolean visit(Node creator, Decls decls, Node body) {
	Boolean ret = lookup(creator);
	if (ret != null)
		return ret;
	boolean retVal = false;
	for (Decl decl : decls) {
		retVal = decl.expression().accept(this) || retVal;
		varsInScope.push(decl.variable());
	}
	retVal = ((Boolean) body.accept(this)) || retVal;
	for (int i = decls.size(); i > 0; i--) {
		varsInScope.pop();
	}
	return cache(creator, retVal);
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
private final Formula cliqueAxiom(Expression color) {
	final Variable[] vars = new Variable[cliqueSize];
	for (int i = 0; i < cliqueSize; i++) {
		vars[i] = Variable.unary("V" + i);
	}
	final List<Expression> members = new ArrayList<Expression>(cliqueSize);
	for (int i = 0, max = cliqueSize - 1; i < max; i++) {
		final List<Expression> tmp = new ArrayList<Expression>();
		for (int j = i + 1; j < cliqueSize; j++) {
			tmp.add(vars[j]);
		}
		members.add(vars[i].product(Expression.union(tmp)));
	}
	Decls d = vars[0].oneOf(node);
	for (int i = 1; i < cliqueSize; i++) {
		d = d.and(vars[i].oneOf(vars[i - 1].join(lessThan)));
	}
	return Expression.union(members).in(color).implies(goalToBeProved()).forAll(d);
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
public final void testQuantifiedFormula() {

		final Variable p = Variable.unary("p"), q = Variable.unary("q");
		final Decl pdecl = p.oneOf(person), qdecl = q.oneOf(person);
		final Decls pqdecls = pdecl.and(qdecl);
		// all p: Person | some p.spouse = true
		assertTrue(eval(p.join(spouse).some().forAll(pdecl)));
		// all p, q: Person | (p.spouse = q) => ! (q in p.shaken) = true
		assertTrue(eval((p.join(spouse).eq(q).implies(q.in(p.join(shaken)).not()).forAll(pqdecls))));
		// some p: Person | no p.shaken = true
		assertTrue(eval(p.join(shaken).no().forSome(pdecl)));
		// all p: Person | some q: Person | p.shaken = q = false
		assertFalse(eval((p.join(shaken).eq(q).forSome(qdecl)).forAll(pdecl)));
		// some p, q: Person | !(p = q) && (p.shaken = q.shaken) = true
		assertTrue(eval(p.eq(q).not().and(p.join(shaken).eq(q.join(shaken))).forSome(pqdecls)));
		// some p: Person | all q: Person-p | p in q.shaken = false
		assertFalse(eval((p.in(q.join(shaken)).forAll(q.oneOf(person.difference(p)))).forSome(pdecl)));
	}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/** Helper method that returns the constraint that the sig has exactly "n" elements, or at most "n" elements */
private Formula size(Sig sig, int n, boolean exact) {
    Expression a = sol.a2k(sig);
    if (n<=0) return a.no();
    if (n==1) return exact ? a.one() : a.lone();
    Formula f = exact ? Formula.TRUE : null;
    Decls d = null;
    Expression sum = null;
    while(n>0) {
       n--;
       Variable v = Variable.unary("v" + Integer.toString(TranslateAlloyToKodkod.cnt++));
       kodkod.ast.Decl dd = v.oneOf(a);
       if (d==null) d=dd; else d=dd.and(d);
       if (sum==null) sum=v; else { if (f!=null) f=v.intersection(sum).no().and(f); sum=v.union(sum); }
    }
    if (f!=null) return sum.eq(a).and(f).forSome(d); else return a.no().or(sum.eq(a).forSome(d));
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/** 
 * Calls lookup(decls) and returns the cached value, if any.  
 * If a replacement has not been cached, visits each of the children's 
 * variable and expression.  If nothing changes, the argument is cached and
 * returned, otherwise a replacement Decls object is cached and returned.
 * @return { d: Decls | d.size = decls.size && 
 *                      all i: [0..d.size) | d.declarations[i] = decls.declarations[i].accept(this) } 
 */
public Decls visit(Decls decls) { 
	Decls ret = lookup(decls);
	if (ret!=null) return ret;
	
	Decls visitedDecls = null;
	boolean allSame = true;
	for(Decl decl : decls) {
		Decls newDecl = visit(decl);
		if (newDecl != decl) 
			allSame = false;
		visitedDecls = (visitedDecls==null) ? newDecl : visitedDecls.and(newDecl);
	}
	ret = allSame ? decls : visitedDecls;
	return cache(decls, ret);
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }" |
 *     { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b, ..., x) }.
 * @param decls the declarations comprehension
 * @param param formula the body of the comprehension
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param partialIndex partial index into the provided matrix; should be 0 initially
 * @param matrix boolean matrix that will retain the final results; should be an empty matrix of dimensions universe.size^decls.length initially
 * @ensures the given matrix contains the translation of the comprehension "{ decls | formula }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, 
		BooleanValue declConstraints, int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl==decls.size()) {
	    //TODO: what about this and overflow???
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int)StrictMath.pow(interpreter.universe().size(), decls.size()-currentDecl-1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), 
				partialIndex + entry.index()*position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " |
 *     sum a: A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b, ..., x) else 0 }.
 * @param decls intexpr declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size()==currentDecl) {
		Int intExpr = expr.accept(this);
           Int newInt = intExpr.choice(declConstraints, factory.integer(0));
           values.add(newInt);
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), decl.expression(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl+1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Returns a slightly different version of the rules that yields
 * better performance than {@linkplain #rules()}.
 * @return rules of the game
 */
public final Formula fastRules() { 
	final List<Formula> rules = new ArrayList<Formula>(3+region.length*region.length);

	final Variable x = Variable.unary("x"), y = Variable.unary("y");
	final Decls decls = x.oneOf(number).and(y.oneOf(number));

	rules.add( grid(x,y).one().forAll(decls) );
	rules.add( grid(x,y).intersection(grid(x, number.difference(y))).no().forAll(decls) );	
	rules.add( grid(x,y).intersection(grid(number.difference(x), y)).no().forAll(decls) );

	for(Relation rx : region) { 
		for(Relation ry: region) { 
			rules.add( complete(rx, ry) );
		}
	}
	return and(rules); 
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
private final Formula cliqueAxiom(Expression color) {
	final Variable[] vars = new Variable[cliqueSize];
	for(int i = 0; i < cliqueSize; i++) { 
		vars[i] = Variable.unary("V"+i);
	}
	final List<Expression> members = new ArrayList<Expression>(cliqueSize);
	for(int i = 0, max = cliqueSize-1; i < max; i++) { 
		final List<Expression> tmp = new ArrayList<Expression>();
		for(int j = i+1; j < cliqueSize; j++) { 
			tmp.add(vars[j]);
		}
		members.add(vars[i].product(Expression.union(tmp)));
	}
	Decls d = vars[0].oneOf(node);
	for(int i = 1; i < cliqueSize; i++) { 
		d = d.and(vars[i].oneOf(vars[i-1].join(lessThan)));
	}
	return Expression.union(members).in(color).implies(goalToBeProved()).forAll(d);
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given comprehension as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let comprehension = "{ a: A, b: B, ..., x: X | F(a, b, ..., x) }" |
 *     { a: A, b: B, ..., x: X | a in A && b in B && ... && x in X && F(a, b, ..., x) }.
 * @param decls the declarations comprehension
 * @param param formula the body of the comprehension
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param partialIndex partial index into the provided matrix; should be 0 initially
 * @param matrix boolean matrix that will retain the final results; should be an empty matrix of dimensions universe.size^decls.length initially
 * @ensures the given matrix contains the translation of the comprehension "{ decls | formula }"
 */
private final void comprehension(Decls decls, Formula formula, int currentDecl, 
		BooleanValue declConstraints, int partialIndex, BooleanMatrix matrix) {
	final BooleanFactory factory = interpreter.factory();

	if (currentDecl==decls.size()) {
		matrix.set(partialIndex, factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final int position = (int)StrictMath.pow(interpreter.universe().size(), decls.size()-currentDecl-1);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		comprehension(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), 
				partialIndex + entry.index()*position, matrix);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given universally quantified formula as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let quantFormula = "all a: A, b: B, ..., x: X | F(a, b, ..., x)" |
 *     (A_0 && B_0 && ... && X_0 => translate(F(A_0, B_0, ..., X_0))) && ... && 
 *     (A_|A| && B_|B| && ... && X_|X| => translate(F(A_|A|, B_|B|, ..., X_|X|))
 * @param decls formula declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.FALSE intially
 * @param acc the accumulator that contains the top level conjunction; should be an empty AND accumulator initially
 * @ensures the given accumulator contains the translation of the formula "all decls | formula"
 */
private void all(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints, BooleanAccumulator acc) {
	if (acc.isShortCircuited()) return;
	final BooleanFactory factory = interpreter.factory();

	if (decls.size()==currentDecl) {
		acc.add(factory.or(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		all(decls, formula, currentDecl+1, factory.or(factory.not(entry.value()), declConstraints), acc);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
	
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given existentially quantified formula as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let quantFormula = "some a: A, b: B, ..., x: X | F(a, b, ..., x)" |
 *     (A_0 && B_0 && ... && X_0 && translate(F(A_0, B_0, ..., X_0))) || ... || 
 *     (A_|A| && B_|B| && ... && X_|X| && translate(F(A_|A|, B_|B|, ..., X_|X|))
 * @param decls formula declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param acc the accumulator that contains the top level conjunction; should be an empty OR accumulator initially
 * @ensures the given accumulator contains the translation of the formula "some decls | formula"
 */
private void some(Decls decls, Formula formula, int currentDecl, BooleanValue declConstraints, BooleanAccumulator acc) {
	if (acc.isShortCircuited()) return;
	final BooleanFactory factory = interpreter.factory();

	if (decls.size()==currentDecl) {
		acc.add(factory.and(declConstraints, formula.accept(this)));
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		some(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), acc);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();

}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Translates the given sum expression as follows 
 * (where A_0...A_|A| stand for boolean variables that represent the 
 * tuples of the expression A, etc.):
 * let sum = "sum a: A, b: B, ..., x: X | IE(a, b, ..., x) " |
 *     sum a: A, b: B, ..., x: X | if (a in A && b in B && ... && x in X) then IE(a, b, ..., x) else 0 }.
 * @param decls intexpr declarations
 * @param formula the formula body
 * @param currentDecl currently processed declaration; should be 0 initially
 * @param declConstraints the constraints implied by the declarations; should be Boolean.TRUE intially
 * @param values integer values computed so far
 */
private final void sum(Decls decls, IntExpression expr, int currentDecl, BooleanValue declConstraints,
		List<Int> values) {
	final BooleanFactory factory = interpreter.factory();
	if (decls.size()==currentDecl) {
		values.add( expr.accept(this).choice(declConstraints, factory.integer(0)) );
		return;
	}

	final Decl decl = decls.get(currentDecl);
	final BooleanMatrix declTransl = visit(decl);
	final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
	env = env.extend(decl.variable(), groundValue);
	for(IndexedEntry<BooleanValue> entry : declTransl) {
		groundValue.set(entry.index(), BooleanConstant.TRUE);
		sum(decls, expr, currentDecl+1, factory.and(entry.value(), declConstraints), values);
		groundValue.set(entry.index(), BooleanConstant.FALSE);	
	}
	env = env.parent();
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
@Test
public final void testQuantifiedFormula() {

	final Variable p = Variable.unary("p"), q = Variable.unary("q");
	final Decl pdecl = p.oneOf(person), qdecl = q.oneOf(person);
	final Decls pqdecls = pdecl.and(qdecl);
	// all p: Person | some p.spouse                            = true
	assertTrue(eval(p.join(spouse).some().forAll(pdecl)));
	// all p, q: Person | (p.spouse = q) => ! (q in p.shaken)   = true
	assertTrue(eval((p.join(spouse).eq(q).implies(q.in(p.join(shaken)).not()).forAll(pqdecls))));
	// some p: Person | no p.shaken                             = true
	assertTrue(eval(p.join(shaken).no().forSome(pdecl)));
	// all p: Person | some q: Person | p.shaken = q            = false
	assertFalse(eval((p.join(shaken).eq(q).forSome(qdecl)).forAll(pdecl)));
	// some p, q: Person | !(p = q) && (p.shaken = q.shaken)    = true
	assertTrue(eval(p.eq(q).not().and(p.join(shaken).eq(q.join(shaken))).forSome(pqdecls)));
	// some p: Person | all q: Person-p | p in q.shaken         = false
	assertFalse(eval((p.in(q.join(shaken)).forAll(q.oneOf(person.difference(p)))).forSome(pdecl)));
}
 

import kodkod.ast.Decls; //导入依赖的package包/类
/**
 * Visits all the children of the given declarations node if
 * this.visited(decls) returns false. Otherwise does nothing.
 * 
 * @ensures all d: declarations.declarations | d.variable.accept(this) &&
 *          d.expression.accept(this)
 */
public void visit(Decls decls) {
	if (visited(decls))
		return;
	for (Decl decl : decls) {
		decl.accept(this);
	}
}