protected Element createTransitionElement(Document document,
			Transition transition) {
		Element te = super.createTransitionElement(document, transition);
		PDATransition t = (PDATransition) transition;
		// Add the characterizing strings for this transition.
		te.appendChild(createElement(document, TRANSITION_READ_NAME, null, t
				.getInputToRead()));
		te.appendChild(createElement(document, TRANSITION_POP_NAME, null, t
				.getStringToPop()));
		te.appendChild(createElement(document, TRANSITION_PUSH_NAME, null, t
				.getStringToPush()));
		return te;
	}