package jkind.util;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;

import jkind.lustre.values.RealValue;
import jkind.lustre.values.Value;
import jkind.results.Counterexample;
import jkind.results.Signal;
import jkind.results.layout.Layout;

public class CounterexampleFormatter {
	private static final int DECIMAL_DIGITS = 3;
	private static final List<String> SEPARATOR = Collections.emptyList();
	private static final String NEWLINE = System.getProperty("line.separator");

	private final Counterexample cex;
	private final Layout layout;

	public CounterexampleFormatter(Counterexample cex, Layout layout) {
		this.cex = cex;
		this.layout = layout;
	}

	@Override
	public String toString() {
		return formatContent(getContent());
	}

	private List<List<String>> getContent() {
		List<List<String>> content = new ArrayList<>();

		content.add(getHeader());
		content.add(getStepCountsRow());

		for (String category : layout.getCategories()) {
			List<Signal<Value>> signals = cex.getCategorySignals(layout, category);
			content.addAll(getSectionRows(category, signals));
		}

		return content;
	}

	private List<String> getHeader() {
		ArrayList<String> header = new ArrayList<>();
		header.add("");
		header.add("Step");
		return header;
	}

	private List<String> getStepCountsRow() {
		List<String> row = new ArrayList<>();
		row.add("variable");
		for (int i = 0; i < cex.getLength(); i++) {
			row.add(Integer.toString(i));
		}
		return row;
	}

	private List<List<String>> getSectionRows(String category, List<Signal<Value>> signals) {
		List<List<String>> rows = new ArrayList<>();
		if (!signals.isEmpty()) {
			rows.add(SEPARATOR);
			rows.add(Collections.singletonList(category.toUpperCase()));
			for (Signal<Value> signal : signals) {
				rows.add(getSignalRow(signal));
			}
		}
		return rows;
	}

	private List<String> getSignalRow(Signal<Value> signal) {
		List<String> row = new ArrayList<>();
		row.add(signal.getName());
		for (int i = 0; i < cex.getLength(); i++) {
			row.add(getString(signal.getValue(i)));
		}
		return row;
	}

	private String getString(Value value) {
		if (Util.isArbitrary(value)) {
			return "-";
		} else if (value instanceof RealValue) {
			RealValue rv = (RealValue) value;
			return rv.value.toTruncatedDecimal(DECIMAL_DIGITS, "~");
		} else {
			return value.toString();
		}
	}

	private String formatContent(List<List<String>> content) {
		List<Integer> minColumnWidths = computeMinimumColumnWidths(content);

		StringBuilder text = new StringBuilder();
		for (int row = 0; row < content.size(); row++) {
			List<String> rowContent = content.get(row);
			for (int col = 0; col < rowContent.size(); col++) {
				String cell = rowContent.get(col);
				String format = getFormatString(col, minColumnWidths.get(col));
				text.append(String.format(format, cell));
			}
			text.append(NEWLINE);
		}

		return text.toString();
	}

	private String getFormatString(int col, int minWidth) {
		if (col == 0) {
			int width = minWidth + 6;
			return "%-" + width + "s ";
		} else {
			int width = minWidth;
			return "%" + width + "s ";
		}

	}

	private List<Integer> computeMinimumColumnWidths(List<List<String>> content) {
		List<Integer> result = new ArrayList<>();
		for (List<String> row : content) {
			for (int i = 0; i < row.size(); i++) {
				expandToFitElement(result, i);
				int curr = result.get(i);
				int next = Math.max(row.get(i).length(), curr);
				result.set(i, next);
			}
		}
		return result;
	}

	private void expandToFitElement(List<Integer> result, int i) {
		while (result.size() - 1 < i) {
			result.add(0);
		}
	}
}

@@ -356,16 +356,68 @@
 TS = 3;%0A
+%09private static final String TRUNCATE_SUFFIX = %22*%22;%0A
 %09private
@@ -530,35 +530,21 @@
 tem.
-getProperty(%22
 line
-.s
+S
 eparator
 %22);%0A
@@ -539,17 +539,17 @@
 eparator
-%22
+(
 );%0A%0A%09pri
@@ -608,16 +608,52 @@
  layout;
+%0A%09private boolean truncated = false;
 %0A%0A%09publi
@@ -836,17 +836,168 @@
 ntent())
-;
+ + footer();%0A%09%7D%0A%0A%09private String footer() %7B%0A%09%09if (truncated) %7B%0A%09%09%09return NEWLINE + %22 * value has been truncated%22 + NEWLINE;%0A%09%09%7D else %7B%0A%09%09%09return %22%22;%0A%09%09%7D
 %0A%09%7D%0A%0A%09pr
@@ -2481,22 +2481,29 @@
 lue;%0A%09%09%09
-return
+String text =
  rv.valu
@@ -2543,12 +2543,108 @@
 TS, 
-%22~%22)
+TRUNCATE_SUFFIX);%0A%09%09%09if (text.contains(TRUNCATE_SUFFIX)) %7B%0A%09%09%09%09truncated = true;%0A%09%09%09%7D%0A%09%09%09return text
 ;%0A%09%09

Use * for truncated values and provide explanation in footer