From 6caf95f62ea049e7a804c3a950f043207579dd6c Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 20 Nov 2012 22:45:29 +0100
Subject: [PATCH 01/17] first version of new parser

---
 src/mrmc-cpp.cpp             |   4 +-
 src/parser/read_tra_file.cpp | 181 +++++++++++++++++++----------------
 2 files changed, 100 insertions(+), 85 deletions(-)

diff --git a/src/mrmc-cpp.cpp b/src/mrmc-cpp.cpp
index d28bcb2d0..179850998 100644
--- a/src/mrmc-cpp.cpp
+++ b/src/mrmc-cpp.cpp
@@ -92,9 +92,7 @@ int main(int argc, char* argv[]) {
 	counter.start();
 	for (i = 0; i < 10000; ++i) {
 		iArray = (uint_fast64_t*)malloc(2097152 * sizeof(uint_fast64_t));
-		for (j = 0; j < 2097152; ++j) {
-			iArray[j] = 0;
-		}
+		memset(iArray, 0, 2097152 * sizeof(uint_fast64_t));
 		free(iArray);
 	}
 	counter.stop();
diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp
index 4a62af89c..2aac6ad7f 100644
--- a/src/parser/read_tra_file.cpp
+++ b/src/parser/read_tra_file.cpp
@@ -17,6 +17,13 @@
 #include "boost/integer/integer_mask.hpp"
 #include <cstdlib>
 #include <cstdio>
+#include <cstring>
+#include <iostream>
+#include <errno.h>
+#include <time.h>
+#include <sys/stat.h>
+#include <sys/mman.h>
+#include <fcntl.h>
 
 #include <pantheios/pantheios.hpp>
 #include <pantheios/inserters/integer.hpp>
@@ -26,6 +33,16 @@ namespace mrmc {
 
 namespace parser{
 
+char* skipWS(char* buf)
+{
+   unsigned int i = 0;
+   while (1)
+   {
+      if ((buf[i] != ' ') && (buf[i] != '\t') && (buf[i] != '\n') && (buf[i] != '\r')) return buf+i;
+      i++;
+   }
+}
+
 // Disable C4996 - This function or variable may be unsafe.
 #pragma warning(disable:4996)
 
@@ -40,47 +57,30 @@ namespace parser{
 * @param p File stream to scan. Is expected to be opened, a NULL pointer will
 *          be rejected!
 */
-static uint_fast32_t make_first_pass(FILE* p) {
-   if(p==NULL) {
-      pantheios::log_ERROR("make_first_pass was called with NULL! (SHOULD NEVER HAPPEN)");
-      throw exceptions::file_IO_exception ("make_first_pass: File not readable (this should be checked before calling this function!)");
-   }
-   char s[BUFFER_SIZE];                 //String buffer
-   uint_fast32_t rows=0, non_zero=0;
-
-   //Reading No. of states
-   if (fgets(s, BUFFER_SIZE, p) != NULL) {
-      if (sscanf( s, "STATES %d", &rows) == 0) {
-         pantheios::log_WARNING(pantheios::integer(rows));
-         (void)fclose(p);
-         throw mrmc::exceptions::wrong_file_format();
-      }
-   }
-
-   //Reading No. of transitions
-   if (fgets(s, BUFFER_SIZE, p) != NULL) {
-      if (sscanf( s, "TRANSITIONS %d", &non_zero) == 0) {
-         (void)fclose(p);
-         throw mrmc::exceptions::wrong_file_format();
-      }
-   }
+static uint_fast32_t make_first_pass(char* buf)
+{
+	uint_fast32_t non_zero = 0;
+   
+	if (strncmp(buf, "STATES ", 7) != 0) return 0;
+	buf += 7; // skip "STATES "
+	if (strtol(buf, &buf, 10) == 0) return 0;
+	buf = skipWS(buf);
+	if (strncmp(buf, "TRANSITIONS ", 12) != 0) return 0;
+	buf += 12; // skip "TRANSITIONS "
+	if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
+	
+	unsigned int row, col;
+	double val;
+	while (1)  
+	{
+		row = strtol(buf, &buf, 10);
+		col = strtol(buf, &buf, 10);
+		val = strtod(buf, &buf);
+		if (val == 0.0) break;
+		if (row == col) non_zero--;
+	}
 
-   //Reading transitions (one per line)
-   //And increase number of transitions
-   while (NULL != fgets( s, BUFFER_SIZE, p ))
-   {
-      uint_fast32_t row=0, col=0;
-      double val=0.0;
-      if (sscanf( s, "%d%d%lf", &row, &col, &val ) != 3) {
-         (void)fclose(p);
-         throw mrmc::exceptions::wrong_file_format();
-      }
-      //Diagonal elements are not counted into the result!
-      if(row == col) {
-         --non_zero;
-      }
-   }
-   return non_zero;
+	return non_zero;
 }
 
 
@@ -93,75 +93,92 @@ static uint_fast32_t make_first_pass(FILE* p) {
  */
 
 sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
-	FILE *p = NULL;
-	char s[BUFFER_SIZE];
-	uint_fast32_t rows, non_zero;
-	sparse::StaticSparseMatrix<double> *sp = NULL;
-
-	p = fopen(filename, "r");
-	if(p == NULL) {
+	/*
+		open file and map to memory
+	*/
+	struct stat st;
+	int f = open(filename, O_RDONLY);
+	if((f < 0) || (stat(filename, &st) != 0)) {
 		pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
 		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
 		return NULL;
 	}
-	non_zero = make_first_pass(p);
-
-	//Set file reader back to the beginning
-	rewind(p);
-
-	//Reading No. of states
-	if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "STATES %d", &rows) == 0)) {
-		pantheios::log_WARNING(pantheios::integer(rows));
-		(void)fclose(p);
-		throw mrmc::exceptions::wrong_file_format();
+	char *data = (char*)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, f, 0);
+	if (data == (char*)-1)
+	{
+		pantheios::log_ERROR("Could not map the file to memory. Something went wrong with mmap.");
+		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error mapping file to memory");
+		close(f);
 		return NULL;
 	}
-
-	/* Reading No. of transitions
-	 * Note that the result is not used in this function as make_first_pass()
-	 * computes the relevant number (non_zero)
-	 */
-	uint_fast32_t nnz=0;
-	if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) {
-		(void)fclose(p);
+	
+	/*
+		perform first pass
+	*/
+	uint_fast32_t non_zero = make_first_pass(data);
+	if (non_zero = 0)
+	{
+		close(f);
+		munmap(data, st.st_size);
 		throw mrmc::exceptions::wrong_file_format();
 		return NULL;
 	}
+	
+	/*
+		perform second pass
+		
+		from here on, we already know that the file format is correct
+	*/
+	char* buf = data;
+	uint_fast32_t rows;
+	sparse::StaticSparseMatrix<double> *sp = NULL;
 
-   pantheios::log_DEBUG("Creating matrix with ",
+	buf += 7; // skip "STATES "
+	rows = strtol(buf, &buf, 10);
+	buf += 12; // skip "TRANSITIONS "
+	strtol(buf, &buf, 10);
+	
+	pantheios::log_DEBUG("Creating matrix with ",
                         pantheios::integer(rows), " rows and ",
                         pantheios::integer(non_zero), " Non-Zero-Elements");
+                        
 	/* Creating matrix
 	 * Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
 	 * non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
 	sp = new sparse::StaticSparseMatrix<double>(rows);
-	if ( NULL == sp ) {
+	if ( NULL == sp )
+	{
+		close(f);
+		munmap(data, st.st_size);
 		throw std::bad_alloc();
 		return NULL;
 	}
 	sp->initialize(non_zero);
 
-	//Reading transitions (one per line) and saving the results in the matrix
-	while (NULL != fgets(s, BUFFER_SIZE, p )) {
-		uint_fast32_t row=0, col=0;
-		double val = 0.0;
-		if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) {
-			(void)fclose(p);
-			throw mrmc::exceptions::wrong_file_format();
-			// Delete Matrix to free allocated memory
-			delete sp;
-			return NULL;
-		}
-		pantheios::log_DEBUG("Write value ",
+	uint_fast32_t row, col;
+	double val;
+	/*
+		read all transitions from file
+		
+		note: the parser will also stop, if a transition with a value of 0.0 occurs
+	*/
+	while (1)
+	{
+		row = strtol(buf, &buf, 10);
+		col = strtol(buf, &buf, 10);
+		val = strtod(buf, &buf);
+		if (val == 0.0) break;
+		pantheios::log_WARNING("Write value ",
 							pantheios::real(val),
 							" to position ",
 							pantheios::integer(row), " x ",
 							pantheios::integer(col));
-		sp->addNextValue(row,col,val);
+		sp->addNextValue(row,col,val);	
 	}
-
-	(void)fclose(p);
+	
+	close(f);
+	munmap(data, st.st_size);
 
 	pantheios::log_DEBUG("Finalizing Matrix");
 	sp->finalize();

From 25e5095a7cf4cd38ad972884865f6570041e3ba9 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 20 Nov 2012 23:19:10 +0100
Subject: [PATCH 02/17] now, the parser even works :-)

---
 resources/3rdparty/gtest-1.6.0/Makefile.in | 111 +++++++-----
 resources/3rdparty/gtest-1.6.0/aclocal.m4  | 201 ++++++++++++++++-----
 src/parser/read_tra_file.cpp               |  43 +++--
 3 files changed, 252 insertions(+), 103 deletions(-)

diff --git a/resources/3rdparty/gtest-1.6.0/Makefile.in b/resources/3rdparty/gtest-1.6.0/Makefile.in
index ed888925e..11c9feb1a 100644
--- a/resources/3rdparty/gtest-1.6.0/Makefile.in
+++ b/resources/3rdparty/gtest-1.6.0/Makefile.in
@@ -1,9 +1,9 @@
-# Makefile.in generated by automake 1.11.1 from Makefile.am.
+# Makefile.in generated by automake 1.11.3 from Makefile.am.
 # @configure_input@
 
 # Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
-# 2003, 2004, 2005, 2006, 2007, 2008, 2009  Free Software Foundation,
-# Inc.
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011 Free Software
+# Foundation, Inc.
 # This Makefile.in is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
@@ -86,6 +86,12 @@ am__nobase_list = $(am__nobase_strip_setup); \
 am__base_list = \
   sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \
   sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g'
+am__uninstall_files_from_dir = { \
+  test -z "$$files" \
+    || { test ! -d "$$dir" && test ! -f "$$dir" && test ! -r "$$dir"; } \
+    || { echo " ( cd '$$dir' && rm -f" $$files ")"; \
+         $(am__cd) "$$dir" && rm -f $$files; }; \
+  }
 am__installdirs = "$(DESTDIR)$(libdir)" "$(DESTDIR)$(m4datadir)" \
 	"$(DESTDIR)$(pkgincludedir)" \
 	"$(DESTDIR)$(pkginclude_internaldir)"
@@ -169,12 +175,16 @@ DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
 distdir = $(PACKAGE)-$(VERSION)
 top_distdir = $(distdir)
 am__remove_distdir = \
-  { test ! -d "$(distdir)" \
-    || { find "$(distdir)" -type d ! -perm -200 -exec chmod u+w {} ';' \
-         && rm -fr "$(distdir)"; }; }
+  if test -d "$(distdir)"; then \
+    find "$(distdir)" -type d ! -perm -200 -exec chmod u+w {} ';' \
+      && rm -rf "$(distdir)" \
+      || { sleep 5 && rm -rf "$(distdir)"; }; \
+  else :; fi
 DIST_ARCHIVES = $(distdir).tar.gz $(distdir).tar.bz2 $(distdir).zip
 GZIP_ENV = --best
 distuninstallcheck_listfiles = find . -type f -print
+am__distuninstallcheck_listfiles = $(distuninstallcheck_listfiles) \
+  | sed 's|^\./|$(prefix)/|' | grep -v '$(infodir)/dir$$'
 distcleancheck_listfiles = find . -type f -print
 ACLOCAL = @ACLOCAL@
 AMTAR = @AMTAR@
@@ -494,7 +504,7 @@ all: all-am
 
 .SUFFIXES:
 .SUFFIXES: .cc .lo .o .obj
-am--refresh:
+am--refresh: Makefile
 	@:
 $(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
 	@for dep in $?; do \
@@ -530,10 +540,8 @@ $(ACLOCAL_M4):  $(am__aclocal_m4_deps)
 $(am__aclocal_m4_deps):
 
 build-aux/config.h: build-aux/stamp-h1
-	@if test ! -f $@; then \
-	  rm -f build-aux/stamp-h1; \
-	  $(MAKE) $(AM_MAKEFLAGS) build-aux/stamp-h1; \
-	else :; fi
+	@if test ! -f $@; then rm -f build-aux/stamp-h1; else :; fi
+	@if test ! -f $@; then $(MAKE) $(AM_MAKEFLAGS) build-aux/stamp-h1; else :; fi
 
 build-aux/stamp-h1: $(top_srcdir)/build-aux/config.h.in $(top_builddir)/config.status
 	@rm -f build-aux/stamp-h1
@@ -597,10 +605,10 @@ src/gtest-all.lo: src/$(am__dirstamp) src/$(DEPDIR)/$(am__dirstamp)
 lib/$(am__dirstamp):
 	@$(MKDIR_P) lib
 	@: > lib/$(am__dirstamp)
-lib/libgtest.la: $(lib_libgtest_la_OBJECTS) $(lib_libgtest_la_DEPENDENCIES) lib/$(am__dirstamp)
+lib/libgtest.la: $(lib_libgtest_la_OBJECTS) $(lib_libgtest_la_DEPENDENCIES) $(EXTRA_lib_libgtest_la_DEPENDENCIES) lib/$(am__dirstamp)
 	$(CXXLINK) -rpath $(libdir) $(lib_libgtest_la_OBJECTS) $(lib_libgtest_la_LIBADD) $(LIBS)
 src/gtest_main.lo: src/$(am__dirstamp) src/$(DEPDIR)/$(am__dirstamp)
-lib/libgtest_main.la: $(lib_libgtest_main_la_OBJECTS) $(lib_libgtest_main_la_DEPENDENCIES) lib/$(am__dirstamp)
+lib/libgtest_main.la: $(lib_libgtest_main_la_OBJECTS) $(lib_libgtest_main_la_DEPENDENCIES) $(EXTRA_lib_libgtest_main_la_DEPENDENCIES) lib/$(am__dirstamp)
 	$(CXXLINK) -rpath $(libdir) $(lib_libgtest_main_la_OBJECTS) $(lib_libgtest_main_la_LIBADD) $(LIBS)
 samples/$(am__dirstamp):
 	@$(MKDIR_P) samples
@@ -614,7 +622,7 @@ samples/sample2.lo: samples/$(am__dirstamp) \
 	samples/$(DEPDIR)/$(am__dirstamp)
 samples/sample4.lo: samples/$(am__dirstamp) \
 	samples/$(DEPDIR)/$(am__dirstamp)
-samples/libsamples.la: $(samples_libsamples_la_OBJECTS) $(samples_libsamples_la_DEPENDENCIES) samples/$(am__dirstamp)
+samples/libsamples.la: $(samples_libsamples_la_OBJECTS) $(samples_libsamples_la_DEPENDENCIES) $(EXTRA_samples_libsamples_la_DEPENDENCIES) samples/$(am__dirstamp)
 	$(CXXLINK)  $(samples_libsamples_la_OBJECTS) $(samples_libsamples_la_LIBADD) $(LIBS)
 
 clean-checkPROGRAMS:
@@ -627,12 +635,12 @@ clean-checkPROGRAMS:
 	rm -f $$list
 samples/sample10_unittest.$(OBJEXT): samples/$(am__dirstamp) \
 	samples/$(DEPDIR)/$(am__dirstamp)
-samples/sample10_unittest$(EXEEXT): $(samples_sample10_unittest_OBJECTS) $(samples_sample10_unittest_DEPENDENCIES) samples/$(am__dirstamp)
+samples/sample10_unittest$(EXEEXT): $(samples_sample10_unittest_OBJECTS) $(samples_sample10_unittest_DEPENDENCIES) $(EXTRA_samples_sample10_unittest_DEPENDENCIES) samples/$(am__dirstamp)
 	@rm -f samples/sample10_unittest$(EXEEXT)
 	$(CXXLINK) $(samples_sample10_unittest_OBJECTS) $(samples_sample10_unittest_LDADD) $(LIBS)
 samples/sample1_unittest.$(OBJEXT): samples/$(am__dirstamp) \
 	samples/$(DEPDIR)/$(am__dirstamp)
-samples/sample1_unittest$(EXEEXT): $(samples_sample1_unittest_OBJECTS) $(samples_sample1_unittest_DEPENDENCIES) samples/$(am__dirstamp)
+samples/sample1_unittest$(EXEEXT): $(samples_sample1_unittest_OBJECTS) $(samples_sample1_unittest_DEPENDENCIES) $(EXTRA_samples_sample1_unittest_DEPENDENCIES) samples/$(am__dirstamp)
 	@rm -f samples/sample1_unittest$(EXEEXT)
 	$(CXXLINK) $(samples_sample1_unittest_OBJECTS) $(samples_sample1_unittest_LDADD) $(LIBS)
 fused-src/gtest/$(am__dirstamp):
@@ -654,7 +662,7 @@ samples/test_fused_gtest_test-sample1_unittest.$(OBJEXT):  \
 test/$(am__dirstamp):
 	@$(MKDIR_P) test
 	@: > test/$(am__dirstamp)
-test/fused_gtest_test$(EXEEXT): $(test_fused_gtest_test_OBJECTS) $(test_fused_gtest_test_DEPENDENCIES) test/$(am__dirstamp)
+test/fused_gtest_test$(EXEEXT): $(test_fused_gtest_test_OBJECTS) $(test_fused_gtest_test_DEPENDENCIES) $(EXTRA_test_fused_gtest_test_DEPENDENCIES) test/$(am__dirstamp)
 	@rm -f test/fused_gtest_test$(EXEEXT)
 	$(CXXLINK) $(test_fused_gtest_test_OBJECTS) $(test_fused_gtest_test_LDADD) $(LIBS)
 test/$(DEPDIR)/$(am__dirstamp):
@@ -662,7 +670,7 @@ test/$(DEPDIR)/$(am__dirstamp):
 	@: > test/$(DEPDIR)/$(am__dirstamp)
 test/gtest_all_test.$(OBJEXT): test/$(am__dirstamp) \
 	test/$(DEPDIR)/$(am__dirstamp)
-test/gtest_all_test$(EXEEXT): $(test_gtest_all_test_OBJECTS) $(test_gtest_all_test_DEPENDENCIES) test/$(am__dirstamp)
+test/gtest_all_test$(EXEEXT): $(test_gtest_all_test_OBJECTS) $(test_gtest_all_test_DEPENDENCIES) $(EXTRA_test_gtest_all_test_DEPENDENCIES) test/$(am__dirstamp)
 	@rm -f test/gtest_all_test$(EXEEXT)
 	$(CXXLINK) $(test_gtest_all_test_OBJECTS) $(test_gtest_all_test_LDADD) $(LIBS)
 
@@ -811,9 +819,7 @@ uninstall-m4dataDATA:
 	@$(NORMAL_UNINSTALL)
 	@list='$(m4data_DATA)'; test -n "$(m4datadir)" || list=; \
 	files=`for p in $$list; do echo $$p; done | sed -e 's|^.*/||'`; \
-	test -n "$$files" || exit 0; \
-	echo " ( cd '$(DESTDIR)$(m4datadir)' && rm -f" $$files ")"; \
-	cd "$(DESTDIR)$(m4datadir)" && rm -f $$files
+	dir='$(DESTDIR)$(m4datadir)'; $(am__uninstall_files_from_dir)
 install-pkgincludeHEADERS: $(pkginclude_HEADERS)
 	@$(NORMAL_INSTALL)
 	test -z "$(pkgincludedir)" || $(MKDIR_P) "$(DESTDIR)$(pkgincludedir)"
@@ -831,9 +837,7 @@ uninstall-pkgincludeHEADERS:
 	@$(NORMAL_UNINSTALL)
 	@list='$(pkginclude_HEADERS)'; test -n "$(pkgincludedir)" || list=; \
 	files=`for p in $$list; do echo $$p; done | sed -e 's|^.*/||'`; \
-	test -n "$$files" || exit 0; \
-	echo " ( cd '$(DESTDIR)$(pkgincludedir)' && rm -f" $$files ")"; \
-	cd "$(DESTDIR)$(pkgincludedir)" && rm -f $$files
+	dir='$(DESTDIR)$(pkgincludedir)'; $(am__uninstall_files_from_dir)
 install-pkginclude_internalHEADERS: $(pkginclude_internal_HEADERS)
 	@$(NORMAL_INSTALL)
 	test -z "$(pkginclude_internaldir)" || $(MKDIR_P) "$(DESTDIR)$(pkginclude_internaldir)"
@@ -851,9 +855,7 @@ uninstall-pkginclude_internalHEADERS:
 	@$(NORMAL_UNINSTALL)
 	@list='$(pkginclude_internal_HEADERS)'; test -n "$(pkginclude_internaldir)" || list=; \
 	files=`for p in $$list; do echo $$p; done | sed -e 's|^.*/||'`; \
-	test -n "$$files" || exit 0; \
-	echo " ( cd '$(DESTDIR)$(pkginclude_internaldir)' && rm -f" $$files ")"; \
-	cd "$(DESTDIR)$(pkginclude_internaldir)" && rm -f $$files
+	dir='$(DESTDIR)$(pkginclude_internaldir)'; $(am__uninstall_files_from_dir)
 
 ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES)
 	list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \
@@ -988,14 +990,15 @@ check-TESTS: $(TESTS)
 	  fi; \
 	  dashes=`echo "$$dashes" | sed s/./=/g`; \
 	  if test "$$failed" -eq 0; then \
-	    echo "$$grn$$dashes"; \
+	    col="$$grn"; \
 	  else \
-	    echo "$$red$$dashes"; \
+	    col="$$red"; \
 	  fi; \
-	  echo "$$banner"; \
-	  test -z "$$skipped" || echo "$$skipped"; \
-	  test -z "$$report" || echo "$$report"; \
-	  echo "$$dashes$$std"; \
+	  echo "$${col}$$dashes$${std}"; \
+	  echo "$${col}$$banner$${std}"; \
+	  test -z "$$skipped" || echo "$${col}$$skipped$${std}"; \
+	  test -z "$$report" || echo "$${col}$$report$${std}"; \
+	  echo "$${col}$$dashes$${std}"; \
 	  test "$$failed" -eq 0; \
 	else :; fi
 
@@ -1042,7 +1045,11 @@ dist-gzip: distdir
 	tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz
 	$(am__remove_distdir)
 dist-bzip2: distdir
-	tardir=$(distdir) && $(am__tar) | bzip2 -9 -c >$(distdir).tar.bz2
+	tardir=$(distdir) && $(am__tar) | BZIP2=$${BZIP2--9} bzip2 -c >$(distdir).tar.bz2
+	$(am__remove_distdir)
+
+dist-lzip: distdir
+	tardir=$(distdir) && $(am__tar) | lzip -c $${LZIP_OPT--9} >$(distdir).tar.lz
 	$(am__remove_distdir)
 
 dist-lzma: distdir
@@ -1050,7 +1057,7 @@ dist-lzma: distdir
 	$(am__remove_distdir)
 
 dist-xz: distdir
-	tardir=$(distdir) && $(am__tar) | xz -c >$(distdir).tar.xz
+	tardir=$(distdir) && $(am__tar) | XZ_OPT=$${XZ_OPT--e} xz -c >$(distdir).tar.xz
 	$(am__remove_distdir)
 
 dist-tarZ: distdir
@@ -1067,7 +1074,7 @@ dist-zip: distdir
 
 dist dist-all: distdir
 	tardir=$(distdir) && $(am__tar) | GZIP=$(GZIP_ENV) gzip -c >$(distdir).tar.gz
-	tardir=$(distdir) && $(am__tar) | bzip2 -9 -c >$(distdir).tar.bz2
+	tardir=$(distdir) && $(am__tar) | BZIP2=$${BZIP2--9} bzip2 -c >$(distdir).tar.bz2
 	-rm -f $(distdir).zip
 	zip -rq $(distdir).zip $(distdir)
 	$(am__remove_distdir)
@@ -1083,6 +1090,8 @@ distcheck: dist
 	  bzip2 -dc $(distdir).tar.bz2 | $(am__untar) ;;\
 	*.tar.lzma*) \
 	  lzma -dc $(distdir).tar.lzma | $(am__untar) ;;\
+	*.tar.lz*) \
+	  lzip -dc $(distdir).tar.lz | $(am__untar) ;;\
 	*.tar.xz*) \
 	  xz -dc $(distdir).tar.xz | $(am__untar) ;;\
 	*.tar.Z*) \
