package de.renew.lola2.test;

import java.io.File;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import org.junit.Assert;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;

import CH.ifa.draw.io.DrawingFileHelper;
import CH.ifa.draw.io.StatusDisplayer;
import de.renew.draw.storables.ontology.Drawing;
import de.renew.gui.CPNDrawing;
import de.renew.lola2.LolaFileCreator;
import de.renew.lola2.analysis.LolaResult;
import de.renew.lola2.analysis.LolaResultStatus;
import de.renew.lola2.analysis.PropertyAnalyzer;

import static org.junit.Assert.fail;


public class LolaTest implements StatusDisplayer {
    File _testNet;
    private List<File> _tasknets;
    private int _taskTests;
    private Map<String, LolaResultStatus> _taskResults;
    private static File _samplesFolder;
    private static File _libFolder;


    /**
     * Finds the samples folder
     */
    @BeforeClass
    public static void setUpOnce() {
        File location = new File("./").getAbsoluteFile().getParentFile();
        System.out.println("PWD is " + location.getAbsolutePath());
        System.out.println("Name is " + location.getName());
        File lolaDir = null;
        if (location.getName().equals("Lola2")) {
            lolaDir = location.getParentFile();
        } else {
            lolaDir = location;
        }

        if (lolaDir != null) {
            _samplesFolder = new File(lolaDir, "Lola2/src/main/resources/samples");
            String os = System.getProperty("os.name").toLowerCase();

            if (os.contains("linux")) {
                _libFolder = new File(lolaDir, "Lola2/lib/linux64");
            } else if (os.contains("mac")) {
                _libFolder = new File(lolaDir, "Lola2/lib/macintel");
            } else if (os.contains("windows")) {
                _libFolder = new File(lolaDir, "Lola2/lib/win64");
            }
            System.out.println("samples Folder is " + _samplesFolder.getAbsolutePath());
        } else {
            fail("Could not find samples folder");
        }
    }

    @Test
    public void testBoundedPlaces() {
        //URL testNetUrl = LolaTest.class.getResource("/samples/test-bounded-places.rnw");
        String netName = "test-bounded-places.rnw";
        _testNet = new File(_samplesFolder, netName);
        System.out.println("Checking net in " + _testNet.getAbsolutePath());
        if (_testNet.exists()) {
            Map<String, LolaResultStatus> places2results = new HashMap<>();
            places2results.put("p1", LolaResultStatus.YES);
            places2results.put("p2", LolaResultStatus.NO);
            places2results.put("p3", LolaResultStatus.YES);
            places2results.put("notexisting", LolaResultStatus.ERROR);
            System.out.println(places2results);
            Drawing drawing = DrawingFileHelper.loadDrawing(_testNet, this);
            File netFile = new LolaFileCreator().writeTemporaryLolaFile((CPNDrawing) drawing);
            PropertyAnalyzer analyzer = new PropertyAnalyzer(_libFolder.toString());

            for (String p : places2results.keySet()) {
                LolaResult bounded = analyzer.checkPlaceBoundedness(p, netFile);
                LolaResultStatus i = places2results.get(p);
                LolaResultStatus j = bounded.getStatus();
                System.out.println("Expected: " + i + " - Returned: " + j);
                Assert.assertEquals(i, j);
            }
        } else {
            fail("Net not found");
        }
    }

