* Gets called after the RoBDD was created with the information stored in the
     * syntax tree. Starts with the last func and recursively calls the Then- and
     * Else- funcs
     */
    private void visualizeRoBDD() {
	RoBDD.Func func = m_model.getRob().m_lastFunc;
	helperRoBDD(func, null, false);
	m_connector.improveLayout();
    }

    private void helperRoBDD(RoBDD.Func func, RoBDD.Func fromFunc, boolean isThen) {
	/*
	 * In case there are multiple funcs/nodes with the same variable, to still get
	 * unique IDs for uDraw, the hashCode of the funcs are added to the var
	 */
	if (fromFunc == null) {
	    m_connector.addRootRoBDD(m_model.getRob().getKeyFromVar(func.m_ciVar), func.m_ciVar, func.hashCode());
	} else {
	    m_connector.addNodeRoBDD(m_model.getRob().getKeyFromVar(func.m_ciVar), func.m_ciVar, func.hashCode(),
		    fromFunc.m_ciVar, fromFunc.hashCode(), isThen);
	}

	if (func.m_cThen != null) {
	    helperRoBDD(func.m_cThen, func, true);
	}
	if (func.m_cElse != null) {
	    helperRoBDD(func.m_cElse, func, false);
	}
    }

    /*
     * always saves the result of genVar or ite in RoBDD.m_lastFunc
     */
    private RoBDD.Func syntaxTreeToRoBDD(Node n) {
	if (n != null) {
	    switch (n.type()) {

	    case VAR:
		m_model.getRob().m_lastFunc = m_model.getRob().genVar(n.name());
		return m_model.getRob().m_lastFunc;

	    case NOT:
		m_model.getRob().m_lastFunc = m_model.getRob().ite(syntaxTreeToRoBDD(n.left()),
			m_model.getRob().m_cFalse, m_model.getRob().m_cTrue);
		return m_model.getRob().m_lastFunc;

	    case AND:
		// ite(f,g,0)
		m_model.getRob().m_lastFunc = m_model.getRob().ite(syntaxTreeToRoBDD(n.left()),
			syntaxTreeToRoBDD(n.right()), m_model.getRob().m_cFalse);
		return m_model.getRob().m_lastFunc;

	    case OR:
		// ite(f,1,g)
		m_model.getRob().m_lastFunc = m_model.getRob().ite(syntaxTreeToRoBDD(n.left()),
			m_model.getRob().m_cTrue, syntaxTreeToRoBDD(n.right()));
		return m_model.getRob().m_lastFunc;

	    case IMPLIES:
		// ite(f,g,1)
		m_model.getRob().m_lastFunc = m_model.getRob().ite(syntaxTreeToRoBDD(n.left()),
			syntaxTreeToRoBDD(n.right()), m_model.getRob().m_cTrue);
		return m_model.getRob().m_lastFunc;

	    case EQUIV:
		// ite(f,g,!g)
		m_model.getRob().m_lastFunc = m_model.getRob().ite(syntaxTreeToRoBDD(n.left()),
			syntaxTreeToRoBDD(n.right()), m_model.getRob().ite(syntaxTreeToRoBDD(n.right()),
				m_model.getRob().m_cFalse, m_model.getRob().m_cTrue));
		return m_model.getRob().m_lastFunc;

	    }
	}
	return null;
    }