Merge lp:~verifydtapn-contributers/verifydtapn/timeDartPtrie into lp:verifydtapn

[Peter Gjøl Jensen]

[Peter Gjøl Jensen (peter-gjoel)]

Merge into trunk.

[Jiri Srba (srba)]

There are many conflicts. Please, resolve them.

review: Needs Fixing

[lp:~verifydtapn-contributers/verifydtapn/timeDartPtrie]

428. By Peter Gjøl Jensen on 2013-03-24

fixed to short deadlock trace

429. By Peter Gjøl Jensen on 2013-03-24

should fix compile error

430. By Peter Gjøl Jensen on 2013-03-24

re-fixed short deadlock trace issue

[Jiri Srba (srba)]

the fix to deadlock trace seems to work;
the conflicts have to be resolved now before we can merge to trunk

[lp:~verifydtapn-contributers/verifydtapn/timeDartPtrie]

431. By Peter Gjøl Jensen on 2013-03-25

merged with trunk

[Peter Gjøl Jensen (peter-gjoel)]

> There are many conflicts. Please, resolve them.

The conflicts should be resolved in last commit.

[Jiri Srba (srba)]

I found a net with wrongly reported deadlock. A separate bug report is made.

review: Needs Fixing

[lp:~verifydtapn-contributers/verifydtapn/timeDartPtrie]

432. By Peter Gjøl Jensen on 2013-03-25

fix trace-loop detection delay for timedarts

433. By Peter Gjøl Jensen on 2013-03-25

trace-error seems fixed for naive engine

434. By Peter Gjøl Jensen on 2013-03-26

Seems to fix the trace issue for 2.xml as well as the delay in trace loop detection for timedarts

[Jiri Srba (srba)]

Now it passed almost all my tests, except for one that is reported as a separate bug.

review: Needs Fixing

[lp:~verifydtapn-contributers/verifydtapn/timeDartPtrie]

435. By Peter Gjøl Jensen on 2013-03-27

Delay forever reported when loop is detected-bug fix

[Jiri Srba (srba)]

The problem seems fixed. The only small issue is that when I try this fix on 10.xml that I attached
to the bug report, sometimes I get

*delay 1
goto *

instead of

delay forever

Could this be fixed to delay for ever (as this is the same thing)?

[Peter Gjøl Jensen (peter-gjoel)]

I think so, yes - there is a bit of ambiguity between delay forever and loop-detection.
As you noted, the previous fix introduced this bug, as the fix was to remove a check.

I will attempt to find a nicer solution.

[lp:~verifydtapn-contributers/verifydtapn/timeDartPtrie]

436. By Peter Gjøl Jensen on 2013-03-31

seems to have fixed the loop/delay for ever issue

437. By Peter Gjøl Jensen on 2013-03-31

fixed reintroduced bug

[Jiri Srba (srba)]

Now it passed all my tests. I suggest to (finally) merge it to trunk!
Any other issues should be then corrected in a separate branch.

Mathias and Jakob, please, take a look at the code to see if you find
any issues by inspecting the code and then approve.

review: Approve

[Mathias Grund Sørensen (mathias.grund)]

I think it looks pretty okay. I have a two (non-critical) comments (line numbers refer to changelog):

Line 2320-2328: Are transport arcs accounted for in GetPostset()? If not, it appears that it will be untimed even if it has transport arcs with timed postset (this might be an issue later I guess?).

Line 3489-3502: This loop should really be an else statement to the condition in line 3480-3486. Currently, we iterate over all tokens to test if any are older than c_max even though we just removed all tokens older than c_max --> twice the iterations for dead places (I know this is small, but because it is in cut it will be run a lot).

review: Approve

[Jakob Taankvist (jakob-taankvist)]

1) The file src/DiscreteVerification/DataStructures/EncodingStructure.cpp is practically empty?

2) The lines

2569 + void Release() const {
2570 + delete[] shadow;
2571 + }

seems a little dodgy? Shouldn't this be in the destructor?

3) The file src/DiscreteVerification/DataStructures/NonStrictMarking.cpp had it's contents deleted - but the file wasn't?

4) The file src/DiscreteVerification/DataStructures/PData.cpp is practically empty?

5) The comment "//possible mem-leek?" in line 3807 seems like it should be investigated?

I don't think the above have any functional implications, but it should be fixed at some point.

review: Approve