@@ -1102,6 +1111,7 @@ distcheck: dist
 	  && am__cwd=`pwd` \
 	  && $(am__cd) $(distdir)/_build \
 	  && ../configure --srcdir=.. --prefix="$$dc_install_base" \
+	    $(AM_DISTCHECK_CONFIGURE_FLAGS) \
 	    $(DISTCHECK_CONFIGURE_FLAGS) \
 	  && $(MAKE) $(AM_MAKEFLAGS) \
 	  && $(MAKE) $(AM_MAKEFLAGS) dvi \
@@ -1130,8 +1140,16 @@ distcheck: dist
 	  list='$(DIST_ARCHIVES)'; for i in $$list; do echo $$i; done) | \
 	  sed -e 1h -e 1s/./=/g -e 1p -e 1x -e '$$p' -e '$$x'
 distuninstallcheck:
-	@$(am__cd) '$(distuninstallcheck_dir)' \
-	&& test `$(distuninstallcheck_listfiles) | wc -l` -le 1 \
+	@test -n '$(distuninstallcheck_dir)' || { \
+	  echo 'ERROR: trying to run $@ with an empty' \
+	       '$$(distuninstallcheck_dir)' >&2; \
+	  exit 1; \
+	}; \
+	$(am__cd) '$(distuninstallcheck_dir)' || { \
+	  echo 'ERROR: cannot chdir into $(distuninstallcheck_dir)' >&2; \
+	  exit 1; \
+	}; \
+	test `$(am__distuninstallcheck_listfiles) | wc -l` -eq 0 \
 	   || { echo "ERROR: files left after uninstall:" ; \
 	        if test -n "$(DESTDIR)"; then \
 	          echo "  (check DESTDIR support)"; \
@@ -1166,10 +1184,15 @@ install-am: all-am
 
 installcheck: installcheck-am
 install-strip:
-	$(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
-	  install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
-	  `test -z '$(STRIP)' || \
-	    echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+	if test -z '$(STRIP)'; then \
+	  $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+	    install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+	      install; \
+	else \
+	  $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+	    install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+	    "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'" install; \
+	fi
 mostlyclean-generic:
 
 clean-generic:
@@ -1274,8 +1297,8 @@ uninstall-am: uninstall-libLTLIBRARIES uninstall-m4dataDATA \
 .PHONY: CTAGS GTAGS all all-am am--refresh check check-TESTS check-am \
 	clean clean-checkPROGRAMS clean-generic clean-libLTLIBRARIES \
 	clean-libtool clean-noinstLTLIBRARIES ctags dist dist-all \
-	dist-bzip2 dist-gzip dist-lzma dist-shar dist-tarZ dist-xz \
-	dist-zip distcheck distclean distclean-compile \
+	dist-bzip2 dist-gzip dist-lzip dist-lzma dist-shar dist-tarZ \
+	dist-xz dist-zip distcheck distclean distclean-compile \
 	distclean-generic distclean-hdr distclean-libtool \
 	distclean-tags distcleancheck distdir distuninstallcheck dvi \
 	dvi-am html html-am info info-am install install-am \
diff --git a/resources/3rdparty/gtest-1.6.0/aclocal.m4 b/resources/3rdparty/gtest-1.6.0/aclocal.m4
index 58917dc7a..3ccdc5de7 100644
--- a/resources/3rdparty/gtest-1.6.0/aclocal.m4
+++ b/resources/3rdparty/gtest-1.6.0/aclocal.m4
@@ -1,7 +1,8 @@
-# generated automatically by aclocal 1.11.1 -*- Autoconf -*-
+# generated automatically by aclocal 1.11.3 -*- Autoconf -*-
 
 # Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004,
-# 2005, 2006, 2007, 2008, 2009  Free Software Foundation, Inc.
+# 2005, 2006, 2007, 2008, 2009, 2010, 2011 Free Software Foundation,
+# Inc.
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
@@ -13,18 +14,120 @@
 
 m4_ifndef([AC_AUTOCONF_VERSION],
   [m4_copy([m4_PACKAGE_VERSION], [AC_AUTOCONF_VERSION])])dnl
-m4_if(m4_defn([AC_AUTOCONF_VERSION]), [2.65],,
-[m4_warning([this file was generated for autoconf 2.65.
+m4_if(m4_defn([AC_AUTOCONF_VERSION]), [2.68],,
+[m4_warning([this file was generated for autoconf 2.68.
 You have another version of autoconf.  It may work, but is not guaranteed to.
 If you have problems, you may need to regenerate the build system entirely.
 To do so, use the procedure documented by the package, typically `autoreconf'.])])
 
-# Copyright (C) 2002, 2003, 2005, 2006, 2007, 2008  Free Software Foundation, Inc.
+# lt~obsolete.m4 -- aclocal satisfying obsolete definitions.    -*-Autoconf-*-
+#
+#   Copyright (C) 2004, 2005, 2007, 2009 Free Software Foundation, Inc.
+#   Written by Scott James Remnant, 2004.
+#
+# This file is free software; the Free Software Foundation gives
+# unlimited permission to copy and/or distribute it, with or without
+# modifications, as long as this notice is preserved.
+
+# serial 5 lt~obsolete.m4
+
+# These exist entirely to fool aclocal when bootstrapping libtool.
+#
+# In the past libtool.m4 has provided macros via AC_DEFUN (or AU_DEFUN)
+# which have later been changed to m4_define as they aren't part of the
+# exported API, or moved to Autoconf or Automake where they belong.
+#
+# The trouble is, aclocal is a bit thick.  It'll see the old AC_DEFUN
+# in /usr/share/aclocal/libtool.m4 and remember it, then when it sees us
+# using a macro with the same name in our local m4/libtool.m4 it'll
+# pull the old libtool.m4 in (it doesn't see our shiny new m4_define
+# and doesn't know about Autoconf macros at all.)
+#
+# So we provide this file, which has a silly filename so it's always
+# included after everything else.  This provides aclocal with the
+# AC_DEFUNs it wants, but when m4 processes it, it doesn't do anything
+# because those macros already exist, or will be overwritten later.
+# We use AC_DEFUN over AU_DEFUN for compatibility with aclocal-1.6. 
+#
+# Anytime we withdraw an AC_DEFUN or AU_DEFUN, remember to add it here.
+# Yes, that means every name once taken will need to remain here until
+# we give up compatibility with versions before 1.7, at which point
+# we need to keep only those names which we still refer to.
+
+# This is to help aclocal find these macros, as it can't see m4_define.
+AC_DEFUN([LTOBSOLETE_VERSION], [m4_if([1])])
+
+m4_ifndef([AC_LIBTOOL_LINKER_OPTION],	[AC_DEFUN([AC_LIBTOOL_LINKER_OPTION])])
+m4_ifndef([AC_PROG_EGREP],		[AC_DEFUN([AC_PROG_EGREP])])
+m4_ifndef([_LT_AC_PROG_ECHO_BACKSLASH],	[AC_DEFUN([_LT_AC_PROG_ECHO_BACKSLASH])])
+m4_ifndef([_LT_AC_SHELL_INIT],		[AC_DEFUN([_LT_AC_SHELL_INIT])])
+m4_ifndef([_LT_AC_SYS_LIBPATH_AIX],	[AC_DEFUN([_LT_AC_SYS_LIBPATH_AIX])])
+m4_ifndef([_LT_PROG_LTMAIN],		[AC_DEFUN([_LT_PROG_LTMAIN])])
+m4_ifndef([_LT_AC_TAGVAR],		[AC_DEFUN([_LT_AC_TAGVAR])])
+m4_ifndef([AC_LTDL_ENABLE_INSTALL],	[AC_DEFUN([AC_LTDL_ENABLE_INSTALL])])
+m4_ifndef([AC_LTDL_PREOPEN],		[AC_DEFUN([AC_LTDL_PREOPEN])])
+m4_ifndef([_LT_AC_SYS_COMPILER],	[AC_DEFUN([_LT_AC_SYS_COMPILER])])
+m4_ifndef([_LT_AC_LOCK],		[AC_DEFUN([_LT_AC_LOCK])])
+m4_ifndef([AC_LIBTOOL_SYS_OLD_ARCHIVE],	[AC_DEFUN([AC_LIBTOOL_SYS_OLD_ARCHIVE])])
+m4_ifndef([_LT_AC_TRY_DLOPEN_SELF],	[AC_DEFUN([_LT_AC_TRY_DLOPEN_SELF])])
+m4_ifndef([AC_LIBTOOL_PROG_CC_C_O],	[AC_DEFUN([AC_LIBTOOL_PROG_CC_C_O])])
+m4_ifndef([AC_LIBTOOL_SYS_HARD_LINK_LOCKS], [AC_DEFUN([AC_LIBTOOL_SYS_HARD_LINK_LOCKS])])
+m4_ifndef([AC_LIBTOOL_OBJDIR],		[AC_DEFUN([AC_LIBTOOL_OBJDIR])])
+m4_ifndef([AC_LTDL_OBJDIR],		[AC_DEFUN([AC_LTDL_OBJDIR])])
+m4_ifndef([AC_LIBTOOL_PROG_LD_HARDCODE_LIBPATH], [AC_DEFUN([AC_LIBTOOL_PROG_LD_HARDCODE_LIBPATH])])
+m4_ifndef([AC_LIBTOOL_SYS_LIB_STRIP],	[AC_DEFUN([AC_LIBTOOL_SYS_LIB_STRIP])])
+m4_ifndef([AC_PATH_MAGIC],		[AC_DEFUN([AC_PATH_MAGIC])])
+m4_ifndef([AC_PROG_LD_GNU],		[AC_DEFUN([AC_PROG_LD_GNU])])
+m4_ifndef([AC_PROG_LD_RELOAD_FLAG],	[AC_DEFUN([AC_PROG_LD_RELOAD_FLAG])])
+m4_ifndef([AC_DEPLIBS_CHECK_METHOD],	[AC_DEFUN([AC_DEPLIBS_CHECK_METHOD])])
+m4_ifndef([AC_LIBTOOL_PROG_COMPILER_NO_RTTI], [AC_DEFUN([AC_LIBTOOL_PROG_COMPILER_NO_RTTI])])
+m4_ifndef([AC_LIBTOOL_SYS_GLOBAL_SYMBOL_PIPE], [AC_DEFUN([AC_LIBTOOL_SYS_GLOBAL_SYMBOL_PIPE])])
+m4_ifndef([AC_LIBTOOL_PROG_COMPILER_PIC], [AC_DEFUN([AC_LIBTOOL_PROG_COMPILER_PIC])])
+m4_ifndef([AC_LIBTOOL_PROG_LD_SHLIBS],	[AC_DEFUN([AC_LIBTOOL_PROG_LD_SHLIBS])])
+m4_ifndef([AC_LIBTOOL_POSTDEP_PREDEP],	[AC_DEFUN([AC_LIBTOOL_POSTDEP_PREDEP])])
+m4_ifndef([LT_AC_PROG_EGREP],		[AC_DEFUN([LT_AC_PROG_EGREP])])
+m4_ifndef([LT_AC_PROG_SED],		[AC_DEFUN([LT_AC_PROG_SED])])
+m4_ifndef([_LT_CC_BASENAME],		[AC_DEFUN([_LT_CC_BASENAME])])
+m4_ifndef([_LT_COMPILER_BOILERPLATE],	[AC_DEFUN([_LT_COMPILER_BOILERPLATE])])
+m4_ifndef([_LT_LINKER_BOILERPLATE],	[AC_DEFUN([_LT_LINKER_BOILERPLATE])])
+m4_ifndef([_AC_PROG_LIBTOOL],		[AC_DEFUN([_AC_PROG_LIBTOOL])])
+m4_ifndef([AC_LIBTOOL_SETUP],		[AC_DEFUN([AC_LIBTOOL_SETUP])])
+m4_ifndef([_LT_AC_CHECK_DLFCN],		[AC_DEFUN([_LT_AC_CHECK_DLFCN])])
+m4_ifndef([AC_LIBTOOL_SYS_DYNAMIC_LINKER],	[AC_DEFUN([AC_LIBTOOL_SYS_DYNAMIC_LINKER])])
+m4_ifndef([_LT_AC_TAGCONFIG],		[AC_DEFUN([_LT_AC_TAGCONFIG])])
+m4_ifndef([AC_DISABLE_FAST_INSTALL],	[AC_DEFUN([AC_DISABLE_FAST_INSTALL])])
+m4_ifndef([_LT_AC_LANG_CXX],		[AC_DEFUN([_LT_AC_LANG_CXX])])
+m4_ifndef([_LT_AC_LANG_F77],		[AC_DEFUN([_LT_AC_LANG_F77])])
+m4_ifndef([_LT_AC_LANG_GCJ],		[AC_DEFUN([_LT_AC_LANG_GCJ])])
+m4_ifndef([AC_LIBTOOL_LANG_C_CONFIG],	[AC_DEFUN([AC_LIBTOOL_LANG_C_CONFIG])])
+m4_ifndef([_LT_AC_LANG_C_CONFIG],	[AC_DEFUN([_LT_AC_LANG_C_CONFIG])])
+m4_ifndef([AC_LIBTOOL_LANG_CXX_CONFIG],	[AC_DEFUN([AC_LIBTOOL_LANG_CXX_CONFIG])])
+m4_ifndef([_LT_AC_LANG_CXX_CONFIG],	[AC_DEFUN([_LT_AC_LANG_CXX_CONFIG])])
+m4_ifndef([AC_LIBTOOL_LANG_F77_CONFIG],	[AC_DEFUN([AC_LIBTOOL_LANG_F77_CONFIG])])
+m4_ifndef([_LT_AC_LANG_F77_CONFIG],	[AC_DEFUN([_LT_AC_LANG_F77_CONFIG])])
+m4_ifndef([AC_LIBTOOL_LANG_GCJ_CONFIG],	[AC_DEFUN([AC_LIBTOOL_LANG_GCJ_CONFIG])])
+m4_ifndef([_LT_AC_LANG_GCJ_CONFIG],	[AC_DEFUN([_LT_AC_LANG_GCJ_CONFIG])])
+m4_ifndef([AC_LIBTOOL_LANG_RC_CONFIG],	[AC_DEFUN([AC_LIBTOOL_LANG_RC_CONFIG])])
+m4_ifndef([_LT_AC_LANG_RC_CONFIG],	[AC_DEFUN([_LT_AC_LANG_RC_CONFIG])])
+m4_ifndef([AC_LIBTOOL_CONFIG],		[AC_DEFUN([AC_LIBTOOL_CONFIG])])
+m4_ifndef([_LT_AC_FILE_LTDLL_C],	[AC_DEFUN([_LT_AC_FILE_LTDLL_C])])
+m4_ifndef([_LT_REQUIRED_DARWIN_CHECKS],	[AC_DEFUN([_LT_REQUIRED_DARWIN_CHECKS])])
+m4_ifndef([_LT_AC_PROG_CXXCPP],		[AC_DEFUN([_LT_AC_PROG_CXXCPP])])
+m4_ifndef([_LT_PREPARE_SED_QUOTE_VARS],	[AC_DEFUN([_LT_PREPARE_SED_QUOTE_VARS])])
+m4_ifndef([_LT_PROG_ECHO_BACKSLASH],	[AC_DEFUN([_LT_PROG_ECHO_BACKSLASH])])
+m4_ifndef([_LT_PROG_F77],		[AC_DEFUN([_LT_PROG_F77])])
+m4_ifndef([_LT_PROG_FC],		[AC_DEFUN([_LT_PROG_FC])])
+m4_ifndef([_LT_PROG_CXX],		[AC_DEFUN([_LT_PROG_CXX])])
+
+# Copyright (C) 2002, 2003, 2005, 2006, 2007, 2008, 2011 Free Software
+# Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 1
+
 # AM_AUTOMAKE_VERSION(VERSION)
 # ----------------------------
 # Automake X.Y traces this macro to ensure aclocal.m4 has been
@@ -34,7 +137,7 @@ AC_DEFUN([AM_AUTOMAKE_VERSION],
 [am__api_version='1.11'
 dnl Some users find AM_AUTOMAKE_VERSION and mistake it for a way to
 dnl require some minimum version.  Point them to the right macro.
-m4_if([$1], [1.11.1], [],
+m4_if([$1], [1.11.3], [],
       [AC_FATAL([Do not call $0, use AM_INIT_AUTOMAKE([$1]).])])dnl
 ])
 
@@ -50,19 +153,21 @@ m4_define([_AM_AUTOCONF_VERSION], [])
 # Call AM_AUTOMAKE_VERSION and AM_AUTOMAKE_VERSION so they can be traced.
 # This function is AC_REQUIREd by AM_INIT_AUTOMAKE.
 AC_DEFUN([AM_SET_CURRENT_AUTOMAKE_VERSION],
-[AM_AUTOMAKE_VERSION([1.11.1])dnl
+[AM_AUTOMAKE_VERSION([1.11.3])dnl
 m4_ifndef([AC_AUTOCONF_VERSION],
   [m4_copy([m4_PACKAGE_VERSION], [AC_AUTOCONF_VERSION])])dnl
 _AM_AUTOCONF_VERSION(m4_defn([AC_AUTOCONF_VERSION]))])
 
 # AM_AUX_DIR_EXPAND                                         -*- Autoconf -*-
 
-# Copyright (C) 2001, 2003, 2005  Free Software Foundation, Inc.
+# Copyright (C) 2001, 2003, 2005, 2011 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 1
+
 # For projects using AC_CONFIG_AUX_DIR([foo]), Autoconf sets
 # $ac_aux_dir to `$srcdir/foo'.  In other projects, it is set to
 # `$srcdir', `$srcdir/..', or `$srcdir/../..'.
@@ -144,14 +249,14 @@ AC_CONFIG_COMMANDS_PRE(
 Usually this means the macro was only invoked conditionally.]])
 fi])])
 
-# Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2009
-# Free Software Foundation, Inc.
+# Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2009,
+# 2010, 2011 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
-# serial 10
+# serial 12
 
 # There are a few dirty hacks below to avoid letting `AC_PROG_CC' be
 # written in clear, in which case automake, when reading aclocal.m4,
@@ -191,6 +296,7 @@ AC_CACHE_CHECK([dependency style of $depcc],
   # instance it was reported that on HP-UX the gcc test will end up
   # making a dummy file named `D' -- because `-MD' means `put the output
   # in D'.
+  rm -rf conftest.dir
   mkdir conftest.dir
   # Copy depcomp to subdir because otherwise we won't find it if we're
   # using a relative directory.
@@ -255,7 +361,7 @@ AC_CACHE_CHECK([dependency style of $depcc],
 	break
       fi
       ;;
-    msvisualcpp | msvcmsys)
+    msvc7 | msvc7msys | msvisualcpp | msvcmsys)
       # This compiler won't grok `-c -o', but also, the minuso test has
       # not run yet.  These depmodes are late enough in the game, and
       # so weak that their functioning should not be impacted.
@@ -320,10 +426,13 @@ AC_DEFUN([AM_DEP_TRACK],
 if test "x$enable_dependency_tracking" != xno; then
   am_depcomp="$ac_aux_dir/depcomp"
   AMDEPBACKSLASH='\'
+  am__nodep='_no'
 fi
 AM_CONDITIONAL([AMDEP], [test "x$enable_dependency_tracking" != xno])
 AC_SUBST([AMDEPBACKSLASH])dnl
 _AM_SUBST_NOTMAKE([AMDEPBACKSLASH])dnl
+AC_SUBST([am__nodep])dnl
+_AM_SUBST_NOTMAKE([am__nodep])dnl
 ])
 
 # Generate code to set up dependency tracking.              -*- Autoconf -*-
@@ -545,12 +654,15 @@ for _am_header in $config_headers :; do
 done
 echo "timestamp for $_am_arg" >`AS_DIRNAME(["$_am_arg"])`/stamp-h[]$_am_stamp_count])
 
-# Copyright (C) 2001, 2003, 2005, 2008  Free Software Foundation, Inc.
+# Copyright (C) 2001, 2003, 2005, 2008, 2011 Free Software Foundation,
+# Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 1
+
 # AM_PROG_INSTALL_SH
 # ------------------
 # Define $install_sh.
@@ -682,12 +794,15 @@ else
 fi
 ])
 
-# Copyright (C) 2003, 2004, 2005, 2006  Free Software Foundation, Inc.
+# Copyright (C) 2003, 2004, 2005, 2006, 2011 Free Software Foundation,
+# Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 1
+
 # AM_PROG_MKDIR_P
 # ---------------
 # Check for `mkdir -p'.
@@ -710,13 +825,14 @@ esac
 
 # Helper functions for option handling.                     -*- Autoconf -*-
 
-# Copyright (C) 2001, 2002, 2003, 2005, 2008  Free Software Foundation, Inc.
+# Copyright (C) 2001, 2002, 2003, 2005, 2008, 2010 Free Software
+# Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
-# serial 4
+# serial 5
 
 # _AM_MANGLE_OPTION(NAME)
 # -----------------------
@@ -724,13 +840,13 @@ AC_DEFUN([_AM_MANGLE_OPTION],
 [[_AM_OPTION_]m4_bpatsubst($1, [[^a-zA-Z0-9_]], [_])])
 
 # _AM_SET_OPTION(NAME)
-# ------------------------------
+# --------------------
 # Set option NAME.  Presently that only means defining a flag for this option.
 AC_DEFUN([_AM_SET_OPTION],
 [m4_define(_AM_MANGLE_OPTION([$1]), 1)])
 
 # _AM_SET_OPTIONS(OPTIONS)
-# ----------------------------------
+# ------------------------
 # OPTIONS is a space-separated list of Automake options.
 AC_DEFUN([_AM_SET_OPTIONS],
 [m4_foreach_w([_AM_Option], [$1], [_AM_SET_OPTION(_AM_Option)])])
@@ -741,13 +857,15 @@ AC_DEFUN([_AM_SET_OPTIONS],
 AC_DEFUN([_AM_IF_OPTION],
 [m4_ifset(_AM_MANGLE_OPTION([$1]), [$2], [$3])])
 
-# Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2008, 2009
-# Free Software Foundation, Inc.
+# Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2008, 2009,
+# 2011 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 2
+
 # AM_PATH_PYTHON([MINIMUM-VERSION], [ACTION-IF-FOUND], [ACTION-IF-NOT-FOUND])
 # ---------------------------------------------------------------------------
 # Adds support for distributing Python modules and packages.  To
@@ -775,8 +893,10 @@ AC_DEFUN([AM_PATH_PYTHON],
   dnl Find a Python interpreter.  Python versions prior to 2.0 are not
   dnl supported. (2.0 was released on October 16, 2000).
   m4_define_default([_AM_PYTHON_INTERPRETER_LIST],
-                    [python python2 python3 python3.0 python2.5 python2.4 python2.3 python2.2 dnl
-python2.1 python2.0])
+[python python2 python3 python3.2 python3.1 python3.0 python2.7 dnl
+ python2.6 python2.5 python2.4 python2.3 python2.2 python2.1 python2.0])
+
+  AC_ARG_VAR([PYTHON], [the Python interpreter])
 
   m4_if([$1],[],[
     dnl No version check is needed.
@@ -848,9 +968,7 @@ python2.1 python2.0])
   dnl   site-packages directory, not the python standard library
   dnl   directory like in previous automake betas.  This behavior
   dnl   is more consistent with lispdir.m4 for example.
-  dnl Query distutils for this directory.  distutils does not exist in
-  dnl Python 1.5, so we fall back to the hardcoded directory if it
-  dnl doesn't work.
+  dnl Query distutils for this directory.
   AC_CACHE_CHECK([for $am_display_PYTHON script directory],
     [am_cv_python_pythondir],
     [if test "x$prefix" = xNONE
@@ -859,8 +977,7 @@ python2.1 python2.0])
      else
        am_py_prefix=$prefix
      fi
-     am_cv_python_pythondir=`$PYTHON -c "import sys; from distutils import sysconfig; sys.stdout.write(sysconfig.get_python_lib(0,0,prefix='$am_py_prefix'))" 2>/dev/null ||
-     echo "$PYTHON_PREFIX/lib/python$PYTHON_VERSION/site-packages"`
+     am_cv_python_pythondir=`$PYTHON -c "import sys; from distutils import sysconfig; sys.stdout.write(sysconfig.get_python_lib(0,0,prefix='$am_py_prefix'))" 2>/dev/null`
      case $am_cv_python_pythondir in
      $am_py_prefix*)
        am__strip_prefix=`echo "$am_py_prefix" | sed 's|.|.|g'`
@@ -886,9 +1003,7 @@ python2.1 python2.0])
 
   dnl pyexecdir -- directory for installing python extension modules
   dnl   (shared libraries)
-  dnl Query distutils for this directory.  distutils does not exist in
-  dnl Python 1.5, so we fall back to the hardcoded directory if it
-  dnl doesn't work.
+  dnl Query distutils for this directory.
   AC_CACHE_CHECK([for $am_display_PYTHON extension module directory],
     [am_cv_python_pyexecdir],
     [if test "x$exec_prefix" = xNONE
@@ -897,8 +1012,7 @@ python2.1 python2.0])
      else
        am_py_exec_prefix=$exec_prefix
      fi
-     am_cv_python_pyexecdir=`$PYTHON -c "import sys; from distutils import sysconfig; sys.stdout.write(sysconfig.get_python_lib(1,0,prefix='$am_py_exec_prefix'))" 2>/dev/null ||
-     echo "$PYTHON_EXEC_PREFIX/lib/python$PYTHON_VERSION/site-packages"`
+     am_cv_python_pyexecdir=`$PYTHON -c "import sys; from distutils import sysconfig; sys.stdout.write(sysconfig.get_python_lib(1,0,prefix='$am_py_exec_prefix'))" 2>/dev/null`
      case $am_cv_python_pyexecdir in
      $am_py_exec_prefix*)
        am__strip_prefix=`echo "$am_py_exec_prefix" | sed 's|.|.|g'`
@@ -946,12 +1060,14 @@ for i in list(range(0, 4)): minverhex = (minverhex << 8) + minver[[i]]
 sys.exit(sys.hexversion < minverhex)"
   AS_IF([AM_RUN_LOG([$1 -c "$prog"])], [$3], [$4])])
 
-# Copyright (C) 2001, 2003, 2005  Free Software Foundation, Inc.
+# Copyright (C) 2001, 2003, 2005, 2011 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 1
+
 # AM_RUN_LOG(COMMAND)
 # -------------------
 # Run COMMAND, save the exit status in ac_status, and log it.
@@ -1028,12 +1144,14 @@ Check your system clock])
 fi
 AC_MSG_RESULT(yes)])
 
-# Copyright (C) 2001, 2003, 2005  Free Software Foundation, Inc.
+# Copyright (C) 2001, 2003, 2005, 2011 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
+# serial 1
+
 # AM_PROG_INSTALL_STRIP
 # ---------------------
 # One issue with vendor `install' (even GNU) is that you can't
@@ -1056,13 +1174,13 @@ fi
 INSTALL_STRIP_PROGRAM="\$(install_sh) -c -s"
 AC_SUBST([INSTALL_STRIP_PROGRAM])])
 
-# Copyright (C) 2006, 2008  Free Software Foundation, Inc.
+# Copyright (C) 2006, 2008, 2010 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
 # with or without modifications, as long as this notice is preserved.
 
-# serial 2
+# serial 3
 
 # _AM_SUBST_NOTMAKE(VARIABLE)
 # ---------------------------
@@ -1071,13 +1189,13 @@ AC_SUBST([INSTALL_STRIP_PROGRAM])])
 AC_DEFUN([_AM_SUBST_NOTMAKE])
 
 # AM_SUBST_NOTMAKE(VARIABLE)
-# ---------------------------
+# --------------------------
 # Public sister of _AM_SUBST_NOTMAKE.
 AC_DEFUN([AM_SUBST_NOTMAKE], [_AM_SUBST_NOTMAKE($@)])
 
 # Check how to create a tarball.                            -*- Autoconf -*-
 
-# Copyright (C) 2004, 2005  Free Software Foundation, Inc.
+# Copyright (C) 2004, 2005, 2012 Free Software Foundation, Inc.
 #
 # This file is free software; the Free Software Foundation
 # gives unlimited permission to copy and/or distribute it,
