~tapaal-contributor/tapaal/fix-tikz-export-1945642

package pipe.gui;

import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.List;

import dk.aau.cs.model.tapn.TimedToken;

import pipe.dataLayer.DataLayer;
import pipe.gui.graphicElements.Arc;
import pipe.gui.graphicElements.ArcPathPoint;
import pipe.gui.graphicElements.Place;
import pipe.gui.graphicElements.Transition;
import pipe.gui.graphicElements.tapn.TimedInhibitorArcComponent;
import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
import pipe.gui.graphicElements.tapn.TimedTransportArcComponent;

public class TikZExporter {

	public enum TikZOutputOption {
		FIGURE_ONLY, FULL_LATEX
	}

	private final DataLayer net;
	private final String fullpath;
	private final TikZOutputOption option;

	public TikZExporter(DataLayer net, String fullpath, TikZOutputOption option) {
		this.net = net;
		this.fullpath = fullpath;
		this.option = option;
	}

	public void ExportToTikZ() {
		FileWriter outFile = null;
		PrintWriter out = null;
		try {
			outFile = new FileWriter(fullpath);
			out = new PrintWriter(outFile);

			if (option == TikZOutputOption.FULL_LATEX) {
				out.println("\\documentclass[a4paper]{article}");
				out.println("\\usepackage{tikz}");
				out.println("\\usetikzlibrary{petri,arrows}");
				out.println("\\usepackage{amstext}");
				out.println();
				out.println("\\begin{document}");
				out.println();
				out.println();
			}

			out.println("%% TikZ style options %%");
			out.print(exportTikZstyle());
			out.println();

			out.println("%% TikZ-figure elements %%");
			out.print(exportPlacesWithTokens(net.getPlaces()));
			out.print(exportTransitions(net.getTransitions()));
			out.print(exportArcs(net.getArcs()));

			out.println("\\end{tikzpicture}");
			if (option == TikZOutputOption.FULL_LATEX) {
				out.println("\\end{document}");

			}

		} catch (IOException e) {

		} finally {
			if (out != null) {
                out.close();
            }
			if (outFile != null) {
                try {
                    outFile.close();
                } catch (IOException e2) {

                }
            }
		}
	}

	private StringBuffer exportArcs(Arc[] arcs) {
		StringBuffer out = new StringBuffer();

		for (Arc arc : arcs) {
			String arcPoints = "";

			for (int i = 1; i < arc.getArcPath().getEndIndex(); i++) {
                ArcPathPoint currentPoint = arc.getArcPath().getArcPathPoint(i);

                if(currentPoint.getPointType() == ArcPathPoint.STRAIGHT) {
                    arcPoints += "to[bend right=0] (" + (currentPoint.getX()) + "," + (currentPoint.getY() * (-1)) + ") ";
                } else if (currentPoint.getPointType() == ArcPathPoint.CURVED) {
                    double xCtrl1 = Math.round(currentPoint.getControl1().getX());
                    double yCtrl1 = Math.round(currentPoint.getControl1().getY() * (-1));
                    double xCtrl2 = Math.round(currentPoint.getControl2().getX());
                    double yCtrl2 = Math.round(currentPoint.getControl2().getY() * (-1));

                    arcPoints += " .. controls(" + xCtrl1 + "," + yCtrl1 + ")";
                    arcPoints += " and ";
                    arcPoints += "(" + xCtrl2 + "," + yCtrl2 + ") .. ";
                    arcPoints += "(" + currentPoint.getX() + "," + currentPoint.getY() * (-1) + ") ";
                }
			}

			String arrowType = getArcArrowType(arc);
			String arcLabel = getArcLabels(arc);

			out.append("\\draw[");
			out.append(arrowType);
			out.append("] (");
			out.append(arc.getSource().getId());
			out.append(") ");
			out.append(arcPoints);
			out.append("to[bend right=0]");
			out.append(" (");
			out.append(arc.getTarget().getId());
			out.append(") {};\n");
			if(!arcLabel.equals(""))
				out.append("%% Label for arc between " + arc.getSource().getName() + " and " + arc.getTarget().getName() + "\n");
			out.append(arcLabel);
		}
		return out;
	}

    private String getArcArrowType(Arc arc) {
        String arrowType = "";
        if (arc instanceof TimedInhibitorArcComponent) {
            arrowType = "inhibArc";
        } else if (arc instanceof TimedTransportArcComponent) {
            arrowType = "transportArc";
        } else if (arc instanceof TimedInputArcComponent) {
            arrowType = "arc";
        } else {
            arrowType = "arc";
        }
        return arrowType;
    }