=== modified file 'src/Core/ArgsParser.cpp'
--- src/Core/ArgsParser.cpp	2012-07-12 15:47:35 +0000
+++ src/Core/ArgsParser.cpp	2013-03-31 13:25:26 +0000
@@ -8,321 +8,370 @@
 #include "boost/tokenizer.hpp"
 
 namespace VerifyTAPN {
-	static const std::string KBOUND_OPTION = "k-bound";
-	static const std::string SEARCH_OPTION = "search-type";
-	static const std::string TRACE_OPTION = "trace";
-	static const std::string MAX_CONSTANT_OPTION = "global-max-constants";
-	static const std::string XML_TRACE_OPTION = "xml-trace";
-	static const std::string LEGACY = "legacy";
-	static const std::string KEEP_DEAD = "keep-dead-tokens";
-
-	std::ostream& operator<<(std::ostream& out, const Switch& flag)
-	{
-		flag.Print(out);
-		return out;
-	}
-
-	std::ostream& operator <<(std::ostream& out, const Version& version)
-	{
-		out << version.maj << "." << version.min << "." << version.build;
-		return out;
-	}
-
-	void PrintIndentedDescription(std::ostream& out, const std::string& description)
-	{
-		typedef boost::tokenizer<boost::char_separator<char> > tokens;
-		tokens lines(description.begin(), description.end(), boost::char_separator<char>("\n", "", boost::keep_empty_tokens));
-		bool first = true;
-		for(tokens::const_iterator it = lines.begin(); it != lines.end(); it++)
-		{
-			if(!first){
-				out << std::setw(WIDTH) << " ";
-			}
-			out << *it << std::endl;
-			first = false;
-		}
-	}
-
-	void Switch::Print(std::ostream& out) const
-	{
-		std::stringstream s;
-		s << "-" << ShortName();
-		s << " [ --" << LongName() << " ]";
-		out << std::setw(WIDTH) << std::left << s.str();
-		PrintIndentedDescription(out, Description());
-	};
-
-	void SwitchWithArg::Print(std::ostream& out) const
-	{
-		std::stringstream s;
-		s << "-" << ShortName();
-		s << " [ --" << LongName() << " ] ";
-		s << " arg (=" << default_value << ")";
-		out << std::setw(WIDTH) << std::left << s.str();
-		PrintIndentedDescription(out, Description());
-	};
-
-	void SwitchWithStringArg::Print(std::ostream& out) const
-	{
-		std::stringstream s;
-		s << "-" << ShortName();
-		s << " [ --" << LongName() << " ] ";
-		s << " a1,a2,.. (=" << default_value << ")";
-		out << std::setw(WIDTH) << std::left << s.str();
-		PrintIndentedDescription(out, Description());
-	};
-
-	bool Switch::Handles(const std::string& flag) const
-	{
-		std::stringstream stream;
-		stream << "-" << name << " ";
-		if(flag.find(stream.str()) != std::string::npos) return true;
-		if(flag.find(long_name) != std::string::npos) return true;
-		return false;
-	};
-
-	option Switch::Parse(const std::string& flag)
-	{
-		assert(Handles(flag));
-		handled_option = true;
-		return option(LongName(), "1");
-	};
-
-
-	option SwitchWithArg::Parse(const std::string& flag)
-	{
-		assert(Handles(flag));
-		handled_option = true;
-		std::string copy(flag);
-		std::stringstream stream;
-		stream << "-" << ShortName() << " ";
-		if(flag.find(stream.str()) != std::string::npos)
-		{
-			boost::erase_all(copy, stream.str());
-		}
-		else
-		{
-			std::stringstream long_name_stream;
-			long_name_stream << "--" << LongName() << " ";
-			boost::erase_all(copy, long_name_stream.str());
-		}
-		boost::trim(copy);
-		return option(LongName(), copy);
-	};
-
-	option SwitchWithStringArg::Parse(const std::string& flag)
-	{
-		assert(Handles(flag));
-		handled_option = true;
-		std::string copy(flag);
-		std::stringstream stream;
-		stream << "-" << ShortName() << " ";
-		if(flag.find(stream.str()) != std::string::npos)
-		{
-			boost::erase_all(copy, stream.str());
-		}
-		else
-		{
-			std::stringstream long_name_stream;
-			long_name_stream << "--" << LongName() << " ";
-			boost::erase_all(copy, long_name_stream.str());
-		}
-		boost::trim(copy);
-		return option(LongName(), copy);
-	};
-
-	void ArgsParser::Initialize()
-	{
-		// NOTE: The Help() function only splits and indents descriptions based on newlines.
-		//       Each line in the description is assumed to fit within the remaining width
-		//       of the console, so keep descriptions short, or implement manual word-wrapping :).
-		parsers.push_back(boost::make_shared<SwitchWithArg>("k", KBOUND_OPTION, "Max tokens to use during exploration.",0));
-		parsers.push_back(boost::make_shared<SwitchWithArg>("o", SEARCH_OPTION, "Specify the desired search strategy.\n - 0: Breadth-First Search\n - 1: Depth-First Search\n - 2: Random Search\n - 3: Heuristic Search",3));
-		parsers.push_back(boost::make_shared<SwitchWithArg>("t", TRACE_OPTION, "Specify the desired trace option.\n - 0: none\n - 1: some",0));
-		parsers.push_back(boost::make_shared<Switch>("d",KEEP_DEAD, "Do not discard dead tokens\n(used for boundedness checking)"));
-		parsers.push_back(boost::make_shared<Switch>("g",MAX_CONSTANT_OPTION, "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
-		parsers.push_back(boost::make_shared<Switch>("s",LEGACY, "Legacy option (no effect)."));
-
-		parsers.push_back(boost::make_shared<Switch>("x",XML_TRACE_OPTION, "Output trace in xml format for TAPAAL."));
-	};
-
-	void ArgsParser::Help() const
-	{
-		std::cout << "Usage: verifydtapn -k <number> [optional arguments] model-file query-file" << std::endl;
-		std::cout << "Allowed Options:" << std::endl;
-		std::cout << std::setw(WIDTH) << std::left << "-h [ --help ]" << "Displays this help message." << std::endl;
-		std::cout << std::setw(WIDTH) << std::left << "-v [ --version ]" << "Displays version information." << std::endl;
-		for(parser_vec::const_iterator arg = parsers.begin(); arg != parsers.end(); arg++)
-		{
-			std::cout << **arg;
-		}
-	};
-
-	void ArgsParser::Version() const
-	{
-		std::cout << "VerifyDTAPN " << version << std::endl;
-		std::cout << "Licensed under BSD." << std::endl;
-	}
-
-	VerificationOptions ArgsParser::Parse(int argc, char* argv[]) const
-	{
-		if(argc == 1 || std::string(argv[1]) == "-h" || std::string(argv[1]) == "--help")
-		{
-			Help();
-			exit(0);
-		}
-
-		if(std::string(argv[1]) == "-v" || std::string(argv[1]) == "--version")
-		{
-			Version();
-			exit(0);
-		}
-
-		if(argc < 3)
-		{
-			std::cout << "too few parameters." << std::endl;
-			std::cout << "Use '-h' for help on correct usage." << std::endl;
-			exit(1);
-		}
-
-		std::string model_file(argv[argc-2]);
-		std::string query_file(argv[argc-1]);
-
-		if(boost::iends_with(query_file,".xml"))
-		{
-			std::cout << "Missing query file." << std::endl;
-			exit(1);
-		}
-
-		if(!boost::iends_with(model_file,".xml"))
-		{
-			std::cout << "Invalid model file specified." << std::endl;
-			exit(1);
-		}
-
-		if(!boost::iends_with(query_file, ".q"))
-		{
-			std::cout << "Invalid query file specified." << std::endl;
-			exit(1);
-		}
-
-		std::vector<std::string> flags;
-		unsigned int i = 1;
-		unsigned int size = static_cast<unsigned int>(argc);
-		while(i < size-2)
-		{
-			std::string arg(argv[i]);
-			if(boost::istarts_with(arg, "-"))
-			{
-				std::string arg2(argv[i+1]);
-				if(!boost::istarts_with(arg2,"-") && i+1 < size-2)
-				{
-					flags.push_back(arg + " " + arg2);
-					i++;
-				}else{
-					flags.push_back(arg + " ");
-				}
-			}
-			i++;
-		}
-
-		option_map options;
-		for(std::vector<std::string>::const_iterator flag = flags.begin(); flag != flags.end(); flag++)
-		{
-			bool handled = false;
-			for(parser_vec::const_iterator it = parsers.begin(); it != parsers.end(); it++)
-			{
-				if((*it)->Handles(*flag))
-				{
-					options.insert((*it)->Parse(*flag));
-					handled = true;
-				}
-			}
-			if(!handled)
-			{
-				std::cout << "Unknown option flag '" << *flag << "'" << std::endl;
-				std::cout << "Use '-h' to see a list of valid options." << std::endl;
-				exit(1);
-			}
-		}
-
-		// Put in default values for non-specified options
-		for(parser_vec::const_iterator it = parsers.begin(); it != parsers.end(); it++)
-		{
-			if(!(*it)->HandledOption())
-			{
-				options.insert((*it)->DefaultOption());
-			}
-		}
-
-		return CreateVerificationOptions(options, model_file, query_file);
-	}
-
-	SearchType intToSearchTypeEnum(int i) {
-		switch(i){
-		case 0:	return BREADTHFIRST;
-		case 1:	return DEPTHFIRST;
-		case 2: return RANDOM;
-		case 3: return COVERMOST;
-		default:
-			std::cout << "Unknown search strategy specified." << std::endl;
-			exit(1);
-		}
-	}
-
-	Trace intToEnum(int i){
-		switch(i)
-		{
-		case 0: return NONE;
-		case 1:	return SOME;
-		default:
-			std::cout << "Unknown trace option specified." << std::endl;
-			exit(1);
-		}
-	}
-
-	unsigned int ArgsParser::TryParseInt(const option& option) const
-	{
-		unsigned int result = 0;
-		try
-		{
-			result = boost::lexical_cast<unsigned int>(option.second);
-		}
-		catch(boost::bad_lexical_cast & e)
-		{
-			std::cout << "Invalid value '" << option.second << "' for option '--" << option.first << "'" << std::endl;
-			exit(1);
-		}
-		return result;
-	}
-
-	std::vector<std::string> ArgsParser::ParseIncPlaces(const std::string& string) const
-	{
-		std::vector<std::string> vec;
-		boost::split( vec, string, boost::is_any_of(",") );
-		return vec;
-	}
-
-	VerificationOptions ArgsParser::CreateVerificationOptions(const option_map& map, const std::string& modelFile, const std::string& queryFile) const
-	{
-		assert(map.find(KBOUND_OPTION) != map.end());
-		unsigned int kbound = TryParseInt(*map.find(KBOUND_OPTION));
-
-		assert(map.find(SEARCH_OPTION) != map.end());
-		SearchType search = intToSearchTypeEnum(TryParseInt(*map.find(SEARCH_OPTION)));
-
-		assert(map.find(TRACE_OPTION) != map.end());
-		Trace trace = intToEnum(TryParseInt(*map.find(TRACE_OPTION)));
-
-		assert(map.find(MAX_CONSTANT_OPTION) != map.end());
-		bool max_constant = boost::lexical_cast<bool>(map.find(MAX_CONSTANT_OPTION)->second);
-
-		assert(map.find(KEEP_DEAD) != map.end());
-		bool keep_dead = boost::lexical_cast<bool>(map.find(KEEP_DEAD)->second);
-
-		assert(map.find(XML_TRACE_OPTION) != map.end());
-		bool xml_trace = boost::lexical_cast<bool>(map.find(XML_TRACE_OPTION)->second);
-
-		return VerificationOptions(modelFile, queryFile, search, kbound, trace, xml_trace, max_constant, keep_dead);
-	}
+static const std::string KBOUND_OPTION = "k-bound";
+static const std::string SEARCH_OPTION = "search-type";
+static const std::string VERIFICATION_OPTION = "verification-method";
+static const std::string MEMORY_OPTIMIZATION_OPTION = "memory-optimization";
+static const std::string TRACE_OPTION = "trace";
+static const std::string MAX_CONSTANT_OPTION = "global-max-constants";
+static const std::string XML_TRACE_OPTION = "xml-trace";
+static const std::string LEGACY = "legacy";
+static const std::string KEEP_DEAD = "keep-dead-tokens";
+
+std::ostream& operator<<(std::ostream& out, const Switch& flag) {
+	flag.Print(out);
+	return out;
+}
+
+std::ostream& operator <<(std::ostream& out, const Version& version) {
+	out << version.maj << "." << version.min << "." << version.build;
+	return out;
+}
+
+void PrintIndentedDescription(std::ostream& out,
+		const std::string& description) {
+	typedef boost::tokenizer<boost::char_separator<char> > tokens;
+	tokens lines(description.begin(), description.end(),
+			boost::char_separator<char>("\n", "", boost::keep_empty_tokens));
+	bool first = true;
+	for (tokens::const_iterator it = lines.begin(); it != lines.end(); it++) {
+		if (!first) {
+			out << std::setw(WIDTH) << " ";
+		}
+		out << *it << std::endl;
+		first = false;
+	}
+}
+
+void Switch::Print(std::ostream& out) const {
+	std::stringstream s;
+	s << "-" << ShortName();
+	s << " [ --" << LongName() << " ]";
+	out << std::setw(WIDTH) << std::left << s.str();
+	PrintIndentedDescription(out, Description());
+}
+;
+
+void SwitchWithArg::Print(std::ostream& out) const {
+	std::stringstream s;
+	s << "-" << ShortName();
+	s << " [ --" << LongName() << " ] ";
+	s << " arg (=" << default_value << ")";
+	out << std::setw(WIDTH) << std::left << s.str();
+	PrintIndentedDescription(out, Description());
+}
+;
+
+void SwitchWithStringArg::Print(std::ostream& out) const {
+	std::stringstream s;
+	s << "-" << ShortName();
+	s << " [ --" << LongName() << " ] ";
+	s << " a1,a2,.. (=" << default_value << ")";
+	out << std::setw(WIDTH) << std::left << s.str();
+	PrintIndentedDescription(out, Description());
+}
+;
+
+bool Switch::Handles(const std::string& flag) const {
+	std::stringstream stream;
+	stream << "-" << name << " ";
+	if (flag.find(stream.str()) != std::string::npos)
+		return true;
+	if (flag.find(long_name) != std::string::npos)
+		return true;
+	return false;
+}
+;
+
+option Switch::Parse(const std::string& flag) {
+	assert(Handles(flag));
+	handled_option = true;
+	return option(LongName(), "1");
+}
+;
+
+option SwitchWithArg::Parse(const std::string& flag) {
+	assert(Handles(flag));
+	handled_option = true;
+	std::string copy(flag);
+	std::stringstream stream;
+	stream << "-" << ShortName() << " ";
+	if (flag.find(stream.str()) != std::string::npos) {
+		boost::erase_all(copy, stream.str());
+	} else {
+		std::stringstream long_name_stream;
+		long_name_stream << "--" << LongName() << " ";
+		boost::erase_all(copy, long_name_stream.str());
+	}
+	boost::trim(copy);
+	return option(LongName(), copy);
+}
+;
+
+option SwitchWithStringArg::Parse(const std::string& flag) {
+	assert(Handles(flag));
+	handled_option = true;
+	std::string copy(flag);
+	std::stringstream stream;
+	stream << "-" << ShortName() << " ";
+	if (flag.find(stream.str()) != std::string::npos) {
+		boost::erase_all(copy, stream.str());
+	} else {
+		std::stringstream long_name_stream;
+		long_name_stream << "--" << LongName() << " ";
+		boost::erase_all(copy, long_name_stream.str());
+	}
+	boost::trim(copy);
+	return option(LongName(), copy);
+}
+;
+
+void ArgsParser::Initialize() {
+    // NOTE: The Help() function only splits and indents descriptions based on newlines.
+    //       Each line in the description is assumed to fit within the remaining width
+    //       of the console, so keep descriptions short, or implement manual word-wrapping :).
+    parsers.push_back(
+            boost::make_shared<SwitchWithArg > ("k", KBOUND_OPTION,
+            "Max tokens to use during exploration.", 0));
+    parsers.push_back(
+            boost::make_shared<SwitchWithArg > ("o", SEARCH_OPTION,
+            "Specify the desired search strategy.\n - 0: Breadth-First Search\n - 1: Depth-First Search\n - 2: Random Search\n - 3: Heuristic Search",
+            3));
+    parsers.push_back(
+            boost::make_shared<SwitchWithArg > ("m", VERIFICATION_OPTION,
+            "Specify the desired verification method.\n - 0: Default (discrete)\n - 1: Time Darts",
+            0)); // TODO change to 0!
+    parsers.push_back(
+            boost::make_shared<SwitchWithArg > ("p", MEMORY_OPTIMIZATION_OPTION,
+            "Specify the desired memory optimization.\n - 0: None \n - 1: PTrie",
+            1)); // TODO change to 0!
+    parsers.push_back(
+            boost::make_shared<SwitchWithArg > ("t", TRACE_OPTION,
+            "Specify the desired trace option.\n - 0: none\n - 1: some",
+            0));
+    parsers.push_back(
+            boost::make_shared<Switch > ("d", KEEP_DEAD,
+            "Do not discard dead tokens\n(used for boundedness checking)"));
+    parsers.push_back(
+            boost::make_shared<Switch > ("g", MAX_CONSTANT_OPTION,
+            "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
+    parsers.push_back(
+            boost::make_shared<Switch > ("s", LEGACY,
+            "Legacy option (no effect)."));
+
+    parsers.push_back(
+            boost::make_shared<Switch > ("x", XML_TRACE_OPTION,
+            "Output trace in xml format for TAPAAL."));
+};
+
+void ArgsParser::Help() const {
+	std::cout
+			<< "Usage: verifydtapn -k <number> [optional arguments] model-file query-file"
+			<< std::endl;
+	std::cout << "Allowed Options:" << std::endl;
+	std::cout << std::setw(WIDTH) << std::left << "-h [ --help ]"
+			<< "Displays this help message." << std::endl;
+	std::cout << std::setw(WIDTH) << std::left << "-v [ --version ]"
+			<< "Displays version information." << std::endl;
+	for (parser_vec::const_iterator arg = parsers.begin(); arg != parsers.end();
+			arg++) {
+		std::cout << **arg;
+	}
+}
+;
+
+void ArgsParser::Version() const {
+	std::cout << "VerifyDTAPN " << version << std::endl;
+	std::cout << "Licensed under BSD." << std::endl;
+}
+
+VerificationOptions ArgsParser::Parse(int argc, char* argv[]) const {
+	if (argc == 1 || std::string(argv[1]) == "-h"
+			|| std::string(argv[1]) == "--help") {
+		Help();
+		exit(0);
+	}
+
+	if (std::string(argv[1]) == "-v" || std::string(argv[1]) == "--version") {
+		Version();
+		exit(0);
+	}
+
+	if (argc < 3) {
+		std::cout << "too few parameters." << std::endl;
+		std::cout << "Use '-h' for help on correct usage." << std::endl;
+		exit(1);
+	}
+
+	std::string model_file(argv[argc - 2]);
+	std::string query_file(argv[argc - 1]);
+
+	if (boost::iends_with(query_file, ".xml")) {
+		std::cout << "Missing query file." << std::endl;
+		exit(1);
+	}
+
+	if (!boost::iends_with(model_file, ".xml")) {
+		std::cout << "Invalid model file specified." << std::endl;
+		exit(1);
+	}
+
+	if (!boost::iends_with(query_file, ".q")) {
+		std::cout << "Invalid query file specified." << std::endl;
+		exit(1);
+	}
+
+	std::vector<std::string> flags;
+	unsigned int i = 1;
+	unsigned int size = static_cast<unsigned int>(argc);
+	while (i < size - 2) {
+		std::string arg(argv[i]);
+		if (boost::istarts_with(arg, "-")) {
+			std::string arg2(argv[i + 1]);
+			if (!boost::istarts_with(arg2, "-") && i + 1 < size - 2) {
+				flags.push_back(arg + " " + arg2);
+				i++;
+			} else {
+				flags.push_back(arg + " ");
+			}
+		}
+		i++;
+	}
+
+	option_map options;
+	for (std::vector<std::string>::const_iterator flag = flags.begin();
+			flag != flags.end(); flag++) {
+		bool handled = false;
+		for (parser_vec::const_iterator it = parsers.begin();
+				it != parsers.end(); it++) {
+			if ((*it)->Handles(*flag)) {
+				options.insert((*it)->Parse(*flag));
+				handled = true;
+			}
+		}
+		if (!handled) {
+			std::cout << "Unknown option flag '" << *flag << "'" << std::endl;
+			std::cout << "Use '-h' to see a list of valid options."
+					<< std::endl;
+			exit(1);
+		}
+	}
+
+	// Put in default values for non-specified options
+	for (parser_vec::const_iterator it = parsers.begin(); it != parsers.end();
+			it++) {
+		if (!(*it)->HandledOption()) {
+			options.insert((*it)->DefaultOption());
+		}
+	}
+
+	return CreateVerificationOptions(options, model_file, query_file);
+}
+
+SearchType intToSearchTypeEnum(int i) {
+	switch (i) {
+	case 0:
+		return BREADTHFIRST;
+	case 1:
+		return DEPTHFIRST;
+	case 2:
+		return RANDOM;
+	case 3:
+		return COVERMOST;
+	default:
+		std::cout << "Unknown search strategy specified." << std::endl;
+		exit(1);
+	}
+}
+
+VerificationType intToVerificationTypeEnum(int i) {
+	switch (i) {
+	case 0:
+		return DISCRETE;
+	case 1:
+		return TIMEDART;
+	default:
+		std::cout << "Unknown verification method specified." << std::endl;
+		exit(1);
+	}
+}
+
+MemoryOptimization intToMemoryOptimizationEnum(int i) {
+	switch (i) {
+	case 0:
+		return NO_MEMORY_OPTIMIZATION;
+	case 1:
+		return PTRIE;
+	default:
+		std::cout << "Unknown memory optimization specified." << std::endl;
+		exit(1);
+	}
+}
+
+
+Trace intToEnum(int i) {
+	switch (i) {
+	case 0:
+		return NONE;
+	case 1:
+		return SOME;
+	default:
+		std::cout << "Unknown trace option specified." << std::endl;
+		exit(1);
+	}
+}
+
+unsigned int ArgsParser::TryParseInt(const option& option) const {
+	unsigned int result = 0;
+	try {
+		result = boost::lexical_cast<unsigned int>(option.second);
+	} catch (boost::bad_lexical_cast & e) {
+		std::cout << "Invalid value '" << option.second << "' for option '--"
+				<< option.first << "'" << std::endl;
+		exit(1);
+	}
+	return result;
+}
+
+std::vector<std::string> ArgsParser::ParseIncPlaces(
+		const std::string& string) const {
+	std::vector<std::string> vec;
+	boost::split(vec, string, boost::is_any_of(","));
+	return vec;
+}
+
+VerificationOptions ArgsParser::CreateVerificationOptions(const option_map& map,
+		const std::string& modelFile, const std::string& queryFile) const {
+	assert(map.find(KBOUND_OPTION) != map.end());
+	unsigned int kbound = TryParseInt(*map.find(KBOUND_OPTION));
+
+	assert(map.find(SEARCH_OPTION) != map.end());
+	SearchType search = intToSearchTypeEnum(
+			TryParseInt(*map.find(SEARCH_OPTION)));
+
+	assert(map.find(VERIFICATION_OPTION) != map.end());
+	VerificationType verification = intToVerificationTypeEnum(
+			TryParseInt(*map.find(VERIFICATION_OPTION)));
+        
+	assert(map.find(MEMORY_OPTIMIZATION_OPTION) != map.end());
+	MemoryOptimization memoptimization = intToMemoryOptimizationEnum(
+			TryParseInt(*map.find(MEMORY_OPTIMIZATION_OPTION)));
+        
+	assert(map.find(TRACE_OPTION) != map.end());
+	Trace trace = intToEnum(TryParseInt(*map.find(TRACE_OPTION)));
+
+	assert(map.find(MAX_CONSTANT_OPTION) != map.end());
+	bool max_constant = boost::lexical_cast<bool>(
+			map.find(MAX_CONSTANT_OPTION)->second);
+
+	assert(map.find(KEEP_DEAD) != map.end());
+	bool keep_dead = boost::lexical_cast<bool>(map.find(KEEP_DEAD)->second);
+
+	assert(map.find(XML_TRACE_OPTION) != map.end());
+	bool xml_trace = boost::lexical_cast<bool>(
+			map.find(XML_TRACE_OPTION)->second);
+        
+	return VerificationOptions(modelFile, queryFile, search, verification, memoptimization, kbound, trace,
+			xml_trace, max_constant, keep_dead);
+}
 }
 
=== modified file 'src/Core/ArgsParser.hpp' (properties changed: +x to -x)
--- src/Core/ArgsParser.hpp	2012-11-29 00:53:29 +0000
+++ src/Core/ArgsParser.hpp	2013-03-31 13:25:26 +0000
@@ -80,7 +80,7 @@
 	class ArgsParser {
 		typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
 	public:
-		ArgsParser() : parsers(), version(1,0,1) { Initialize(); };
+		ArgsParser() : parsers(), version(2,0,0) { Initialize(); };
 		virtual ~ArgsParser() {};
 
 		VerificationOptions Parse(int argc, char* argv[]) const;
 
=== modified file 'src/Core/QueryParser/Generated/lexer.cpp'
--- src/Core/QueryParser/Generated/lexer.cpp	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/Generated/lexer.cpp	2013-03-31 13:25:26 +0000
@@ -1,6 +1,6 @@
-#line 2 "Generated/lexer.cpp"
+#line 2 "Core/QueryParser/Generated/lexer.cpp"
 
-#line 4 "Generated/lexer.cpp"
+#line 4 "Core/QueryParser/Generated/lexer.cpp"
 
 #define  YY_INT_ALIGNED short int
 
@@ -54,7 +54,6 @@
 typedef unsigned char flex_uint8_t; 
 typedef unsigned short int flex_uint16_t;
 typedef unsigned int flex_uint32_t;
-#endif /* ! C99 */
 
 /* Limits of integral types. */
 #ifndef INT8_MIN
@@ -85,6 +84,8 @@
 #define UINT32_MAX             (4294967295U)
 #endif
 
+#endif /* ! C99 */
+
 #endif /* ! FLEXINT_H */
 
 #ifdef __cplusplus
@@ -141,7 +142,15 @@
 
 /* Size of default input buffer. */
 #ifndef YY_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k.
+ * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
+ * Ditto for the __ia64__ case accordingly.
+ */
+#define YY_BUF_SIZE 32768
+#else
 #define YY_BUF_SIZE 16384
+#endif /* __ia64__ */
 #endif
 
 /* The state buf must be large enough to hold one state per character in the main buffer.
@@ -153,12 +162,7 @@
 typedef struct yy_buffer_state *YY_BUFFER_STATE;
 #endif
 
-#ifndef YY_TYPEDEF_YY_SIZE_T
-#define YY_TYPEDEF_YY_SIZE_T
-typedef size_t yy_size_t;
-#endif
-
-extern yy_size_t yyleng;
+extern int yyleng;
 
 extern FILE *yyin, *yyout;
 
@@ -184,6 +188,11 @@
 
 #define unput(c) yyunput( c, (yytext_ptr)  )
 
+#ifndef YY_TYPEDEF_YY_SIZE_T
+#define YY_TYPEDEF_YY_SIZE_T
+typedef size_t yy_size_t;
+#endif
+
 #ifndef YY_STRUCT_YY_BUFFER_STATE
 #define YY_STRUCT_YY_BUFFER_STATE
 struct yy_buffer_state
@@ -201,7 +210,7 @@
 	/* Number of characters read into yy_ch_buf, not including EOB
 	 * characters.
 	 */
-	yy_size_t yy_n_chars;
+	int yy_n_chars;
 
 	/* Whether we "own" the buffer - i.e., we know we created it,
 	 * and can realloc() it to grow it, and should free() it to
@@ -271,8 +280,8 @@
 
 /* yy_hold_char holds the character lost when yytext is formed. */
 static char yy_hold_char;
-static yy_size_t yy_n_chars;		/* number of characters read into yy_ch_buf */
-yy_size_t yyleng;
+static int yy_n_chars;		/* number of characters read into yy_ch_buf */
+int yyleng;
 
 /* Points to current character in buffer. */
 static char *yy_c_buf_p = (char *) 0;
@@ -300,7 +309,7 @@
 
 YY_BUFFER_STATE yy_scan_buffer (char *base,yy_size_t size  );
 YY_BUFFER_STATE yy_scan_string (yyconst char *yy_str  );
-YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,yy_size_t len  );
+YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,int len  );
 
 void *yyalloc (yy_size_t  );
 void *yyrealloc (void *,yy_size_t  );
@@ -478,8 +487,8 @@
 #define YY_MORE_ADJ 0
 #define YY_RESTORE_YY_MORE_OFFSET
 char *yytext;
-#line 1 "flex.ll"
-#line 2 "flex.ll"
+#line 1 "Core/QueryParser/flex.ll"
+#line 2 "Core/QueryParser/flex.ll"
 # include <string>
 # include "../TAPNQueryParser.hpp"
 # include "parser.hpp"
@@ -495,9 +504,9 @@
    Unfortunately yyterminate by default returns 0, which is
    not of token_type.  */
 #define yyterminate() return token::END
-#line 26 "flex.ll"
+#line 26 "Core/QueryParser/flex.ll"
 # define YY_USER_ACTION  yylloc->columns (yyleng);
-#line 501 "Generated/lexer.cpp"
+#line 510 "Core/QueryParser/Generated/lexer.cpp"
 
 #define INITIAL 0
 
@@ -536,7 +545,7 @@
 
 void yyset_out  (FILE * out_str  );
 
-yy_size_t yyget_leng (void );
+int yyget_leng (void );
 
 char *yyget_text (void );
 
@@ -576,7 +585,12 @@
 
 /* Amount of stuff to slurp up with each read. */
 #ifndef YY_READ_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k */
+#define YY_READ_BUF_SIZE 16384
+#else
 #define YY_READ_BUF_SIZE 8192
+#endif /* __ia64__ */
 #endif
 
 /* Copy whatever the last rule matched to the standard output. */
@@ -584,7 +598,7 @@
 /* This used to be an fputs(), but since the string might contain NUL's,
  * we now use fwrite().
  */
-#define ECHO fwrite( yytext, yyleng, 1, yyout )
+#define ECHO do { if (fwrite( yytext, yyleng, 1, yyout )) {} } while (0)
 #endif
 
 /* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
@@ -595,7 +609,7 @@
 	if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
 		{ \
 		int c = '*'; \
-		yy_size_t n; \
+		size_t n; \
 		for ( n = 0; n < max_size && \
 			     (c = getc( yyin )) != EOF && c != '\n'; ++n ) \
 			buf[n] = (char) c; \
@@ -680,12 +694,12 @@
 	register char *yy_cp, *yy_bp;
 	register int yy_act;
     
-#line 28 "flex.ll"
+#line 28 "Core/QueryParser/flex.ll"
 
 
   yylloc->step ();
 
-#line 689 "Generated/lexer.cpp"
+#line 703 "Core/QueryParser/Generated/lexer.cpp"
 
 	if ( !(yy_init) )
 		{
@@ -767,13 +781,13 @@
 
 case 1:
 YY_RULE_SETUP
-#line 32 "flex.ll"
+#line 32 "Core/QueryParser/flex.ll"
 { yylloc->step (); }
 	YY_BREAK
 case 2:
 /* rule 2 can match eol */
 YY_RULE_SETUP
-#line 33 "flex.ll"
+#line 33 "Core/QueryParser/flex.ll"
 { yylloc->lines (yyleng); yylloc->step (); }
 	YY_BREAK
 
@@ -781,105 +795,105 @@
 
 case 3:
 YY_RULE_SETUP
-#line 39 "flex.ll"
+#line 39 "Core/QueryParser/flex.ll"
 { yylval->number = atoi(yytext); return token::NUMBER; }
 	YY_BREAK
 case 4:
 YY_RULE_SETUP
-#line 40 "flex.ll"
+#line 40 "Core/QueryParser/flex.ll"
 { return token::EF; }
 	YY_BREAK
 case 5:
 YY_RULE_SETUP
-#line 41 "flex.ll"
+#line 41 "Core/QueryParser/flex.ll"
 { return token::AG; }
 	YY_BREAK
 case 6:
 YY_RULE_SETUP
-#line 42 "flex.ll"
+#line 42 "Core/QueryParser/flex.ll"
 { return token::AF; }
 	YY_BREAK
 case 7:
 YY_RULE_SETUP
-#line 43 "flex.ll"
+#line 43 "Core/QueryParser/flex.ll"
 { return token::EG; }
 	YY_BREAK
 case 8:
 YY_RULE_SETUP
-#line 44 "flex.ll"
+#line 44 "Core/QueryParser/flex.ll"
 { return token::OR; }
 	YY_BREAK
 case 9:
 YY_RULE_SETUP
-#line 45 "flex.ll"
+#line 45 "Core/QueryParser/flex.ll"
 { return token::AND; }
 	YY_BREAK
 case 10:
 YY_RULE_SETUP
-#line 46 "flex.ll"
+#line 46 "Core/QueryParser/flex.ll"
 { return token::BOOL_TRUE; }
 	YY_BREAK
 case 11:
 YY_RULE_SETUP
-#line 47 "flex.ll"
+#line 47 "Core/QueryParser/flex.ll"
 { return token::BOOL_FALSE; }
 	YY_BREAK
 case 12:
 YY_RULE_SETUP
-#line 48 "flex.ll"
+#line 48 "Core/QueryParser/flex.ll"
 { return token::NOT; }
 	YY_BREAK
 case 13:
 YY_RULE_SETUP
-#line 49 "flex.ll"
+#line 49 "Core/QueryParser/flex.ll"
 { return token::LPARAN; }
 	YY_BREAK
 case 14:
 YY_RULE_SETUP
-#line 50 "flex.ll"
+#line 50 "Core/QueryParser/flex.ll"
 { return token::RPARAN; }
 	YY_BREAK
 case 15:
 YY_RULE_SETUP
-#line 51 "flex.ll"
+#line 51 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::LESS; }
 	YY_BREAK
 case 16:
 YY_RULE_SETUP
-#line 52 "flex.ll"
+#line 52 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::LESSEQUAL; }
 	YY_BREAK
 case 17:
 YY_RULE_SETUP
-#line 53 "flex.ll"
+#line 53 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::EQUAL; }
 	YY_BREAK
 case 18:
 YY_RULE_SETUP
-#line 54 "flex.ll"
+#line 54 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::EQUAL; }
 	YY_BREAK
 case 19:
 YY_RULE_SETUP
-#line 55 "flex.ll"
+#line 55 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::GREATEREQUAL; }
 	YY_BREAK
 case 20:
 YY_RULE_SETUP
-#line 56 "flex.ll"
+#line 56 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::GREATER; }
 	YY_BREAK
 case 21:
 YY_RULE_SETUP
-#line 57 "flex.ll"
+#line 57 "Core/QueryParser/flex.ll"
 { yylval->string = new std::string(yytext); return token::IDENTIFIER; }
 	YY_BREAK
 case 22:
 YY_RULE_SETUP
-#line 59 "flex.ll"
+#line 59 "Core/QueryParser/flex.ll"
 ECHO;
 	YY_BREAK
-#line 883 "Generated/lexer.cpp"
+#line 897 "Core/QueryParser/Generated/lexer.cpp"
 case YY_STATE_EOF(INITIAL):
 	yyterminate();
 
@@ -1066,7 +1080,7 @@
 
 	else
 		{
-			yy_size_t num_to_read =
+			int num_to_read =
 			YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
 
 		while ( num_to_read <= 0 )
@@ -1080,7 +1094,7 @@
 
 			if ( b->yy_is_our_buffer )
 				{
-				yy_size_t new_size = b->yy_buf_size * 2;
+				int new_size = b->yy_buf_size * 2;
 
 				if ( new_size <= 0 )
 					b->yy_buf_size += b->yy_buf_size / 8;
@@ -1111,7 +1125,7 @@
 
 		/* Read in more data. */
 		YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
-			(yy_n_chars), num_to_read );
+			(yy_n_chars), (size_t) num_to_read );
 
 		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
 		}
@@ -1234,7 +1248,7 @@
 
 		else
 			{ /* need more input */
-			yy_size_t offset = (yy_c_buf_p) - (yytext_ptr);
+			int offset = (yy_c_buf_p) - (yytext_ptr);
 			++(yy_c_buf_p);
 
 			switch ( yy_get_next_buffer(  ) )
@@ -1258,7 +1272,7 @@
 				case EOB_ACT_END_OF_FILE:
 					{
 					if ( yywrap( ) )
-						return 0;
+						return EOF;
 
 					if ( ! (yy_did_buffer_switch_on_eof) )
 						YY_NEW_FILE;
@@ -1512,7 +1526,7 @@
  */
 static void yyensure_buffer_stack (void)
 {
-	yy_size_t num_to_alloc;
+	int num_to_alloc;
     
 	if (!(yy_buffer_stack)) {
 
@@ -1604,16 +1618,17 @@
 
 /** Setup the input buffer state to scan the given bytes. The next call to yylex() will
  * scan from a @e copy of @a bytes.
- * @param bytes the byte buffer to scan
- * @param len the number of bytes in the buffer pointed to by @a bytes.
+ * @param yybytes the byte buffer to scan
+ * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes.
  * 
  * @return the newly allocated buffer state object.
  */
-YY_BUFFER_STATE yy_scan_bytes  (yyconst char * yybytes, yy_size_t  _yybytes_len )
+YY_BUFFER_STATE yy_scan_bytes  (yyconst char * yybytes, int  _yybytes_len )
 {
 	YY_BUFFER_STATE b;
 	char *buf;
-	yy_size_t n, i;
+	yy_size_t n;
+	int i;
     
 	/* Get memory for full buffer, including space for trailing EOB's. */
 	n = _yybytes_len + 2;
@@ -1695,7 +1710,7 @@
 /** Get the length of the current token.
  * 
  */
-yy_size_t yyget_leng  (void)
+int yyget_leng  (void)
 {
         return yyleng;
 }
@@ -1843,7 +1858,7 @@
 
 #define YYTABLES_NAME "yytables"
 
-#line 59 "flex.ll"
+#line 59 "Core/QueryParser/flex.ll"
 
 
 namespace VerifyTAPN
 
=== modified file 'src/Core/QueryParser/Generated/location.hh'
--- src/Core/QueryParser/Generated/location.hh	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/Generated/location.hh	2013-03-31 13:25:26 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.6.5.  */
 
 /* Locations for Bison parsers in C++
    
-      Copyright (C) 2002-2007, 2009-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2007, 2009-2012 Free Software Foundation, Inc.
    
    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
@@ -31,41 +31,56 @@
    version 2.2 of Bison.  */
 
 /**
- ** \file location.hh
+ ** \file Core/QueryParser/Generated/location.hh
  ** Define the VerifyTAPN::location class.
  */
 
-#ifndef BISON_LOCATION_HH
-# define BISON_LOCATION_HH
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_LOCATION_HH_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_LOCATION_HH_INCLUDED
 
-# include <iostream>
-# include <string>
 # include "position.hh"
 
-
-/* Line 162 of location.cc  */
-#line 5 "grammar.yy"
+/* Line 164 of location.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 162 of location.cc  */
-#line 52 "Generated/location.hh"
+/* Line 164 of location.cc  */
+#line 48 "Core/QueryParser/Generated/location.hh"
 
   /// Abstract a location.
   class location
   {
   public:
 
-    /// Construct a location.
-    location ()
-      : begin (), end ()
+    /// Construct a location from \a b to \a e.
+    location (const position& b, const position& e)
+      : begin (b)
+      , end (e)
+    {
+    }
+
+    /// Construct a 0-width location in \a p.
+    explicit location (const position& p = position ())
+      : begin (p)
+      , end (p)
+    {
+    }
+
+    /// Construct a 0-width location in \a f, \a l, \a c.
+    explicit location (std::string* f,
+                       unsigned int l = 1u,
+                       unsigned int c = 1u)
+      : begin (f, l, c)
+      , end (f, l, c)
     {
     }
 
 
     /// Initialization.
-    inline void initialize (std::string* fn)
+    void initialize (std::string* f = YY_NULL,
+                     unsigned int l = 1u,
+                     unsigned int c = 1u)
     {
-      begin.initialize (fn);
+      begin.initialize (f, l, c);
       end = begin;
     }
 
@@ -73,19 +88,19 @@
      ** \{ */
   public:
     /// Reset initial location to final location.
-    inline void step ()
+    void step ()
     {
       begin = end;
     }
 
     /// Extend the current location to the COUNT next columns.
-    inline void columns (unsigned int count = 1)
+    void columns (unsigned int count = 1)
     {
       end += count;
     }
 
     /// Extend the current location to the COUNT next lines.
-    inline void lines (unsigned int count = 1)
+    void lines (unsigned int count = 1)
     {
       end.lines (count);
     }
@@ -157,12 +172,10 @@
     return ostr;
   }
 
-
-/* Line 271 of location.cc  */
-#line 5 "grammar.yy"
+/* Line 292 of location.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 271 of location.cc  */
-#line 167 "Generated/location.hh"
-
-#endif // not BISON_LOCATION_HH
+/* Line 292 of location.cc  */
+#line 180 "Core/QueryParser/Generated/location.hh"
+
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_LOCATION_HH_INCLUDED  */
 
=== modified file 'src/Core/QueryParser/Generated/parser.cpp'
--- src/Core/QueryParser/Generated/parser.cpp	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/Generated/parser.cpp	2013-03-31 13:25:26 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.6.5.  */
 
 /* Skeleton implementation for Bison LALR(1) parsers in C++
    
-      Copyright (C) 2002-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2012 Free Software Foundation, Inc.
    
    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
@@ -33,29 +33,34 @@
 
 /* First part of user declarations.  */
 
-
-/* Line 293 of lalr1.cc  */
-#line 39 "Generated/parser.cpp"
+/* Line 278 of lalr1.cc  */
+#line 38 "Core/QueryParser/Generated/parser.cpp"
 
 
 #include "parser.hpp"
 
 /* User implementation prologue.  */
 
-
-/* Line 299 of lalr1.cc  */
-#line 48 "Generated/parser.cpp"
+/* Line 284 of lalr1.cc  */
+#line 46 "Core/QueryParser/Generated/parser.cpp"
 /* Unqualified %code blocks.  */
-
-/* Line 300 of lalr1.cc  */
-#line 37 "grammar.yy"
+/* Line 285 of lalr1.cc  */
+#line 37 "Core/QueryParser/grammar.yy"
 
 	#include "../TAPNQueryParser.hpp"
 
 
-
-/* Line 300 of lalr1.cc  */
-#line 59 "Generated/parser.cpp"
+/* Line 285 of lalr1.cc  */
+#line 55 "Core/QueryParser/Generated/parser.cpp"
+
+
+# ifndef YY_NULL
+#  if defined __cplusplus && 201103L <= __cplusplus
+#   define YY_NULL nullptr
+#  else
+#   define YY_NULL 0
+#  endif
+# endif
 
 #ifndef YY_
 # if defined YYENABLE_NLS && YYENABLE_NLS
@@ -69,25 +74,26 @@
 # endif
 #endif
 
+#define YYRHSLOC(Rhs, K) ((Rhs)[K])
 /* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N].
    If N is 0, then set CURRENT to the empty location which ends
    the previous symbol: RHS[0] (always defined).  */
 
-#define YYRHSLOC(Rhs, K) ((Rhs)[K])
-#ifndef YYLLOC_DEFAULT
-# define YYLLOC_DEFAULT(Current, Rhs, N)                               \
- do                                                                    \
-   if (N)                                                              \
-     {                                                                 \
-       (Current).begin = YYRHSLOC (Rhs, 1).begin;                      \
-       (Current).end   = YYRHSLOC (Rhs, N).end;                        \
-     }                                                                 \
-   else                                                                \
-     {                                                                 \
-       (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end;        \
-     }                                                                 \
- while (false)
-#endif
+# ifndef YYLLOC_DEFAULT
+#  define YYLLOC_DEFAULT(Current, Rhs, N)                               \
+    do                                                                  \
+      if (N)                                                            \
+        {                                                               \
+          (Current).begin  = YYRHSLOC (Rhs, 1).begin;                   \
+          (Current).end    = YYRHSLOC (Rhs, N).end;                     \
+        }                                                               \
+      else                                                              \
+        {                                                               \
+          (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end;      \
+        }                                                               \
+    while (/*CONSTCOND*/ false)
+# endif
+
 
 /* Suppress unused-variable warnings by "using" E.  */
 #define YYUSE(e) ((void) (e))
@@ -137,13 +143,11 @@
 #define YYERROR		goto yyerrorlab
 #define YYRECOVERING()  (!!yyerrstatus_)
 
-
-/* Line 382 of lalr1.cc  */
-#line 5 "grammar.yy"
+/* Line 352 of lalr1.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 382 of lalr1.cc  */
-#line 147 "Generated/parser.cpp"
+/* Line 352 of lalr1.cc  */
+#line 151 "Core/QueryParser/Generated/parser.cpp"
 
   /* Return YYSTR after stripping away unnecessary quotes and
      backslashes, so that it's suitable for yyerror.  The heuristic is
@@ -209,6 +213,9 @@
   {
     YYUSE (yylocationp);
     YYUSE (yyvaluep);
+    std::ostream& yyo = debug_stream ();
+    std::ostream& yyoutput = yyo;
+    YYUSE (yyoutput);
     switch (yytype)
       {
          default:
@@ -241,140 +248,110 @@
 
     switch (yytype)
       {
-        case 3: /* "IDENTIFIER" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 252 "Generated/parser.cpp"
-	break;
-      case 4: /* "LESS" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 261 "Generated/parser.cpp"
-	break;
-      case 5: /* "LESSEQUAL" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 270 "Generated/parser.cpp"
-	break;
-      case 6: /* "EQUAL" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 279 "Generated/parser.cpp"
-	break;
-      case 7: /* "GREATEREQUAL" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 288 "Generated/parser.cpp"
-	break;
-      case 8: /* "GREATER" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 297 "Generated/parser.cpp"
-	break;
-      case 22: /* "query" */
-
-/* Line 480 of lalr1.cc  */
-#line 54 "grammar.yy"
-	{ delete (yyvaluep->query); };
-
-/* Line 480 of lalr1.cc  */
-#line 306 "Generated/parser.cpp"
-	break;
-      case 23: /* "expression" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 315 "Generated/parser.cpp"
-	break;
-      case 24: /* "parExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 324 "Generated/parser.cpp"
-	break;
-      case 25: /* "notExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 333 "Generated/parser.cpp"
-	break;
-      case 26: /* "orExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 342 "Generated/parser.cpp"
-	break;
-      case 27: /* "andExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 351 "Generated/parser.cpp"
-	break;
-      case 28: /* "boolExpression" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 360 "Generated/parser.cpp"
-	break;
-      case 29: /* "atomicProposition" */
-
-/* Line 480 of lalr1.cc  */
-#line 53 "grammar.yy"
-	{ delete (yyvaluep->expr); };
-
-/* Line 480 of lalr1.cc  */
-#line 369 "Generated/parser.cpp"
-	break;
-      case 30: /* "compareOp" */
-
-/* Line 480 of lalr1.cc  */
-#line 52 "grammar.yy"
-	{ delete (yyvaluep->string); };
-
-/* Line 480 of lalr1.cc  */
-#line 378 "Generated/parser.cpp"
+        case 3: /* IDENTIFIER */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 257 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 4: /* LESS */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 264 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 5: /* LESSEQUAL */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 271 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 6: /* EQUAL */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 278 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 7: /* GREATEREQUAL */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 285 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 8: /* GREATER */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 292 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 22: /* query */
+/* Line 453 of lalr1.cc  */
+#line 54 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).query); };
+/* Line 453 of lalr1.cc  */
+#line 299 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 23: /* expression */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 306 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 24: /* parExpression */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 313 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 25: /* notExpression */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 320 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 26: /* orExpression */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 327 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 27: /* andExpression */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 334 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 28: /* boolExpression */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 341 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 29: /* atomicProposition */
+/* Line 453 of lalr1.cc  */
+#line 53 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).expr); };
+/* Line 453 of lalr1.cc  */
+#line 348 "Core/QueryParser/Generated/parser.cpp"
+	break;
+      case 30: /* compareOp */
+/* Line 453 of lalr1.cc  */
+#line 52 "Core/QueryParser/grammar.yy"
+	{ delete ((*yyvaluep).string); };
+/* Line 453 of lalr1.cc  */
+#line 355 "Core/QueryParser/Generated/parser.cpp"
 	break;
 
 	default:
@@ -436,17 +413,18 @@
     int yychar = yyempty_;
     int yytoken = 0;
 
-    /* State.  */
+    // State.
     int yyn;
     int yylen = 0;
     int yystate = 0;
 
-    /* Error handling.  */
+    // Error handling.
     int yynerrs_ = 0;
     int yyerrstatus_ = 0;
 
     /// Semantic value of the lookahead.
-    semantic_type yylval;
+    static semantic_type yyval_default;
+    semantic_type yylval = yyval_default;
     /// Location of the lookahead.
     location_type yylloc;
     /// The locations where the error started and ended.
@@ -462,17 +440,15 @@
     YYCDEBUG << "Starting parse" << std::endl;
 
 
-    /* User initialization code.  */
-    
-/* Line 565 of lalr1.cc  */
-#line 21 "grammar.yy"
+/* User initialization code.  */
+/* Line 539 of lalr1.cc  */
+#line 21 "Core/QueryParser/grammar.yy"
 {
   // Initialize the initial location.
   yylloc.begin.filename = yylloc.end.filename = &driver.file;
 }
-
-/* Line 565 of lalr1.cc  */
-#line 476 "Generated/parser.cpp"
+/* Line 539 of lalr1.cc  */
+#line 452 "Core/QueryParser/Generated/parser.cpp"
 
     /* Initialize the stacks.  The initial state will be pushed in
        yynewstate, since the latter expects the semantical and the
@@ -510,7 +486,6 @@
 	yychar = yylex (&yylval, &yylloc, driver);
       }
 
-
     /* Convert token to internal form.  */
     if (yychar <= yyeof_)
       {
@@ -589,121 +564,104 @@
     switch (yyn)
       {
 	  case 2:
-
-/* Line 690 of lalr1.cc  */
-#line 58 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 58 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EF, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
     break;
 
   case 3:
-
-/* Line 690 of lalr1.cc  */
-#line 59 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 59 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AG, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
     break;
 
   case 4:
-
-/* Line 690 of lalr1.cc  */
-#line 60 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 60 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::EG, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
     break;
 
   case 5:
-
-/* Line 690 of lalr1.cc  */
-#line 61 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 61 "Core/QueryParser/grammar.yy"
     { (yyval.query) = new VerifyTAPN::AST::Query(VerifyTAPN::AST::AF, (yysemantic_stack_[(2) - (2)].expr)); driver.SetAST((yyval.query)); }
     break;
 
   case 6:
-
-/* Line 690 of lalr1.cc  */
-#line 64 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 64 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 7:
-
-/* Line 690 of lalr1.cc  */
-#line 65 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 65 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 8:
-
-/* Line 690 of lalr1.cc  */
-#line 66 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 66 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 9:
-
-/* Line 690 of lalr1.cc  */
-#line 67 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 67 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 10:
-
-/* Line 690 of lalr1.cc  */
-#line 68 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 68 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 11:
-
-/* Line 690 of lalr1.cc  */
-#line 69 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 69 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = (yysemantic_stack_[(1) - (1)].expr); }
     break;
 
   case 12:
-
-/* Line 690 of lalr1.cc  */
-#line 75 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 75 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::ParExpression((yysemantic_stack_[(3) - (2)].expr)); }
     break;
 
   case 13:
-
-/* Line 690 of lalr1.cc  */
-#line 76 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 76 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::NotExpression((yysemantic_stack_[(2) - (2)].expr)); }
     break;
 
   case 14:
-
-/* Line 690 of lalr1.cc  */
-#line 77 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 77 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::OrExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
     break;
 
   case 15:
-
-/* Line 690 of lalr1.cc  */
-#line 78 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 78 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::AndExpression((yysemantic_stack_[(3) - (1)].expr), (yysemantic_stack_[(3) - (3)].expr)); }
     break;
 
   case 16:
-
-/* Line 690 of lalr1.cc  */
-#line 79 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 79 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(true); }
     break;
 
   case 17:
-
-/* Line 690 of lalr1.cc  */
-#line 80 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 80 "Core/QueryParser/grammar.yy"
     { (yyval.expr) = new VerifyTAPN::AST::BoolExpression(false); }
     break;
 
   case 18:
-
-/* Line 690 of lalr1.cc  */
-#line 82 "grammar.yy"
+/* Line 661 of lalr1.cc  */
+#line 82 "Core/QueryParser/grammar.yy"
     { 
 		int placeIndex = driver.tapn().GetPlaceIndex(*(yysemantic_stack_[(3) - (1)].string));
 		if(placeIndex == -1) error((yylocation_stack_[(3) - (1)]), "unknown place"); 
@@ -712,9 +670,8 @@
     break;
 
 
-
-/* Line 690 of lalr1.cc  */
-#line 718 "Generated/parser.cpp"
+/* Line 661 of lalr1.cc  */
+#line 675 "Core/QueryParser/Generated/parser.cpp"
 	default:
           break;
       }
@@ -956,7 +913,7 @@
           }
       }
 
-    char const* yyformat = 0;
+    char const* yyformat = YY_NULL;
     switch (yycount)
       {
 #define YYCASE_(N, S)                         \
@@ -1086,7 +1043,7 @@
        1,     1,     1,     1
   };
 
-#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
+
   /* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
      First, the terminals, then, starting at \a yyntokens_, nonterminals.  */
   const char*
@@ -1097,9 +1054,8 @@
   "LPARAN", "RPARAN", "OR", "AND", "NOT", "BOOL_TRUE", "BOOL_FALSE",
   "$accept", "query", "expression", "parExpression", "notExpression",
   "orExpression", "andExpression", "boolExpression", "atomicProposition",
-  "compareOp", 0
+  "compareOp", YY_NULL
   };
-#endif
 
 #if YYDEBUG
   /* YYRHS -- A `-1'-separated list of the rules' RHS.  */
@@ -1217,17 +1173,13 @@
   const unsigned int Parser::yyuser_token_number_max_ = 275;
   const Parser::token_number_type Parser::yyundef_token_ = 2;
 
-
-/* Line 1136 of lalr1.cc  */
-#line 5 "grammar.yy"
+/* Line 1106 of lalr1.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 1136 of lalr1.cc  */
-#line 1227 "Generated/parser.cpp"
-
-
-/* Line 1138 of lalr1.cc  */
-#line 89 "grammar.yy"
+/* Line 1106 of lalr1.cc  */
+#line 1181 "Core/QueryParser/Generated/parser.cpp"
+/* Line 1107 of lalr1.cc  */
+#line 89 "Core/QueryParser/grammar.yy"
 
 
 void 
@@ -1237,4 +1189,3 @@
 	driver.error (l, m);
 	exit(1);
 }
-
 
=== modified file 'src/Core/QueryParser/Generated/parser.hpp'
--- src/Core/QueryParser/Generated/parser.hpp	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/Generated/parser.hpp	2013-03-31 13:25:26 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.6.5.  */
 
 /* Skeleton interface for Bison LALR(1) parsers in C++
    
-      Copyright (C) 2002-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2012 Free Software Foundation, Inc.
    
    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
@@ -30,15 +30,19 @@
    This special exception was added by the Free Software Foundation in
    version 2.2 of Bison.  */
 
+/**
+ ** \file Core/QueryParser/Generated/parser.hpp
+ ** Define the VerifyTAPN::parser class.
+ */
+
 /* C++ LALR(1) parser skeleton written by Akim Demaille.  */
 
-#ifndef PARSER_HEADER_H
-# define PARSER_HEADER_H
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED
 
 /* "%code requires" blocks.  */
-
-/* Line 35 of lalr1.cc  */
-#line 7 "grammar.yy"
+/* Line 36 of lalr1.cc  */
+#line 7 "Core/QueryParser/grammar.yy"
 
 # include <string>
 #include "../AST.hpp"
@@ -47,9 +51,8 @@
 }
 
 
-
-/* Line 35 of lalr1.cc  */
-#line 53 "Generated/parser.hpp"
+/* Line 36 of lalr1.cc  */
+#line 56 "Core/QueryParser/Generated/parser.hpp"
 
 
 #include <string>
@@ -62,26 +65,11 @@
 # define YYDEBUG 0
 #endif
 
-/* Enabling verbose error messages.  */
-#ifdef YYERROR_VERBOSE
-# undef YYERROR_VERBOSE
-# define YYERROR_VERBOSE 1
-#else
-# define YYERROR_VERBOSE 1
-#endif
-
-/* Enabling the token table.  */
-#ifndef YYTOKEN_TABLE
-# define YYTOKEN_TABLE 0
-#endif
-
-
-/* Line 35 of lalr1.cc  */
-#line 5 "grammar.yy"
+/* Line 36 of lalr1.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 35 of lalr1.cc  */
-#line 85 "Generated/parser.hpp"
+/* Line 36 of lalr1.cc  */
+#line 73 "Core/QueryParser/Generated/parser.hpp"
 
   /// A Bison parser.
   class Parser
@@ -91,9 +79,8 @@
 #ifndef YYSTYPE
     union semantic_type
     {
-
-/* Line 35 of lalr1.cc  */
-#line 30 "grammar.yy"
+/* Line 36 of lalr1.cc  */
+#line 30 "Core/QueryParser/grammar.yy"
 
 	int          					number;
 	std::string* 					string;
@@ -101,9 +88,8 @@
 	VerifyTAPN::AST::Query*		 	query;
 
 
-
-/* Line 35 of lalr1.cc  */
-#line 107 "Generated/parser.hpp"
+/* Line 36 of lalr1.cc  */
+#line 93 "Core/QueryParser/Generated/parser.hpp"
     };
 #else
     typedef YYSTYPE semantic_type;
@@ -246,16 +232,14 @@
     /// For a rule, its LHS.
     static const unsigned char yyr1_[];
     /// For a rule, its RHS length.
-    static const unsigned char yyr2_[];
-
-#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
+    static const unsigned char yyr2_[]; 
+
+    /// Convert the symbol name \a n to a form suitable for a diagnostic.
+    static std::string yytnamerr_ (const char *n);
+
+
     /// For a symbol, its name in clear.
     static const char* const yytname_[];
-#endif
-
-    /// Convert the symbol name \a n to a form suitable for a diagnostic.
-    static std::string yytnamerr_ (const char *n);
-
 #if YYDEBUG
     /// A type to store symbol numbers and -1.
     typedef signed char rhs_number_type;
@@ -309,14 +293,12 @@
     /* User arguments.  */
     VerifyTAPN::TAPNQueryParser& driver;
   };
-
-/* Line 35 of lalr1.cc  */
-#line 5 "grammar.yy"
+/* Line 36 of lalr1.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 35 of lalr1.cc  */
-#line 319 "Generated/parser.hpp"
-
-
-
-#endif /* ! defined PARSER_HEADER_H */
+/* Line 36 of lalr1.cc  */
+#line 301 "Core/QueryParser/Generated/parser.hpp"
+
+
+
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_PARSER_HPP_INCLUDED  */
 
=== modified file 'src/Core/QueryParser/Generated/position.hh'
--- src/Core/QueryParser/Generated/position.hh	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/Generated/position.hh	2013-03-31 13:25:26 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.6.5.  */
 
 /* Positions for Bison parsers in C++
    
-      Copyright (C) 2002-2007, 2009-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2007, 2009-2012 Free Software Foundation, Inc.
    
    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
@@ -31,62 +31,72 @@
    version 2.2 of Bison.  */
 
 /**
- ** \file position.hh
+ ** \file Core/QueryParser/Generated/position.hh
  ** Define the VerifyTAPN::position class.
  */
 
-#ifndef BISON_POSITION_HH
-# define BISON_POSITION_HH
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_POSITION_HH_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_POSITION_HH_INCLUDED
 
+# include <algorithm> // std::max
 # include <iostream>
 # include <string>
-# include <algorithm>
-
-
-/* Line 37 of location.cc  */
-#line 5 "grammar.yy"
+
+# ifndef YY_NULL
+#  if defined __cplusplus && 201103L <= __cplusplus
+#   define YY_NULL nullptr
+#  else
+#   define YY_NULL 0
+#  endif
+# endif
+
+/* Line 38 of location.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 37 of location.cc  */
-#line 52 "Generated/position.hh"
+/* Line 38 of location.cc  */
+#line 58 "Core/QueryParser/Generated/position.hh"
   /// Abstract a position.
   class position
   {
   public:
 
     /// Construct a position.
-    position ()
-      : filename (0), line (1), column (1)
+    explicit position (std::string* f = YY_NULL,
+                       unsigned int l = 1u,
+                       unsigned int c = 1u)
+      : filename (f)
+      , line (l)
+      , column (c)
     {
     }
 
 
     /// Initialization.
-    inline void initialize (std::string* fn)
+    void initialize (std::string* fn = YY_NULL,
+                     unsigned int l = 1u,
+                     unsigned int c = 1u)
     {
       filename = fn;
-      line = 1;
-      column = 1;
+      line = l;
+      column = c;
     }
 
     /** \name Line and Column related manipulators
      ** \{ */
-  public:
     /// (line related) Advance to the COUNT next lines.
-    inline void lines (int count = 1)
+    void lines (int count = 1)
     {
-      column = 1;
+      column = 1u;
       line += count;
     }
 
     /// (column related) Advance to the COUNT next columns.
-    inline void columns (int count = 1)
+    void columns (int count = 1)
     {
       column = std::max (1u, column + count);
     }
     /** \} */
 
-  public:
     /// File name to which this position refers.
     std::string* filename;
     /// Current line number.
@@ -96,7 +106,7 @@
   };
 
   /// Add and assign a position.
-  inline const position&
+  inline position&
   operator+= (position& res, const int width)
   {
     res.columns (width);
@@ -112,7 +122,7 @@
   }
 
   /// Add and assign a position.
-  inline const position&
+  inline position&
   operator-= (position& res, const int width)
   {
     return res += -width;
@@ -155,11 +165,9 @@
     return ostr << pos.line << '.' << pos.column;
   }
 
-
-/* Line 144 of location.cc  */
-#line 5 "grammar.yy"
+/* Line 149 of location.cc  */
+#line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 144 of location.cc  */
-#line 165 "Generated/position.hh"
-#endif // not BISON_POSITION_HH
+/* Line 149 of location.cc  */
+#line 173 "Core/QueryParser/Generated/position.hh"
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_POSITION_HH_INCLUDED  */
 
=== modified file 'src/Core/QueryParser/Generated/stack.hh'
--- src/Core/QueryParser/Generated/stack.hh	2012-04-19 12:40:05 +0000
+++ src/Core/QueryParser/Generated/stack.hh	2013-03-31 13:25:26 +0000
@@ -1,8 +1,8 @@
-/* A Bison parser, made by GNU Bison 2.5.  */
+/* A Bison parser, made by GNU Bison 2.6.5.  */
 
 /* Stack handling for Bison parsers in C++
    
-      Copyright (C) 2002-2011 Free Software Foundation, Inc.
+      Copyright (C) 2002-2012 Free Software Foundation, Inc.
    
    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
@@ -30,23 +30,25 @@
    This special exception was added by the Free Software Foundation in
    version 2.2 of Bison.  */
 
-#ifndef BISON_STACK_HH
-# define BISON_STACK_HH
-
-#include <deque>
-
-
-/* Line 1149 of lalr1.cc  */
-#line 5 "grammar.yy"
+/**
+ ** \file Core/QueryParser/Generated/stack.hh
+ ** Define the VerifyTAPN::stack class.
+ */
+
+#ifndef YY_YY_CORE_QUERYPARSER_GENERATED_STACK_HH_INCLUDED
+# define YY_YY_CORE_QUERYPARSER_GENERATED_STACK_HH_INCLUDED
+
+# include <deque>
+
+/* Line 37 of stack.hh  */
+#line 5 "Core/QueryParser/grammar.yy"
 namespace VerifyTAPN {
-
-/* Line 1149 of lalr1.cc  */
-#line 45 "Generated/stack.hh"
+/* Line 37 of stack.hh  */
+#line 48 "Core/QueryParser/Generated/stack.hh"
   template <class T, class S = std::deque<T> >
   class stack
   {
   public:
-
     // Hide our reversed order.
     typedef typename S::reverse_iterator iterator;
     typedef typename S::const_reverse_iterator const_iterator;
@@ -85,7 +87,7 @@
     pop (unsigned int n = 1)
     {
       for (; n; --n)
-	seq_.pop_front ();
+        seq_.pop_front ();
     }
 
     inline
@@ -99,7 +101,6 @@
     inline const_iterator end () const { return seq_.rend (); }
 
   private:
-
     S seq_;
   };
 
@@ -108,10 +109,9 @@
   class slice
   {
   public:
-
-    slice (const S& stack,
-	   unsigned int range) : stack_ (stack),
-				 range_ (range)
+    slice (const S& stack, unsigned int range)
+      : stack_ (stack)
+      , range_ (range)
     {
     }
 
@@ -123,17 +123,13 @@
     }
 
   private:
-
     const S& stack_;
     unsigned int range_;
   };
-
-/* Line 1235 of lalr1.cc  */
-#line 5 "grammar.yy"
+/* Line 119 of stack.hh  */
+#line 5 "Core/QueryParser/grammar.yy"
 } // VerifyTAPN
-
-/* Line 1235 of lalr1.cc  */
-#line 137 "Generated/stack.hh"
-
-#endif // not BISON_STACK_HH[]dnl
-
+/* Line 119 of stack.hh  */
+#line 134 "Core/QueryParser/Generated/stack.hh"
+
+#endif /* !YY_YY_CORE_QUERYPARSER_GENERATED_STACK_HH_INCLUDED  */
 
=== modified file 'src/Core/TAPN/TimedArcPetriNet.cpp'
--- src/Core/TAPN/TimedArcPetriNet.cpp	2012-07-12 15:47:35 +0000
+++ src/Core/TAPN/TimedArcPetriNet.cpp	2013-03-31 13:25:26 +0000
@@ -189,6 +189,15 @@
 					}
 				}
 			}
+
+			for(TimedTransition::Vector::iterator iter = transitions.begin(); iter != transitions.end(); iter++){
+				for(OutputArc::WeakPtrVector::const_iterator place_iter = iter->get()->GetPostset().begin(); place_iter != iter->get()->GetPostset().end(); place_iter++){
+					if(place_iter->lock()->OutputPlace().GetMaxConstant() > -1){
+						iter->get()->setUntimedPostset(false);
+						break;
+					}
+				}
+			}
 		}
 
 		void TimedArcPetriNet::calculateCausality(TimedPlace& p, std::vector< TimedPlace* >* result) const
 
=== modified file 'src/Core/TAPN/TimedTransition.hpp'
--- src/Core/TAPN/TimedTransition.hpp	2012-03-02 10:59:16 +0000
+++ src/Core/TAPN/TimedTransition.hpp	2013-03-31 13:25:26 +0000
@@ -21,8 +21,8 @@
 		public: // typedefs
 			typedef std::vector< boost::shared_ptr<TimedTransition> > Vector;
 		public:
-			TimedTransition(const std::string& name, const std::string& id) : name(name), id(id), preset(), postset(), transportArcs(), index(-1) { };
-			TimedTransition() : name("*EMPTY*"), id("-1"), preset(), postset(), transportArcs(), index(-1) { };
+			TimedTransition(const std::string& name, const std::string& id) : name(name), id(id), preset(), postset(), transportArcs(), index(-1), untimedPostset(true) { };
+			TimedTransition() : name("*EMPTY*"), id("-1"), preset(), postset(), transportArcs(), index(-1), untimedPostset(true) { };
 			virtual ~TimedTransition() { /* empty */ }
 
 		public: // modifiers
@@ -46,7 +46,9 @@
 			inline unsigned int NumberOfTransportArcs() const { return transportArcs.size(); };
 		//	bool isEnabledBy(const TimedArcPetriNet& tapn, const VerifyTAPN::SymMarking& marking) const;
 			inline const bool isConservative() const { return preset.size() == postset.size(); }
-			inline unsigned int GetIndex() const { return index; };
+			inline unsigned int GetIndex() const { return index; }
+			inline const bool hasUntimedPostset() const { return untimedPostset; }
+			inline void setUntimedPostset(bool untimed){ untimedPostset = untimed; }
 
 		private: // data
 			std::string name;
@@ -56,6 +58,7 @@
 			TransportArc::WeakPtrVector transportArcs;
 			InhibitorArc::WeakPtrVector inhibitorArcs;
 			unsigned int index;
+			bool untimedPostset;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedTransition& transition)
 