@@ -1099,10 +1217,11 @@ AC_DEFUN([AM_SUBST_NOTMAKE], [_AM_SUBST_NOTMAKE($@)])
 # a tarball read from stdin.
 #     $(am__untar) < result.tar
 AC_DEFUN([_AM_PROG_TAR],
-[# Always define AMTAR for backward compatibility.
-AM_MISSING_PROG([AMTAR], [tar])
+[# Always define AMTAR for backward compatibility.  Yes, it's still used
+# in the wild :-(  We should find a proper way to deprecate it ...
+AC_SUBST([AMTAR], ['$${TAR-tar}'])
 m4_if([$1], [v7],
-     [am__tar='${AMTAR} chof - "$$tardir"'; am__untar='${AMTAR} xf -'],
+     [am__tar='$${TAR-tar} chof - "$$tardir"' am__untar='$${TAR-tar} xf -'],
      [m4_case([$1], [ustar],, [pax],,
               [m4_fatal([Unknown tar format])])
 AC_MSG_CHECKING([how to create a $1 tar archive])
diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp
index 2aac6ad7f..1e494d40d 100644
--- a/src/parser/read_tra_file.cpp
+++ b/src/parser/read_tra_file.cpp
@@ -5,8 +5,8 @@
  *
  * Reuses code from the file "read_tra_file.c" from the old MRMC project.
  *
- *  Created on: 15.08.2012
- *      Author: Thomas Heinemann
+ * Created on: 20.11.2012
+ *      Author: Gereon Kremer
  */
 
 #include "parser.h"
@@ -35,12 +35,11 @@ namespace parser{
 
 char* skipWS(char* buf)
 {
-   unsigned int i = 0;
-   while (1)
-   {
-      if ((buf[i] != ' ') && (buf[i] != '\t') && (buf[i] != '\n') && (buf[i] != '\r')) return buf+i;
-      i++;
-   }
+	while(1)
+	{
+		if ((buf[0] != ' ') && (buf[0] != '\t') && (buf[0] != '\n') && (buf[0] != '\r')) return buf;
+		buf++;
+	}
 }
 
 // Disable C4996 - This function or variable may be unsafe.
@@ -54,13 +53,15 @@ char* skipWS(char* buf)
 * (Diagonal elements are treated in a special way).
 *
 * @return The number of non-zero elements that are not on the diagonal
-* @param p File stream to scan. Is expected to be opened, a NULL pointer will
-*          be rejected!
+* @param buf Data to scan. Is expected to be some char array.
 */
 static uint_fast32_t make_first_pass(char* buf)
 {
 	uint_fast32_t non_zero = 0;
-   
+	
+	/*
+		check file header and extract number of transitions
+	*/
 	if (strncmp(buf, "STATES ", 7) != 0) return 0;
 	buf += 7; // skip "STATES "
 	if (strtol(buf, &buf, 10) == 0) return 0;
@@ -69,6 +70,9 @@ static uint_fast32_t make_first_pass(char* buf)
 	buf += 12; // skip "TRANSITIONS "
 	if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
 	
+	/*
+		check all transitions for non-zero diagonal entrys
+	*/
 	unsigned int row, col;
 	double val;
 	while (1)  
@@ -116,7 +120,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 		perform first pass
 	*/
 	uint_fast32_t non_zero = make_first_pass(data);
-	if (non_zero = 0)
+	if (non_zero == 0)
 	{
 		close(f);
 		munmap(data, st.st_size);
@@ -127,14 +131,18 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	/*
 		perform second pass
 		
-		from here on, we already know that the file format is correct
+		from here on, we already know that the file header is correct
 	*/
 	char* buf = data;
 	uint_fast32_t rows;
 	sparse::StaticSparseMatrix<double> *sp = NULL;
 
+	/*
+		read file header, extract number of states
+	*/
 	buf += 7; // skip "STATES "
 	rows = strtol(buf, &buf, 10);
+	buf = skipWS(buf);
 	buf += 12; // skip "TRANSITIONS "
 	strtol(buf, &buf, 10);
 	
@@ -147,7 +155,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	 * non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
 	sp = new sparse::StaticSparseMatrix<double>(rows);
-	if ( NULL == sp )
+	if (sp == NULL)
 	{
 		close(f);
 		munmap(data, st.st_size);
@@ -156,12 +164,10 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	}
 	sp->initialize(non_zero);
 
-	uint_fast32_t row, col;
+	uint_fast64_t row, col;
 	double val;
 	/*
 		read all transitions from file
-		
-		note: the parser will also stop, if a transition with a value of 0.0 occurs
 	*/
 	while (1)
 	{
@@ -169,7 +175,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 		col = strtol(buf, &buf, 10);
 		val = strtod(buf, &buf);
 		if (val == 0.0) break;
-		pantheios::log_WARNING("Write value ",
+		pantheios::log_DEBUG("Write value ",
 							pantheios::real(val),
 							" to position ",
 							pantheios::integer(row), " x ",
@@ -177,6 +183,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 		sp->addNextValue(row,col,val);	
 	}
 	
+	// clean up
 	close(f);
 	munmap(data, st.st_size);
 

From e35b950eea7ffa65deffc34c52a24b7f70ee7d6b Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 00:04:58 +0100
Subject: [PATCH 03/17] fixing locale issue

---
 src/parser/read_tra_file.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp
index 1e494d40d..842f1a697 100644
--- a/src/parser/read_tra_file.cpp
+++ b/src/parser/read_tra_file.cpp
@@ -18,12 +18,14 @@
 #include <cstdlib>
 #include <cstdio>
 #include <cstring>
+#include <clocale>
 #include <iostream>
 #include <errno.h>
 #include <time.h>
 #include <sys/stat.h>
 #include <sys/mman.h>
 #include <fcntl.h>
+#include <locale.h>
 
 #include <pantheios/pantheios.hpp>
 #include <pantheios/inserters/integer.hpp>
@@ -97,6 +99,10 @@ static uint_fast32_t make_first_pass(char* buf)
  */
 
 sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
+	if (setlocale( LC_NUMERIC, "de_DE" ) == 0)
+	{
+		fprintf(stderr, "could not set locale\n");
+	}
 	/*
 		open file and map to memory
 	*/

From 2cf8f3baec88ba30d84baca331bcdd685c399488 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 20:32:15 +0100
Subject: [PATCH 04/17] more work on refactoring / rewriting parsers

---
 src/parser/readLabFile.cpp                    | 123 ++++++++++++
 src/parser/readLabFile.h                      |  19 ++
 .../{read_tra_file.cpp => readTraFile.cpp}    | 107 ++++++-----
 src/parser/readTraFile.h                      |  19 ++
 src/parser/read_lab_file.cpp                  | 181 ------------------
 src/parser/read_lab_file.h                    |  24 ---
 src/parser/read_tra_file.h                    |  20 --
 7 files changed, 220 insertions(+), 273 deletions(-)
 create mode 100644 src/parser/readLabFile.cpp
 create mode 100644 src/parser/readLabFile.h
 rename src/parser/{read_tra_file.cpp => readTraFile.cpp} (70%)
 create mode 100644 src/parser/readTraFile.h
 delete mode 100644 src/parser/read_lab_file.cpp
 delete mode 100644 src/parser/read_lab_file.h
 delete mode 100644 src/parser/read_tra_file.h

diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
new file mode 100644
index 000000000..c09fd2db5
--- /dev/null
+++ b/src/parser/readLabFile.cpp
@@ -0,0 +1,123 @@
+/*
+ * readLabFile.cpp
+ *
+ *  Created on: 21.11.2012
+ *      Author: Gereon Kremer
+ */
+
+#include "parser.h"
+
+#include "readLabFile.h"
+
+#include "src/exceptions/wrong_file_format.h"
+#include "src/exceptions/file_IO_exception.h"
+
+#include <cstdlib>
+#include <cstdio>
+#include <cstring>
+#include <clocale>
+#include <iostream>
+#include <errno.h>
+#include <time.h>
+#include <sys/stat.h>
+#include <sys/mman.h>
+#include <fcntl.h>
+#include <locale.h>
+
+#include <pantheios/pantheios.hpp>
+#include <pantheios/inserters/integer.hpp>
+
+namespace mrmc {
+
+namespace parser {
+
+
+/*!
+ * Reads a .lab file and puts the result in a labeling structure.
+ *
+ * Labelings created with this method have to be freed with the delete operator.
+ * @param node_count the number of states.
+ * @param filename   input .lab file's name.
+ * @return The pointer to the created labeling object.
+ */
+mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename)
+{
+	/*!
+	 *	open file and map to memory
+	 */
+	struct stat st;
+	int f = open(filename, O_RDONLY);
+	if ((f < 0) || (stat(filename, &st) != 0)) {
+		/*!
+		 * 
+		 */
+		pantheios::log_ERROR("File could not be opened.");
+		throw mrmc::exceptions::file_IO_exception();
+		return NULL;
+	}
+	
+	char* data = (char*) mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE, f, 0);
+	if (data == (char*)-1)
+	{
+		pantheios::log_ERROR("File could not be mapped. Something went wrong with mmap.");
+		close(f);
+		throw mrmc::exceptions::file_IO_exception();
+		return NULL;
+	}
+
+	char* buf = data;
+	char sep[] = " \n\t";
+	uint_fast32_t proposition_count = 0;
+	size_t cnt = 0;
+
+	do {
+		buf += cnt;
+		cnt = strcspn(buf, sep);
+		if (cnt > 0) {
+			if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
+			if (strncmp(buf, "#END", cnt) == 0) break;
+			proposition_count++;
+		}
+		else cnt = 1;
+	} while (cnt > 0);
+	
+	mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
+	char proposition[128];
+	buf = data;
+	cnt = 0;
+	do {
+		buf += cnt;
+		cnt = strcspn(buf, sep);
+		if (cnt > 0) {
+			if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
+			if (strncmp(buf, "#END", cnt) == 0) break;
+			strncpy(proposition, buf, cnt);
+			proposition[cnt] = '\0';
+			result->addAtomicProposition(proposition);
+		}
+		else cnt = 1;
+	} while (cnt > 0);
+	buf += 4;
+	
+	uint_fast32_t node;
+	while (1) {
+		node = strtol(buf, &buf, 10);
+		while (*buf != '\0') {
+			cnt = strcspn(buf, sep);
+			if (cnt == 0) buf++;
+			else break;
+		}
+		strncpy(proposition, buf, cnt);
+		proposition[cnt] = '\0';
+		result->addAtomicPropositionToState(proposition, node);
+		buf += cnt;
+	}
+	
+	munmap(data, st.st_size);
+	close(f);	
+	return result;
+}
+
+} //namespace parser
+
+} //namespace mrmc
diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h
new file mode 100644
index 000000000..4019864e0
--- /dev/null
+++ b/src/parser/readLabFile.h
@@ -0,0 +1,19 @@
+/*
+ * read_lab_file.h
+ *
+ */
+
+#pragma once
+
+#include "src/models/atomic_propositions_labeling.h"
+
+
+namespace mrmc {
+
+namespace parser {
+
+mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename);
+
+}
+
+}
diff --git a/src/parser/read_tra_file.cpp b/src/parser/readTraFile.cpp
similarity index 70%
rename from src/parser/read_tra_file.cpp
rename to src/parser/readTraFile.cpp
index 842f1a697..af5350693 100644
--- a/src/parser/read_tra_file.cpp
+++ b/src/parser/readTraFile.cpp
@@ -3,15 +3,13 @@
  * system of a Markov chain (DTMC) and saving it into a corresponding
  * matrix.
  *
- * Reuses code from the file "read_tra_file.c" from the old MRMC project.
- *
  * Created on: 20.11.2012
  *      Author: Gereon Kremer
  */
 
 #include "parser.h"
 
-#include "src/parser/read_tra_file.h"
+#include "src/parser/readTraFile.h"
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
 #include "boost/integer/integer_mask.hpp"
@@ -44,26 +42,23 @@ char* skipWS(char* buf)
 	}
 }
 
-// Disable C4996 - This function or variable may be unsafe.
-#pragma warning(disable:4996)
-
 /*!
-* This method does the first pass through the .tra file and computes
-* the number of non-zero elements that are not diagonal elements,
-* which correspondents to the number of transitions that are not
-* self-loops.
-* (Diagonal elements are treated in a special way).
-*
-* @return The number of non-zero elements that are not on the diagonal
-* @param buf Data to scan. Is expected to be some char array.
-*/
-static uint_fast32_t make_first_pass(char* buf)
+ * This method does the first pass through the .tra file and computes
+ * the number of non-zero elements that are not diagonal elements,
+ * which correspondents to the number of transitions that are not
+ * self-loops.
+ * (Diagonal elements are treated in a special way).
+ *
+ * @return The number of non-zero elements that are not on the diagonal
+ * @param buf Data to scan. Is expected to be some char array.
+ */
+static uint_fast32_t makeFirstPass(char* buf)
 {
 	uint_fast32_t non_zero = 0;
 	
-	/*
-		check file header and extract number of transitions
-	*/
+	/*!
+	 *	check file header and extract number of transitions
+	 */
 	if (strncmp(buf, "STATES ", 7) != 0) return 0;
 	buf += 7; // skip "STATES "
 	if (strtol(buf, &buf, 10) == 0) return 0;
@@ -72,9 +67,9 @@ static uint_fast32_t make_first_pass(char* buf)
 	buf += 12; // skip "TRANSITIONS "
 	if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
 	
-	/*
-		check all transitions for non-zero diagonal entrys
-	*/
+	/*!
+	 *	check all transitions for non-zero diagonal entrys
+	 */
 	unsigned int row, col;
 	double val;
 	while (1)  
@@ -98,17 +93,21 @@ static uint_fast32_t make_first_pass(char* buf)
  * @return a pointer to the created sparse matrix.
  */
 
-sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
-	if (setlocale( LC_NUMERIC, "de_DE" ) == 0)
-	{
-		fprintf(stderr, "could not set locale\n");
-	}
-	/*
-		open file and map to memory
+sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
+	/*!
+	*	enforce locale where decimal point is '.'
 	*/
+	setlocale( LC_NUMERIC, "C" );
+	
+	/*!
+	 *	open file and map to memory
+	 */
 	struct stat st;
 	int f = open(filename, O_RDONLY);
 	if((f < 0) || (stat(filename, &st) != 0)) {
+		/*!
+		 *	stat() or open() failed
+		 */
 		pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
 		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
 		return NULL;
@@ -116,36 +115,42 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	char *data = (char*)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, f, 0);
 	if (data == (char*)-1)
 	{
+		/*!
+		 *	mmap() failed
+		 */
 		pantheios::log_ERROR("Could not map the file to memory. Something went wrong with mmap.");
 		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error mapping file to memory");
 		close(f);
 		return NULL;
 	}
 	
-	/*
-		perform first pass
-	*/
-	uint_fast32_t non_zero = make_first_pass(data);
+	/*!
+	 *	perform first pass, i.e. count entries that are not zero and not on the diagonal
+	 */
+	uint_fast32_t non_zero = makeFirstPass(data);
 	if (non_zero == 0)
 	{
+		/*!
+		 *	first pass returned zero, this means the file format was wrong
+		 */
 		close(f);
 		munmap(data, st.st_size);
 		throw mrmc::exceptions::wrong_file_format();
 		return NULL;
 	}
 	
-	/*
-		perform second pass
-		
-		from here on, we already know that the file header is correct
-	*/
+	/*!
+	 *	perform second pass
+	 *	
+	 *	from here on, we already know that the file header is correct
+	 */
 	char* buf = data;
 	uint_fast32_t rows;
 	sparse::StaticSparseMatrix<double> *sp = NULL;
 
-	/*
-		read file header, extract number of states
-	*/
+	/*!
+	 *	read file header, extract number of states
+	 */
 	buf += 7; // skip "STATES "
 	rows = strtol(buf, &buf, 10);
 	buf = skipWS(buf);
@@ -156,13 +161,17 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
                         pantheios::integer(rows), " rows and ",
                         pantheios::integer(non_zero), " Non-Zero-Elements");
                         
-	/* Creating matrix
-	 * Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
-	 * non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
+	/*!	
+	 *	Creating matrix
+	 *	Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
+	 *	non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
 	sp = new sparse::StaticSparseMatrix<double>(rows);
 	if (sp == NULL)
 	{
+		/*!
+		 *	creating the matrix failed
+		 */
 		close(f);
 		munmap(data, st.st_size);
 		throw std::bad_alloc();
@@ -172,9 +181,9 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 
 	uint_fast64_t row, col;
 	double val;
-	/*
-		read all transitions from file
-	*/
+	/*!
+	 *	read all transitions from file
+	 */
 	while (1)
 	{
 		row = strtol(buf, &buf, 10);
@@ -189,7 +198,9 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 		sp->addNextValue(row,col,val);	
 	}
 	
-	// clean up
+	/*!
+	 * clean up
+	 */	
 	close(f);
 	munmap(data, st.st_size);
 
diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h
new file mode 100644
index 000000000..c4b025a64
--- /dev/null
+++ b/src/parser/readTraFile.h
@@ -0,0 +1,19 @@
+/*
+ * read_tra_file.h
+ *
+ *  Created on: 15.08.2012
+ *      Author: Thomas Heinemann
+ */
+
+#pragma once
+
+#include "src/sparse/static_sparse_matrix.h"
+
+namespace mrmc {
+	namespace parser {
+	
+		mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
+		
+	}
+}
+
diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp
deleted file mode 100644
index 2a3742afe..000000000
--- a/src/parser/read_lab_file.cpp
+++ /dev/null
@@ -1,181 +0,0 @@
-/*
- * read_lab_file.cpp
- *
- *  Created on: 10.09.2012
- *      Author: Thomas Heinemann
- */
-
-#include "parser.h"
-
-#include "read_lab_file.h"
-
-#include "src/exceptions/wrong_file_format.h"
-#include "src/exceptions/file_IO_exception.h"
-
-#include <cstring>
-#include <cstdlib>
-#include <cstdio>
-
-#include <pantheios/pantheios.hpp>
-#include <pantheios/inserters/integer.hpp>
-
-#ifdef WIN32
-#	define STRTOK_FUNC strtok_s
-#else
-#	define STRTOK_FUNC strtok_r
-#endif
-
-// Disable C4996 - This function or variable may be unsafe.
-#pragma warning(disable:4996)
-
-
-namespace mrmc {
-
-namespace parser {
-
-
-/*!
- * Reads a .lab file and puts the result in a labeling structure.
- *
- * Labelings created with this method have to be freed with the delete operator.
- * @param node_count the number of states.
- * @param filename   input .lab file's name.
- * @return The pointer to the created labeling object.
- */
-mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const char * filename)
-{
-   /* Note that this function uses strtok_r on char-array s.
-    * This function will modify this string.
-    * However, as only the result of its tokenization is used, this is not a problem.
-    *
-    * Thread-safety is ensured by using strtok_r instead of strtok.
-    */
-   FILE *P;
-
-   //TODO (Thomas Heinemann): handle files with lines that are longer than BUFFER_SIZE
-   //TODO (Thomas Heinemann): Throw errors if fgets return NULL in the declaration. (fixed by Philipp. Or?)
-
-   char s[BUFFER_SIZE];              //String buffer
-   char *saveptr = NULL;             //Buffer for strtok_r
-   char sep[] = " \n\t";             //Separators for the tokens
-
-   P = fopen(filename, "r");
-
-   if (P == NULL) {
-      pantheios::log_ERROR("File could not be opened.");
-      throw mrmc::exceptions::file_IO_exception();
-	  return NULL;
-   }
-
-   if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#DECLARATION\n")) {
-		fclose(P);
-		pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing).");
-		throw mrmc::exceptions::wrong_file_format();
-		return NULL;
-   }
-
-
-
-   uint_fast32_t buffer_size_count = 1;
-   uint_fast32_t buffer_start = 0;
-   char* decl_buffer = new char[buffer_size_count*BUFFER_SIZE];
-   bool need_next_iteration = true;
-
-   do {
-      decl_buffer[buffer_size_count*BUFFER_SIZE - 1] = '\xff';
-      if (fgets(decl_buffer + buffer_start, buffer_size_count*BUFFER_SIZE - buffer_start, P)) {
-         if ((decl_buffer[buffer_size_count*BUFFER_SIZE - 1] != '\xff') &&
-             (decl_buffer[buffer_size_count*BUFFER_SIZE - 2] != '\n')) {
-            //fgets changed the last bit -> read string has maximum length
-            //AND line is longer than size of decl_buffer
-            char* temp_buffer = decl_buffer;
-            decl_buffer = NULL;
-
-            buffer_size_count++;
-            decl_buffer = new char[buffer_size_count*BUFFER_SIZE];
-
-            buffer_start = (buffer_size_count - 1) * BUFFER_SIZE;
-
-            memcpy(decl_buffer, temp_buffer, buffer_start - 1);
-            delete[] temp_buffer;
-         } else {
-            need_next_iteration = false;
-         }
-      } else {
-         pantheios::log_ERROR("EOF in the declaration section");
-         throw mrmc::exceptions::wrong_file_format();
-		 delete[] decl_buffer;
-		 return NULL;
-      }
-   } while (need_next_iteration);
-
-   uint_fast32_t proposition_count = 0;
-   char * proposition;
-   int pos = 0;
-
-   if (decl_buffer[pos] != ' ' && decl_buffer[pos] != '\t' && decl_buffer[pos] != '\0') {
-      proposition_count++;
-   }
-
-   while (decl_buffer[pos] != '\0') {
-      if ((decl_buffer[pos] == ' ' || decl_buffer[pos] == '\t') &&
-          (decl_buffer[pos + 1] != ' ' && decl_buffer[pos + 1] != '\t' && decl_buffer[pos + 1] != '\0')) {
-         proposition_count++;
-      }
-      pos++;
-   }
-
-   mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
-
-   //Here, all propositions are to be declared...
-   for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr);
-        proposition != NULL;
-        proposition = STRTOK_FUNC(NULL, sep, &saveptr)) {
-      result -> addAtomicProposition(proposition);
-   }
-
-   // Free decl_buffer
-   delete[] decl_buffer;
-
-
-   saveptr = NULL;                        //resetting save pointer for strtok_r
-
-   if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#END\n")) {
-		fclose(P);
-		delete result;
-		pantheios::log_ERROR("Wrong declaration section (\"#END\" missing).");
-		throw mrmc::exceptions::wrong_file_format();
-		return NULL;
-   }
-
-   while (fgets(s, BUFFER_SIZE, P)) {
-      char * token = NULL;
-      uint_fast32_t node = 0;
-      /* First token has to be a number identifying the node,
-       * hence it is treated differently from the other tokens.
-       */
-      token = STRTOK_FUNC(s, sep, &saveptr);
-      if (sscanf(token, "%u", &node) == 0) {
-         fclose(P);
-         delete result;
-         pantheios::log_ERROR("Line assigning propositions does not start with a node number.");
-         throw mrmc::exceptions::wrong_file_format();
-		 return NULL;
-      }
-      do {
-         token = STRTOK_FUNC(NULL, sep, &saveptr);
-         if (token == NULL) {
-            break;
-         }
-         result->addAtomicPropositionToState(token, node);
-      } while (token != NULL);
-
-   }
-
-   fclose(P);
-   return result;
-}
-
-} //namespace parser
-
-} //namespace mrmc
diff --git a/src/parser/read_lab_file.h b/src/parser/read_lab_file.h
deleted file mode 100644
index ddbb7f82a..000000000
--- a/src/parser/read_lab_file.h
+++ /dev/null
@@ -1,24 +0,0 @@
-/*
- * read_lab_file.h
- *
- *  Created on: 10.09.2012
- *      Author: thomas
- */
-
-#ifndef READ_LAB_FILE_H_
-#define READ_LAB_FILE_H_
-
-#include "src/models/atomic_propositions_labeling.h"
-
-
-namespace mrmc {
-
-namespace parser {
-
-mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const char * filename);
-
-}
-
-}
-
-#endif /* READ_LAB_FILE_H_ */
diff --git a/src/parser/read_tra_file.h b/src/parser/read_tra_file.h
deleted file mode 100644
index 20886d2f6..000000000
--- a/src/parser/read_tra_file.h
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
- * read_tra_file.h
- *
- *  Created on: 15.08.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef READ_TRA_FILE_H_
-#define READ_TRA_FILE_H_
-#include "src/sparse/static_sparse_matrix.h"
-namespace mrmc{
-namespace parser {
-
-mrmc::sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename);
-
-}
-}
-
-
-#endif /* READ_TRA_FILE_H_ */

