/*-
 * APT - Analysis of Petri Nets and labeled Transition systems
 * Copyright (C) 2012-2013  Members of the project group APT
 *
 * 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.io.parser.impl;

import static org.hamcrest.MatcherAssert.assertThat;
import static org.hamcrest.Matchers.contains;
import static org.hamcrest.Matchers.containsInAnyOrder;
import static org.hamcrest.Matchers.empty;
import static org.hamcrest.Matchers.hasSize;
import static org.hamcrest.Matchers.is;
import static uniol.apt.adt.matcher.Matchers.flowThatConnects;
import static uniol.apt.adt.matcher.Matchers.nodeWithID;

import org.testng.annotations.Test;

import uniol.apt.adt.pn.Flow;
import uniol.apt.adt.pn.Node;
import uniol.apt.adt.pn.PetriNet;
import uniol.apt.adt.pn.Place;
import uniol.apt.adt.pn.Token;
import uniol.apt.adt.pn.Transition;
import uniol.apt.io.parser.ParseException;

/**
 * Test wether the Petrify parser works.
 * @author Sören, Uli Schlachter
 */
@SuppressWarnings("unchecked")
public class PetrifyPNParserTest {
	@Test
	public void testOnePlaceOneTrans() throws Exception {
		PetriNet pn = new PetrifyPNParser().parseString(".inputs t1\n.graph\nt1 p1\n.marking  { } \n.end\n");
		assertThat(pn.getTransitions(), contains(nodeWithID("t1")));
		assertThat(pn.getPlaces(), contains(nodeWithID("p1")));
		assertThat(pn.getEdges(), contains(flowThatConnects("t1", "p1")));
	}

	@Test
	public void testIsolatedPlace() throws Exception {
		PetriNet pn = new PetrifyPNParser().parseString(".inputs\n.graph\nfoo\n.marking{}\n.end\n");
		assertThat(pn.getTransitions(), hasSize(0));
		assertThat(pn.getPlaces(), contains(nodeWithID("foo")));
		assertThat(pn.getEdges(), hasSize(0));
	}

	@Test
	public void testEmptyPN() throws Exception {
		PetriNet pn = new PetrifyPNParser().parseString(".inputs\n.graph\n\n.marking{}\n.end\n");
		assertThat(pn.getTransitions(), empty());
		assertThat(pn.getPlaces(), empty());
		assertThat(pn.getEdges(), empty());
	}

	@Test
	public void testInitialMarking() throws Exception {
		PetriNet pn = new PetrifyPNParser().parseString(".inputs\n.graph\nfoo\n.marking{foo=3}\n.end\n");
		assertThat(pn.getTransitions(), hasSize(0));
		assertThat(pn.getPlaces(), contains(nodeWithID("foo")));
		assertThat(pn.getEdges(), hasSize(0));
		assertThat(pn.getPlace("foo").getInitialToken(), is(Token.valueOf(3)));
	}

	@Test
	public void testInitialMarking2() throws Exception {
		PetriNet pn = new PetrifyPNParser().parseString(".inputs a\n.graph\na a\n.marking{<a,a>=42}\n.end\n");
		assertThat(pn.getTransitions(), contains(nodeWithID("a")));
		assertThat(pn.getPlaces(), contains(nodeWithID("<a,a>")));
		assertThat(pn.getEdges(), containsInAnyOrder(
					flowThatConnects("a", "<a,a>"), flowThatConnects("<a,a>", "a")));
		assertThat(pn.getPlace("<a,a>").getInitialToken(), is(Token.valueOf(42)));
	}

	@Test
	public void testFlowWeightExplicit() throws Exception {
		// Generated by genet synthesizing the lts with language (aa|b)c
		PetriNet pn = new PetrifyPNParser().parseString(".outputs b a c\n.graph\np0 b(2)\np0 a\np1 c(2)\n"
				+ "b p1(2)\na p1\n.marking { p0=2 }\n.end\n");
		assertThat(pn.getTransitions(), containsInAnyOrder(nodeWithID("a"), nodeWithID("b"), nodeWithID("c")));
		assertThat(pn.getPlaces(), containsInAnyOrder(nodeWithID("p0"), nodeWithID("p1")));
		assertThat(pn.getEdges(), hasSize(5));
		for (Flow flow : pn.getPresetEdges("a"))
			assertThat(flow.getWeight(), is(1));
		for (Flow flow : pn.getPostsetEdges("a"))
			assertThat(flow.getWeight(), is(1));
		for (Flow flow : pn.getPresetEdges("b"))
			assertThat(flow.getWeight(), is(2));
		for (Flow flow : pn.getPostsetEdges("b"))
			assertThat(flow.getWeight(), is(2));
		for (Flow flow : pn.getPresetEdges("c"))
			assertThat(flow.getWeight(), is(2));
		assertThat(pn.getPostsetEdges("c"), empty());
	}

