private void secondBfs(IntersectionNode initialNode, QueueElement parentQueueElement,
    		List<Pair<List<IntersectionTransition>, Integer>> counterexamples,
    		Set<IntersectionNode> visited) {
    	final Deque<QueueElement> queue = new LinkedList<>();
        queue.addLast(new QueueElement(new IntersectionTransition(null, initialNode), null));
        
        while (!queue.isEmpty()) {
        	final QueueElement element = queue.pollFirst();
        	if (visited.contains(element.dest)) {
        		if (element.dest == initialNode && element.predecessor != null) {
	        		// found a loop
        			final List<IntersectionTransition> path = new ArrayList<>();
            		QueueElement elem = element;
            		do {
            			path.add(elem.trans);
            			elem = elem.predecessor;
            		} while (elem != null);
            		path.remove(path.size() - 1);
            		int loopLength = path.size();
            		elem = parentQueueElement;
            		do {
            			path.add(elem.trans);
            			elem = elem.predecessor;
            		} while (elem != null);
            		path.remove(path.size() - 1);
            		Collections.reverse(path);
	        		counterexamples.add(Pair.of(path, loopLength));
	        		return;
	        	}
        	} else {
	        	visited.add(element.dest);
	        	IntersectionTransition trans;
	        	element.dest.resetIterator();
	        	
	        	while ((trans = element.dest.next()) != null) {
	        		if (trans.transition.event != null) {
	        			queue.addLast(new QueueElement(trans, element));
	        		}
	        	}
        	}
        }
    }