=== modified file 'src/Core/VerificationOptions.cpp'
--- src/Core/VerificationOptions.cpp	2012-07-09 13:19:22 +0000
+++ src/Core/VerificationOptions.cpp	2013-03-31 13:25:26 +0000
@@ -25,22 +25,31 @@
 		}
 	}
 
-	std::string FactoryEnumToString(Factory factory){
-		switch(factory)
-		{
-		case OLD_FACTORY:
-			return "old DBM";
-		case DISCRETE_INCLUSION:
-			return "discrete inclusion";
-		default:
-			return "default";
+	std::string VerificationTypeEnumToString(VerificationType s){
+			switch(s){
+			case TIMEDART:
+				return "Time darts";
+			default:
+				return "Default (discrete)";
+			}
 		}
-	}
-
-
+
+        std::string MemoryOptimizationEnumToString(MemoryOptimization m){
+            switch(m){
+                case NONE:
+                    return "None";
+                case PTRIE:
+                    return "PTrie ";
+                default:
+                    return "None";
+            }
+        }
+        
 	std::ostream& operator<<(std::ostream& out, const VerificationOptions& options)
 	{
-		out << "Using " << SearchTypeEnumToString(options.GetSearchType()) << std::endl;
+		out << "Search type: " << SearchTypeEnumToString(options.GetSearchType()) << std::endl;
+		out << "Verification method: " << VerificationTypeEnumToString(options.GetVerificationType()) << std::endl;
+                out << "Memory optimization: " << MemoryOptimizationEnumToString(options.GetMemoryOptimization()) << std::endl;
 		out << "k-bound is: " << options.GetKBound() << std::endl;
 		out << "Generating " << enumToString(options.GetTrace()) << " trace";
 		if(options.GetTrace() != NONE) out << " in " << (options.XmlTrace() ? "xml format" : "human readable format");
 
=== modified file 'src/Core/VerificationOptions.hpp'
--- src/Core/VerificationOptions.hpp	2012-07-12 15:47:35 +0000
+++ src/Core/VerificationOptions.hpp	2013-03-31 13:25:26 +0000
@@ -8,14 +8,18 @@
 namespace VerifyTAPN {
 	enum Trace { NONE, SOME };
 	enum SearchType { BREADTHFIRST, DEPTHFIRST, RANDOM, COVERMOST };
-	enum Factory { DEFAULT, DISCRETE_INCLUSION, OLD_FACTORY };
+	enum VerificationType { DISCRETE, TIMEDART };
+        enum MemoryOptimization { NO_MEMORY_OPTIMIZATION, PTRIE };
 
 	class VerificationOptions {
 		public:
+                        VerificationOptions(){}
 			VerificationOptions(
 				const std::string& inputFile,
 				const std::string& queryFile,
 				SearchType searchType,
+				VerificationType verificationType,
+                                MemoryOptimization memOptimization,
 				unsigned int k_bound,
 				Trace trace,
 				bool xml_trace,
@@ -24,12 +28,16 @@
 			) :	inputFile(inputFile),
 				queryFile(queryFile),
 				searchType(searchType),
+				verificationType(verificationType),
+                                memOptimization(memOptimization),
 				k_bound(k_bound),
 				trace(trace),
 				xml_trace(xml_trace),
 				useGlobalMaxConstants(useGlobalMaxConstants),
 				keepDeadTokens(keepDeadTokens)
-			{ };
+			{ 
+                        
+                        };
 
 		public: // inspectors
 			const std::string GetInputFile() const { return inputFile; }
@@ -39,19 +47,20 @@
 			inline const bool XmlTrace() const { return xml_trace; };
 			inline const bool GetGlobalMaxConstantsEnabled() const { return useGlobalMaxConstants; }
 			inline const SearchType GetSearchType() const { return searchType; }
+			inline const VerificationType GetVerificationType() const { return verificationType; }
+                        inline const MemoryOptimization GetMemoryOptimization() const { return memOptimization; }
 			inline const bool GetKeepDeadTokens() const { return keepDeadTokens; };
-			inline Factory GetFactory() const { return DEFAULT; };
-			inline void SetFactory(Factory f) { factory = f; };
 		private:
 			std::string inputFile;
 			std::string queryFile;
 			SearchType searchType;
+			VerificationType verificationType;
+                        MemoryOptimization memOptimization;
 			unsigned int k_bound;
 			Trace trace;
 			bool xml_trace;
 			bool useGlobalMaxConstants;
 			bool keepDeadTokens;
-			Factory factory;
 	};
 
 	std::ostream& operator<<(std::ostream& out, const VerificationOptions& options);
 
=== added file 'src/DiscreteVerification/DataStructures/EncodingStructure.cpp'
--- src/DiscreteVerification/DataStructures/EncodingStructure.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/EncodingStructure.cpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,14 @@
+/* 
+ * File:   Encoding.cpp
+ * Author: floop
+ * 
+ * Created on 27. oktober 2012, 12:36
+ */
+
+#include "EncodingStructure.h"
+namespace VerifyTAPN {
+    namespace DiscreteVerification {
+
+
+    }
+}
 \ No newline at end of file
 
=== added file 'src/DiscreteVerification/DataStructures/EncodingStructure.h'
--- src/DiscreteVerification/DataStructures/EncodingStructure.h	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/EncodingStructure.h	2013-03-31 13:25:26 +0000
@@ -0,0 +1,241 @@
+/* 
+ * File:   Encoding.h
+ * Author: Peter Gjøl Jense
+ *
+ * Created on 27. oktober 2012, 12:36
+ */
+
+#include <math.h>
+#include <stdio.h>
+#include <iostream>
+#include <string.h>
+
+#ifndef ENCODING_H
+#define	ENCODING_H
+using namespace std;
+namespace VerifyTAPN {
+    namespace DiscreteVerification {
+
+        template<class T>
+        class EncodingStructure {
+        public:
+            typedef unsigned int uint;
+
+            EncodingStructure() {
+            };
+            EncodingStructure(uint size);
+            EncodingStructure(const EncodingStructure &other, uint offset);
+            EncodingStructure(const EncodingStructure &other, uint size, uint offset, uint encsize);
+            EncodingStructure(char* raw, uint size, uint offset, uint encsize);
+            EncodingStructure(char* raw, uint size){
+                shadow = raw;
+                rsize = size;
+            };
+            virtual ~EncodingStructure();
+
+            EncodingStructure Clone() {
+                EncodingStructure s;
+                s.rsize = rsize;
+                s.shadow = new char[rsize + sizeof (T)];
+                memcpy(s.shadow, shadow, rsize + sizeof (T));
+                return s;
+            }
+
+            void Copy(const EncodingStructure &other, unsigned int offset) {
+                memcpy(&(shadow[offset / 8]), other.shadow, other.rsize);
+            }
+            
+            void Copy(const char* raw, unsigned int size){
+                shadow = new char[size + sizeof(T)];
+                memcpy(shadow, raw, size);
+            }
+
+            bool At(const uint place) const;
+            void Set(const uint place, const bool value) const;
+
+            void Zero() const {
+                memset(shadow, 0x0, rsize);
+            }
+
+            unsigned short int Size() const {
+                return rsize;
+            }
+
+            void Release() const {
+                delete[] shadow;
+            }
+
+            char* GetRaw() const {
+                return shadow;
+            }
+
+            void PrintEncoding() const {
+                for (unsigned short int i = 0; i < rsize * 8; i++)
+                    cout << this->At(i);
+                cout << endl;
+            }
+
+            inline static uint Overhead(uint size) {
+                size = size % 8;
+                if (size == 0)
+                    return 0;
+                else
+                    return 8 - size;
+            }
+
+            inline void SetMetaData(T data) const {
+                memcpy(&(shadow[rsize]), &data, sizeof (T));
+            }
+
+            inline T GetMetaData() const {
+                T res;
+                memcpy(&res, &(shadow[rsize]), sizeof (T));
+                return res;
+            }
+
+            const char operator[](int i) {
+
+                if (i >= rsize) {
+                    return 0x0;
+                }
+                return shadow[i];
+            }
+            
+            friend bool operator==(const EncodingStructure &enc1, const EncodingStructure &enc2) {
+                if(enc1.rsize != enc2.rsize)
+                    return false;
+                for(int i = 0; i < enc1.rsize; i++)
+                    if(enc1.shadow[i] != enc2.shadow[i])
+                        return false;
+                return true;
+            }
+            
+            
+            friend bool operator<(const EncodingStructure &enc1, const EncodingStructure &enc2) {
+                int count = enc1.rsize > enc2.rsize ? enc1.rsize : enc2.rsize;
+
+                for (int i = 0; i < count; i++) {
+                    if (enc1.rsize > i && enc2.rsize > i && enc1.shadow[i] != enc2.shadow[i]) {
+                        return ((unsigned short int) enc1.shadow[i]) < ((unsigned short int) enc2.shadow[i]);
+                    }
+
+                }
+                if (enc1.rsize > enc2.rsize) {
+                    return false;
+
+                } else if (enc1.rsize < enc2.rsize) {
+                    return true;
+                }
+
+                return false;
+            }
+
+        private:
+            char* shadow;
+            unsigned short rsize;
+            const static char masks[8];
+        };
+
+        template<class T>
+        const char EncodingStructure<T>::masks[8] = {
+            0x01,
+            0x02,
+            0x04,
+            0x08,
+            0x10,
+            0x20,
+            0x40,
+            0x80
+        };
+
+        template<class T>
+        EncodingStructure<T>::EncodingStructure(uint size) {
+            rsize = (size + Overhead(size)) / 8;
+            shadow = new char[rsize + sizeof (T)];
+            memset(shadow, 0x0, rsize + sizeof (T));
+        }
+
+        template<class T>
+        EncodingStructure<T>::EncodingStructure(const EncodingStructure &other, uint offset) {
+            offset = offset / 8;
+
+            rsize = other.rsize;
+            if (rsize > offset)
+                rsize -= offset;
+            else {
+                rsize = 0;
+            }
+
+            shadow = new char[rsize + sizeof (T)];
+            memcpy(shadow, &(other.shadow[offset]), rsize);
+            SetMetaData(other.GetMetaData());
+        }
+
+        template<class T>
+        EncodingStructure<T>::EncodingStructure(const EncodingStructure &other, uint size, uint offset, uint encsize) {
+
+            uint so = size + offset;
+            offset = ((so - 1) / 8) - ((size - 1) / 8);
+
+            rsize = ((encsize + this->Overhead(encsize)) / 8);
+            if (rsize > offset)
+                rsize -= offset;
+            else {
+                rsize = 0;
+            }
+
+            shadow = new char[rsize + sizeof (T)];
+            memcpy(shadow, &(other.shadow[offset]), rsize);
+            SetMetaData(other.GetMetaData());
+        }
+
+        template<class T>
+        EncodingStructure<T>::EncodingStructure(char* raw, uint size, uint offset, uint encsize) {
+
+            uint so = size + offset;
+            offset = ((so - 1) / 8) - ((size - 1) / 8);
+
+            rsize = ((encsize + this->Overhead(encsize)) / 8);
+            if (rsize > offset)
+                rsize -= offset;
+            else {
+                rsize = 0;
+            }
+
+            shadow = &(raw[offset]);
+        }
+
+        template<class T>
+        EncodingStructure<T>::~EncodingStructure() {
+
+        }
+
+        template<class T>
+        bool EncodingStructure<T>::At(const uint place) const {
+            //    return data[place];
+            uint offset = place % 8;
+            bool res2;
+            if (place / 8 < rsize)
+                res2 = (shadow[place / 8] & masks[offset]) != 0;
+            else
+                res2 = false;
+
+            return res2;
+        }
+
+        template<class T>
+        void EncodingStructure<T>::Set(const uint place, const bool value) const {
+            uint offset = place % 8;
+            uint theplace = place / 8;
+            if (value) {
+                shadow[theplace] |= masks[offset];
+            } else {
+                shadow[theplace] &= ~masks[offset];
+            }
+
+        }
+
+    }
+}
+#endif	/* ENCODING_H */
+
 
=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarking.cpp	2012-07-13 17:50:33 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarking.cpp	2013-03-31 13:25:26 +0000
@@ -11,245 +11,5 @@
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
-
-NonStrictMarking::NonStrictMarking() : inTrace(false), children(0), passed(false){
-	// TODO Auto-generated constructor stub
-
-}
-
-NonStrictMarking::NonStrictMarking(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v) : inTrace(false), children(0), passed(false){
-	int prevPlaceId = -1;
-	for(std::vector<int>::const_iterator iter = v.begin(); iter != v.end(); iter++){
-		if(*iter == prevPlaceId){
-			Place& p = places.back();
-			if(p.tokens.size() == 0){
-				Token t(0,1);
-				p.tokens.push_back(t);
-			}else{
-				p.tokens.begin()->add(1);
-			}
-		}else{
-
-			Place p(&tapn.GetPlace(*iter));
-			Token t(0,1);
-			p.tokens.push_back(t);
-			places.push_back(p);
-		}
-		prevPlaceId = *iter;
-	}
-}
-
-NonStrictMarking::NonStrictMarking(const NonStrictMarking& nsm) : inTrace(false), children(0), passed(false){
-	for(PlaceList::const_iterator it = nsm.places.begin(); it != nsm.places.end(); it++){
-		places.push_back(Place(*it));
-	}
-
-	parent = nsm.parent;
-	generatedBy = nsm.generatedBy;
-}
-
-unsigned int NonStrictMarking::size(){
-	int count = 0;
-	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
-		for(TokenList::const_iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
-			count += it->getCount();
-		}
-	}
-	return count;
-}
-
-//int NonStrictMarking::NumberOfTokensInPlace(const Place& place) const{
-//	int count = 0;
-//	for(TokenList::const_iterator it = place.tokens.begin(); it != place.tokens.end(); it++){
-//		count = count + it->getCount();
-//	}
-//	return count;
-//}
-
-int NonStrictMarking::NumberOfTokensInPlace(int placeId) const{
-	int count = 0;
-	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
-		if(iter->place->GetIndex() == placeId){
-			for(TokenList::const_iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
-				count = count + it->getCount();
-			}
-		}
-	}
-	return count;
-}
-
-const TokenList& NonStrictMarking::GetTokenList(int placeId){
-	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
-		if(iter->place->GetIndex() == placeId) return iter->tokens;
-	}
-	return emptyTokenList;
-}
-
-bool NonStrictMarking::RemoveToken(int placeId, int age){
-	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
-		if(pit->place->GetIndex() == placeId){
-			for(TokenList::iterator tit = pit->tokens.begin(); tit != pit->tokens.end(); tit++){
-				if(tit->getAge() == age){
-					return RemoveToken(*pit, *tit);
-				}
-			}
-		}
-	}
-	return false;
-}
-
-void NonStrictMarking::RemoveRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end){
-	place.tokens.erase(begin, end);
-}
-
-bool NonStrictMarking::RemoveToken(Place& place, Token& token){
-	if(token.getCount() > 1){
-		token.remove(1);
-		return true;
-	}else{
-		for(TokenList::iterator iter = place.tokens.begin(); iter != place.tokens.end(); iter++){
-			if(iter->getAge() == token.getAge()){
-				place.tokens.erase(iter);
-				if(place.tokens.empty()){
-					for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
-						if(it->place->GetIndex() == place.place->GetIndex()){
-							places.erase(it);
-							return true;
-						}
-					}
-				}
-				return true;
-			}
-		}
-	}
-	return false;
-}
-
-void NonStrictMarking::AddTokenInPlace(TAPN::TimedPlace& place, int age){
-	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
-		if(pit->place->GetIndex() == place.GetIndex()){
-			for(TokenList::iterator tit = pit->tokens.begin(); tit != pit->tokens.end(); tit++){
-				if(tit->getAge() == age){
-					Token t(age, 1);
-					AddTokenInPlace(*pit, t);
-					return;
-				}
-			}
-			Token t(age,1);
-			AddTokenInPlace(*pit, t);
-			return;
-		}
-	}
-	Token t(age,1);
-	Place p(&place);
-	AddTokenInPlace(p,t);
-
-	// Insert place
-	bool inserted = false;
-	for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
-		if(it->place->GetIndex() > place.GetIndex()){
-			places.insert(it, p);
-			inserted = true;
-			break;
-		}
-	}
-	if(!inserted){
-		places.push_back(p);
-	}
-}
-
-void NonStrictMarking::AddTokenInPlace(TAPN::TimedPlace& place, Token& token){
-	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
-		if(pit->place->GetIndex() == place.GetIndex()){
-			AddTokenInPlace(*pit, token);
-			return;
-		}
-	}
-
-	Place p(&place);
-	AddTokenInPlace(p,token);
-
-	// Insert place
-	bool inserted = false;
-	for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
-		if(it->place->GetIndex() > place.GetIndex()){
-			places.insert(it, p);
-			inserted = true;
-			break;
-		}
-	}
-	if(!inserted){
-		places.push_back(p);
-	}
-}
-
-void NonStrictMarking::AddTokenInPlace(Place& place, Token& token){
-	if(token.getCount() == 0) return;
-	for(TokenList::iterator iter = place.tokens.begin(); iter != place.tokens.end(); iter++){
-		if(iter->getAge() == token.getAge()){
-			iter->add(token.getCount());
-			return;
-		}
-	}
-	// Insert token
-	bool inserted = false;
-	for(TokenList::iterator it = place.tokens.begin(); it != place.tokens.end(); it++){
-		if(it->getAge() > token.getAge()){
-			place.tokens.insert(it, token);
-			inserted = true;
-			break;
-		}
-	}
-	if(!inserted){
-		place.tokens.push_back(token);
-	}
-}
-
-void NonStrictMarking::incrementAge(){
-	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
-		iter->incrementAge();
-	}
-}
-void NonStrictMarking::decrementAge(){
-	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
-		iter->decrementAge();
-	}
-}
-
-NonStrictMarking::~NonStrictMarking() {
-	// TODO: Should we destruct something here? (places)
-}
-
-bool NonStrictMarking::equals(const NonStrictMarking &m1) const{
-	if(m1.places.size() != places.size())	return false;
-
-	PlaceList::const_iterator p_iter = m1.places.begin();
-	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++, p_iter++){
-		if(iter->place->GetIndex() != p_iter->place->GetIndex())	return false;
-		if(iter->tokens.size() != p_iter->tokens.size())	return false;
-		TokenList::const_iterator pt_iter = p_iter->tokens.begin();
-		for(TokenList::const_iterator t_iter = iter->tokens.begin(); t_iter != iter->tokens.end(); t_iter++, pt_iter++){
-			if(!t_iter->equals(*pt_iter))	return false;
-		}
-	}
-
-	return true;
-}
-
-std::ostream& operator<<(std::ostream& out, NonStrictMarking& x ) {
-	out << "-";
-	for(PlaceList::iterator iter = x.places.begin(); iter != x.places.end(); iter++){
-		out << "place " << iter->place->GetId() << " has tokens (age, count): ";
-		for(TokenList::iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
-			out << "(" << it->getAge() << ", " << it->getCount() << ") ";
-		}
-		if(iter != x.places.end()-1){
-			out << endl;
-		}
-	}
-
-	return out;
-}
-
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */
 
