/*-
 * APT - Analysis of Petri Nets and labeled Transition systems
 * Copyright (C) 2014-2016  Uli Schlachter
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along
 * with this program; if not, write to the Free Software Foundation, Inc.,
 * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 */

package uniol.apt.analysis.synthesize;

import static org.apache.commons.collections4.iterators.EmptyIterator.emptyIterator;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.NoSuchElementException;
import java.util.SortedSet;
import java.util.concurrent.Callable;
import java.util.concurrent.CompletionService;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorCompletionService;
import java.util.concurrent.ForkJoinPool;

import org.apache.commons.collections4.IteratorUtils;
import org.apache.commons.collections4.Transformer;

import uniol.apt.adt.ts.TransitionSystem;
import uniol.apt.analysis.exception.NonDeterministicException;
import uniol.apt.analysis.exception.PreconditionFailedException;
import uniol.apt.util.Pair;

/**
 * Find all words that can be generated by a Petri net from a given class.
 * @author Uli Schlachter
 */
public class FindWords {

	private FindWords() { /* hide constructor */ }

	/**
	 * Number of Runnables that should always be pending for the thread pool. Must be positive.
	 */
	static private final int TARGET_JOB_QUEUE_SIZE = 5;

	static public interface WordCallback {
		public void call(List<Character> wordAsList, String wordAsString, SynthesizePN synthesize);
	}

	static public interface LengthDoneCallback {
		public void call(int length);
	}

	static private SynthesizePN solveWord(List<Character> wordList, PNProperties properties, boolean quickFail) {
		TransitionSystem ts = SynthesizeUtils.makeTS(toStringList(wordList));
		try {
			return SynthesizePN.Builder.createForLanguageEquivalence(ts)
				.setProperties(properties)
				// we don't need failed separation points, if we don't show them
				.setQuickFail(quickFail)
				.build();
		} catch (MissingLocationException e) {
			throw new RuntimeException("Not generating locations and "
					+ " yet they were generated wrongly?!", e);
		} catch (NonDeterministicException e) {
			throw new RuntimeException("Generated a deterministic TS and "
					+ " yet it is non-deterministic?!", e);
		}
	}

	/**
	 * Generate Petri net solvable words with the given characteristics.
	 * @param properties The properties that should be considered.
	 * @param alphabet The alphabet from which words should be generated.
	 * @param quickFail Should quick-fail synthesis be done or should full synthesis be attempted?
	 * @param wordCallback Callback that should be called for each word that is found.
	 * @param lengthDoneCallback Callback that should be called when all words of a given length were handled.
	 * @throws PreconditionFailedException If a combination of properties is specified for which there is no
	 * sensible definition of 'minimally unsolvable word', i.e. plain+k-marking.
	 */
	static public void generateList(PNProperties properties, SortedSet<Character> alphabet, boolean quickFail,
			WordCallback wordCallback, LengthDoneCallback lengthDoneCallback)
			throws PreconditionFailedException {
		// Java 8 provides ForkJoinPool.commonPool(). Java 7 does not, so we need to create our own pool.
		ForkJoinPool executor = new ForkJoinPool();
		try {
			generateList(properties, alphabet, quickFail, wordCallback, lengthDoneCallback, executor);
		} finally {
			executor.shutdownNow();
		}
	}

	static private class NextWordsIterator implements Iterator<String> {
		private final PNProperties properties;
		private final SortedSet<Character> alphabet;
		private final List<String> solvableShorterWords;
		private final Iterator<String> solvableWordsIterator;
		private Iterator<Character> alphabetIterator = emptyIterator();
		private String currentWordToExtend = null;
		private String nextWord = null;

		public NextWordsIterator(PNProperties properties, SortedSet<Character> alphabet,
				List<String> solvableShorterWords) {
			this.properties = properties;
			this.alphabet = alphabet;
			this.solvableShorterWords = solvableShorterWords;
			this.solvableWordsIterator = solvableShorterWords.iterator();

			if (alphabet.isEmpty())
				throw new IllegalArgumentException("Alphabet must not be empty");
		}

		@Override
		public boolean hasNext() {
			if (nextWord != null)
				return true;

			while (alphabetIterator.hasNext() || solvableWordsIterator.hasNext()) {
				if (!alphabetIterator.hasNext()) {
					currentWordToExtend = solvableWordsIterator.next();
					alphabetIterator = alphabet.iterator();

					// They better don't modify the alphabet beneath us!
					assert alphabetIterator.hasNext();
				}

				// If "currentWordToExtend" is unsolvable, then "word" must also be unsolvable.
				// Otherwise we get a contradiction: The net solving "word" will solve "currentWord"
				// after firing "c" once.
				// Put differently: By prepending letters to solvable words, we are sure to
				// generate all solvable words.
				Character c = alphabetIterator.next();
				boolean newLetter = currentWordToExtend.indexOf(c) == -1;
				String word = c + currentWordToExtend;
				word = normalizeWord(toList(word), alphabet);

				if (!properties.isKBounded()) {
					// If we have unbounded places, then every prefix of a solvable word is
					// also solvable: Just add a place from which every transition consumes
					// one token. This place's initial marking limits the length of the
					// word.
					// For our purpose this means: If the prefix isn't solvable, then we
					// already know that the word itself isn't solvable either.
					// This is also important for the definition of "minimally unsolvable"
					// (= unsolvable + all proper subwords are solvable).
					if (Collections.binarySearch(solvableShorterWords,
								word.substring(0, word.length() - 1)) < 0)
						continue;
				} else {
					// In a k-bounded Petri net, every suffix of a solvable word is also
					// solvable. However, a prefix might still be unsolvable. Thus, we use a
					// different definition of "minimally unsolvable" here (= unsolvable +
					// all proper suffixes are solvable).
				}

				nextWord = word;
				if (newLetter)
					// The alphabet is a sorted set. We only extend words in the order that they
					// appear in the alphabet. So if the current letter was new, then all the
					// following ones will be new, too. When extending "ba", "cab" is solvable if
					// and only if "dab" is solvable. So trying other new letters won't produce
					// really "new" words, but only words that are symmetric in the sense that they
					// can be transformed into each other by replacing one letter with another.
					// Avoiding these symmetries in the words we generate helps speeding up this
					// algorithm.
					alphabetIterator = emptyIterator();

				return true;
			}

			return false;
		}