	@Test
	public void testFlowWeightExplicitOwn() throws Exception {
		// Based on the interpretation used by ProM
		PetriNet pn = new PetrifyPNParser().parseString(".outputs a b\n.graph\np0 b(2) a\n"
				+ ".marking { }\n.end\n");
		assertThat(pn.getTransitions(), containsInAnyOrder(nodeWithID("a"), nodeWithID("b")));
		assertThat(pn.getPlaces(), contains(nodeWithID("p0")));
		assertThat(pn.getEdges(), hasSize(2));
		assertThat(pn.getPostsetEdges("a"), empty());
		assertThat(pn.getPostsetEdges("b"), empty());
		for (Flow flow : pn.getPresetEdges("a"))
			assertThat(flow.getWeight(), is(1));
		for (Flow flow : pn.getPresetEdges("b"))
			assertThat(flow.getWeight(), is(2));
	}

	@Test
	public void testFlowWeightImplicitOwn() throws Exception {
		// Based on the interpretation used by ProM
		PetriNet pn = new PetrifyPNParser().parseString(".outputs a b\n.graph\na b(2)\n"
				+ ".marking { }\n.end\n");
		assertThat(pn.getTransitions(), containsInAnyOrder(nodeWithID("a"), nodeWithID("b")));
		assertThat(pn.getPlaces(), contains(nodeWithID("<a,b>")));
		assertThat(pn.getEdges(), hasSize(2));
		assertThat(pn.getPresetEdges("a"), empty());
		assertThat(pn.getPostsetEdges("b"), empty());
		for (Flow flow : pn.getPostsetEdges("a"))
			assertThat(flow.getWeight(), is(2));
		for (Flow flow : pn.getPresetEdges("b"))
			assertThat(flow.getWeight(), is(2));
	}

	@Test
	public void testLabel() throws Exception {
		PetriNet pn = new PetrifyPNParser().parseString(
				".inputs a\n.graph\np0 a\na/0 a/1\n.marking{p0}\n.end\n");
		assertThat(pn.getTransitions(), containsInAnyOrder(nodeWithID("a"), nodeWithID("a/1")));
		assertThat(pn.getPlaces(), containsInAnyOrder(nodeWithID("p0"), nodeWithID("<a,a/1>")));

		Place p0 = pn.getPlace("p0");
		Place pImpl = pn.getPlace("<a,a/1>");
		Transition ta = pn.getTransition("a");
		Transition ta1 = pn.getTransition("a/1");

		assertThat(p0.getInitialToken().getValue(), is(1l));
		assertThat(pImpl.getInitialToken().getValue(), is(0l));

		assertThat(ta.getLabel(), is("a"));
		assertThat(ta1.getLabel(), is("a"));

		assertThat(p0.getPresetEdges(), hasSize(0));
		assertThat(p0.getPostsetEdges(), hasSize(1));
		assertThat(ta.getPresetEdges(), hasSize(1));
		assertThat(ta.getPostsetEdges(), hasSize(1));
		assertThat(pImpl.getPresetEdges(), hasSize(1));
		assertThat(pImpl.getPostsetEdges(), hasSize(1));
		assertThat(ta1.getPresetEdges(), hasSize(1));
		assertThat(ta1.getPostsetEdges(), hasSize(0));

		assertThat(p0.getPostsetNodes(), contains((Node) ta));
		assertThat(ta.getPostsetNodes(), contains((Node) pImpl));
		assertThat(pImpl.getPostsetNodes(), contains((Node) ta1));
	}

	@Test
	public void testABBAA() throws Exception {
		// Actual output of petrify (except for comments) when synthesizing a solution to the word "abbaa"
		PetriNet pn = new PetrifyPNParser().parseString(".model abbaa.g\n.inputs  a b\n.graph\na a/2\nb b/1\n"
				+ "a/1 b\nb/1 a\np0 a/1\n.marking { p0 }\n.end\n");
		assertThat(pn.getTransitions(), containsInAnyOrder(nodeWithID("a"), nodeWithID("a/1"),
					nodeWithID("a/2"), nodeWithID("b"), nodeWithID("b/1")));
		assertThat(pn.getPlaces(), containsInAnyOrder(nodeWithID("p0"), nodeWithID("<a,a/2>"),
					nodeWithID("<b,b/1>"), nodeWithID("<a/1,b>"), nodeWithID("<b/1,a>")));
		assertThat(pn.getEdges(), containsInAnyOrder(flowThatConnects("p0", "a/1"),
					flowThatConnects("a/1", "<a/1,b>"), flowThatConnects("<a/1,b>", "b"),
					flowThatConnects("b", "<b,b/1>"), flowThatConnects("<b,b/1>", "b/1"),
					flowThatConnects("b/1", "<b/1,a>"), flowThatConnects("<b/1,a>", "a"),
					flowThatConnects("a", "<a,a/2>"), flowThatConnects("<a,a/2>", "a/2")));

		for (Place place : pn.getPlaces()) {
			if ("p0".equals(place.getId()))
				assertThat(place.getInitialToken(), is(Token.valueOf(1)));
			else
				assertThat(place.getInitialToken(), is(Token.ZERO));
		}
	}