=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2012-09-10 18:54:32 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp	2013-03-31 13:25:26 +0000
@@ -11,171 +11,49 @@
 #include <assert.h>
 #include <vector>
 #include "boost/functional/hash.hpp"
-#include "NonStrictMarking.hpp"
+#include "NonStrictMarkingBase.hpp"
 #include <iostream>
 #include "../../Core/TAPN/TAPN.hpp"
-#include <iostream>
 
 using namespace std;
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
-
-class Place;
-class Token;
-typedef vector<Token> TokenList;
-
-class Token {
-private:
-	int age;
-	int count;
-public:
-	Token(int age, int count) : age(age), count(count) {  };
-	Token(const Token& t) : age(t.age), count(t.count) {  };
-
-	bool equals(const Token &t) const { return (this->age == t.age && this->count == t.count); };
-
-	void add(int num){ count = count + num; };
-	int getCount() const { return count; };
-	int getAge() const { return age; };
-	void setAge(int i) { age = i; };
-	void setCount(int i) { count = i; };
-	void remove(int num){ count = count - num; };
-
-	// Ages all tokens by 1
-	inline void incrementAge(){
-		age++;
-	}
-	inline void decrementAge(){
-		age--;
-	}
-
-	friend std::size_t hash_value(Token const& t)
-	{
-		size_t seed = 0;
-		boost::hash_combine(seed, t.getAge());
-		boost::hash_combine(seed, t.getCount());
-		return seed;
-	}
-};
-
-class Place {
-public:
-	const TAPN::TimedPlace* place;
-	TokenList tokens;
-
-	Place(const TAPN::TimedPlace* place) : place(place){};
-	Place(const Place& p) : place(p.place){
-		for(TokenList::const_iterator it = p.tokens.begin(); it != p.tokens.end(); it++){
-			tokens.push_back(*it);
-		}
-	};
-
-	friend std::size_t hash_value(Place const& p)
-	{
-		std::size_t seed = boost::hash_range(p.tokens.begin(), p.tokens.end());
-		boost::hash_combine(seed, p.place->GetIndex());
-
-		return seed;
-	}
-
-	int NumberOfTokens() const{
-		int count = 0;
-		for(TokenList::const_iterator iter = tokens.begin(); iter != tokens.end(); iter++){
-			count += iter->getCount();
-		}
-		return count;
-	}
-
-	int MaxTokenAge() const{
-		int max = -1;
-		for(TokenList::const_iterator iter = tokens.begin(); iter != tokens.end(); iter++){
-			if(iter->getAge() > max) max = iter->getAge();
-		}
-		return max;
-	}
-
-	// Ages all tokens by 1
-	void incrementAge(){
-		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
-			iter->incrementAge();
-		}
-	}
-
-	void decrementAge(){
-		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
-			iter->decrementAge();
-		}
-	}
-};
-
-typedef vector<Place> PlaceList;
-
-class NonStrictMarking {
-public:
-	NonStrictMarking();
-	NonStrictMarking(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v);
-	NonStrictMarking(const NonStrictMarking& nsm);
-
-public:
-	friend std::ostream& operator<<(std::ostream& out, NonStrictMarking& x );
-	friend class DiscreteVerification;
-
-	virtual ~NonStrictMarking();
-
-	virtual size_t HashKey() const { return boost::hash_range(places.begin(), places.end()); };
-
-	virtual NonStrictMarking& Clone()
-		{
-			NonStrictMarking* clone = new NonStrictMarking(*this);
-			return *clone;
-		};
-
-	public: // inspectors
-		//int NumberOfTokensInPlace(const Place& palce) const;
-		int NumberOfTokensInPlace(int placeId) const;
-		const TokenList& GetTokenList(int placeId);
-		const PlaceList& GetPlaceList() const{ return places; }
-		unsigned int size();
-		const NonStrictMarking* GetParent() const { return parent; }
-		const TAPN::TimedTransition* GetGeneratedBy() const { return generatedBy; }
-
-
-	public: // modifiers
-		bool RemoveToken(int placeId, int age);
-		bool RemoveToken(Place& place, Token& token);
-		void AddTokenInPlace(TAPN::TimedPlace& place, int age);
-		void AddTokenInPlace(Place& place, Token& token);
-		void AddTokenInPlace(TAPN::TimedPlace& place, Token& token);
-		void incrementAge();	// increment
-		void decrementAge();	// decrement
-		void RemoveRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end);
-		void SetParent(NonStrictMarking* parent) { this->parent = parent; }
-		void SetGeneratedBy(const TAPN::TimedTransition* generatedBy) { this->generatedBy = generatedBy; }
-		void CleanUp() {
-			for(unsigned int i = 0; i < places.size(); i++){
-				if(places[i].tokens.empty()){
-					places.erase(places.begin()+i);
-				}
-			}
-		}
-
-	public:
-		bool equals(const NonStrictMarking &m1) const;
-
-	public:
-		bool inTrace;
-		int children;
-		bool passed;
-		PlaceList places;
-		TokenList emptyTokenList;
-
-	public:
-		NonStrictMarking* parent;
-		const TAPN::TimedTransition* generatedBy;
-};
-
-std::ostream& operator<<(std::ostream& out, NonStrictMarking& x);
+ 
+   struct MetaData {
+    public:
+        MetaData() : passed(false), inTrace(false) {};
+        bool passed;
+        bool inTrace;
+    };
+    
+    struct MetaDataWithTrace : public MetaData {
+        const TAPN::TimedTransition* generatedBy;
+    };
+    
+    // ugly forward declaration
+    template<class MetaData>
+    class EncodingPointer;
+    
+    struct MetaDataWithTraceAndEncoding : public MetaDataWithTrace {
+        EncodingPointer<MetaData>* ep;
+        MetaDataWithTraceAndEncoding* parent;
+    };
+    
+    class NonStrictMarking : public NonStrictMarkingBase{
+    public:
+        NonStrictMarking():NonStrictMarkingBase(), meta(new MetaData()){}
+	NonStrictMarking(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v):NonStrictMarkingBase(tapn, v){}
+	NonStrictMarking(const NonStrictMarkingBase& nsm):NonStrictMarkingBase(nsm){
+
+        }
+        NonStrictMarking(const NonStrictMarking& nsm):NonStrictMarkingBase(nsm){
+
+        }
+    public:
+        MetaData* meta;
+    };
+    
 
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */
 