From 408290d72b325dd4b62f5f94f465453e654d29d4 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 20:34:37 +0100
Subject: [PATCH 05/17] moved file mapping logic to parser.h

---
 src/parser/parser.h        | 63 +++++++++++++++++++++++++++++++++-----
 src/parser/readLabFile.cpp | 29 ++----------------
 src/parser/readTraFile.cpp | 36 ++--------------------
 3 files changed, 62 insertions(+), 66 deletions(-)

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 2ebefdb9d..b36f8dc70 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -1,15 +1,64 @@
 /*
  * parser.h
  *
- *  Created on: 12.09.2012
- *      Author: Thomas Heinemann
+ *  Created on: 21.11.2012
+ *      Author: Gereon Kremer
  */
 
-#ifndef PARSER_H_
-#define PARSER_H_
+#pragma once
 
-#include "boost/integer/integer_mask.hpp"
+#include <sys/stat.h>
+#include <sys/mman.h>
+#include <fcntl.h>
+#include <errno.h>
 
-const uint_fast32_t BUFFER_SIZE=1024;
+#include <pantheios/pantheios.hpp>
+#include "src/exceptions/file_IO_exception.h"
 
-#endif /* PARSER_H_ */
+namespace mrmc
+{
+namespace parser
+{
+
+	class MappedFile
+	{
+		private:
+			int file;
+			struct stat st;
+			
+		public:
+			 char* data;
+
+		MappedFile(const char* filename)
+		{
+			if (stat(filename, &(this->st)) != 0)
+			{
+				pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
+			}
+			
+			this->file = open(filename, O_RDONLY);
+			if (this->file < 0)
+			{
+				pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in open()");
+			}
+			
+			this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, this->file, 0);
+			if (this->data == (char*)-1)
+			{
+				close(this->file);
+				pantheios::log_ERROR("Could not mmap ", filename, ".");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()");
+			}
+		}
+		
+		~MappedFile()
+		{
+			munmap(this->data, this->st.st_size);
+			close(this->file);
+		}
+	};
+
+}
+}
\ No newline at end of file
diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
index c09fd2db5..15b66aaba 100644
--- a/src/parser/readLabFile.cpp
+++ b/src/parser/readLabFile.cpp
@@ -42,30 +42,9 @@ namespace parser {
  */
 mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename)
 {
-	/*!
-	 *	open file and map to memory
-	 */
-	struct stat st;
-	int f = open(filename, O_RDONLY);
-	if ((f < 0) || (stat(filename, &st) != 0)) {
-		/*!
-		 * 
-		 */
-		pantheios::log_ERROR("File could not be opened.");
-		throw mrmc::exceptions::file_IO_exception();
-		return NULL;
-	}
-	
-	char* data = (char*) mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE, f, 0);
-	if (data == (char*)-1)
-	{
-		pantheios::log_ERROR("File could not be mapped. Something went wrong with mmap.");
-		close(f);
-		throw mrmc::exceptions::file_IO_exception();
-		return NULL;
-	}
+	MappedFile file(filename);
 
-	char* buf = data;
+	char* buf = file.data;
 	char sep[] = " \n\t";
 	uint_fast32_t proposition_count = 0;
 	size_t cnt = 0;
@@ -83,7 +62,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 	
 	mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
 	char proposition[128];
-	buf = data;
+	buf = file.data;
 	cnt = 0;
 	do {
 		buf += cnt;
@@ -113,8 +92,6 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 		buf += cnt;
 	}
 	
-	munmap(data, st.st_size);
-	close(f);	
 	return result;
 }
 
diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index af5350693..c11dfdf9a 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -99,42 +99,17 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	*/
 	setlocale( LC_NUMERIC, "C" );
 	
-	/*!
-	 *	open file and map to memory
-	 */
-	struct stat st;
-	int f = open(filename, O_RDONLY);
-	if((f < 0) || (stat(filename, &st) != 0)) {
-		/*!
-		 *	stat() or open() failed
-		 */
-		pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
-		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
-		return NULL;
-	}
-	char *data = (char*)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, f, 0);
-	if (data == (char*)-1)
-	{
-		/*!
-		 *	mmap() failed
-		 */
-		pantheios::log_ERROR("Could not map the file to memory. Something went wrong with mmap.");
-		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error mapping file to memory");
-		close(f);
-		return NULL;
-	}
+	MappedFile file(filename);
 	
 	/*!
 	 *	perform first pass, i.e. count entries that are not zero and not on the diagonal
 	 */
-	uint_fast32_t non_zero = makeFirstPass(data);
+	uint_fast32_t non_zero = makeFirstPass(file.data);
 	if (non_zero == 0)
 	{
 		/*!
 		 *	first pass returned zero, this means the file format was wrong
 		 */
-		close(f);
-		munmap(data, st.st_size);
 		throw mrmc::exceptions::wrong_file_format();
 		return NULL;
 	}
@@ -144,7 +119,7 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	 *	
 	 *	from here on, we already know that the file header is correct
 	 */
-	char* buf = data;
+	char* buf = file.data;
 	uint_fast32_t rows;
 	sparse::StaticSparseMatrix<double> *sp = NULL;
 
@@ -172,8 +147,6 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 		/*!
 		 *	creating the matrix failed
 		 */
-		close(f);
-		munmap(data, st.st_size);
 		throw std::bad_alloc();
 		return NULL;
 	}
@@ -201,9 +174,6 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	/*!
 	 * clean up
 	 */	
-	close(f);
-	munmap(data, st.st_size);
-
 	pantheios::log_DEBUG("Finalizing Matrix");
 	sp->finalize();
 	return sp;

From ea8504a84e670642d3aa177b03cb167375e5a280 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 20:55:06 +0100
Subject: [PATCH 06/17] some fixes to new parser, calculate maximum node number
 manually

---
 src/parser/readLabFile.cpp | 13 ++++++++-----
 src/parser/readTraFile.cpp | 17 ++++++++++-------
 2 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
index 15b66aaba..5fa97a0d3 100644
--- a/src/parser/readLabFile.cpp
+++ b/src/parser/readLabFile.cpp
@@ -60,6 +60,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 		else cnt = 1;
 	} while (cnt > 0);
 	
+	printf("node count %d\n", node_count);
 	mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
 	char proposition[128];
 	buf = file.data;
@@ -79,18 +80,20 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 	buf += 4;
 	
 	uint_fast32_t node;
-	while (1) {
+	do {
 		node = strtol(buf, &buf, 10);
 		while (*buf != '\0') {
 			cnt = strcspn(buf, sep);
 			if (cnt == 0) buf++;
 			else break;
 		}
-		strncpy(proposition, buf, cnt);
-		proposition[cnt] = '\0';
-		result->addAtomicPropositionToState(proposition, node);
+		if (cnt > 0) {
+			strncpy(proposition, buf, cnt);
+			proposition[cnt] = '\0';
+			result->addAtomicPropositionToState(proposition, node);
+		}
 		buf += cnt;
-	}
+	} while (cnt > 0);
 	
 	return result;
 }
diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index c11dfdf9a..032ff0214 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -52,7 +52,7 @@ char* skipWS(char* buf)
  * @return The number of non-zero elements that are not on the diagonal
  * @param buf Data to scan. Is expected to be some char array.
  */
-static uint_fast32_t makeFirstPass(char* buf)
+static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 {
 	uint_fast32_t non_zero = 0;
 	
@@ -70,12 +70,15 @@ static uint_fast32_t makeFirstPass(char* buf)
 	/*!
 	 *	check all transitions for non-zero diagonal entrys
 	 */
-	unsigned int row, col;
+	uint_fast32_t row, col;
 	double val;
+	maxnode = 0;
 	while (1)  
 	{
 		row = strtol(buf, &buf, 10);
+		if (row > maxnode) maxnode = row;
 		col = strtol(buf, &buf, 10);
+		if (col > maxnode) maxnode = col;
 		val = strtod(buf, &buf);
 		if (val == 0.0) break;
 		if (row == col) non_zero--;
@@ -104,7 +107,8 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	/*!
 	 *	perform first pass, i.e. count entries that are not zero and not on the diagonal
 	 */
-	uint_fast32_t non_zero = makeFirstPass(file.data);
+	uint_fast32_t maxnode;
+	uint_fast32_t non_zero = makeFirstPass(file.data, maxnode);
 	if (non_zero == 0)
 	{
 		/*!
@@ -120,20 +124,19 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	 *	from here on, we already know that the file header is correct
 	 */
 	char* buf = file.data;
-	uint_fast32_t rows;
 	sparse::StaticSparseMatrix<double> *sp = NULL;
 
 	/*!
 	 *	read file header, extract number of states
 	 */
 	buf += 7; // skip "STATES "
-	rows = strtol(buf, &buf, 10);
+	strtol(buf, &buf, 10);
 	buf = skipWS(buf);
 	buf += 12; // skip "TRANSITIONS "
 	strtol(buf, &buf, 10);
 	
 	pantheios::log_DEBUG("Creating matrix with ",
-                        pantheios::integer(rows), " rows and ",
+                        pantheios::integer(maxnode + 1), " maxnodes and ",
                         pantheios::integer(non_zero), " Non-Zero-Elements");
                         
 	/*!	
@@ -141,7 +144,7 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	 *	Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
 	 *	non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
-	sp = new sparse::StaticSparseMatrix<double>(rows);
+	sp = new sparse::StaticSparseMatrix<double>(maxnode + 1);
 	if (sp == NULL)
 	{
 		/*!

From ad0c802fcc89d4d3abc0d723784fabd7c93f4fb9 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 21:42:54 +0100
Subject: [PATCH 07/17] minor cleanups, added documentation.

---
 src/parser/parser.h        |  50 +++++++++--
 src/parser/readLabFile.cpp | 168 +++++++++++++++++++++++++------------
 src/parser/readLabFile.h   |  14 ++--
 src/parser/readTraFile.cpp | 106 +++++++++++++----------
 src/parser/readTraFile.h   |  19 ++---
 5 files changed, 229 insertions(+), 128 deletions(-)

diff --git a/src/parser/parser.h b/src/parser/parser.h
index b36f8dc70..fcad8fa35 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -15,20 +15,47 @@
 #include <pantheios/pantheios.hpp>
 #include "src/exceptions/file_IO_exception.h"
 
-namespace mrmc
-{
-namespace parser
-{
-
+namespace mrmc {
+namespace parser {
+	
+	/*!
+	 *	@brief Opens a file and maps it to memory providing a char*
+	 *	containing the file content.
+	 * 
+	 *	This class is a very simple interface to read files efficiently.
+	 *	The given file is opened and mapped to memory using mmap().
+	 *	The public member data is a pointer to the actual file content.
+	 *	Using this method, the kernel will take care of all buffering. This is
+	 *	most probably much more efficient than doing this manually.
+	 */
+	 
 	class MappedFile
 	{
 		private:
+			/*!
+			 *	@brief file descriptor obtained by open().
+			 */
 			int file;
+			
+			/*!
+			 *	@brief stat information about the file.
+			 */
 			struct stat st;
 			
 		public:
-			 char* data;
-
+			/*!
+			 *	@brief pointer to actual file content.
+			 */
+			char* data;
+		
+		/*!
+		 *	@brief Constructor of MappedFile.
+		 *	
+		 *	Will stat the given file, open it and map it to memory.
+		 *	If anything of this fails, an appropriate exception is raised
+		 *	and a log entry is written.
+		 *	@filename file to be opened
+		 */
 		MappedFile(const char* filename)
 		{
 			if (stat(filename, &(this->st)) != 0)
@@ -53,6 +80,11 @@ namespace parser
 			}
 		}
 		
+		/*!
+		 *	@brief Destructor of MappedFile.
+		 *	
+		 *	Will unmap the data and close the file.
+		 */
 		~MappedFile()
 		{
 			munmap(this->data, this->st.st_size);
@@ -60,5 +92,5 @@ namespace parser
 		}
 	};
 
-}
-}
\ No newline at end of file
+} // namespace parser
+} // namespace mrmc
\ No newline at end of file
diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
index 5fa97a0d3..f910e8dce 100644
--- a/src/parser/readLabFile.cpp
+++ b/src/parser/readLabFile.cpp
@@ -1,4 +1,4 @@
-/*
+/*!
  * readLabFile.cpp
  *
  *  Created on: 21.11.2012
@@ -28,76 +28,138 @@
 #include <pantheios/inserters/integer.hpp>
 
 namespace mrmc {
-
 namespace parser {
 
 
 /*!
- * Reads a .lab file and puts the result in a labeling structure.
+ *	Reads a label file and puts the result in a labeling structure.
  *
- * Labelings created with this method have to be freed with the delete operator.
- * @param node_count the number of states.
- * @param filename   input .lab file's name.
- * @return The pointer to the created labeling object.
+ *	Labelings created with this method have to be freed with the delete operator.
+ *	@param node_count the number of states.
+ *	@param filename   input .lab file's name.
+ *	@return The pointer to the created labeling object.
  */
 mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename)
 {
+	/*
+	 *	open file
+	 */
 	MappedFile file(filename);
-
 	char* buf = file.data;
-	char sep[] = " \n\t";
-	uint_fast32_t proposition_count = 0;
-	size_t cnt = 0;
 
-	do {
-		buf += cnt;
-		cnt = strcspn(buf, sep);
-		if (cnt > 0) {
-			if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
-			if (strncmp(buf, "#END", cnt) == 0) break;
-			proposition_count++;
-		}
-		else cnt = 1;
-	} while (cnt > 0);
+	/*
+	 *	first run: obtain number of propositions
+	 */
+	char separator[] = " \n\t";
+	uint_fast32_t proposition_count = 0;
+	{
+		size_t cnt = 0;
+		do
+		{
+			buf += cnt;
+			cnt = strcspn(buf, separator); // position of next separator
+			if (cnt > 0)
+			{
+				/*
+				 *	next token is #DECLARATION: just skip it
+				 *	next token is #END: stop search
+				 *	otherwise increase proposition_count
+				 */
+				if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
+				if (strncmp(buf, "#END", cnt) == 0) break;
+				proposition_count++;
+			}
+			else cnt = 1; // next char is separator, one step forward
+		} while (cnt > 0);
+	}
 	
-	printf("node count %d\n", node_count);
+	/*
+	 *	create labeling object with given node and proposition count
+	 */
 	mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
-	char proposition[128];
+	
+	/*
+	 *	second run: add propositions and node labels to labeling
+	 *
+	 *	first thing to do: reset file pointer
+	 */	
 	buf = file.data;
-	cnt = 0;
-	do {
-		buf += cnt;
-		cnt = strcspn(buf, sep);
-		if (cnt > 0) {
-			if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
-			if (strncmp(buf, "#END", cnt) == 0) break;
-			strncpy(proposition, buf, cnt);
-			proposition[cnt] = '\0';
-			result->addAtomicProposition(proposition);
-		}
-		else cnt = 1;
-	} while (cnt > 0);
-	buf += 4;
+	{
+		/*
+		 *	load propositions
+		 */
+		char proposition[128]; // buffer for proposition names
+		size_t cnt = 0;
+		do
+		{
+			buf += cnt;
+			cnt = strcspn(buf, separator); // position of next separator
+			if (cnt > 0)
+			{
+				/*
+				 *	next token is: #DECLARATION: just skip it
+				 *	next token is: #END: stop search
+				 *	otherwise: copy token to buffer, append trailing null byte and hand it to labeling
+				 */
+				if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
+				if (strncmp(buf, "#END", cnt) == 0) break;
+				strncpy(proposition, buf, cnt);
+				proposition[cnt] = '\0';
+				result->addAtomicProposition(proposition);
+			}
+			else cnt = 1; // next char is separator, one step forward
+		} while (cnt > 0);
+		/*
+		 *	Right here, the buf pointer is still pointing to our last token,
+		 *	i.e. to #END. We want to skip this one...
+		 */
+		buf += 4;
+	}
 	
-	uint_fast32_t node;
-	do {
-		node = strtol(buf, &buf, 10);
-		while (*buf != '\0') {
-			cnt = strcspn(buf, sep);
-			if (cnt == 0) buf++;
-			else break;
-		}
-		if (cnt > 0) {
-			strncpy(proposition, buf, cnt);
-			proposition[cnt] = '\0';
-			result->addAtomicPropositionToState(proposition, node);
-		}
-		buf += cnt;
-	} while (cnt > 0);
+	{
+		/*
+		 *	now parse node label assignments
+		 */
+		uint_fast32_t node;
+		char proposition[128];
+		size_t cnt;
+		do
+		{
+			node = strtol(buf, &buf, 10); // parse node number
+			while (*buf != '\0') // while not at end of file
+			{
+				cnt = strcspn(buf, separator); // position of next separator
+				if (cnt == 0) buf++; // next char is separator, one step forward
+				else break;
+			}
+			/*
+			 *	if cnt > 0, buf points to the next proposition
+			 *	otherwise, we have reached the end of the file
+			 */
+			if (cnt > 0)
+			{
+				/*
+				 *	copy proposition to buffer, add assignment to labeling
+				 */
+				strncpy(proposition, buf, cnt);
+				proposition[cnt] = '\0';
+				result->addAtomicPropositionToState(proposition, node);
+			}
+			else if (node == 0)
+			{
+				/*
+				 *	If this is executed, we could read a number but there
+				 *	was no proposition after that. This strongly suggests a
+				 *	broken file, but it's not fatal...
+				 */
+				 pantheios::log_WARNING("The label file ended on a node number. Is the file malformated?");
+			}
+			buf += cnt;
+		} while (cnt > 0);
+	}
 	
 	return result;
 }
 
 } //namespace parser
-
 } //namespace mrmc
diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h
index 4019864e0..e948a2ce3 100644
--- a/src/parser/readLabFile.h
+++ b/src/parser/readLabFile.h
@@ -1,19 +1,15 @@
-/*
- * read_lab_file.h
- *
- */
-
 #pragma once
 
 #include "src/models/atomic_propositions_labeling.h"
 
 
 namespace mrmc {
-
 namespace parser {
 
+/*!
+ *	@brief Load label file and return initialized AtomicPropositionsLabeling object.
+ */
 mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename);
 
-}
-
-}
+} // namespace parser
+} // namespace mrmc
diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index 032ff0214..335699138 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -1,10 +1,8 @@
-/*! read_tra_file.cpp
- * Provides functions for reading a *.tra file describing the transition
- * system of a Markov chain (DTMC) and saving it into a corresponding
- * matrix.
+/*!
+ *	readTraFile.cpp
  *
- * Created on: 20.11.2012
- *      Author: Gereon Kremer
+ *	Created on: 20.11.2012
+ *		Author: Gereon Kremer
  */
 
 #include "parser.h"
@@ -30,9 +28,13 @@
 #include <pantheios/inserters/real.hpp>
 
 namespace mrmc {
-
 namespace parser{
 
+/*!
+ *	Skips all whitespaces and returns new pointer.
+ *
+ *	@todo	should probably be replaced by strspn et.al.
+ */
 char* skipWS(char* buf)
 {
 	while(1)
@@ -43,20 +45,25 @@ char* skipWS(char* buf)
 }
 
 /*!
- * This method does the first pass through the .tra file and computes
- * the number of non-zero elements that are not diagonal elements,
- * which correspondents to the number of transitions that are not
- * self-loops.
- * (Diagonal elements are treated in a special way).
+ *	@brief	Perform first pass through the file and obtain number of
+ *	non-zero cells and maximum node id.
+ *
+ *	This method does the first pass through the .tra file and computes
+ *	the number of non-zero elements that are not diagonal elements,
+ *	which correspondents to the number of transitions that are not
+ *	self-loops.
+ *	(Diagonal elements are treated in a special way).
+ *	It also calculates the maximum node id and stores it in maxnode.
  *
- * @return The number of non-zero elements that are not on the diagonal
- * @param buf Data to scan. Is expected to be some char array.
+ *	@return The number of non-zero elements that are not on the diagonal
+ *	@param buf Data to scan. Is expected to be some char array.
+ *	@param maxnode Is set to highest id of all nodes.
  */
 static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 {
 	uint_fast32_t non_zero = 0;
 	
-	/*!
+	/*
 	 *	check file header and extract number of transitions
 	 */
 	if (strncmp(buf, "STATES ", 7) != 0) return 0;
@@ -67,7 +74,7 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 	buf += 12; // skip "TRANSITIONS "
 	if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
 	
-	/*!
+	/*
 	 *	check all transitions for non-zero diagonal entrys
 	 */
 	uint_fast32_t row, col;
@@ -75,10 +82,20 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 	maxnode = 0;
 	while (1)  
 	{
+		/*
+		 *	read row and column
+		 */
 		row = strtol(buf, &buf, 10);
-		if (row > maxnode) maxnode = row;
 		col = strtol(buf, &buf, 10);
+		/*
+		 *	check if one is larger than the current maximum id
+		 */
+		if (row > maxnode) maxnode = row;
 		if (col > maxnode) maxnode = col;
+		/*
+		 *	read value. if value is zero, we have reached the end of the file.
+		 *	if row == col, we have a diagonal element which is treated seperately and this non_zero must be decreased.
+		 */
 		val = strtod(buf, &buf);
 		if (val == 0.0) break;
 		if (row == col) non_zero--;
@@ -89,44 +106,44 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 
 
 
-/*!Reads a .tra file and produces a sparse matrix representing the described Markov Chain.
+/*!
+ *	Reads a .tra file and produces a sparse matrix representing the described Markov Chain.
  *
- * Matrices created with this method have to be freed with the delete operator.
- * @param filename input .tra file's name.
- * @return a pointer to the created sparse matrix.
+ *	Matrices created with this method have to be freed with the delete operator.
+ *	@param filename input .tra file's name.
+ *	@return a pointer to the created sparse matrix.
  */
 
 sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
-	/*!
+	/*
 	*	enforce locale where decimal point is '.'
 	*/
 	setlocale( LC_NUMERIC, "C" );
 	
+	/*
+	 *	open file
+	 */
 	MappedFile file(filename);
+	char* buf = file.data;
 	
-	/*!
+	/*
 	 *	perform first pass, i.e. count entries that are not zero and not on the diagonal
 	 */
 	uint_fast32_t maxnode;
 	uint_fast32_t non_zero = makeFirstPass(file.data, maxnode);
-	if (non_zero == 0)
-	{
-		/*!
-		 *	first pass returned zero, this means the file format was wrong
-		 */
-		throw mrmc::exceptions::wrong_file_format();
-		return NULL;
-	}
+	/*
+	 *	if first pass returned zer, the file format was wrong
+	 */
+	if (non_zero == 0) throw mrmc::exceptions::wrong_file_format();
 	
-	/*!
+	/*
 	 *	perform second pass
 	 *	
 	 *	from here on, we already know that the file header is correct
 	 */
-	char* buf = file.data;
 	sparse::StaticSparseMatrix<double> *sp = NULL;
 
-	/*!
+	/*
 	 *	read file header, extract number of states
 	 */
 	buf += 7; // skip "STATES "
@@ -139,29 +156,27 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
                         pantheios::integer(maxnode + 1), " maxnodes and ",
                         pantheios::integer(non_zero), " Non-Zero-Elements");
                         
-	/*!	
+	/*
 	 *	Creating matrix
 	 *	Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
 	 *	non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
 	sp = new sparse::StaticSparseMatrix<double>(maxnode + 1);
-	if (sp == NULL)
-	{
-		/*!
-		 *	creating the matrix failed
-		 */
-		throw std::bad_alloc();
-		return NULL;
-	}
+	if (sp == NULL)	throw std::bad_alloc();
 	sp->initialize(non_zero);
 
 	uint_fast64_t row, col;
 	double val;
-	/*!
+
+	/*
 	 *	read all transitions from file
 	 */
 	while (1)
 	{
+		/*
+		 *	read row, col and value. if value == 0.0, we have reached the
+		 *	end of the file.
+		 */
 		row = strtol(buf, &buf, 10);
 		col = strtol(buf, &buf, 10);
 		val = strtod(buf, &buf);
@@ -174,7 +189,7 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 		sp->addNextValue(row,col,val);	
 	}
 	
-	/*!
+	/*
 	 * clean up
 	 */	
 	pantheios::log_DEBUG("Finalizing Matrix");
@@ -183,5 +198,4 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 }
 
 } //namespace parser
-
 } //namespace mrmc
diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h
index c4b025a64..629acde67 100644
--- a/src/parser/readTraFile.h
+++ b/src/parser/readTraFile.h
@@ -1,19 +1,16 @@
-/*
- * read_tra_file.h
- *
- *  Created on: 15.08.2012
- *      Author: Thomas Heinemann
- */
-
 #pragma once
 
 #include "src/sparse/static_sparse_matrix.h"
 
 namespace mrmc {
-	namespace parser {
+namespace parser {
 	
-		mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
+/*!
+ *	@brief	Load transition system from file and return initialized
+ *	StaticSparseMatrix object.
+ */
+mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
 		
-	}
-}
+} // namespace parser
+} // namespace mrmc
 

From 7eaedbfe9b664eae24f96a02dbfbda72a6ff95af Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 22:16:42 +0100
Subject: [PATCH 08/17] changing names of parsers

---
 src/mrmc-cpp.cpp                   | 12 +++++++-----
 src/utility/utility.cpp            |  8 ++++----
 test/parser/read_lab_file_test.cpp | 12 ++++++------
 test/parser/read_tra_file_test.cpp | 12 ++++++------
 4 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/src/mrmc-cpp.cpp b/src/mrmc-cpp.cpp
index f6aa66154..94843cbff 100644
--- a/src/mrmc-cpp.cpp
+++ b/src/mrmc-cpp.cpp
@@ -26,8 +26,8 @@ PANTHEIOS_EXTERN_C PAN_CHAR_T const PANTHEIOS_FE_PROCESS_IDENTITY[] = "mrmc-cpp"
 #include "src/models/dtmc.h"
 #include "src/sparse/static_sparse_matrix.h"
 #include "src/models/atomic_propositions_labeling.h"
-#include "src/parser/read_lab_file.h"
-#include "src/parser/read_tra_file.h"
+#include "src/parser/readLabFile.h"
+#include "src/parser/readTraFile.h"
 #include "Eigen/Sparse"
  
 int main(int argc, char* argv[]) {
@@ -39,9 +39,11 @@ int main(int argc, char* argv[]) {
 		std::cout << "Required argument #1 inputTraFile.tra not found!" << std::endl;
 		exit(-1);
 	}
-
-	mrmc::sparse::StaticSparseMatrix<double>* probMatrix = mrmc::parser::read_tra_file(argv[1]);
-	mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), argv[2]);
+	
+	printf("read tra...\n");
+	mrmc::sparse::StaticSparseMatrix<double>* probMatrix = mrmc::parser::readTraFile(argv[1]);
+	printf("read lab...\n");
+	mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::readLabFile(probMatrix->getRowCount(), argv[2]);
 	mrmc::models::Dtmc<double> dtmc(probMatrix, labeling);
 
 	return 0;
diff --git a/src/utility/utility.cpp b/src/utility/utility.cpp
index 656e51ac1..f00686bb2 100644
--- a/src/utility/utility.cpp
+++ b/src/utility/utility.cpp
@@ -6,8 +6,8 @@
  */
 
 #include "src/utility/utility.h"
-#include "src/parser/read_tra_file.h"
-#include "src/parser/read_lab_file.h"
+#include "src/parser/readTraFile.h"
+#include "src/parser/readLabFile.h"
 
 #include "src/sparse/static_sparse_matrix.h"
 #include "src/models/dtmc.h"
