package jkind.writers;

import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.PrintWriter;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

import jkind.lustre.Type;
import jkind.solvers.BoolValue;
import jkind.solvers.Model;
import jkind.solvers.Value;

public class XmlWriter extends Writer {
	private PrintWriter out;
	private Map<String, Type> types;

	public XmlWriter(String filename, Map<String, Type> types) throws FileNotFoundException {
		this.types = types;
		this.out = new PrintWriter(new FileOutputStream(filename), true);
	}

	@Override
	public void begin() {
		out.println("<?xml version='1.0'?>");
		out.println("<Results xmlns:xsi='http://www.w3.org/2001/XMLSchema-instance'>");
	}

	@Override
	public void end() {
		out.println("</Results>");
	}

	@Override
	public void writeValid(List<String> props, int k) {
		out.println("  <Property name='" + spaces(props) + "'>");
		out.println("    <K>" + k + "</K>");
		out.println("    <Answer>valid</Answer>");
		out.println("  </Property>");
	}

	private String spaces(List<String> strings) {
		StringBuilder sb = new StringBuilder();
		Iterator<String> iterator = strings.iterator();
		while (iterator.hasNext()) {
			sb.append(iterator.next());
			if (iterator.hasNext()) {
				sb.append(" ");
			}
		}
		return sb.toString();
	}

	@Override
	public void writeInvalid(List<String> props, int k, Model model) {
		out.println("  <Property name='" + spaces(props) + "'>");
		out.println("    <K>" + k + "</K>");
		out.println("    <Answer>falsifiable</Answer>");
		writeCounterexample(k, model);
		out.println("  </Property>");
	}

	private void writeCounterexample(int k, Model model) {
		out.println("    <Counterexample>");
		for (String fn : sort(model.getFunctions())) {
			writeSignal(fn, k, model);
		}
		out.println("    </Counterexample>");
	}

	private void writeSignal(String fn, int k, Model model) {
		out.println("      <Signal name='" + fn + "' type='" + types.get(fn) + "'>");
		Map<Integer, Value> fnMap = model.getFunction(fn);
		for (int i = 0; i < k; i++) {
			if (fnMap.containsKey(i)) {
				out.println("        <Value time='" + i + "'>" + formatValue(fnMap.get(i))
						+ "</Value>");
			}
		}
		out.println("      </Signal>");
	}

	/**
	 * pkind prints booleans as 0/1. We do the same for compatibility, but we
	 * should eventually switch to true/false
	 */
	private String formatValue(Value value) {
		if (value instanceof BoolValue) {
			BoolValue boolValue = (BoolValue) value;
			return boolValue.getBool() ? "1" : "0";
		} else {
			return value.toString();
		}
	}

	public void writeTimeout(List<String> props) {
		out.println("  <Property name='" + spaces(props) + "'>");
		out.println("    <Answer>unknown</Answer>");
		out.println("  </Property>");
	}
}

@@ -682,13 +682,15 @@
 ion=
-'1.0'
+%5C%221.0%5C%22
 ?%3E%22)
@@ -726,17 +726,18 @@
 lns:xsi=
-'
+%5C%22
 http://w
@@ -769,17 +769,18 @@
 instance
-'
+%5C%22
 %3E%22);%0D%0A%09%7D
@@ -943,33 +943,34 @@
  %3CProperty name=
-'
+%5C%22
 %22 + spaces(props
@@ -966,33 +966,34 @@
 paces(props) + %22
-'
+%5C%22
 %3E%22);%0D%0A%09%09out.prin
@@ -1511,33 +1511,34 @@
  %3CProperty name=
-'
+%5C%22
 %22 + spaces(props
@@ -1534,33 +1534,34 @@
 paces(props) + %22
-'
+%5C%22
 %3E%22);%0D%0A%09%09out.prin
@@ -2035,25 +2035,26 @@
 Signal name=
-'
+%5C%22
 %22 + fn + %22' 
@@ -2055,16 +2055,18 @@
  + %22
-'
+%5C%22
  type=
-'
+%5C%22
 %22 + 
@@ -2078,25 +2078,26 @@
 .get(fn) + %22
-'
+%5C%22
 %3E%22);%0D%0A%09%09Map%3C
@@ -2246,17 +2246,18 @@
 ue time=
-'
+%5C%22
 %22 + i + 
@@ -2257,17 +2257,18 @@
  + i + %22
-'
+%5C%22
 %3E%22 + for
@@ -2800,17 +2800,18 @@
 ty name=
-'
+%5C%22
 %22 + spac
@@ -2827,9 +2827,10 @@
  + %22
-'
+%5C%22
 %3E%22);

Use double quotes in XML to match pkind output