=== added file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.cpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,339 @@
+/*
+ * NonStrictMarkingBase.cpp
+ *
+ *  Created on: 29/02/2012
+ *      Author: MathiasGS
+ */
+
+#include "NonStrictMarkingBase.hpp"
+
+using namespace std;
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+NonStrictMarkingBase::NonStrictMarkingBase() : children(0), generatedBy(NULL){
+	// TODO Auto-generated constructor stub
+
+}
+
+NonStrictMarkingBase::NonStrictMarkingBase(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v) :children(0), generatedBy(NULL){
+	int prevPlaceId = -1;
+	for(std::vector<int>::const_iterator iter = v.begin(); iter != v.end(); iter++){
+		if(*iter == prevPlaceId){
+			Place& p = places.back();
+			if(p.tokens.size() == 0){
+				Token t(0,1);
+				p.tokens.push_back(t);
+			}else{
+				p.tokens.begin()->add(1);
+			}
+		}else{
+
+			Place p(&tapn.GetPlace(*iter));
+			Token t(0,1);
+			p.tokens.push_back(t);
+			places.push_back(p);
+		}
+		prevPlaceId = *iter;
+	}
+}
+
+NonStrictMarkingBase::NonStrictMarkingBase(const NonStrictMarkingBase& nsm) : children(0), generatedBy(NULL){
+	//for(PlaceList::const_iterator it = nsm.places.begin(); it != nsm.places.end(); it++){
+	//	places.push_back(Place(*it));
+	//}
+
+	places = nsm.places;
+
+	parent = nsm.parent;
+	generatedBy = nsm.generatedBy;
+}
+
+unsigned int NonStrictMarkingBase::size(){
+	int count = 0;
+	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
+		for(TokenList::const_iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
+			count += it->getCount();
+		}
+	}
+	return count;
+}
+
+//int NonStrictMarkingBase::NumberOfTokensInPlace(const Place& place) const{
+//	int count = 0;
+//	for(TokenList::const_iterator it = place.tokens.begin(); it != place.tokens.end(); it++){
+//		count = count + it->getCount();
+//	}
+//	return count;
+//}
+
+int NonStrictMarkingBase::NumberOfTokensInPlace(int placeId) const{
+	int count = 0;
+	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
+		if(iter->place->GetIndex() == placeId){
+			for(TokenList::const_iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
+				count = count + it->getCount();
+			}
+		}
+	}
+	return count;
+}
+
+const TokenList& NonStrictMarkingBase::GetTokenList(int placeId) const{
+	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++){
+		if(iter->place->GetIndex() == placeId) return iter->tokens;
+	}
+	return emptyTokenList;
+}
+
+bool NonStrictMarkingBase::RemoveToken(int placeId, int age){
+	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
+		if(pit->place->GetIndex() == placeId){
+			for(TokenList::iterator tit = pit->tokens.begin(); tit != pit->tokens.end(); tit++){
+				if(tit->getAge() == age){
+					return RemoveToken(*pit, *tit);
+				}
+			}
+		}
+	}
+	return false;
+}
+
+void NonStrictMarkingBase::RemoveRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end){
+	place.tokens.erase(begin, end);
+}
+
+bool NonStrictMarkingBase::RemoveToken(Place& place, Token& token){
+	if(token.getCount() > 1){
+		token.remove(1);
+		return true;
+	}else{
+		for(TokenList::iterator iter = place.tokens.begin(); iter != place.tokens.end(); iter++){
+			if(iter->getAge() == token.getAge()){
+				place.tokens.erase(iter);
+				if(place.tokens.empty()){
+					for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
+						if(it->place->GetIndex() == place.place->GetIndex()){
+							places.erase(it);
+							return true;
+						}
+					}
+				}
+				return true;
+			}
+		}
+	}
+	return false;
+}
+
+void NonStrictMarkingBase::AddTokenInPlace(TAPN::TimedPlace& place, int age){
+	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
+		if(pit->place->GetIndex() == place.GetIndex()){
+			for(TokenList::iterator tit = pit->tokens.begin(); tit != pit->tokens.end(); tit++){
+				if(tit->getAge() == age){
+					Token t(age, 1);
+					AddTokenInPlace(*pit, t);
+					return;
+				}
+			}
+			Token t(age,1);
+			AddTokenInPlace(*pit, t);
+			return;
+		}
+	}
+	Token t(age,1);
+	Place p(&place);
+	AddTokenInPlace(p,t);
+
+	// Insert place
+	bool inserted = false;
+	for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
+		if(it->place->GetIndex() > place.GetIndex()){
+			places.insert(it, p);
+			inserted = true;
+			break;
+		}
+	}
+	if(!inserted){
+		places.push_back(p);
+	}
+}
+
+void NonStrictMarkingBase::AddTokenInPlace(const TAPN::TimedPlace& place, Token& token){
+	for(PlaceList::iterator pit = places.begin(); pit != places.end(); pit++){
+		if(pit->place->GetIndex() == place.GetIndex()){
+			AddTokenInPlace(*pit, token);
+			return;
+		}
+	}
+
+	Place p(&place);
+	AddTokenInPlace(p,token);
+
+	// Insert place
+	bool inserted = false;
+	for(PlaceList::iterator it = places.begin(); it != places.end(); it++){
+		if(it->place->GetIndex() > place.GetIndex()){
+			places.insert(it, p);
+			inserted = true;
+			break;
+		}
+	}
+	if(!inserted){
+		places.push_back(p);
+	}
+}
+
+void NonStrictMarkingBase::AddTokenInPlace(Place& place, Token& token){
+	if(token.getCount() == 0) return;
+	for(TokenList::iterator iter = place.tokens.begin(); iter != place.tokens.end(); iter++){
+		if(iter->getAge() == token.getAge()){
+			iter->add(token.getCount());
+			return;
+		}
+	}
+	// Insert token
+	bool inserted = false;
+	for(TokenList::iterator it = place.tokens.begin(); it != place.tokens.end(); it++){
+		if(it->getAge() > token.getAge()){
+			place.tokens.insert(it, token);
+			inserted = true;
+			break;
+		}
+	}
+	if(!inserted){
+		place.tokens.push_back(token);
+	}
+}
+
+void NonStrictMarkingBase::incrementAge(){
+	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
+		iter->incrementAge();
+	}
+}
+
+void NonStrictMarkingBase::incrementAge(int age){
+	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
+		iter->incrementAge(age);
+	}
+}
+
+void NonStrictMarkingBase::decrementAge(){
+	for(PlaceList::iterator iter = places.begin(); iter != places.end(); iter++){
+		iter->decrementAge();
+	}
+}
+
+NonStrictMarkingBase::~NonStrictMarkingBase() { }
+
+bool NonStrictMarkingBase::equals(const NonStrictMarkingBase &m1) const{
+	if(m1.places.size() != places.size())	return false;
+
+	PlaceList::const_iterator p_iter = m1.places.begin();
+	for(PlaceList::const_iterator iter = places.begin(); iter != places.end(); iter++, p_iter++){
+		if(iter->place->GetIndex() != p_iter->place->GetIndex())	return false;
+		if(iter->tokens.size() != p_iter->tokens.size())	return false;
+		TokenList::const_iterator pt_iter = p_iter->tokens.begin();
+		for(TokenList::const_iterator t_iter = iter->tokens.begin(); t_iter != iter->tokens.end(); t_iter++, pt_iter++){
+			if(!t_iter->equals(*pt_iter))	return false;
+		}
+	}
+
+	return true;
+}
+
+std::ostream& operator<<(std::ostream& out, NonStrictMarkingBase& x ) {
+	out << "-";
+	for(PlaceList::iterator iter = x.places.begin(); iter != x.places.end(); iter++){
+		out << "place " << iter->place->GetId() << " has tokens (age, count): ";
+		for(TokenList::iterator it = iter->tokens.begin(); it != iter->tokens.end(); it++){
+			out << "(" << it->getAge() << ", " << it->getCount() << ") ";
+		}
+		if(iter != x.places.end()-1){
+			out << endl;
+		}
+	}
+
+	return out;
+}
+
+void NonStrictMarkingBase::cut(){
+#ifdef DEBUG
+	std::cout << "Before cut: " << *this << std::endl;
+#endif
+	for(PlaceList::iterator place_iter = this->places.begin(); place_iter != this->places.end(); place_iter++){
+		//remove dead tokens
+		if (place_iter->place->GetType() ==  TAPN::Dead) {
+			for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
+				if(token_iter->getAge() > place_iter->place->GetMaxConstant()){
+					token_iter->remove(token_iter->getCount());
+				}
+			}
+		}
+		//set age of too old tokens to max age
+		int count = 0;
+		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
+			if(token_iter->getAge() > place_iter->place->GetMaxConstant()){
+				TokenList::iterator beginDelete = token_iter;
+				if(place_iter->place->GetType() == TAPN::Std){
+					for(; token_iter != place_iter->tokens.end(); token_iter++){
+						count += token_iter->getCount();
+					}
+				}
+				this->RemoveRangeOfTokens(*place_iter, beginDelete, place_iter->tokens.end());
+				break;
+			}
+		}
+		Token t(place_iter->place->GetMaxConstant()+1,count);
+		this->AddTokenInPlace(*place_iter, t);
+	}
+	this->CleanUp();
+	#ifdef DEBUG
+		std::cout << "After cut: " << *this << std::endl;
+	#endif
+}
+
+int NonStrictMarkingBase::getYoungest(){
+    	int youngest = INT_MAX;
+	for(PlaceList::const_iterator place_iter = GetPlaceList().begin(); place_iter != GetPlaceList().end(); place_iter++){
+		if(youngest > place_iter->tokens.front().getAge() && place_iter->tokens.front().getAge() <= place_iter->place->GetMaxConstant()){
+			youngest = place_iter->tokens.front().getAge();
+		}
+	}
+
+	if(youngest == INT_MAX){
+		youngest = 0;
+	}
+        return youngest;
+}
+
+int NonStrictMarkingBase::makeBase(TAPN::TimedArcPetriNet* tapn){
+	#ifdef DEBUG
+		std::cout << "Before makeBase: " << *this << std::endl;
+	#endif
+	int youngest = getYoungest();
+
+	for(PlaceList::iterator place_iter = places.begin(); place_iter != places.end(); place_iter++){
+		for(TokenList::iterator token_iter = place_iter->tokens.begin(); token_iter != place_iter->tokens.end(); token_iter++){
+			if(token_iter->getAge() != place_iter->place->GetMaxConstant() + 1){
+				token_iter->setAge(token_iter->getAge()-youngest);
+			}
+#ifdef DEBUG
+			else if(token_iter->getAge() > place_iter->place->GetMaxConstant() + 1){
+				assert(false);
+			}
+#endif
+		}
+	}
+
+	#ifdef DEBUG
+		std::cout << "After makeBase: " << *this << std::endl;
+		std::cout << "Youngest: " << youngest << std::endl;
+	#endif
+
+	return youngest;
+}
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
 