@@ -79,11 +79,11 @@ void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename) {
 
 mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
    mrmc::sparse::StaticSparseMatrix<double>* transition_matrix =
-         mrmc::parser::read_tra_file(tra_file);
+         mrmc::parser::readTraFile(tra_file);
    uint_fast64_t node_count = transition_matrix->getRowCount();
 
    mrmc::models::AtomicPropositionsLabeling* labeling =
-         mrmc::parser::read_lab_file(node_count, lab_file);
+         mrmc::parser::readLabFile(node_count, lab_file);
 
    mrmc::models::Dtmc<double>* result =
          new mrmc::models::Dtmc<double>(transition_matrix, labeling);
diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp
index 7a273a35d..928d27996 100644
--- a/test/parser/read_lab_file_test.cpp
+++ b/test/parser/read_lab_file_test.cpp
@@ -8,13 +8,13 @@
 #include "gtest/gtest.h"
 #include "MRMCConfig.h"
 #include "src/models/atomic_propositions_labeling.h"
-#include "src/parser/read_lab_file.h"
+#include "src/parser/readLabFile.h"
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
 
 TEST(ReadLabFileTest, NonExistingFileTest) {
    //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
-   ASSERT_THROW(mrmc::parser::read_lab_file(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
+   ASSERT_THROW(mrmc::parser::readLabFile(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
 }
 
 TEST(ReadLabFileTest, ParseTest) {
@@ -22,7 +22,7 @@ TEST(ReadLabFileTest, ParseTest) {
 	mrmc::models::AtomicPropositionsLabeling* labeling = NULL;
 
 	//Parsing the file
-	ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
+	ASSERT_NO_THROW(labeling = mrmc::parser::readLabFile(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
 
 	//Checking whether all propositions are in the labelling
 
@@ -82,14 +82,14 @@ TEST(ReadLabFileTest, ParseTest) {
 }
 
 TEST(ReadLabFileTest, WrongHeaderTest1) {
-   ASSERT_THROW(mrmc::parser::read_lab_file(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::readLabFile(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::wrong_file_format);
 }
 
 TEST(ReadLabFileTest, WrongHeaderTest2) {
-   ASSERT_THROW(mrmc::parser::read_lab_file(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::readLabFile(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::wrong_file_format);
 }
 
 TEST(ReadLabFileTest, WrongPropositionTest) {
-   ASSERT_THROW(mrmc::parser::read_lab_file(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::readLabFile(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::wrong_file_format);
 }
 
diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp
index b0e54b8ae..54229da76 100644
--- a/test/parser/read_tra_file_test.cpp
+++ b/test/parser/read_tra_file_test.cpp
@@ -8,7 +8,7 @@
 #include "gtest/gtest.h"
 #include "MRMCConfig.h"
 #include "src/sparse/static_sparse_matrix.h"
-#include "src/parser/read_tra_file.h"
+#include "src/parser/readTraFile.h"
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
 #include <pantheios/pantheios.hpp>
@@ -16,7 +16,7 @@
 TEST(ReadTraFileTest, NonExistingFileTest) {
    pantheios::log_INFORMATIONAL("Started NonExistingFileTest");
    //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
-   ASSERT_THROW(mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
+   ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
 }
 
 /* The following test case is based on one of the original MRMC test cases
@@ -24,7 +24,7 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
 TEST(ReadTraFileTest, ParseFileTest1) {
 	pantheios::log_INFORMATIONAL("Started ParseFileTest1");
 	mrmc::sparse::StaticSparseMatrix<double> *result = NULL;
-	ASSERT_NO_THROW(result = mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
+	ASSERT_NO_THROW(result = mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
 
 	if (result != NULL) {
 		double val = 0;
@@ -73,17 +73,17 @@ TEST(ReadTraFileTest, ParseFileTest1) {
 TEST(ReadTraFileTest, WrongFormatTestHeader1) {
    pantheios::log_INFORMATIONAL("Started WrongFormatTestHeader1");
 
-   ASSERT_THROW(mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestHeader2) {
    pantheios::log_INFORMATIONAL("Started WrongFormatTestHeader2");
 
-   ASSERT_THROW(mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestTransition) {
    pantheios::log_INFORMATIONAL("Started WrongFormatTestTransition");
 
-   ASSERT_THROW(mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format);
 }

From 48323c005ad5ee5b7f7e0ef7c48b0e4330eeb8c6 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 21 Nov 2012 23:00:27 +0100
Subject: [PATCH 09/17] added header to make os detection at one point added
 ifdefs to implement file mapping for windows implemented file mapping for
 windows, but did not compile yet (no windows available...)

---
 src/parser/parser.h       | 73 ++++++++++++++++++++++++++++++++++++---
 src/utility/osDetection.h | 11 ++++++
 2 files changed, 80 insertions(+), 4 deletions(-)
 create mode 100644 src/utility/osDetection.h

diff --git a/src/parser/parser.h b/src/parser/parser.h
index fcad8fa35..180b96347 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -7,8 +7,14 @@
 
 #pragma once
 
+#include "src/utility/osDetection.h"
+
+#if defined LINUX || defined MACOSX
+	#include <sys/mman.h>
+#elif defined WINDOWS
+#endif
+
 #include <sys/stat.h>
-#include <sys/mman.h>
 #include <fcntl.h>
 #include <errno.h>
 
@@ -28,6 +34,10 @@ namespace parser {
 	 *	Using this method, the kernel will take care of all buffering. This is
 	 *	most probably much more efficient than doing this manually.
 	 */
+
+#if !defined LINUX && !defined MACOSX && !defined WINDOWS
+	#error Platform not supported
+#endif
 	 
 	class MappedFile
 	{
@@ -35,12 +45,21 @@ namespace parser {
 			/*!
 			 *	@brief file descriptor obtained by open().
 			 */
+#if defined LINUX || defined MACOSX
 			int file;
+#elif defined WINDOWS
+			HFILE file;
+			HANDLE mapping;
+#endif
 			
 			/*!
 			 *	@brief stat information about the file.
 			 */
-			struct stat st;
+#if defined LINUX || defined MACOSX
+			struct stat64 st;
+#elif defined WINDOWS
+			struct __stat64 st;
+#endif
 			
 		public:
 			/*!
@@ -58,12 +77,17 @@ namespace parser {
 		 */
 		MappedFile(const char* filename)
 		{
-			if (stat(filename, &(this->st)) != 0)
+#if defined LINUX || defined MACOSX
+			/*
+			 *	Do file mapping for reasonable systems.
+			 *	stat64(), open(), mmap()
+			 */
+			if (stat64(filename, &(this->st)) != 0)
 			{
 				pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
 			}
-			
+
 			this->file = open(filename, O_RDONLY);
 			if (this->file < 0)
 			{
@@ -78,6 +102,42 @@ namespace parser {
 				pantheios::log_ERROR("Could not mmap ", filename, ".");
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()");
 			}
+#elif defined WINDOWS
+#warning Windows support is implemented but has not been compiled yet...
+			/*
+			 *	Do file mapping for windows.
+			 *	_stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
+			 */
+			if (_stat64(filename, &(this->st)) != 0)
+			{
+				pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
+			}
+			
+			this->file = CreateFile(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
+			if (this->file == INVALID_HANDLE_VALUE)
+			{
+				pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFile()");
+			}
+			
+			this->mapping = CreateFileMapping(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
+			if (this->mapping == NULL)
+			{
+				CloseHandle(this->file);
+				pantheios::log_ERROR("Could not create file mapping for ", filename, ".");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMapping()");
+			}
+			
+			this->data = MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, st.st_size);
+			if (this->data == NULL)
+			{
+				CloseHandle(this->mapping);
+				CloseHandle(this->file);
+				pantheios::log_ERROR("Could not create file map view for ", filename, ".");
+				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in MapViewOfFile()");
+			}
+#endif
 		}
 		
 		/*!
@@ -87,8 +147,13 @@ namespace parser {
 		 */
 		~MappedFile()
 		{
+#if defined LINUX || defined MACOSX
 			munmap(this->data, this->st.st_size);
 			close(this->file);
+#elif defined WINDOWS
+			CloseHandle(this->mapping);
+			CloseHandle(this->file);
+#endif
 		}
 	};
 
diff --git a/src/utility/osDetection.h b/src/utility/osDetection.h
new file mode 100644
index 000000000..c6c863a60
--- /dev/null
+++ b/src/utility/osDetection.h
@@ -0,0 +1,11 @@
+#pragma once
+
+#if defined __linux__ || defined __linux
+	#define LINUX
+#elif defined TARGET_OS_MAC || defined __apple__
+	#define MACOSX
+#elif defined _WIN32 || defined _WIN64
+	#define WINDOWS
+#else
+	#error Could not detect Operating System
+#endif
\ No newline at end of file

From 2eb08a603a6b7124b4d169e1f0e50ac3bcca3511 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 28 Nov 2012 19:48:41 +0100
Subject: [PATCH 10/17] made stuff compile with new CMakeLists started a parser
 built with boost::spirit. It compiles, but does not do anything useful yet...

---
 CMakeLists.txt              |  3 +++
 src/parser/readPctlFile.cpp | 32 ++++++++++++++++++++++++++++++++
 src/parser/readPctlFile.h   | 15 +++++++++++++++
 3 files changed, 50 insertions(+)
 create mode 100644 src/parser/readPctlFile.cpp
 create mode 100644 src/parser/readPctlFile.h

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 06b47443a..212274456 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -7,6 +7,9 @@ set (MRMC_CPP_VERSION_MAJOR 1)
 set (MRMC_CPP_VERSION_MINOR 0)
 
 option(DEFINE_UNIX "Defines the UNIX flag for compilation." OFF)
+set (GTEST_INCLUDE_DIR resources/3rdparty/gtest-1.6.0/include)
+set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.a)
+set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.a)
 
 #Configurations for GCC
 if(CMAKE_COMPILER_IS_GNUCC) 
diff --git a/src/parser/readPctlFile.cpp b/src/parser/readPctlFile.cpp
new file mode 100644
index 000000000..1c9325758
--- /dev/null
+++ b/src/parser/readPctlFile.cpp
@@ -0,0 +1,32 @@
+#include "src/parser/readPctlFile.h"
+
+#include <boost/spirit/include/classic_core.hpp>
+#include <boost/spirit/include/qi_grammar.hpp>
+#include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/qi_char_class.hpp>
+
+namespace bs = boost::spirit;
+namespace bsq = bs::qi;
+
+namespace
+{
+	using namespace bsq;
+	struct Parser : public bsq::grammar< char const* >
+	{
+		typedef rule< char const* > rule_t;
+	
+		rule_t atom, term, formula;
+	
+		Parser() : Parser::base_type(formula, "PCTL parser")
+		{
+			atom = double_ | (char_('(') >> formula >> char_(')') );
+			term = atom >> *( char_('*') >> atom );
+			formula = term >> *( char_('+') >> term );
+		}
+	};
+}
+
+void readPctlFile(const char* filename)
+{
+	Parser p;
+}
\ No newline at end of file
diff --git a/src/parser/readPctlFile.h b/src/parser/readPctlFile.h
new file mode 100644
index 000000000..77e5fd3a4
--- /dev/null
+++ b/src/parser/readPctlFile.h
@@ -0,0 +1,15 @@
+#ifndef READPCTLFILE_H_
+#define READPCTLFILE_H_
+
+namespace mrmc {
+namespace parser {
+
+/*!
+ *	@brief Load PCTL file
+ */
+void readPctlFile(const char * filename);
+
+} // namespace parser
+} // namespace mrmc
+
+#endif /* READPCTLFILE_H_ */
\ No newline at end of file

From 925a9bd8c00e673cdf43e3d3082169c69471798d Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Wed, 28 Nov 2012 20:32:55 +0100
Subject: [PATCH 11/17] changing pragma to ifdef, starting implementation of
 PRCTLParser

---
 src/parser/parser.h          | 16 +++++++--
 src/parser/readLabFile.h     |  5 ++-
 src/parser/readPctlFile.cpp  | 32 -----------------
 src/parser/readPctlFile.h    | 15 --------
 src/parser/readPrctlFile.cpp | 66 ++++++++++++++++++++++++++++++++++++
 src/parser/readPrctlFile.h   | 15 ++++++++
 src/parser/readTraFile.h     |  4 ++-
 7 files changed, 101 insertions(+), 52 deletions(-)
 delete mode 100644 src/parser/readPctlFile.cpp
 delete mode 100644 src/parser/readPctlFile.h
 create mode 100644 src/parser/readPrctlFile.cpp
 create mode 100644 src/parser/readPrctlFile.h

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 180b96347..f1b772040 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -5,7 +5,8 @@
  *      Author: Gereon Kremer
  */
 
-#pragma once
+#ifndef PARSER_H_
+#define PARSER_H_
 
 #include "src/utility/osDetection.h"
 
@@ -66,6 +67,11 @@ namespace parser {
 			 *	@brief pointer to actual file content.
 			 */
 			char* data;
+			
+			/*!
+			 *	@brief pointer to end of file content.
+			 */
+			char* dataend;
 		
 		/*!
 		 *	@brief Constructor of MappedFile.
@@ -102,6 +108,7 @@ namespace parser {
 				pantheios::log_ERROR("Could not mmap ", filename, ".");
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()");
 			}
+			this->dataend = this->data + this->st.st_size;
 #elif defined WINDOWS
 #warning Windows support is implemented but has not been compiled yet...
 			/*
@@ -129,7 +136,7 @@ namespace parser {
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMapping()");
 			}
 			
-			this->data = MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, st.st_size);
+			this->data = MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size);
 			if (this->data == NULL)
 			{
 				CloseHandle(this->mapping);
@@ -137,6 +144,7 @@ namespace parser {
 				pantheios::log_ERROR("Could not create file map view for ", filename, ".");
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in MapViewOfFile()");
 			}
+			this->dataend = this->data + this->st.st_size;
 #endif
 		}
 		
@@ -158,4 +166,6 @@ namespace parser {
 	};
 
 } // namespace parser
-} // namespace mrmc
\ No newline at end of file
+} // namespace mrmc
+
+#endif /* PARSER_H_ */
\ No newline at end of file
diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h
index e948a2ce3..31375ced8 100644
--- a/src/parser/readLabFile.h
+++ b/src/parser/readLabFile.h
@@ -1,4 +1,5 @@
-#pragma once
+#ifndef READLABFILE_H_
+#define READLABFILE_H_
 
 #include "src/models/atomic_propositions_labeling.h"
 
@@ -13,3 +14,5 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 
 } // namespace parser
 } // namespace mrmc
+
+#endif /* READLABFILE_H_ */
\ No newline at end of file
diff --git a/src/parser/readPctlFile.cpp b/src/parser/readPctlFile.cpp
deleted file mode 100644
index 1c9325758..000000000
--- a/src/parser/readPctlFile.cpp
+++ /dev/null
@@ -1,32 +0,0 @@
-#include "src/parser/readPctlFile.h"
-
-#include <boost/spirit/include/classic_core.hpp>
-#include <boost/spirit/include/qi_grammar.hpp>
-#include <boost/spirit/include/qi.hpp>
-#include <boost/spirit/include/qi_char_class.hpp>
-
-namespace bs = boost::spirit;
-namespace bsq = bs::qi;
-
-namespace
-{
-	using namespace bsq;
-	struct Parser : public bsq::grammar< char const* >
-	{
-		typedef rule< char const* > rule_t;
-	
-		rule_t atom, term, formula;
-	
-		Parser() : Parser::base_type(formula, "PCTL parser")
-		{
-			atom = double_ | (char_('(') >> formula >> char_(')') );
-			term = atom >> *( char_('*') >> atom );
-			formula = term >> *( char_('+') >> term );
-		}
-	};
-}
-
-void readPctlFile(const char* filename)
-{
-	Parser p;
-}
\ No newline at end of file
diff --git a/src/parser/readPctlFile.h b/src/parser/readPctlFile.h
deleted file mode 100644
index 77e5fd3a4..000000000
--- a/src/parser/readPctlFile.h
+++ /dev/null
@@ -1,15 +0,0 @@
-#ifndef READPCTLFILE_H_
-#define READPCTLFILE_H_
-
-namespace mrmc {
-namespace parser {
-
-/*!
- *	@brief Load PCTL file
- */
-void readPctlFile(const char * filename);
-
-} // namespace parser
-} // namespace mrmc
-
-#endif /* READPCTLFILE_H_ */
\ No newline at end of file
diff --git a/src/parser/readPrctlFile.cpp b/src/parser/readPrctlFile.cpp
new file mode 100644
index 000000000..0453fc15f
--- /dev/null
+++ b/src/parser/readPrctlFile.cpp
@@ -0,0 +1,66 @@
+#include "src/parser/readPrctlFile.h"
+
+#include "src/parser/parser.h"
+
+#include <iostream>
+
+#include <boost/spirit/include/classic_core.hpp>
+#include <boost/spirit/include/qi_grammar.hpp>
+#include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/qi_char_class.hpp>
+
+namespace bs = boost::spirit;
+
+namespace
+{
+	using namespace bs::qi;
+	using namespace bs::standard;
+	
+	struct PRCTLParser : public grammar< char const* >
+	{
+		typedef rule< char const* > rule_t;
+	
+		/*!
+		 *	@brief Generic Nonterminals.
+		 */
+		rule_t variable, value;
+		
+		/*!
+		 *	@brief Nonterminals for file header.
+		 */
+		rule_t varDef, type;
+		
+		/*!
+		 *	@brief Nonterminals for formula.
+		 */
+		rule_t formula, opP;
+		
+		/*!
+		 *	@brief Nonterminals for high-level file structure.
+		 */
+		rule_t file, header;
+	
+		PRCTLParser() : PRCTLParser::base_type(file, "PRCTL parser")
+		{
+			variable = alnum;
+			value = int_ | double_;
+			type = string("int") | string("double");
+			varDef = string("const") >> type >> variable >> string("=") >> value >> string(";");
+			
+			header = *( varDef );
+			
+			file = header;
+		}
+	};
+}
+
+void readPrctlFile(const char* filename)
+{
+	PRCTLParser p;
+	mrmc::parser::MappedFile file(filename);
+	
+	if (bs::qi::parse< char const* >(file.data, file.dataend, p))
+	{
+		std::cout << "File was parsed" << std::endl;
+	}
+}
\ No newline at end of file
diff --git a/src/parser/readPrctlFile.h b/src/parser/readPrctlFile.h
new file mode 100644
index 000000000..c7d508b18
--- /dev/null
+++ b/src/parser/readPrctlFile.h
@@ -0,0 +1,15 @@
+#ifndef READPRCTLFILE_H_
+#define READPRCTLFILE_H_
+
+namespace mrmc {
+namespace parser {
+
+/*!
+ *	@brief Load PRCTL file
+ */
+void readPrctlFile(const char * filename);
+
+} // namespace parser
+} // namespace mrmc
+
+#endif /* READPRCTLFILE_H_ */
\ No newline at end of file
diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h
index 629acde67..2d74242a6 100644
--- a/src/parser/readTraFile.h
+++ b/src/parser/readTraFile.h
@@ -1,4 +1,5 @@
-#pragma once
+#ifndef READTRAFILE_H_
+#define READTRAFILE_H_
 
 #include "src/sparse/static_sparse_matrix.h"
 
@@ -14,3 +15,4 @@ mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
 } // namespace parser
 } // namespace mrmc
 
+#endif /* READTRAFILE_H_ */
\ No newline at end of file

From 4f7cbd450a845d6a5fbcc6063b70ad1b7faeb534 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Sat, 1 Dec 2012 15:31:34 +0100
Subject: [PATCH 12/17] Fixed bugs in the Windows Part of the parser,
 refactored includes to meet Windows Requirements.

Deleted a #warning
---
 src/formula/BoundedUntil.h | 4 +++-
 src/parser/parser.h        | 9 ++++-----
 src/parser/readLabFile.cpp | 6 +++++-
 src/parser/readTraFile.cpp | 5 ++++-
 4 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index bc1510fe3..425e5afaf 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -9,6 +9,8 @@
 #define BOUNDEDUNTIL_H_
 
 #include "PCTLPathFormula.h"
+#include "PCTLStateFormula.h"
+#include "boost/integer/integer_mask.hpp"
 
 namespace mrmc {
 
@@ -62,7 +64,7 @@ class BoundedUntil : public PCTLPathFormula {
          std::string result = "(";
          result += left->toString();
          result += " U<=";
-         result += bound;
+         result +=  std::to_string(bound);
          result += " ";
          result += right->toString();
          result += ")";
diff --git a/src/parser/parser.h b/src/parser/parser.h
index f1b772040..584019b99 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -49,7 +49,7 @@ namespace parser {
 #if defined LINUX || defined MACOSX
 			int file;
 #elif defined WINDOWS
-			HFILE file;
+			HANDLE file;
 			HANDLE mapping;
 #endif
 			
@@ -110,7 +110,6 @@ namespace parser {
 			}
 			this->dataend = this->data + this->st.st_size;
 #elif defined WINDOWS
-#warning Windows support is implemented but has not been compiled yet...
 			/*
 			 *	Do file mapping for windows.
 			 *	_stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
@@ -121,14 +120,14 @@ namespace parser {
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
 			}
 			
-			this->file = CreateFile(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
+			this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
 			if (this->file == INVALID_HANDLE_VALUE)
 			{
 				pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFile()");
 			}
 			
-			this->mapping = CreateFileMapping(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
+			this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
 			if (this->mapping == NULL)
 			{
 				CloseHandle(this->file);
@@ -136,7 +135,7 @@ namespace parser {
 				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMapping()");
 			}
 			
-			this->data = MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size);
+			this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
 			if (this->data == NULL)
 			{
 				CloseHandle(this->mapping);
diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
index f910e8dce..01c44d420 100644
--- a/src/parser/readLabFile.cpp
+++ b/src/parser/readLabFile.cpp
@@ -20,7 +20,11 @@
 #include <errno.h>
 #include <time.h>
 #include <sys/stat.h>
-#include <sys/mman.h>
+#if defined LINUX || defined MACOSX
+	#include <sys/mman.h>
+#elif defined WINDOWS
+#define strncpy strncpy_s
+#endif
 #include <fcntl.h>
 #include <locale.h>
 
diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index 335699138..e5e58baf5 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -19,7 +19,10 @@
 #include <errno.h>
 #include <time.h>
 #include <sys/stat.h>
-#include <sys/mman.h>
+#if defined LINUX || defined MACOSX
+	#include <sys/mman.h>
+#elif defined WINDOWS
+#endif
 #include <fcntl.h>
 #include <locale.h>
 

From 93d568bd829308c4979df765df4ceebc98bbadfb Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 1 Dec 2012 20:04:06 +0100
Subject: [PATCH 13/17] working on prctl parser

---
 src/parser/readPrctlFile.cpp | 81 ++++++++++++++++++++++++++++++------
 src/parser/readPrctlFile.h   |  4 +-
 2 files changed, 72 insertions(+), 13 deletions(-)

diff --git a/src/parser/readPrctlFile.cpp b/src/parser/readPrctlFile.cpp
index 0453fc15f..737f6e61a 100644
--- a/src/parser/readPrctlFile.cpp
+++ b/src/parser/readPrctlFile.cpp
@@ -4,63 +4,120 @@
 
 #include <iostream>
 
+#include <map>
+//#include <pair>
+
 #include <boost/spirit/include/classic_core.hpp>
 #include <boost/spirit/include/qi_grammar.hpp>
+#include <boost/spirit/include/qi_rule.hpp>
 #include <boost/spirit/include/qi.hpp>
+#include <boost/spirit/include/phoenix_operator.hpp>
 #include <boost/spirit/include/qi_char_class.hpp>
 
+#include <boost/bind.hpp>
+
 namespace bs = boost::spirit;
 
 namespace
 {
+	using namespace bs;
 	using namespace bs::qi;
 	using namespace bs::standard;
 	
 	struct PRCTLParser : public grammar< char const* >
 	{
-		typedef rule< char const* > rule_t;
-	
+		typedef rule< char const* > rule_none;
+		typedef rule< char const*, double() > rule_double;
+		typedef rule< char const*, std::string() > rule_string;
+			
 		/*!
 		 *	@brief Generic Nonterminals.
 		 */
-		rule_t variable, value;
+		rule_none ws;
+		rule_string variable;
+		rule_double value;
 		
 		/*!
 		 *	@brief Nonterminals for file header.
 		 */
-		rule_t varDef, type;
+		rule< char const* > varDef;
+		rule_none type;
 		
 		/*!
 		 *	@brief Nonterminals for formula.
 		 */
-		rule_t formula, opP;
+		rule_none formula, opP;
 		
 		/*!
 		 *	@brief Nonterminals for high-level file structure.
 		 */
-		rule_t file, header;
+		rule_none file, header;
+		
+		/*!
+		 *	@brief Variable assignments.
+		 */
+		std::map<std::string, double> variables;
+		
+		/*!
+		 *	@brief Resulting formula.
+		 */
+		mrmc::formula::PCTLFormula* result;
+		
+		struct dump
+		{
+			void print(double const& i, std::string& s)
+			{
+				std::cout << s << " = " << i << std::endl;
+			}
+			void operator()(double const& a, unused_type, unused_type) const
+			{
+				std::cout << a << std::endl;
+			}
+			void operator()(std::string const& a, unused_type, unused_type) const
+			{
+				std::cout << a << std::endl;
+			}
+			void operator()(utree const& a, unused_type, unused_type) const
+			{
+				std::cout << &a << std::endl;
+			}
+		};
 	
 		PRCTLParser() : PRCTLParser::base_type(file, "PRCTL parser")
 		{
-			variable = alnum;
-			value = int_ | double_;
+			variable %= alnum;
+			ws = *( space );
+			value %= ( double_ | int_ ); // double_ must be *before* int_
 			type = string("int") | string("double");
-			varDef = string("const") >> type >> variable >> string("=") >> value >> string(";");
+			varDef = 
+				string("const") >> ws >> 
+				type >> ws >> 
+				variable >> ws >>
+				string("=") >> ws >>
+				value >> ws >>
+				string(";");
 			
-			header = *( varDef );
+			header = +( varDef >> ws );
 			
 			file = header;
 		}
+		
+		
 	};
 }
 
-void readPrctlFile(const char* filename)
+mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename)
 {
 	PRCTLParser p;
 	mrmc::parser::MappedFile file(filename);
 	
-	if (bs::qi::parse< char const* >(file.data, file.dataend, p))
+	char* data = file.data;
+	if (bs::qi::parse< char const* >(data, file.dataend, p))
 	{
 		std::cout << "File was parsed" << std::endl;
+		std::string rest(data, file.dataend);
+		std::cout << "Rest: " << rest << std::endl;
+		return p.result;
 	}
+	else return NULL;
 }
\ No newline at end of file
diff --git a/src/parser/readPrctlFile.h b/src/parser/readPrctlFile.h
index c7d508b18..c9f8ba470 100644
--- a/src/parser/readPrctlFile.h
+++ b/src/parser/readPrctlFile.h
@@ -1,13 +1,15 @@
 #ifndef READPRCTLFILE_H_
 #define READPRCTLFILE_H_
 
+#include "src/formula/PCTLformula.h"
+
 namespace mrmc {
 namespace parser {
 
 /*!
  *	@brief Load PRCTL file
  */
-void readPrctlFile(const char * filename);
+mrmc::formula::PCTLFormula* readPrctlFile(const char * filename);
 
 } // namespace parser
 } // namespace mrmc

From 82b502970ee59216f72302f7580866363e5de724 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 1 Dec 2012 20:29:24 +0100
Subject: [PATCH 14/17] patched tra parser, test cases work now

---
 src/parser/readTraFile.cpp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index e5e58baf5..7bb653da9 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -135,7 +135,7 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	uint_fast32_t maxnode;
 	uint_fast32_t non_zero = makeFirstPass(file.data, maxnode);
 	/*
-	 *	if first pass returned zer, the file format was wrong
+	 *	if first pass returned zero, the file format was wrong
 	 */
 	if (non_zero == 0) throw mrmc::exceptions::wrong_file_format();
 	
@@ -174,22 +174,29 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	/*
 	 *	read all transitions from file
 	 */
-	while (1)
+	while (buf[0] != '\0')
 	{
 		/*
 		 *	read row, col and value. if value == 0.0, we have reached the
 		 *	end of the file.
 		 */
 		row = strtol(buf, &buf, 10);
+		if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format();
+		
 		col = strtol(buf, &buf, 10);
+		if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format();
+		
 		val = strtod(buf, &buf);
+		if ((buf[0] != '\n') && (buf[0] != '\r')) throw mrmc::exceptions::wrong_file_format();
+		
 		if (val == 0.0) break;
 		pantheios::log_DEBUG("Write value ",
 							pantheios::real(val),
 							" to position ",
 							pantheios::integer(row), " x ",
 							pantheios::integer(col));
-		sp->addNextValue(row,col,val);	
+		sp->addNextValue(row,col,val);
+		buf = skipWS(buf);
 	}
 	
 	/*

From bb1dae23fc7af08b45f536d4dc842a531facaef8 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 1 Dec 2012 21:23:54 +0100
Subject: [PATCH 15/17] Lab and Tra parser pass test cases

Some more fixing, error handling and restructuring.
Both parsers now pass all test cases.
---
 src/parser/parser.h        | 35 ++++++++++++++-
 src/parser/readLabFile.cpp | 89 +++++++++++++++++++++++---------------
 src/parser/readLabFile.h   |  2 +-
 src/parser/readTraFile.cpp | 42 ++++++------------
 4 files changed, 103 insertions(+), 65 deletions(-)

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 584019b99..f66369bd2 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -18,13 +18,46 @@
 #include <sys/stat.h>
 #include <fcntl.h>
 #include <errno.h>
+#include <iostream>
 
 #include <pantheios/pantheios.hpp>
 #include "src/exceptions/file_IO_exception.h"
+#include "src/exceptions/wrong_file_format.h"
 
 namespace mrmc {
 namespace parser {
 	
+	/*!
+	 *	@brief Parses integer and checks, if something has been parsed.
+	 *
+	 *	Calls strtol() internally and checks if the new pointer is different
+	 *	from the original one, i.e. if str != *end. If they are the same, a
+	 *	mrmc::exceptions::wrong_file_format will be thrown.
+	 *	@param str String to parse
+	 *	@param end New pointer will be written there
+	 *	@return Result of strtol()
+	 */
+	inline uint_fast64_t checked_strtol(const char* str, char** end)
+	{
+		uint_fast64_t res = strtol(str, end, 10);
+		if (str == *end) throw mrmc::exceptions::wrong_file_format();
+		return res;
+	}
+	
+	/*!
+	 *	@brief Skips common whitespaces in a string.
+	 *
+	 *	Skips spaces, tabs, newlines and carriage returns. Returns pointer
+	 *	to first char that is not a whitespace.
+	 *	@param buf String buffer
+	 *	@return	pointer to first non-whitespace character
+	 */
+	inline char* skipWS(char* buf)
+	{
+		while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
+		return buf;
+	}
+	
 	/*!
 	 *	@brief Opens a file and maps it to memory providing a char*
 	 *	containing the file content.
@@ -79,7 +112,7 @@ namespace parser {
 		 *	Will stat the given file, open it and map it to memory.
 		 *	If anything of this fails, an appropriate exception is raised
 		 *	and a log entry is written.
-		 *	@filename file to be opened
+		 *	@param filename file to be opened
 		 */
 		MappedFile(const char* filename)
 		{
diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp
index 01c44d420..c9e6f2f12 100644
--- a/src/parser/readLabFile.cpp
+++ b/src/parser/readLabFile.cpp
@@ -43,7 +43,7 @@ namespace parser {
  *	@param filename   input .lab file's name.
  *	@return The pointer to the created labeling object.
  */
-mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename)
+mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename)
 {
 	/*
 	 *	open file
@@ -55,10 +55,14 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 	 *	first run: obtain number of propositions
 	 */
 	char separator[] = " \n\t";
+	bool foundDecl = false, foundEnd = false;
 	uint_fast32_t proposition_count = 0;
 	{
 		size_t cnt = 0;
-		do
+		/*
+		 *	iterate over tokens while not at end of file
+		 */
+		while(buf[0] != '\0')
 		{
 			buf += cnt;
 			cnt = strcspn(buf, separator); // position of next separator
@@ -69,12 +73,25 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 				 *	next token is #END: stop search
 				 *	otherwise increase proposition_count
 				 */
-				if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
-				if (strncmp(buf, "#END", cnt) == 0) break;
+				if (strncmp(buf, "#DECLARATION", cnt) == 0)
+				{
+					foundDecl = true;
+					continue;
+				}
+				if (strncmp(buf, "#END", cnt) == 0)
+				{
+					foundEnd = true;
+					break;
+				}
 				proposition_count++;
 			}
-			else cnt = 1; // next char is separator, one step forward
-		} while (cnt > 0);
+			else buf++; // next char is separator, one step forward
+		}
+		
+		/*
+		 *	If #DECLARATION or #END were not found, the file format is wrong
+		 */
+		if (! (foundDecl && foundEnd)) throw mrmc::exceptions::wrong_file_format();
 	}
 	
 	/*
@@ -91,6 +108,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 	{
 		/*
 		 *	load propositions
+		 *	As we already checked the file format, we can be a bit sloppy here...
 		 */
 		char proposition[128]; // buffer for proposition names
 		size_t cnt = 0;
@@ -126,40 +144,43 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
 		 */
 		uint_fast32_t node;
 		char proposition[128];
+		char* tmp;
 		size_t cnt;
-		do
+		/*
+		 *	iterate over nodes
+		 */
+		while (buf[0] != '\0')
 		{
-			node = strtol(buf, &buf, 10); // parse node number
-			while (*buf != '\0') // while not at end of file
-			{
-				cnt = strcspn(buf, separator); // position of next separator
-				if (cnt == 0) buf++; // next char is separator, one step forward
-				else break;
-			}
 			/*
-			 *	if cnt > 0, buf points to the next proposition
-			 *	otherwise, we have reached the end of the file
+			 *	parse node number, then iterate over propositions
 			 */
-			if (cnt > 0)
-			{
-				/*
-				 *	copy proposition to buffer, add assignment to labeling
-				 */
-				strncpy(proposition, buf, cnt);
-				proposition[cnt] = '\0';
-				result->addAtomicPropositionToState(proposition, node);
-			}
-			else if (node == 0)
+			node = checked_strtol(buf, &buf);
+			while (buf[0] != '\n') 
 			{
-				/*
-				 *	If this is executed, we could read a number but there
-				 *	was no proposition after that. This strongly suggests a
-				 *	broken file, but it's not fatal...
-				 */
-				 pantheios::log_WARNING("The label file ended on a node number. Is the file malformated?");
+				cnt = strcspn(buf, separator);
+				if (cnt == 0)
+				{
+					/*
+					 *	next char is a separator
+					 *	if it's a newline, we continue with next node
+					 *	otherwise we skip it and try again
+					 */
+					if (buf[0] == '\n') break;
+					buf++;
+				}
+				else
+				{
+					/*
+					 *	copy proposition to buffer and add it to result
+					 */
+					strncpy(proposition, buf, cnt);
+					proposition[cnt] = '\0';
+					result->addAtomicPropositionToState(proposition, node);
+					buf += cnt;
+				}
 			}
-			buf += cnt;
-		} while (cnt > 0);
+			buf = skipWS(buf);
+		}
 	}
 	
 	return result;
diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h
index 31375ced8..625bd5685 100644
--- a/src/parser/readLabFile.h
+++ b/src/parser/readLabFile.h
@@ -10,7 +10,7 @@ namespace parser {
 /*!
  *	@brief Load label file and return initialized AtomicPropositionsLabeling object.
  */
-mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename);
+mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename);
 
 } // namespace parser
 } // namespace mrmc
diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp
index 7bb653da9..6130c9751 100644
--- a/src/parser/readTraFile.cpp
+++ b/src/parser/readTraFile.cpp
@@ -33,20 +33,6 @@
 namespace mrmc {
 namespace parser{
 
-/*!
- *	Skips all whitespaces and returns new pointer.
- *
- *	@todo	should probably be replaced by strspn et.al.
- */
-char* skipWS(char* buf)
-{
-	while(1)
-	{
-		if ((buf[0] != ' ') && (buf[0] != '\t') && (buf[0] != '\n') && (buf[0] != '\r')) return buf;
-		buf++;
-	}
-}
-
 /*!
  *	@brief	Perform first pass through the file and obtain number of
  *	non-zero cells and maximum node id.
@@ -83,13 +69,13 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 	uint_fast32_t row, col;
 	double val;
 	maxnode = 0;
-	while (1)  
+	while (buf[0] != '\0')
 	{
 		/*
 		 *	read row and column
 		 */
-		row = strtol(buf, &buf, 10);
-		col = strtol(buf, &buf, 10);
+		row = checked_strtol(buf, &buf);
+		col = checked_strtol(buf, &buf);
 		/*
 		 *	check if one is larger than the current maximum id
 		 */
@@ -102,6 +88,7 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
 		val = strtod(buf, &buf);
 		if (val == 0.0) break;
 		if (row == col) non_zero--;
+		buf = skipWS(buf);
 	}
 
 	return non_zero;
@@ -150,10 +137,10 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	 *	read file header, extract number of states
 	 */
 	buf += 7; // skip "STATES "
-	strtol(buf, &buf, 10);
+	checked_strtol(buf, &buf);
 	buf = skipWS(buf);
 	buf += 12; // skip "TRANSITIONS "
-	strtol(buf, &buf, 10);
+	checked_strtol(buf, &buf);
 	
 	pantheios::log_DEBUG("Creating matrix with ",
                         pantheios::integer(maxnode + 1), " maxnodes and ",
@@ -177,19 +164,16 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
 	while (buf[0] != '\0')
 	{
 		/*
-		 *	read row, col and value. if value == 0.0, we have reached the
-		 *	end of the file.
+		 *	read row, col and value.
 		 */
-		row = strtol(buf, &buf, 10);
-		if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format();
-		
-		col = strtol(buf, &buf, 10);
-		if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format();
-		
+		row = checked_strtol(buf, &buf);
+		col = checked_strtol(buf, &buf);
 		val = strtod(buf, &buf);
-		if ((buf[0] != '\n') && (buf[0] != '\r')) throw mrmc::exceptions::wrong_file_format();
 		
-		if (val == 0.0) break;
+		/*
+		 *	only values in (0, 1] are meaningful
+		 */
+		if ((val <= 0.0) || (val > 1.0)) throw mrmc::exceptions::wrong_file_format();
 		pantheios::log_DEBUG("Write value ",
 							pantheios::real(val),
 							" to position ",

From 9156fa6d6199a124a5f61a5238919e3930a3cd1e Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 1 Dec 2012 22:04:49 +0100
Subject: [PATCH 16/17] moving implementation of MappedFile and helper
 functions to .cpp

---
 src/parser/parser.cpp | 128 ++++++++++++++++++++++++++++++++++++++++++
 src/parser/parser.h   | 109 ++---------------------------------
 2 files changed, 132 insertions(+), 105 deletions(-)
 create mode 100644 src/parser/parser.cpp

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
new file mode 100644
index 000000000..fd075da59
--- /dev/null
+++ b/src/parser/parser.cpp
@@ -0,0 +1,128 @@
+#include "src/parser/parser.h"
+
+#if defined LINUX || defined MACOSX
+	#include <sys/mman.h>
+#elif defined WINDOWS
+#endif
+
+#include <sys/stat.h>
+#include <fcntl.h>
+#include <errno.h>
+#include <iostream>
+
+#include <pantheios/pantheios.hpp>
+#include "src/exceptions/file_IO_exception.h"
+#include "src/exceptions/wrong_file_format.h"
+
+/*!
+ *	Calls strtol() internally and checks if the new pointer is different
+ *	from the original one, i.e. if str != *end. If they are the same, a
+ *	mrmc::exceptions::wrong_file_format will be thrown.
+ *	@param str String to parse
+ *	@param end New pointer will be written there
+ *	@return Result of strtol()
+ */
+uint_fast64_t mrmc::parser::checked_strtol(const char* str, char** end)
+{
+	uint_fast64_t res = strtol(str, end, 10);
+	if (str == *end) throw mrmc::exceptions::wrong_file_format();
+	return res;
+}
+
+/*!
+ *	Skips spaces, tabs, newlines and carriage returns. Returns pointer
+ *	to first char that is not a whitespace.
+ *	@param buf String buffer
+ *	@return	pointer to first non-whitespace character
+ */
+char* mrmc::parser::skipWS(char* buf)
+{
+	while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
+	return buf;
+}
+	
+/*!
+ *	Will stat the given file, open it and map it to memory.
+ *	If anything of this fails, an appropriate exception is raised
+ *	and a log entry is written.
+ *	@param filename file to be opened
+ */
+mrmc::parser::MappedFile::MappedFile(const char* filename)
+{
+#if defined LINUX || defined MACOSX
+	/*
+	 *	Do file mapping for reasonable systems.
+	 *	stat64(), open(), mmap()
+	 */
+	if (stat64(filename, &(this->st)) != 0)
+	{
+		pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
+	}
+	this->file = open(filename, O_RDONLY);
+
+	if (this->file < 0)
+	{
+		pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in open()");
+	}
+			
+	this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, this->file, 0);
+	if (this->data == (char*)-1)
+	{
+		close(this->file);
+		pantheios::log_ERROR("Could not mmap ", filename, ".");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()");
+	}
+	this->dataend = this->data + this->st.st_size;
+#elif defined WINDOWS
+	/*
+	 *	Do file mapping for windows.
+	 *	_stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
+	 */
+	if (_stat64(filename, &(this->st)) != 0)
+	{
+		pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
+	}
+		
+	this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
+	if (this->file == INVALID_HANDLE_VALUE)
+	{
+		pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFile()");
+	}
+			
+	this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
+	if (this->mapping == NULL)
+	{
+		CloseHandle(this->file);
+		pantheios::log_ERROR("Could not create file mapping for ", filename, ".");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMapping()");
+	}
+			
+	this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
+	if (this->data == NULL)
+	{
+		CloseHandle(this->mapping);
+		CloseHandle(this->file);
+		pantheios::log_ERROR("Could not create file map view for ", filename, ".");
+		throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in MapViewOfFile()");
+	}
+	this->dataend = this->data + this->st.st_size;
+#endif
+}
+		
+/*!
+ *	Will unmap the data and close the file.
+ */
+mrmc::parser::MappedFile::~MappedFile()
+{
+#if defined LINUX || defined MACOSX
+	munmap(this->data, this->st.st_size);
+	close(this->file);
+#elif defined WINDOWS
+	CloseHandle(this->mapping);
+	CloseHandle(this->file);
+#endif
+}
diff --git a/src/parser/parser.h b/src/parser/parser.h
index f66369bd2..d3777108c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -29,34 +29,13 @@ namespace parser {
 	
 	/*!
 	 *	@brief Parses integer and checks, if something has been parsed.
-	 *
-	 *	Calls strtol() internally and checks if the new pointer is different
-	 *	from the original one, i.e. if str != *end. If they are the same, a
-	 *	mrmc::exceptions::wrong_file_format will be thrown.
-	 *	@param str String to parse
-	 *	@param end New pointer will be written there
-	 *	@return Result of strtol()
 	 */
-	inline uint_fast64_t checked_strtol(const char* str, char** end)
-	{
-		uint_fast64_t res = strtol(str, end, 10);
-		if (str == *end) throw mrmc::exceptions::wrong_file_format();
-		return res;
-	}
+	uint_fast64_t checked_strtol(const char* str, char** end);
 	
 	/*!
 	 *	@brief Skips common whitespaces in a string.
-	 *
-	 *	Skips spaces, tabs, newlines and carriage returns. Returns pointer
-	 *	to first char that is not a whitespace.
-	 *	@param buf String buffer
-	 *	@return	pointer to first non-whitespace character
 	 */
-	inline char* skipWS(char* buf)
-	{
-		while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
-		return buf;
-	}
+	char* skipWS(char* buf);
 	
 	/*!
 	 *	@brief Opens a file and maps it to memory providing a char*
@@ -108,93 +87,13 @@ namespace parser {
 		
 		/*!
 		 *	@brief Constructor of MappedFile.
-		 *	
-		 *	Will stat the given file, open it and map it to memory.
-		 *	If anything of this fails, an appropriate exception is raised
-		 *	and a log entry is written.
-		 *	@param filename file to be opened
 		 */
-		MappedFile(const char* filename)
-		{
-#if defined LINUX || defined MACOSX
-			/*
-			 *	Do file mapping for reasonable systems.
-			 *	stat64(), open(), mmap()
-			 */
-			if (stat64(filename, &(this->st)) != 0)
-			{
-				pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
-			}
-
-			this->file = open(filename, O_RDONLY);
-			if (this->file < 0)
-			{
-				pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in open()");
-			}
-			
-			this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, this->file, 0);
-			if (this->data == (char*)-1)
-			{
-				close(this->file);
-				pantheios::log_ERROR("Could not mmap ", filename, ".");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()");
-			}
-			this->dataend = this->data + this->st.st_size;
-#elif defined WINDOWS
-			/*
-			 *	Do file mapping for windows.
-			 *	_stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
-			 */
-			if (_stat64(filename, &(this->st)) != 0)
-			{
-				pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()");
-			}
-			
-			this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
-			if (this->file == INVALID_HANDLE_VALUE)
-			{
-				pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFile()");
-			}
-			
-			this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
-			if (this->mapping == NULL)
-			{
-				CloseHandle(this->file);
-				pantheios::log_ERROR("Could not create file mapping for ", filename, ".");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMapping()");
-			}
-			
-			this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
-			if (this->data == NULL)
-			{
-				CloseHandle(this->mapping);
-				CloseHandle(this->file);
-				pantheios::log_ERROR("Could not create file map view for ", filename, ".");
-				throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in MapViewOfFile()");
-			}
-			this->dataend = this->data + this->st.st_size;
-#endif
-		}
+		MappedFile(const char* filename);
 		
 		/*!
 		 *	@brief Destructor of MappedFile.
-		 *	
-		 *	Will unmap the data and close the file.
 		 */
-		~MappedFile()
-		{
-#if defined LINUX || defined MACOSX
-			munmap(this->data, this->st.st_size);
-			close(this->file);
-#elif defined WINDOWS
-			CloseHandle(this->mapping);
-			CloseHandle(this->file);
-#endif
-		}
+		~MappedFile();
 	};
 
 } // namespace parser

From 7e9ba03ec65954b8dda6f16093553b07b37c5eda Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 1 Dec 2012 22:06:36 +0100
Subject: [PATCH 17/17] added boost header for uint_fastX types

---
 src/parser/readLabFile.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h
index 625bd5685..afd575f2d 100644
--- a/src/parser/readLabFile.h
+++ b/src/parser/readLabFile.h
@@ -2,6 +2,7 @@
 #define READLABFILE_H_
 
 #include "src/models/atomic_propositions_labeling.h"
+#include "boost/integer/integer_mask.hpp"
 
 
 namespace mrmc {