	protected String getArcLabels(Arc arc) {
		String arcLabel = "";
		String arcLabelPositionString = "\\draw (" + (arc.getNameLabel().getX()) + "," + (arc.getNameLabel().getY())*(-1) + ") node {";

		if (arc instanceof TimedInputArcComponent) {
            if (!(arc.getSource() instanceof TimedTransitionComponent)) {
				arcLabel = arcLabelPositionString;
                if (arc.getWeight().value() > 1) {
                        arcLabel += "$" + arc.getWeight().value() + "\\times$\\ ";
                }

                if(CreateGui.getApp().getCurrentTab().getLens().isTimed()) {
                    arcLabel += "$\\mathrm{" + replaceWithMathLatex(getGuardAsStringIfNotHidden((TimedInputArcComponent) arc)) + "}$";
                    if (arc instanceof TimedTransportArcComponent)
                        arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr();
                    arcLabel += "};\n";
                } else {
                    arcLabel += "};\n";
                }

			} else {
				arcLabel = arcLabelPositionString;
                if (arc.getWeight().value() > 1) {
                        arcLabel += "$" + arc.getWeight().value() + "\\times$\\ ";
                }
				arcLabel += ":" + ((TimedTransportArcComponent) arc).getGroupNr() + "};\n";
			}

		} else {
            if (arc.getWeight().value() > 1) {
                arcLabel += arcLabelPositionString + "$" + arc.getWeight().value() + "\\times$\\ };\n";
            }
    	}
		return arcLabel;
	}

	private String getGuardAsStringIfNotHidden(TimedInputArcComponent arc) {
        if (!CreateGui.getApp().showZeroToInfinityIntervals() && arc.getGuardAsString().equals("[0,inf)")){
			return "";
		} else {
			return arc.getGuardAsString();
		}
	}

	private StringBuffer exportTransitions(Transition[] transitions) {
		StringBuffer out = new StringBuffer();
		for (Transition trans : transitions) {
			String angle = "";
			if (trans.getAngle() != 0)
				angle = ",rotate=-" + (trans.getAngle());


			out.append("\\node[transition");
			out.append(angle);		
			out.append("] at (");
			out.append((trans.getPositionX()));
			out.append(',');
			out.append((trans.getPositionY() * (-1)));
			out.append(") (");
			out.append(trans.getId());
			out.append(") {};\n");
			
			if(((TimedTransitionComponent)trans).underlyingTransition().isShared()){
				out.append("\\node[sharedtransition");
				out.append(angle);
				out.append("] at (");
				out.append(trans.getId());
				out.append(".center) { };\n");
			}
                        
			if(((TimedTransitionComponent)trans).underlyingTransition().isUrgent()){
				out.append("\\node[urgenttransition");
				out.append(angle);
				out.append("] at (");
				out.append(trans.getId());
				out.append(".center) { };\n");
			}
            if (((TimedTransitionComponent)trans).underlyingTransition().isUncontrollable()) {
                out.append("\\node[uncontrollabletransition");
                out.append(angle);
                out.append("] at (");
                out.append(trans.getId());
                out.append(".center) { };\n");
            }
			if (trans.getAttributesVisible()){
                boolean isLabelAboveTransition = trans.getY() > trans.getNameLabel().getY();
                boolean isLabelBehindTrans = trans.getX() < trans.getNameLabel().getX();
                double xOffset = trans.getName().length() > 5 && !isLabelAboveTransition && !isLabelBehindTrans ? trans.getLayerOffset() : 0;

				out.append("%% label for transition " + trans.getName() + "\n");
				out.append("\\draw (");
				out.append(trans.getNameLabel().getX() + xOffset + "," + (trans.getNameLabel().getY() * -1) + ")");
				out.append(" node ");
				out.append(" {");
				out.append(exportMathName(trans.getName()));
				out.append("};\n");
			}	
		}
		return out;
	}

