private void invalidDefinitionConstraints(List<BooleanFormula> constraints) {
		for (NegativeMealyNode parent : negativeTree.nodes()) {
			for (MealyTransition t : parent.transitions()) {
				MealyNode child = t.dst();
				String event = t.event();
				FormulaList options = new FormulaList(BinaryOperations.OR);
				options.add(invalid(parent));
				for (int colorParent = 0; colorParent < colorSize; colorParent++) {
					// either no transition
					FormulaList innerYConstraints = new FormulaList(BinaryOperations.AND);
					for (int colorChild = 0; colorChild < colorSize; colorChild++) {
						innerYConstraints.add(yVar(colorParent, colorChild, event).not());
					}
					BooleanFormula yFormula = completenessType == CompletenessType.NORMAL ?
							FalseFormula.INSTANCE : innerYConstraints.assemble();
					
					// or actions on the transition are invalid
					FormulaList innerZConstraints = new FormulaList(BinaryOperations.OR);
					for (String action : actions) {
						BooleanFormula v = zVar(colorParent, action, event);
						if (ArrayUtils.contains(t.actions().getActions(), action)) {
							v = v.not();
						}
						innerZConstraints.add(v);
					}
					
					options.add(xxVar(parent.number(), colorParent)
							.and(innerZConstraints.assemble().or(yFormula)));
				}
				constraints.add(invalid(child).equivalent(options.assemble()));
			}
		}
	}