=== added file 'src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp'
--- src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/NonStrictMarkingBase.hpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,196 @@
+/*
+ * NonStrictMarkingBase.hpp
+ *
+ *  Created on: 29/02/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef NonStrictMarkingBase_HPP_
+#define NonStrictMarkingBase_HPP_
+
+#include <assert.h>
+#include <vector>
+#include "boost/functional/hash.hpp"
+#include <iostream>
+#include "../../Core/TAPN/TAPN.hpp"
+#include <iostream>
+
+using namespace std;
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+class Place;
+class Token;
+typedef vector<Token> TokenList;
+
+class Token {
+private:
+	int age;
+	int count;
+public:
+	Token(int age, int count) : age(age), count(count) {  };
+	Token(const Token& t) : age(t.age), count(t.count) {  };
+
+	bool equals(const Token &t) const { return (this->age == t.age && this->count == t.count); };
+
+	void add(int num){ count = count + num; };
+	int getCount() const { return count; };
+	int getAge() const { return age; };
+	void setAge(int i) { age = i; };
+	void setCount(int i) { count = i; };
+	void remove(int num){ count = count - num; };
+
+	// Ages all tokens by 1
+	inline void incrementAge(){
+		age++;
+	}
+
+	inline void incrementAge(int x){
+		age += x;
+	}
+
+	inline void decrementAge(){
+		age--;
+	}
+
+	friend std::size_t hash_value(Token const& t)
+	{
+		size_t seed = 0;
+		boost::hash_combine(seed, t.getAge());
+		boost::hash_combine(seed, t.getCount());
+		return seed;
+	}
+};
+
+class Place {
+public:
+	const TAPN::TimedPlace* place;
+	TokenList tokens;
+
+	Place(const TAPN::TimedPlace* place) : place(place){};
+	Place(const Place& p) : place(p.place){
+		for(TokenList::const_iterator it = p.tokens.begin(); it != p.tokens.end(); it++){
+			tokens.push_back(*it);
+		}
+	};
+
+	friend std::size_t hash_value(Place const& p)
+	{
+		std::size_t seed = boost::hash_range(p.tokens.begin(), p.tokens.end());
+		boost::hash_combine(seed, p.place->GetIndex());
+
+		return seed;
+	}
+
+	int NumberOfTokens() const{
+		int count = 0;
+		for(TokenList::const_iterator iter = tokens.begin(); iter != tokens.end(); iter++){
+			count += iter->getCount();
+		}
+		return count;
+	}
+
+	int MaxTokenAge() const{
+		int max = -1;
+		for(TokenList::const_iterator iter = tokens.begin(); iter != tokens.end(); iter++){
+			if(iter->getAge() > max) max = iter->getAge();
+		}
+		return max;
+	}
+
+	// Ages all tokens by 1
+	void incrementAge(){
+		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
+			iter->incrementAge();
+		}
+	}
+
+	void incrementAge(int age){
+		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
+			iter->incrementAge(age);
+		}
+	}
+
+	void decrementAge(){
+		for(TokenList::iterator iter = tokens.begin(); iter != tokens.end(); iter++){
+			iter->decrementAge();
+		}
+	}
+};
+
+typedef vector<Place> PlaceList;
+
+class NonStrictMarkingBase {
+public:
+	NonStrictMarkingBase();
+	NonStrictMarkingBase(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v);
+	NonStrictMarkingBase(const NonStrictMarkingBase& nsm);
+
+public:
+	friend std::ostream& operator<<(std::ostream& out, NonStrictMarkingBase& x );
+	friend class DiscreteVerification;
+
+	virtual ~NonStrictMarkingBase();
+
+	virtual size_t HashKey() const { return boost::hash_range(places.begin(), places.end()); };
+
+	virtual NonStrictMarkingBase& Clone()
+		{
+			NonStrictMarkingBase* clone = new NonStrictMarkingBase(*this);
+			return *clone;
+		};
+
+	public: // inspectors
+		//int NumberOfTokensInPlace(const Place& palce) const;
+		int NumberOfTokensInPlace(int placeId) const;
+		const TokenList& GetTokenList(int placeId) const;
+		const PlaceList& GetPlaceList() const{ return places; }
+		unsigned int size();
+		const NonStrictMarkingBase* GetParent() const { return parent; }
+		const TAPN::TimedTransition* GetGeneratedBy() const { return generatedBy; }
+
+
+	public: // modifiers
+		void cut();
+		bool RemoveToken(int placeId, int age);
+		bool RemoveToken(Place& place, Token& token);
+		void AddTokenInPlace(TAPN::TimedPlace& place, int age);
+		void AddTokenInPlace(Place& place, Token& token);
+		void AddTokenInPlace(const TAPN::TimedPlace& place, Token& token);
+		void incrementAge();	// increment
+		void incrementAge(int age);
+		void decrementAge();	// decrement
+		void RemoveRangeOfTokens(Place& place, TokenList::iterator begin, TokenList::iterator end);
+		void SetParent(NonStrictMarkingBase* parent) { this->parent = parent; }
+		void SetGeneratedBy(const TAPN::TimedTransition* generatedBy) { this->generatedBy = generatedBy; }
+		void CleanUp() {
+			for(unsigned int i = 0; i < places.size(); i++){
+				if(places[i].tokens.empty()){
+					places.erase(places.begin()+i);
+					i--;
+				}
+			}
+		}
+                int getYoungest();
+		int makeBase(TAPN::TimedArcPetriNet* tapn);
+
+	public:
+		bool equals(const NonStrictMarkingBase &m1) const;
+
+	public:
+		int children;
+		PlaceList places;
+		TokenList emptyTokenList;
+
+	public:
+		NonStrictMarkingBase* parent;
+		const TAPN::TimedTransition* generatedBy;
+};
+
+std::ostream& operator<<(std::ostream& out, NonStrictMarkingBase& x);
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
+
+#endif /* NonStrictMarkingBase_HPP_ */
 
=== added file 'src/DiscreteVerification/DataStructures/PData.cpp'
--- src/DiscreteVerification/DataStructures/PData.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/PData.cpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,16 @@
+/* 
+ * File:   PData.cpp
+ * Author: floop
+ * 
+ * Created on 5. november 2012, 10:22
+ */
+
+#include <set>
+
+#include "PData.h"
+namespace VerifyTAPN {
+    namespace DiscreteVerification {
+
+ 
+    }
+}
 \ No newline at end of file
 