	private StringBuffer exportPlacesWithTokens(Place[] places) {
		StringBuffer out = new StringBuffer();

		for (Place place : places) {
			String invariant = getPlaceInvariantString(place);
			String tokensInPlace = getTokenListStringFor(place);

			out.append("\\node[place");
			out.append("] at (");
			out.append(place.getPositionX());
			out.append(',');
			out.append(place.getPositionY() * (-1));
			out.append(") (");
			out.append(place.getId());
			out.append(") {};\n");

            exportPlaceTokens(place, out, ((TimedPlaceComponent) place).underlyingPlace().tokens().size());
			
			if(((TimedPlaceComponent)place).underlyingPlace().isShared()){
				out.append("\\node[sharedplace] at (");
				out.append(place.getId());
				out.append(".center) { };\n");
			}
			if (place.getAttributesVisible() || !invariant.equals("")){
			    boolean isLabelAbovePlace = place.getY() > place.getNameLabel().getY();
			    boolean isLabelBehindPlace = place.getX() < place.getNameLabel().getX();
			    double xOffset = place.getName().length() > 6 && !isLabelAbovePlace && !isLabelBehindPlace ? place.getLayerOffset() : 0;
			    double yOffset = isLabelAbovePlace ? (place.getNameLabel().getHeight() / 2) : 0;

				out.append("%% label for place " + place.getName() + "\n");
				out.append("\\draw (");
				out.append((place.getNameLabel().getX() + xOffset)  + "," + ((place.getNameLabel().getY() * -1) + yOffset) +")");
				out.append(" node[align=left] ");
				out.append("{");
				if(place.getAttributesVisible())
					out.append(exportMathName(place.getName()));					
				if(!invariant.equals("")) {
					if((place.getAttributesVisible()))
						out.append("\\\\");
					out.append(invariant);
				}else {
					out.append("};\n");
				}
					
			}
		}

		return out;
	}

	private void exportPlaceTokens(Place place, StringBuffer out, int numOfTokens) {
        // Dot radius
        final double tRadius = 1;

        // Token dot position offsets
        final double tLeftX = 7;
        final double tRightX = 7;
        final double tTopY = 7;
        final double tBotY = 7;

        boolean isTimed = CreateGui.getApp().getCurrentTab().getLens().isTimed();

        double placeXpos = (place.getPositionX());
        double placeYpos = (place.getPositionY() * (-1));
        double xPos, yPos;

        if(isTimed && numOfTokens > 0) {
            switch (numOfTokens) {
                case 2:
                    out.append("\\node at ("); // Top
                    out.append(placeXpos);
                    out.append(",");
                    out.append(placeYpos + 4);
                    out.append(")");
                    out.append("{0,0};\n");

                    out.append("\\node at ("); // Bottom
                    out.append(placeXpos);
                    out.append(",");
                    out.append(placeYpos - 5);
                    out.append(")");
                    out.append("{0,0};\n");
                    return;
                case 1:
                    out.append("\\node at ("); // Top
                    out.append(placeXpos);
                    out.append(",");
                    out.append(placeYpos);
                    out.append(")");
                    out.append("{0,0};\n");
                    return;
                default:
                    out.append("\\node at (");
                    out.append(placeXpos);
                    out.append(",");
                    out.append(placeYpos);
                    out.append(")");
                    out.append("{$\\mathrm{");
                    out.append("\\#" + numOfTokens + "}$};\n");
                    return;
            }
        } else if(numOfTokens > 5 && !isTimed ) {
            out.append("\\node at (");
            out.append(placeXpos);
            out.append(",");
            out.append(placeYpos);
            out.append(")");
            out.append("{$\\mathrm{");
            out.append("\\#" + numOfTokens + "}$};\n");
            return;
        }

        switch (numOfTokens) {
            case 5: // middle
                out.append("\\node at (");
                out.append(placeXpos);
                out.append(",");
                out.append(placeYpos);
                out.append(")");
                out.append("[circle,fill,inner sep=");
                out.append(tRadius);
                out.append("pt]{};\n");
                /* falls through */
            case 4: // top left
                out.append("\\node at (");
                out.append(placeXpos - tLeftX);
                out.append(",");
                out.append(placeYpos + tTopY);
                out.append(")");
                out.append("[circle,fill,inner sep=");
                out.append(tRadius);
                out.append("pt]{};\n");
                /* falls through */
            case 3:
                if(numOfTokens == 5 || numOfTokens == 4) { // top right
                    xPos = placeXpos + tRightX;
                    yPos = placeYpos + tTopY;
                } else { // top left
                    xPos = placeXpos - tLeftX;
                    yPos = placeYpos + tTopY;
                }
                out.append("\\node at (");
                out.append(xPos);
                out.append(",");
                out.append(yPos);
                out.append(")");
                out.append("[circle,fill,inner sep=");
                out.append(tRadius);
                out.append("pt]{};\n");
                /* falls through */
            case 2:
                if(numOfTokens == 5 || numOfTokens == 4) { // bottom left
                    xPos = placeXpos - tLeftX;
                    yPos = placeYpos - tBotY;
                } else if (numOfTokens == 3){ // middle
                    xPos = placeXpos;
                    yPos = placeYpos;
                } else { // left middle
                    xPos = placeXpos - tLeftX;
                    yPos = placeYpos;
                }
                out.append("\\node at (");
                out.append(xPos);
                out.append(",");
                out.append(yPos);
                out.append(")");
                out.append("[circle,fill,inner sep=");
                out.append(tRadius);
                out.append("pt]{};\n");
                /* falls through */
            case 1:
                if(numOfTokens == 5 || numOfTokens == 4 || numOfTokens == 3) { // bottom right
                    xPos = placeXpos + tRightX;
                    yPos = placeYpos - tBotY;
                } else if (numOfTokens == 2){ // right middle
                    xPos = placeXpos + tRightX;
                    yPos = placeYpos;
                } else { // middle
                    xPos = placeXpos;
                    yPos = placeYpos;
                }
                out.append("\\node at (");
                out.append(xPos);
                out.append(",");
                out.append(yPos);
                out.append(")");
                out.append("[circle,fill,inner sep=");
                out.append(tRadius);
                out.append("pt]{};\n");
            default:
                break;
        }
    }