	@Test(expectedExceptions = { ParseException.class }, expectedExceptionsMessageRegExp = "^Tried to create arc between two places 'p0' and 'p1'$")
	public void testArcBetweenPlaces() throws Exception {
		PetrifyPNParser p = new PetrifyPNParser();
		p.parseString(".inputs\n.graph\np0 p1\n.marking { }\n.end\n");
	}

	@Test(expectedExceptions = { ParseException.class }, expectedExceptionsMessageRegExp = "^Duplicate initial marking for place '<a,b>'$")
	public void testDuplicateMarking() throws Exception {
		PetrifyPNParser p = new PetrifyPNParser();
		p.parseString(".inputs a b\n.graph\na b\nb a\n.marking { <a, b> <a, b> }\n.end\n");
	}

	@Test(expectedExceptions = { ParseException.class }, expectedExceptionsMessageRegExp = "^Duplicate initial marking for place 'p'$")
	public void testDuplicateMarking2() throws Exception {
		PetrifyPNParser p = new PetrifyPNParser();
		p.parseString(".inputs a b\n.graph\np a\np b\n.marking { p p }\n.end\n");
	}

	@Test(expectedExceptions = { ParseException.class }, expectedExceptionsMessageRegExp = "^Arc with sourceId 'a' and targetId 'p' already exists in graph ''$")
	public void testDuplicateArc() throws Exception {
		PetrifyPNParser p = new PetrifyPNParser();
		p.parseString(".inputs a b\n.graph\na p\na p\n.marking { p }\n.end\n");
	}

	@Test(expectedExceptions = { ParseException.class }, expectedExceptionsMessageRegExp = "^There is no implicit place between 'a' and 'b' whose initial marking can be set$")
	public void testPlaceDoesNotExist() throws Exception {
		PetrifyPNParser p = new PetrifyPNParser();
		p.parseString(".inputs a b\n.graph\n.marking { <a, b> }\n.end\n");
	}

	@Test(expectedExceptions = { ParseException.class }, expectedExceptionsMessageRegExp = "^A non-existent event was split in 'c/1'$")
	public void testSplitNonExistentEvent() throws Exception {
		PetrifyPNParser p = new PetrifyPNParser();
		p.parseString(".inputs a b\n.graph\na/0 b c/1\n.marking { <a, b> }\n.end\n");
	}

	@Test
	public void testGenetOutput() throws Exception {
		// This is GENET's output when synthesising the reachability graph
		// of a connected-2-bit-net with -k 100. The special thing here is the .capacity-line.
		PetriNet pn = new PetrifyPNParser().parseString("# Usage:\n#  -k 100\n"
				+ "# Event-based state space encoding\n# number of necessary regions: 4\n"
				+ " .outputs unset1 set0 unset0_set1\n.graph\n"
				+ "p2 unset1\np0 set0\np1 unset0_set1\np3 unset0_set1\n"
				+ "unset1 p3\nset0 p1\nunset0_set1 p0\nunset0_set1 p2\n"
				+ ".capacity  p0=1 p1=1 p2=1 p3=1\n.marking { p0 p3 }\n.end\n");
		assertThat(pn.getTransitions(), containsInAnyOrder(
					nodeWithID("unset1"), nodeWithID("set0"), nodeWithID("unset0_set1")));
		assertThat(pn.getPlaces(), containsInAnyOrder(nodeWithID("p0"), nodeWithID("p1"),
					nodeWithID("p2"), nodeWithID("p3")));
		assertThat(pn.getEdges(), containsInAnyOrder(flowThatConnects("p2", "unset1"),
					flowThatConnects("p0", "set0"), flowThatConnects("p1", "unset0_set1"),
					flowThatConnects("p3", "unset0_set1"), flowThatConnects("unset1", "p3"),
					flowThatConnects("set0", "p1"), flowThatConnects("unset0_set1", "p0"),
					flowThatConnects("unset0_set1", "p2")));

		for (Place place : pn.getPlaces()) {
			switch (place.getId()) {
				case "p0":
				case "p3":
					assertThat(place.getInitialToken(), is(Token.valueOf(1)));
					break;
				default:
					assertThat(place.getInitialToken(), is(Token.ZERO));
					break;
			}
		}
	}
}

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