=== added file 'src/DiscreteVerification/DataStructures/PData.h'
--- src/DiscreteVerification/DataStructures/PData.h	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/PData.h	2013-03-31 13:25:26 +0000
@@ -0,0 +1,427 @@
+/* 
+ * File:   PData.h
+ * Author: Peter Gjøl Jensen
+ *
+ * Created on 5. november 2012, 10:22
+ */
+
+
+#include "NonStrictMarking.hpp"
+#include "EncodingStructure.h"
+#include "TimeDart.hpp"
+
+#ifndef PDATA_H
+#define	PDATA_H
+namespace VerifyTAPN {
+    namespace DiscreteVerification {
+
+        // pointer containing enough data to reconstruct the stored data at any time!
+        template<typename T>
+        struct EncodingPointer {
+            EncodingStructure<T*> encoding;
+            unsigned int node;
+
+            EncodingPointer() {
+            };
+
+            EncodingPointer(EncodingPointer<T> &en) : encoding(en.encoding.Clone()), node(en.node) {};  // possible mem-leak?
+            
+            EncodingPointer(EncodingStructure<T*> &en, unsigned int n) : encoding(en.Clone()), node(n) {
+            }
+        };
+        
+        template<typename T>
+        class PData {
+        public:
+            typedef unsigned int uint;
+            typedef EncodingStructure<T*> MarkingEncoding;
+
+            struct Result {
+                bool isNew;
+                MarkingEncoding encoding;
+                uint pos;
+
+                Result(bool ex, MarkingEncoding en, uint node) : isNew(ex), encoding(en), pos(node) {
+                };
+            };
+
+
+            PData(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, int knumber, int nplaces, int mage) :
+            k(knumber),
+            maxAge(mage + 1),
+            numberOfPlaces(nplaces),
+            countSize(ceil(log2((knumber ? knumber : 1)) + 1)),
+            enumeratedOffset(ceil(log2((nplaces * (mage + 1))) + 1) + countSize),
+            numberOfVariables(enumeratedOffset * (knumber ? knumber : 1)),
+            cachesize(128),
+            tapn(tapn) {
+                overhead = MarkingEncoding::Overhead(this->numberOfVariables);
+                this->numberOfVariables += overhead;
+                stored = 0;
+                bddsize = cachesize;
+                this->BDDArr.push_back(new PNode[this->bddsize]);
+                memset(this->BDDArr[0], 0xffffffff, this->bddsize * sizeof (PNode));
+                BDDArr[0][0].shadow = NULL;
+                BDDArr[0][0].highCount = BDDArr[0][0].lowCount = 0;
+                BDDArr[0][0].lowpos = BDDArr[0][0].highpos = 0;
+                BDDArr[0][0].parent = 0;
+                bddnext = 1;
+                encoding = MarkingEncoding(this->numberOfVariables);
+                listcount = 0;
+                maxCount = sizeof (PNode) * 4 + sizeof (std::list<PNode>) * 4;
+
+            };
+            virtual ~PData();
+
+            uint maxCount;
+
+            struct PNode {
+                MarkingEncoding* shadow;
+                uint highpos;
+
+                uint lowpos;
+
+                short int highCount;
+                short int lowCount;
+                uint parent;
+            };
+
+            bool search(MarkingEncoding* arr, MarkingEncoding en, int size) {
+                for (int i = 0; i < size; i++) {
+                    if (arr[i] == en)
+                        return true;
+                }
+                return false;
+            }
+            /*            bool equal(MarkingEncoding* arr, EncodingList* lst){
+                            EncodingList::const_iterator it = lst->begin();
+                            while(it != lst->end()){
+                                if(!search(arr, *it, lst->size()))
+                                    return false;
+                                it++;
+                            }
+                            return true;
+                        }*/
+
+            Result Add(NonStrictMarkingBase* marking);
+
+            unsigned int size() {
+                return stored;
+            }
+            void PrintMemStats();
+            void PrintEncoding(bool* encoding, int length);
+
+            inline PNode* FetchNode(uint i) {
+                return &BDDArr[i / cachesize][i % cachesize];
+            }
+            NonStrictMarkingBase* EnumerateDecode(const EncodingPointer<T>& pointer);
+
+            int EnumeratedEncoding(NonStrictMarkingBase* marking);
+            const uint k;
+            const uint maxAge;
+            const uint numberOfPlaces;
+            const uint countSize;
+            const uint enumeratedOffset;
+            uint numberOfVariables;
+            const uint cachesize;
+
+            boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn;
+
+            MarkingEncoding encoding;
+            vector<PNode*> BDDArr;
+            uint bddsize;
+            uint stored;
+            uint bddnext;
+            uint overhead;
+            uint listcount;
+        };
+
+        template<typename T>
+        PData<T>::~PData() {
+        }
+
+
+        template<typename T>
+        int PData<T>::EnumeratedEncoding(NonStrictMarkingBase* marking) {
+            encoding.Zero();
+
+            int tc = 0;
+            uint bitcount = 0;
+
+            for (vector<Place>::const_iterator pi = marking->places.begin();
+                    pi != marking->places.end();
+                    pi++) { // for each place
+
+                int pc = pi->place->GetIndex();
+
+                for (TokenList::const_iterator ti = pi->tokens.begin(); // for each token-element
+                        ti != pi->tokens.end();
+                        ti++) {
+
+                    //                   for (int i = 0; i < ti->getCount(); i++) // for each ACTUAL token
+                    //                   {
+                    int offset = tc * this->enumeratedOffset; // the offset of the variables for this token
+                    uint number = ti->getCount();
+                    bitcount = 0;
+                    while (number) { // set the vars while there are bits left
+                        if (number & 1) {
+                            this->encoding.Set(overhead + offset + bitcount, true);
+                        }
+                        bitcount++;
+                        number = number >> 1;
+                    }
+                    uint pos = pc + this->numberOfPlaces * ti->getAge(); // the enumerated configuration of the token
+                    bitcount = countSize;
+                    /* binary */
+                    while (pos) { // set the vars while there are bits left
+                        if (pos & 1) {
+                            this->encoding.Set(overhead + offset + bitcount, true);
+                        }
+                        bitcount++;
+                        pos = pos >> 1;
+                    }
+                    tc++;
+                    //                    }
+
+                }
+            }
+            if (tc == 0)
+                return 0;
+            else
+                return ((tc - 1) * this->enumeratedOffset) + bitcount;
+        }
+
+        template<typename T>
+        NonStrictMarkingBase* PData<T>::EnumerateDecode(const EncodingPointer<T> &pointer) {
+            NonStrictMarkingBase* m = new NonStrictMarkingBase();
+            this->encoding.Zero();
+
+            uint var = 0;
+            uint n = pointer.node;
+            while (n) {
+                n = FetchNode(n)->parent;
+                var++;
+            }
+            var += this->overhead;
+
+            //            m->meta = pointer.encoding.GetMetaData();
+            this->encoding.Copy(pointer.encoding, var);
+            uint nbits = (var - (var % 8)) + pointer.encoding.Size()*8;
+            uint self = pointer.node;
+
+            while (self) {
+                var--;
+                n = FetchNode(self)->parent;
+                bool branch = FetchNode(n)->highpos == self;
+                this->encoding.Set(var, branch);
+                self = n;
+
+            }
+
+            var = this->numberOfVariables - 1;
+            // foreach token
+            uint data = 0;
+            uint count = 0;
+            for (int i = this->k - 1; i >= 0; i--) {
+                uint offset = (this->enumeratedOffset * i) + this->overhead + this->countSize;
+                while (nbits >= offset) {
+                    data = data << 1;
+
+                    if (encoding.At(nbits)) {
+                        data = data | 1;
+                    }
+                    if (nbits == 0) {
+                        break;
+                    }
+                    nbits--;
+                }
+                offset -= this->countSize;
+                while (nbits >= offset) {
+                    count = count << 1;
+
+                    if (encoding.At(nbits)) {
+                        count = count | 1;
+                    }
+                    if (nbits == 0) {
+                        break;
+                    }
+                    nbits--;
+                }
+
+                if (count) {
+                    int age = floor(data / this->numberOfPlaces);
+                    uint place = (data % this->numberOfPlaces);
+                    Token t = Token(age, count);
+                    m->AddTokenInPlace(tapn->GetPlace(place), t);
+                    data = 0;
+                    count = 0;
+                }
+            }
+            return m;
+        }
+
+        template<typename T>
+        typename PData<T>::Result PData<T>::Add(NonStrictMarkingBase* marking) {
+
+            int encsize = this->EnumeratedEncoding(marking) + overhead;
+            // go through the BDD as far as possible with the encoding of the marking
+            uint c_count = 0;
+            uint prev_count = 0;
+            int var = overhead;
+            do {
+
+                prev_count = c_count;
+                if (encoding.At(var)) {
+                    c_count = BDDArr[c_count / cachesize][c_count % cachesize].highpos;
+
+                } else {
+                    c_count = BDDArr[c_count / cachesize][c_count % cachesize].lowpos;
+                }
+
+                var++;
+
+            } while (c_count != 0);
+            var--;
+
+            PNode* prev_node = FetchNode(prev_count);
+
+            int listsize = 0;
+            if (prev_node->highCount >= 0) {
+                listsize += prev_node->highCount;
+            }
+            if (prev_node->lowCount >= 0) {
+                listsize += prev_node->lowCount;
+            }
+
+            int size = this->numberOfVariables - var;
+            MarkingEncoding en = MarkingEncoding(encoding.GetRaw(), size, var, encsize);
+
+            int ins = 0;
+
+            for (; ins < listsize; ins++) {
+                if (prev_node->shadow[ins] == en) {
+                    break;
+                }
+            }
+            if (ins != listsize) {
+                return Result(false, prev_node->shadow[ins], prev_count);
+            }
+
+            en = MarkingEncoding(encoding, size, var, encsize);
+            short unsigned int count;
+
+            MarkingEncoding* nlist = new MarkingEncoding[listsize + 1];
+            nlist[listsize] = en;
+
+            for (int i = 0; i < listsize; i++) {
+                nlist[i] = prev_node->shadow[i];
+            }
+            delete[] prev_node->shadow;
+            prev_node->shadow = nlist;
+
+
+            bool branch = encoding.At(var);
+            if (branch) {
+                count = (++prev_node->highCount);
+            } else {
+                count = (++prev_node->lowCount);
+            }
+
+            if (count > maxCount) {
+
+                size--;
+                int testclist = 0;
+                int testnlist = 0;
+                PNode* c_node = &this->BDDArr[floor(this->bddnext / this->cachesize)][this->bddnext % this->cachesize];
+                if (branch) {
+                    prev_node->highpos = this->bddnext;
+                    c_node->shadow = new MarkingEncoding[testclist = prev_node->highCount];
+                    prev_node->highCount = -1;
+                    if (prev_node->lowCount > 0)
+                        nlist = new MarkingEncoding[testnlist = prev_node->lowCount];
+                    else
+                        nlist = NULL;
+                } else {
+                    prev_node->lowpos = this->bddnext;
+                    c_node->shadow = new MarkingEncoding[testclist = prev_node->lowCount];
+                    prev_node->lowCount = -1;
+                    if (prev_node->highCount > 0)
+                        nlist = new MarkingEncoding[testnlist = prev_node->highCount];
+                    else
+                        nlist = NULL;
+                }
+                c_node->parent = prev_count;
+                prev_count = this->bddnext;
+                listcount++;
+                c_node->lowCount = c_node->highCount = 0;
+                c_node->lowpos = c_node->highpos = 0;
+                uint npos = ((this->numberOfVariables - (size + 1)) % 8);
+
+                MarkingEncoding nee;
+                int clistcount = 0;
+                int nlistcount = 0;
+                for (int i = 0; i < listsize + 1; i++) {
+                    if (prev_node->shadow[i].At(npos) == branch) {
+                        if (!(size % 8)) {
+                            nee = MarkingEncoding(prev_node->shadow[i], 8);
+                            if (i == ins) {
+                                en = nee;
+                            }
+                            prev_node->shadow[i].Release();
+                        } else {
+                            nee = prev_node->shadow[i];
+                        }
+                        if (nee.At((npos + 1) % 8)) {
+                            c_node->highCount++;
+                        } else {
+                            c_node->lowCount++;
+                        }
+                        c_node->shadow[clistcount] = nee;
+                        clistcount++;
+                    } else {
+                        nlist[nlistcount] = prev_node->shadow[i];
+                        nlistcount++;
+                    }
+
+                }
+                delete[] prev_node->shadow;
+                prev_node->shadow = nlist;
+
+                if (prev_node->highCount == -1 && prev_node->lowCount == -1) {
+                    listcount--;
+                    delete[] prev_node->shadow;
+                }
+
+                this->bddnext++;
+                if (this->bddnext == this->bddsize) {
+                    this->bddsize += this->cachesize;
+                    this->BDDArr.push_back(new PNode[this->cachesize]);
+                    memset(this->BDDArr[floor(this->bddsize / this->cachesize) - 1], 0xffffffff, (this->cachesize) * sizeof (PNode));
+                }
+            }
+
+            stored++;
+            return Result(true, en, prev_count);
+
+        }
+
+        template<typename T>
+        void PData<T>::PrintMemStats() {
+            cout << endl << "Encoding size;" << endl <<
+                    "\t\t\t" << this->numberOfVariables << endl;
+            cout << "Lists:" << endl <<
+                    "\t count \t\t" << this->listcount << endl;
+            cout << "Nodes:" << endl <<
+                    "\t count \t\t" << this->bddnext - 1 << endl;
+        }
+
+        template<typename T>
+        void PData<T>::PrintEncoding(bool* encoding, int length) {
+            for (int i = 0; i < length; i++)
+                cout << encoding[i];
+            cout << endl;
+        }
+    }
+}
+#endif	/* PDATA_H */
+
 
=== modified file 'src/DiscreteVerification/DataStructures/PWList.cpp' (properties changed: +x to -x)
--- src/DiscreteVerification/DataStructures/PWList.cpp	2012-11-24 11:35:27 +0000
+++ src/DiscreteVerification/DataStructures/PWList.cpp	2013-03-31 13:25:26 +0000
@@ -17,22 +17,26 @@
 			iter != m.end();
 			iter++){
 		if((*iter)->equals(*marking)){
-			if(!(*iter)->passed){
-				waiting_list->Add(*iter);
-				return true;
-			}
-			return false;
+                    if(isLiveness){
+                        marking->meta = (*iter)->meta;
+                        if(!marking->meta->passed){
+                                (*iter)->SetGeneratedBy(marking->GetGeneratedBy());
+                                waiting_list->Add(*iter, *iter);
+                                return true;
+                        }
+                    }
+                    return false;
 		}
 	}
         stored++;
 	m.push_back(marking);
-	waiting_list->Add(marking);
+        marking->meta = new MetaData();
+	waiting_list->Add(marking, marking);
 	return true;
 }
 
 NonStrictMarking* PWList::GetNextUnexplored(){
-	// TODO: Is this really it?
-	return waiting_list->Next();
+	return waiting_list->Pop();
 }
 
 PWList::~PWList() {
@@ -50,5 +54,70 @@
 	return out;
 }
 
+        bool PWListHybrid::Add(NonStrictMarking* marking) {
+
+            discoveredMarkings++;
+            // reset the encoding array
+
+            PData<MetaData>::Result res = passed->Add(marking);
+            if(res.isNew){
+                if(isLiveness){
+                    MetaData* meta;
+                    if(this->makeTrace){
+                        meta = new MetaDataWithTrace();   
+                        ((MetaDataWithTrace*)meta)->generatedBy = marking->generatedBy;
+                    } else {
+                        meta = new MetaData();
+                    }
+                    res.encoding.SetMetaData(meta);
+                    marking->meta = meta;
+                } else if(this->makeTrace){
+                    MetaDataWithTraceAndEncoding* meta = new MetaDataWithTraceAndEncoding();
+                    meta->generatedBy = marking->generatedBy;
+                    res.encoding.SetMetaData(meta);
+                    meta->ep = new EncodingPointer<MetaData > (res.encoding, res.pos);
+                    meta->parent = parent;
+                }
+                this->waiting_list->Add(marking, new EncodingPointer<MetaData > (res.encoding, res.pos));
+            } else{
+                if(isLiveness){
+                        marking->meta = res.encoding.GetMetaData();
+                        if(this->makeTrace){
+                            ((MetaDataWithTrace*)marking->meta)->generatedBy = marking->generatedBy;
+                        }
+                }
+                if(isLiveness && !marking->meta->passed){
+                    this->waiting_list->Add(marking, new EncodingPointer<MetaData > (res.encoding, res.pos));
+                    return true;
+                }
+            }
+            return res.isNew;
+        }
+
+        NonStrictMarking* PWListHybrid::GetNextUnexplored() {
+            // TODO: Is this really it?
+            EncodingPointer<MetaData>* p = waiting_list->Pop();
+            NonStrictMarkingBase* base = passed->EnumerateDecode(*p);
+            NonStrictMarking* m = new NonStrictMarking(*base);
+            delete base;
+            
+            m->meta = p->encoding.GetMetaData();
+            
+            if(this->makeTrace){
+                if(isLiveness){
+                        m->generatedBy = ((MetaDataWithTrace*)(m->meta))->generatedBy;
+                } else {
+                    this->parent = (MetaDataWithTraceAndEncoding*)(m->meta);
+                }
+            }
+            if(isLiveness || !this->makeTrace)
+                p->encoding.Release();
+            return m;
+        }
+
+        PWListHybrid::~PWListHybrid() {
+            // TODO Auto-generated destructor stub
+        }
+
 } /* namespace DiscreteVerification */
 } /* namespace VerifyTAPN */
 