	protected String getTokenListStringFor(Place place) {
		List<TimedToken> tokens = ((TimedPlaceComponent) place).underlyingPlace().tokens();

		String tokensInPlace = "";
		if (tokens.size() > 0) {
            if (tokens.size() == 1) {
				tokensInPlace = ", structured tokens={" + tokens.get(0).age().setScale(1) + "},";
			} else {
				tokensInPlace = exportMultipleTokens(tokens);
			}
		}
		return tokensInPlace;
	}

	protected String getPlaceInvariantString(Place place) {
        String invariant = "";

		if (!((TimedPlaceComponent) place).getInvariantAsString().contains("inf"))
			invariant = "$\\mathrm{" + replaceWithMathLatex(((TimedPlaceComponent) place).getInvariantAsString()) + "}$};\n";
		return invariant;
	}

	private String exportMultipleTokens(List<TimedToken> tokens) {
		StringBuilder out = new StringBuilder();

		out.append(", structured tokens={\\#");
		out.append(tokens.size());

		out.append("},");
        out.append("pin=above:{\\{");
        for (int i = 0; i < tokens.size() - 1; i++) {
            out.append(tokens.get(i).age().setScale(1));
            out.append(',');
        }
        out.append(tokens.get(tokens.size() - 1).age().setScale(1));
        out.append("\\}},");
        return out.toString();
	}

	private StringBuffer exportTikZstyle() {
		StringBuffer out = new StringBuffer();

		out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n");
                out.append("%% the figure can be scaled by changing xscale and yscale\n");
                out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n");
                out.append("%% can be adjusted so that they do not cover arcs\n");
                out.append("%% similarly the curving of arcs can be done by adjusting bend left/right=XX\n");
                out.append("%% labels may be slightly skewed compared to the tapaal drawing due to rounding.\n");
                out.append("%% This can be adjusted by tuning the coordinates of the label\n");
		out.append("\\tikzstyle{arc}=[->,>=stealth,thick]\n");

        out.append("\\tikzstyle{transportArc}=[->,>=diamond,thick]\n");
		out.append("\\tikzstyle{inhibArc}=[->,>=o,thick]\n");

		out.append("\\tikzstyle{every place}=[minimum size=6mm,thick]\n");
		out.append("\\tikzstyle{every transition} = [fill=black,minimum width=2mm,minimum height=5mm]\n");
		out.append("\\tikzstyle{every token}=[fill=white,text=black]\n");
		out.append("\\tikzstyle{sharedplace}=[place,minimum size=7.5mm,dashed,thin]\n");
		out.append("\\tikzstyle{sharedtransition}=[transition, fill opacity=0, minimum width=3.5mm, minimum height=6.5mm,dashed]\n");
		out.append("\\tikzstyle{urgenttransition}=[place,fill=white,minimum size=2.0mm,thin]");
        out.append("\\tikzstyle{uncontrollabletransition}=[transition,fill=white,draw=black,very thick]");
        return out;
	}

	protected String replaceWithMathLatex(String text) {
		return text.replace("inf", "\\infty").replace("<=", "\\leq ").replace("*", "\\cdot ");
	}

	private String exportMathName(String name) {
		StringBuilder out = new StringBuilder("$\\mathrm{");
		int subscripts = 0;
		for (int i = 0; i < name.length() - 1; i++) {
			char c = name.charAt(i);
			if (c == '_') {
				out.append("_{");
				subscripts++;
			} else {
				out.append(c);
			}
		}

		char last = name.charAt(name.length() - 1);
		if (last == '_') {
			out.append("\\_");
		} else
			out.append(last);

		for (int i = 0; i < subscripts; i++) {
			out.append('}');
		}
		out.append("}$");
		return out.toString();
	}

}