		@Override
		public String next() {
			if (!hasNext())
				throw new NoSuchElementException();
			String result = nextWord;
			nextWord = null;
			return result;
		}

		@Override
		public void remove() {
			throw new UnsupportedOperationException();
		}
	}

	static private void generateList(final PNProperties properties, SortedSet<Character> alphabet,
			final boolean quickFail, WordCallback wordCallback, LengthDoneCallback lengthDoneCallback,
			ForkJoinPool executor) throws PreconditionFailedException {
		if (properties.isPlain() && properties.isKMarking())
			throw new PreconditionFailedException("The combination of plain and k-marking is not supported"
					+ ", because 'minimal unsolvable' cannot be defined");

		CompletionService<Pair<String, SynthesizePN>> completion = new ExecutorCompletionService<>(executor);
		List<String> currentLevel = Collections.singletonList("");
		while (!currentLevel.isEmpty()) {

			// Lazily create new Callables to avoid OOM errors
			Iterator<Callable<Pair<String, SynthesizePN>>> jobGenerator = IteratorUtils.transformedIterator(
					new NextWordsIterator(properties, alphabet, currentLevel),
					new Transformer<String, Callable<Pair<String, SynthesizePN>>>() {
						@Override
						public Callable<Pair<String, SynthesizePN>> transform(
								final String word) {
							return new Callable<Pair<String, SynthesizePN>>() {
								@Override
								public Pair<String, SynthesizePN> call() {
									List<Character> wordList = toList(word);
									SynthesizePN synthesize = solveWord(wordList,
											properties, quickFail);
									return new Pair<>(word, synthesize);
								}
							};
						}
					});

			// Wait for and handle results
			List<String> nextLevel = new ArrayList<>();
			int tasksSubmitted = submitTasks(executor, completion, jobGenerator);
			int tasksFinished = 0;
			while (tasksSubmitted != tasksFinished) {
				String word;
				SynthesizePN synthesize;
				try {
					Pair<String, SynthesizePN> pair = completion.take().get();
					word = pair.getFirst();
					synthesize = pair.getSecond();
				} catch (ExecutionException e) {
					throw new RuntimeException(e);
				} catch (InterruptedException e) {
					Thread.currentThread().interrupt();
					return;
				}

				List<Character> wordList = toList(word);
				wordCallback.call(wordList, word, synthesize);
				if (synthesize.wasSuccessfullySeparated()) {
					nextLevel.add(word);
				}
				tasksFinished++;

				tasksSubmitted += submitTasks(executor, completion, jobGenerator);
			}

			int currentLength = currentLevel.iterator().next().length() + 1;
			lengthDoneCallback.call(currentLength);
			currentLevel = nextLevel;
			Collections.sort(currentLevel);
		}
	}

	static private <T> int submitTasks(ForkJoinPool executor, CompletionService<T> completion,
			Iterator<Callable<T>> jobGenerator) {
		int submitted = 0;
		while (jobGenerator.hasNext() && executor.getQueuedSubmissionCount() < TARGET_JOB_QUEUE_SIZE) {
			completion.submit(jobGenerator.next());
			submitted++;
		}
		return submitted;
	}

	/**
	 * Transform a string into the list of its characters. Note that this does not handle surrogate pairs correctly!
	 * @param word A string to split into characters
	 * @return The list of its characters.
	 */
	static List<Character> toList(String word) {
		List<Character> result = new ArrayList<>(word.length());
		for (int i = 0; i < word.length(); i++)
			result.add(word.charAt(i));
		return result;
	}

	/**
	 * Transform a list of characters into a list of strings, each having length one.
	 * @param argument The list of characters to transform.
	 * @return The equivalent list of strings.
	 */
	static List<String> toStringList(List<Character> argument) {
		List<String> result = new ArrayList<>(argument.size());
		for (char c : argument)
			result.add(String.valueOf(c));
		return result;
	}

	// Normalize a word into the form that the above loop would generate it in. This means e.g. that the word ends
	// with the first letter of the alphabet.
	static private String normalizeWord(List<Character> word, SortedSet<Character> alphabet)
	{
		StringBuilder result = new StringBuilder();
		Map<Character, Character> morphism = new HashMap<>();
		Iterator<Character> alphabetIter = alphabet.iterator();

		for (Character letter : word) {
			Character replacement = morphism.get(letter);
			if (replacement == null) {
				assert alphabetIter.hasNext();
				replacement = alphabetIter.next();
				morphism.put(letter, replacement);
			}
			result.append(replacement);
		}
		return result.toString();
	}
}

// vim: ft=java:noet:sw=8:sts=8:ts=8:tw=120