=== modified file 'src/DiscreteVerification/DataStructures/PWList.hpp' (properties changed: +x to -x)
--- src/DiscreteVerification/DataStructures/PWList.hpp	2012-11-24 11:35:27 +0000
+++ src/DiscreteVerification/DataStructures/PWList.hpp	2013-03-31 13:25:26 +0000
@@ -17,13 +17,31 @@
 
 namespace VerifyTAPN {
 namespace DiscreteVerification {
-class PWList {
+    
+    class PWListBase {
+    public:
+        PWListBase() : stored(0), discoveredMarkings(0), maxNumTokensInAnyMarking(-1), isLiveness(false) {};
+        PWListBase(bool isLiveness) : stored(0), discoveredMarkings(0), maxNumTokensInAnyMarking(-1), isLiveness(isLiveness){};
+        int stored;
+    	int discoveredMarkings;
+	int maxNumTokensInAnyMarking;
+        bool isLiveness;
+        
+        virtual bool HasWaitingStates() = 0;
+        virtual long long Size() const = 0;
+        virtual bool Add(NonStrictMarking* marking) = 0;
+	virtual NonStrictMarking* GetNextUnexplored() = 0;
+        virtual long long Explored()= 0;
+	inline void SetMaxNumTokensIfGreater(int i){ if(i>maxNumTokensInAnyMarking) maxNumTokensInAnyMarking = i; };
+    };
+    
+class PWList : public PWListBase {
 public:
 	typedef std::vector<NonStrictMarking*> NonStrictMarkingList;
 	typedef google::sparse_hash_map<size_t, NonStrictMarkingList> HashMap;
 public:
-	PWList() : markings_storage(256000), waiting_list(), discoveredMarkings(0), maxNumTokensInAnyMarking(-1), stored(0) {};
-	PWList(WaitingList* w_l) : markings_storage(256000), waiting_list(w_l), discoveredMarkings(0), maxNumTokensInAnyMarking(-1), stored(0) {};
+	PWList() : PWListBase(false), markings_storage(256000), waiting_list(){};
+	PWList(WaitingList<NonStrictMarking>* w_l, bool isLiveness) :PWListBase(isLiveness), markings_storage(256000), waiting_list(w_l) {};
 	virtual ~PWList();
 	friend std::ostream& operator<<(std::ostream& out, PWList& x);
 
@@ -36,18 +54,65 @@
 		return stored;
 	};
 
+        virtual long long Explored() {return waiting_list->Size();};
+        
 public: // modifiers
 	virtual bool Add(NonStrictMarking* marking);
 	virtual NonStrictMarking* GetNextUnexplored();
-	inline void SetMaxNumTokensIfGreater(int i){ if(i>maxNumTokensInAnyMarking) maxNumTokensInAnyMarking = i; };
 
 public:
 	HashMap markings_storage;
-	WaitingList* waiting_list;
-	int discoveredMarkings;
-	int maxNumTokensInAnyMarking;
-private:
-        unsigned int stored;
+	WaitingList<NonStrictMarking>* waiting_list;
+};
+
+class PWListHybrid : public PWListBase {
+        public:
+            typedef unsigned int uint;
+            //            typedef google::sparse_hash_map<size_t, EncodingList> HashMap;
+            PData<MetaData>* passed;
+
+        public:
+
+            PWListHybrid(boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, WaitingList<EncodingPointer<MetaData> >* w_l, int knumber, int nplaces, int mage, bool isLiveness, bool makeTrace) :
+            PWListBase(isLiveness),
+            waiting_list(w_l),
+            makeTrace(makeTrace) {
+                discoveredMarkings = 0;
+                passed = new PData<MetaData>(tapn, knumber,nplaces,mage);
+                parent = NULL;
+            };
+            virtual ~PWListHybrid();
+            friend std::ostream& operator<<(std::ostream& out, PWListHybrid& x);
+
+        public: // inspectors
+            NonStrictMarking* Decode(EncodingPointer<MetaData>* ep){
+                NonStrictMarkingBase* base = this->passed->EnumerateDecode(*ep);
+                NonStrictMarking* m = new NonStrictMarking(*base);
+                delete base;
+                return m;
+            };
+            virtual bool HasWaitingStates() {
+                return (waiting_list->Size() > 0);
+            };
+
+            virtual long long Size() const {
+                return passed->stored;
+            };
+            virtual long long Explored() {return waiting_list->Size();};
+            void PrintMemStats() {
+                passed->PrintMemStats();
+            }
+
+        public: // modifiers
+            virtual bool Add(NonStrictMarking* marking);
+            virtual NonStrictMarking* GetNextUnexplored();
+
+        public:
+
+             WaitingList<EncodingPointer<MetaData> >* waiting_list;
+             bool makeTrace;
+            //ugly tracefix
+             MetaDataWithTraceAndEncoding* parent;
 };
 
 std::ostream& operator<<(std::ostream& out, PWList& x);
 
=== added file 'src/DiscreteVerification/DataStructures/TimeDart.hpp'
--- src/DiscreteVerification/DataStructures/TimeDart.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/TimeDart.hpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,128 @@
+/*
+ * TimeDart.hpp
+ *
+ *  Created on: 18/09/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef TIMEDART_HPP_
+#define TIMEDART_HPP_
+
+#include "NonStrictMarking.hpp"
+#include "PData.h"
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+struct WaitingDart;
+struct TraceDart;
+class TimeDartBase;
+
+typedef EncodingPointer<TimeDartBase> TimeDartEncodingPointer;  // used for memory-optimization for reachability
+typedef EncodingPointer<WaitingDart> WaitingDartEncodingPointer; // mem-optimization for liveness
+
+
+typedef vector<WaitingDart*> TraceMetaDataList;
+
+class TimeDartBase {
+public:
+	TimeDartBase(NonStrictMarkingBase* base, int waiting, int passed)
+		: base(base), waiting(waiting), passed(passed){
+	}
+	~TimeDartBase(){
+	}
+
+	//Getters
+	inline NonStrictMarkingBase* getBase(){ return base; }
+        inline void setBase(NonStrictMarkingBase* newbase) { base = newbase;}
+	inline int getWaiting(){ return waiting; }
+	inline int getPassed(){ return passed; }
+
+	//Getters
+	inline void setWaiting(int w){ waiting = w; }
+	inline void setPassed(int p){ passed = p; }
+
+private:
+	NonStrictMarkingBase* base;
+	int waiting;
+	int passed;
+};
+
+
+class ReachabilityTraceableDart : public TimeDartBase {
+public:
+    ReachabilityTraceableDart(NonStrictMarkingBase* base, int waiting, int passed)
+            : TimeDartBase(base, waiting, passed), trace(NULL){
+    }
+    TraceDart* trace;
+};
+
+class EncodedReachabilityTraceableDart : public ReachabilityTraceableDart {
+public:
+    EncodedReachabilityTraceableDart(NonStrictMarkingBase* base, int waiting, int passed) 
+        : ReachabilityTraceableDart(base, waiting, passed) {
+        
+        
+    }
+    TimeDartEncodingPointer* encoding;
+};
+
+class LivenessDart : public TimeDartBase {
+public:
+    LivenessDart(NonStrictMarkingBase* base, int waiting, int passed)
+		: TimeDartBase(base, waiting, passed), traceData(NULL){
+        }
+    TraceMetaDataList* traceData;
+};
+
+class EncodedLivenessDart : public LivenessDart {
+public:
+    EncodedLivenessDart(NonStrictMarkingBase* base, int waiting, int passed) 
+        : LivenessDart(base, waiting, passed) {
+
+    }
+    WaitingDartEncodingPointer* encoding;
+};
+
+struct WaitingDart{
+	TimeDartBase* dart;
+	WaitingDart* parent;
+	int w;
+	int upper;
+
+	WaitingDart(TimeDartBase* dart, WaitingDart* parent, int w, int upper) : dart(dart), parent(parent), w(w), upper(upper){
+
+	}
+
+	~WaitingDart(){
+                        
+			if(parent != NULL && ((LivenessDart*)parent->dart)->traceData != NULL){
+				for(TraceMetaDataList::iterator iter = ((LivenessDart*)parent->dart)->traceData->begin(); iter != ((LivenessDart*)parent->dart)->traceData->end(); iter++){
+					if((*iter) == this){
+						((LivenessDart*)parent->dart)->traceData->erase(iter);
+						break;
+					}
+				}
+				if(((LivenessDart*)parent->dart)->traceData->empty()){
+					delete ((LivenessDart*)parent->dart)->traceData;
+					((LivenessDart*)parent->dart)->traceData = NULL;
+				}
+			}
+		}
+};
+
+struct TraceDart : WaitingDart {
+    const TAPN::TimedTransition* generatedBy;
+    const int start;
+    TraceDart(TraceDart &t) : WaitingDart(t.dart, t.parent, t.w, t.upper), generatedBy(t.generatedBy), start(t.start){
+        
+    };
+    TraceDart(TimeDartBase* dart, WaitingDart* parent, int w, int start, int upper, const TAPN::TimedTransition* GeneratedBy) : WaitingDart(dart, parent, w, upper), generatedBy(GeneratedBy), start(start){
+
+	}
+    
+};
+}
+}
+
+#endif /* TIMEDART_HPP_ */
 
=== added file 'src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp'
--- src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.cpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,164 @@
+/*
+ * PWList.cpp
+ *
+ *  Created on: 01/03/2012
+ *      Author: MathiasGS
+ */
+
+#include "TimeDartLivenessPWList.hpp"
+
+namespace VerifyTAPN {
+    namespace DiscreteVerification {
+
+        std::pair<LivenessDart*, bool> TimeDartLivenessPWHashMap::Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) {
+            discoveredMarkings++;
+            TimeDartList& m = markings_storage[marking->HashKey()];
+            for (TimeDartList::const_iterator iter = m.begin();
+                    iter != m.end();
+                    iter++) {
+                if ((*iter)->getBase()->equals(*marking)) {
+                    std::pair < LivenessDart*, bool> result(*iter, false);
+                    (*iter)->setWaiting(min((*iter)->getWaiting(), youngest));
+
+                    if ((*iter)->getWaiting() < (*iter)->getPassed()) {
+                        if(options.GetTrace()){
+                            waiting_list->Add((*iter)->getBase(), new TraceDart((*iter), parent, youngest, start, upper, marking->generatedBy));
+
+                        } else {
+                            waiting_list->Add((*iter)->getBase(), new WaitingDart((*iter), parent, youngest, upper));
+                        }
+                        result.second = true;
+                        delete marking;
+                    }
+
+                    return result;
+                }
+            }
+            stored++;
+            LivenessDart* dart = new LivenessDart(marking, youngest, INT_MAX);
+            m.push_back(dart);
+            if(options.GetTrace()){
+
+                waiting_list->Add(dart->getBase(), new TraceDart(dart, parent, youngest, start, upper, marking->generatedBy));
+
+            } else {
+                waiting_list->Add(dart->getBase(), new WaitingDart(dart, parent, youngest, upper));                
+            }
+            std::pair < LivenessDart*, bool> result(dart, true);
+            return result;
+        }
+
+        WaitingDart* TimeDartLivenessPWHashMap::GetNextUnexplored() {
+            return waiting_list->Peek();
+        }
+
+        void TimeDartLivenessPWHashMap::PopWaiting() {
+            delete waiting_list->Pop();
+        }
+
+        void TimeDartLivenessPWHashMap::flushBuffer() {
+            // Flush buffer if w has changed
+            waiting_list->flushBuffer();
+        }
+
+        std::pair<LivenessDart*, bool> TimeDartLivenessPWPData::Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start) {
+
+            
+            discoveredMarkings++;
+            PData<LivenessDart>::Result res = passed.Add(marking);
+
+                if (!res.isNew) {
+                    LivenessDart* td = res.encoding.GetMetaData();
+                    td->setBase(marking);
+                    std::pair < LivenessDart*, bool> result(td, false);
+                    td->setWaiting(min(td->getWaiting(), youngest));
+                           
+                    if (td->getWaiting() < td->getPassed()) {
+                        EncodingStructure<WaitingDart*> es(res.encoding.GetRaw(), res.encoding.Size());
+
+                        EncodingPointer<WaitingDart>* ewp = new EncodingPointer<WaitingDart > (es, res.pos);
+                        WaitingDart *wd;
+                        if(options.GetTrace()){
+                            wd =  new TraceDart(td, parent, youngest, start, upper, marking->generatedBy);
+
+                        } else {
+                            wd = new WaitingDart(td, parent, youngest, upper);
+                        }
+                        ewp->encoding.SetMetaData(wd);
+                        
+                        waiting_list->Add(marking, ewp);
+                        result.second = true;
+                    } else {
+                        if(options.GetTrace() == SOME){
+                            EncodingStructure<WaitingDart*> es(res.encoding.GetRaw(), res.encoding.Size());
+                           ((EncodedLivenessDart*)td)->encoding = new EncodingPointer<WaitingDart > (es, res.pos);
+                           result.first = td;
+                        }
+                    }
+                    return result;
+                }
+            
+            stored++;
+            LivenessDart* dart;
+            if(options.GetTrace()){
+                dart= new EncodedLivenessDart(marking, youngest, INT_MAX);
+            } else {
+                dart = new LivenessDart(marking, youngest, INT_MAX);
+            }
+            res.encoding.SetMetaData(dart);
+            
+            EncodingStructure<WaitingDart*> es(res.encoding.GetRaw(), res.encoding.Size());
+            EncodingPointer<WaitingDart>* ewp = new EncodingPointer<WaitingDart > (es, res.pos);
+            
+            WaitingDart *wd;
+            if(options.GetTrace()){
+                wd =  new TraceDart(dart, parent, youngest, start, upper, marking->generatedBy);
+                ((EncodedLivenessDart*)dart)->encoding = ewp;
+            } else {
+                wd = new WaitingDart(dart, parent, youngest, upper);
+            }
+            ewp->encoding.SetMetaData(wd);
+            
+            waiting_list->Add(marking, ewp);
+            std::pair < LivenessDart*, bool> result(dart, true);
+            return result;
+        }
+
+        WaitingDart* TimeDartLivenessPWPData::GetNextUnexplored() {
+            EncodingPointer<WaitingDart>* ewp =  waiting_list->Peek();
+            WaitingDart* wd = ewp->encoding.GetMetaData();
+            NonStrictMarkingBase* base = passed.EnumerateDecode(*((EncodingPointer<LivenessDart>*)ewp));
+            wd->dart->setBase(base);
+            if(options.GetTrace() == SOME){
+                ((EncodedLivenessDart*)wd->dart)->encoding = ewp;
+            }
+            return wd;
+        }
+
+        void TimeDartLivenessPWPData::PopWaiting() {
+            EncodingPointer<WaitingDart>* ewp =  waiting_list->Pop();
+            WaitingDart* wd = ewp->encoding.GetMetaData();
+            delete wd->dart->getBase();
+            delete wd;
+            ewp->encoding.Release();
+            delete ewp;
+        }
+
+        void TimeDartLivenessPWPData::flushBuffer() {
+            // Flush buffer if w has changed
+            waiting_list->flushBuffer();
+        }
+
+        std::ostream& operator<<(std::ostream& out, TimeDartLivenessPWHashMap& x) {
+            out << "Passed and waiting:" << std::endl;
+            for (TimeDartLivenessPWHashMap::HashMap::iterator iter = x.markings_storage.begin(); iter != x.markings_storage.end(); iter++) {
+                for (TimeDartLivenessPWHashMap::TimeDartList::iterator m_iter = iter->second.begin(); m_iter != iter->second.end(); m_iter++) {
+                    out << "- " << *m_iter << std::endl;
+                }
+            }
+            out << "Waiting:" << std::endl << x.waiting_list;
+            return out;
+        }
+
+    } /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
 
=== added file 'src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp'
--- src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartLivenessPWList.hpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,118 @@
+/*
+ * PWList.hpp
+ *
+ *  Created on: 01/03/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef TimeDartLivenessPWList_HPP_
+#define TimeDartLivenessPWList_HPP_
+
+#include "WaitingList.hpp"
+#include <iostream>
+#include "google/sparse_hash_map"
+#include "NonStrictMarkingBase.hpp"
+#include "WaitingList.hpp"
+#include "TimeDart.hpp"
+#include "PData.h"
+
+namespace VerifyTAPN {
+    namespace DiscreteVerification {
+        class TimeDartLivenessPWBase;
+        class TimeDartLivenessPWHashMap;
+        //       class TimeDartPWPData;
+
+        class TimeDartLivenessPWBase {
+        public:
+            typedef std::vector<LivenessDart*> TimeDartList;
+            typedef google::sparse_hash_map<size_t, TimeDartList> HashMap;
+        
+        public:
+
+            TimeDartLivenessPWBase() : discoveredMarkings(0), maxNumTokensInAnyMarking(-1), stored(0) {
+            };
+
+            virtual ~TimeDartLivenessPWBase() {
+            };
+
+
+        public: // inspectors
+            virtual bool HasWaitingStates() = 0;
+
+            virtual long long Size() const {
+                return stored;
+            };
+
+        public: // modifiers
+            virtual std::pair<LivenessDart*, bool> Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start) = 0;
+            virtual WaitingDart* GetNextUnexplored() = 0;
+            virtual void PopWaiting() = 0;
+            virtual void flushBuffer() = 0;
+
+            inline void SetMaxNumTokensIfGreater(int i) {
+                if (i > maxNumTokensInAnyMarking) maxNumTokensInAnyMarking = i;
+            };
+
+        public:
+            int discoveredMarkings;
+            int maxNumTokensInAnyMarking;
+            long long stored;
+        };
+
+        class TimeDartLivenessPWHashMap : public TimeDartLivenessPWBase {
+        public:
+
+            TimeDartLivenessPWHashMap() : markings_storage(), waiting_list(){};
+            
+            TimeDartLivenessPWHashMap(VerificationOptions options, WaitingList<WaitingDart>* w_l) : TimeDartLivenessPWBase(), options(options), markings_storage(256000), waiting_list(w_l) {
+            };
+
+            ~TimeDartLivenessPWHashMap() {
+            };
+            friend std::ostream& operator<<(std::ostream& out, TimeDartLivenessPWHashMap& x);
+            virtual std::pair<LivenessDart*, bool> Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start);
+            virtual WaitingDart* GetNextUnexplored();
+            virtual void PopWaiting();
+
+            virtual bool HasWaitingStates() {
+                return (waiting_list->Size() > 0);
+            };
+            virtual void flushBuffer();
+        private:
+            VerificationOptions options;
+            HashMap markings_storage;
+            WaitingList<WaitingDart>* waiting_list;
+        };
+
+        class TimeDartLivenessPWPData : public TimeDartLivenessPWBase {
+        public:
+
+
+            
+            TimeDartLivenessPWPData(VerificationOptions options, WaitingList<EncodingPointer<WaitingDart> >* w_l, boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, int nplaces, int mage) : TimeDartLivenessPWBase(), options(options), waiting_list(w_l), passed(tapn,  options.GetKBound(), nplaces, mage) {
+            };
+
+            ~TimeDartLivenessPWPData() {
+            };
+            friend std::ostream& operator<<(std::ostream& out, TimeDartLivenessPWHashMap& x);
+            virtual std::pair<LivenessDart*, bool> Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* base, int youngest, WaitingDart* parent, int upper, int start);
+            virtual WaitingDart* GetNextUnexplored();
+            virtual void PopWaiting();
+
+            virtual bool HasWaitingStates() {
+                return (waiting_list->Size() > 0);
+            };
+            virtual void flushBuffer();
+            NonStrictMarkingBase* Decode(EncodingPointer<LivenessDart> *ewp){
+                return passed.EnumerateDecode(*ewp);
+            }
+            
+        private:
+            VerificationOptions options;
+            WaitingList<EncodingPointer<WaitingDart> >* waiting_list;
+            PData<LivenessDart> passed;
+        };
+
+    } /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
+#endif /* PWLIST_HPP_ */
 
=== added file 'src/DiscreteVerification/DataStructures/TimeDartPWList.cpp'
--- src/DiscreteVerification/DataStructures/TimeDartPWList.cpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartPWList.cpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,126 @@
+/*
+ * PWList.cpp
+ *
+ *  Created on: 01/03/2012
+ *      Author: MathiasGS
+ */
+
+#include "TimeDartPWList.hpp"
+
+namespace VerifyTAPN {
+namespace DiscreteVerification {
+
+bool TimeDartPWHashMap::Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start){
+	discoveredMarkings++;
+	TimeDartList& m = markings_storage[marking->HashKey()];
+	for(TimeDartList::const_iterator iter = m.begin();
+			iter != m.end();
+			iter++){
+		if((*iter)->getBase()->equals(*marking)){
+				bool inWaiting = (*iter)->getWaiting() < (*iter)->getPassed();
+
+				(*iter)->setWaiting(min((*iter)->getWaiting(),youngest));
+
+				if((*iter)->getWaiting() < (*iter)->getPassed() && !inWaiting){
+					waiting_list->Add((*iter)->getBase(),(*iter));
+                                        if(this->trace){
+                                            ((ReachabilityTraceableDart*)(*iter))->trace = new TraceDart((*iter), parent, youngest, start, upper, marking->generatedBy);
+                                            this->last = ((ReachabilityTraceableDart*)(*iter))->trace;
+                                        }
+				}
+
+			delete marking;
+
+			return false;
+		}
+	}
+        TimeDartBase* dart;
+        if(this->trace){
+             dart = new ReachabilityTraceableDart(marking, youngest, INT_MAX);
+             ((ReachabilityTraceableDart*)dart)->trace = new TraceDart(dart, parent, youngest, start,  upper, marking->generatedBy);
+            this->last = ((ReachabilityTraceableDart*)(dart))->trace;
+        } else {
+            dart = new TimeDartBase(marking, youngest, INT_MAX);
+        }
+        stored++;
+	m.push_back(dart);
+
+	waiting_list->Add(dart->getBase(), dart);
+	return true;
+}
+
+TimeDartBase* TimeDartPWHashMap::GetNextUnexplored(){
+	return waiting_list->Pop();
+}
+
+bool TimeDartPWPData::Add(TAPN::TimedArcPetriNet* tapn, NonStrictMarkingBase* marking, int youngest, WaitingDart* parent, int upper, int start){
+	discoveredMarkings++;
+        PData<TimeDartBase>::Result res = passed.Add(marking);
+
+        if(!res.isNew){
+            TimeDartBase* t = res.encoding.GetMetaData();
+            bool inWaiting = t->getWaiting() < t->getPassed();
+            t->setWaiting(min(t->getWaiting(),youngest));
+
+            if(t->getWaiting() < t->getPassed() && !inWaiting){
+                    if(this->trace){
+                        ((EncodedReachabilityTraceableDart*)t)->trace = new TraceDart(t, parent, youngest, start, upper, marking->generatedBy);
+                        this->last = ((EncodedReachabilityTraceableDart*)t)->trace;
+                    }
+                    waiting_list->Add(marking, new EncodingPointer<TimeDartBase>(res.encoding, res.pos));
+ //               waiting_list->Add(t->getBase(), t);
+            }
+            return false;
+        }
+
+        
+	TimeDartBase* dart;
+         if (this->trace) {
+             dart = new EncodedReachabilityTraceableDart(marking, youngest, INT_MAX);
+            ((EncodedReachabilityTraceableDart*) dart)->trace = new TraceDart(dart, parent, youngest, start, upper, marking->generatedBy);
+            this->last = ((ReachabilityTraceableDart*) (dart))->trace;
+        } else {
+                dart = new TimeDartBase(marking, youngest, INT_MAX);
+        }
+        stored++;
+        res.encoding.SetMetaData(dart);
+        EncodingPointer<TimeDartBase>* ep = new EncodingPointer<TimeDartBase>(res.encoding, res.pos);
+	waiting_list->Add(marking, ep);
+        if (this->trace) {
+            // if trace, create new (persistent) encodingpointer as regular one gets deleted every time we pop from waiting.
+                ((EncodedReachabilityTraceableDart*) dart)->encoding = new EncodingPointer<TimeDartBase>(res.encoding, res.pos);
+        }
+//        waiting_list->Add(dart->getBase(), dart);
+	return true;
+}
+
+TimeDartBase* TimeDartPWPData::GetNextUnexplored(){
+  
+    EncodingPointer<TimeDartBase>* p = waiting_list->Pop();
+    NonStrictMarkingBase* m = passed.EnumerateDecode(*p);
+    TimeDartBase* dart = p->encoding.GetMetaData();
+    dart->setBase(m);
+    
+    p->encoding.Release();
+    delete p;
+    return dart;
+}
+
+
+TimeDartPWHashMap::~TimeDartPWHashMap() {
+	// TODO Auto-generated destructor stub
+}
+
+std::ostream& operator<<(std::ostream& out, TimeDartPWHashMap& x){
+	out << "Passed and waiting:" << std::endl;
+	for(TimeDartPWHashMap::HashMap::iterator iter = x.markings_storage.begin(); iter != x.markings_storage.end(); iter++){
+		for(TimeDartPWHashMap::TimeDartList::iterator m_iter = iter->second.begin(); m_iter != iter->second.end(); m_iter++){
+			out << "- "<< *m_iter << std::endl;
+		}
+	}
+	out << "Waiting:" << std::endl << x.waiting_list;
+	return out;
+}
+
+} /* namespace DiscreteVerification */
+} /* namespace VerifyTAPN */
 
=== added file 'src/DiscreteVerification/DataStructures/TimeDartPWList.hpp'
--- src/DiscreteVerification/DataStructures/TimeDartPWList.hpp	1970-01-01 00:00:00 +0000
+++ src/DiscreteVerification/DataStructures/TimeDartPWList.hpp	2013-03-31 13:25:26 +0000
@@ -0,0 +1,112 @@
+/*
+ * PWList.hpp
+ *
+ *  Created on: 01/03/2012
+ *      Author: MathiasGS
+ */
+
+#ifndef TIMEDARTPWLIST_HPP_
+#define TIMEDARTPWLIST_HPP_
+
+#include "WaitingList.hpp"