    @Test
    public void testQuasiLiveTransitions() {
        String netName = "test-dead-transitions.rnw";
        _testNet = new File(_samplesFolder, netName);
        System.out.println("Checking net in " + _testNet.getAbsolutePath());
        if (_testNet.exists()) {
            Map<String, LolaResultStatus> transitions2results = new HashMap<>();
            transitions2results.put("t1", LolaResultStatus.YES);
            transitions2results.put("t2", LolaResultStatus.YES);
            transitions2results.put("t3", LolaResultStatus.YES);
            transitions2results.put("t4", LolaResultStatus.YES);
            transitions2results.put("t5", LolaResultStatus.YES);
            // according to LoLA1, t6 and t7 are dead but LoLA2 is not able to compute this
            transitions2results.put("t6", LolaResultStatus.ERROR);
            transitions2results.put("t7", LolaResultStatus.ERROR);
            transitions2results.put("notexisting", LolaResultStatus.ERROR);
            System.out.println(transitions2results);
            Drawing drawing = DrawingFileHelper.loadDrawing(_testNet, this);
            File netFile = new LolaFileCreator().writeTemporaryLolaFile((CPNDrawing) drawing);
            PropertyAnalyzer analyzer = new PropertyAnalyzer(_libFolder.toString());

            for (String t : transitions2results.keySet()) {
                LolaResult quasiLive = analyzer.checkTransitionQuasiLiveness(t, netFile);
                LolaResultStatus i = transitions2results.get(t);
                LolaResultStatus j = quasiLive.getStatus();
                System.out.println("Expected: " + i + " - Returned: " + j);
                Assert.assertEquals(i, j);
            }
        } else {
            fail("Net not found");
        }
    }

    @Test
    public void testLiveDeadTransitions() {
        // TODO
    }

    @Before
    public void setupTaskRelated() {
        String task1 = "FORMULA EF (p_end1 = 4 AND p_end2 = 1 AND p_end2 = 0)";
        String task2 = "FORMULA EF (p_end1 = 4 AND p_start2 = 1 AND p_end2 = 1)";
        String task3 = "FORMULA AG p_end1 < oo";
        String task4 = "FORMULA AG p1 < oo";

        _tasknets = new ArrayList<File>();
        File net1 = new File(_samplesFolder, "test-tasks-marking.rnw");
        _tasknets.add(net1);

        _taskResults = new HashMap<>();
        _taskResults.put(task1, LolaResultStatus.YES); // marking (0,4,0,1) is reachable
        _taskResults.put(task2, LolaResultStatus.NO); // marking (0,4,1,1) is not reachable
        _taskResults.put(task3, LolaResultStatus.YES); // place is bounded
        _taskResults.put(task4, LolaResultStatus.ERROR); // syntax error p1 does not exist

        _taskTests = 1;
    }

    /**
     * Reads all sample _tasknets, creates LolaTask objects for all
     * TextFigures in the net, writes them into lola task files and
     * checks them with lola.
     */
    @Test
    public void testLolaTask() {
        // TODO: Create meningful CTL tests. The following test is supposed to be run with the JavaNetCompiler, which 
        // is problematic because the LolaFileCreator gets the used compiler from the FormalismPlugin
        // The corresponding test works in LoLA1 (not sure why).
        //        assertTrue("Number of task tests should match number of test nets.", tasknets.size() == taskTests);
        //        System.out.println("--------------------- testLolaTask ----------------------");
        //        LolaAnalyzer analyzer = new LolaAnalyzer(libFolder.getPath());
        //        for (File f : tasknets) {
        //            Drawing taskDrawing = DrawingFileHelper.loadDrawing(f, (StatusDisplayer) this);
        //            if (!(taskDrawing instanceof CPNDrawing)) {
        //                fail("Net " + f + " is not a CPNDrawing");
        //            }
        //            FigureEnumeration figs = taskDrawing.figures();
        //            while (figs.hasMoreElements()) {
        //                Figure fig = figs.nextElement();
        //                if (fig instanceof TextFigure) {
        //                    TextFigure textFig = (TextFigure) fig;
        //                    String text = textFig.getText();
        //                    if (text.toLowerCase().startsWith("formula")) {
        //                        LolaTask task = new LolaTask((TextFigure) fig, (CPNDrawing) taskDrawing);
        //                        LolaResultStatus status = task.check(analyzer).getStatus();
        //                        LolaResultStatus expected = taskResults.get(text);
        //                        System.out.println("[Text Figure] " + text);
        //                        System.out.println("[TaskResult Expected] " + expected);
        //                        System.out.println("[Result] " + status);
        //                        assertEquals("Result must match expected result", expected, status);
        //                    }
        //                }
        //            }
        //        }
    }


    @Override
    public void showStatus(String message) {
        // TODO Auto-generated method stub
        System.out.println(">>" + message);
    }
}