Refactored ltl2ba to compile under windows

Added a CMakeLists.txt for ltl2ba


Former-commit-id: 47a102e0ce

resources/3rdparty/ltl2ba-1.1/CMakeLists.txt

@@ -0,0 +1,20 @@
+cmake_minimum_required (VERSION 2.8.6)
+
+# Set project name
+project (ltl2ba CXX C)
+
+# Main Sources
+file(GLOB_RECURSE LTL2BA_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h)
+file(GLOB_RECURSE LTL2BA_SOURCES ${PROJECT_SOURCE_DIR}/src/*.c)
+
+
+# Add base folder for better inclusion paths
+include_directories("${PROJECT_SOURCE_DIR}/src")
+
+if(MSVC)
+	# required for GMM to compile, ugly error directive in their code
+	add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS)
+endif()
+
+# Add the executables
+add_executable(ltl2ba ${LTL2BA_SOURCES} ${LTL2BA_HEADERS})

resources/3rdparty/ltl2ba-1.1/alternating.c → resources/3rdparty/ltl2ba-1.1/src/alternating.c

@@ -39,8 +39,10 @@ extern int tl_verbose, tl_stats, tl_simp_diff;
 Node **label;
 char **sym_table;
 ATrans **transition;
+#ifndef WIN32
 struct rusage tr_debut, tr_fin;
 struct timeval t_diff;
+#endif
 int *final_set, node_id = 1, sym_id = 0, node_size, sym_size;
 int astate_count = 0, atrans_count = 0;
 
@@ -403,7 +405,9 @@ void print_alternating() /* dumps the alternating automaton */
 
 void mk_alternating(Node *p) /* generates an alternating automaton for p */
 {
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   node_size = calculate_node_size(p) + 1; /* number of states in the automaton */
   label = (Node **) tl_emalloc(node_size * sizeof(Node *));
@@ -431,13 +435,14 @@ void mk_alternating(Node *p) /* generates an alternating automaton for p */
   }
   
   if(tl_stats) {
+#ifndef WIN32
     getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nBuilding and simplification of the alternating automaton: %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i states, %i transitions\n", astate_count, atrans_count);
   }
-
   releasenode(1, p);
   tfree(label);
 }

resources/3rdparty/ltl2ba-1.1/buchi.c → resources/3rdparty/ltl2ba-1.1/src/buchi.c

@@ -82,8 +82,9 @@ int simplify_btrans() /* simplifies the transitions */
   BState *s;
   BTrans *t, *t1;
   int changed = 0;
-
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   for (s = bstates->nxt; s != bstates; s = s->nxt)
     for (t = s->trans->nxt; t != s->trans;) {
@@ -108,10 +109,12 @@ int simplify_btrans() /* simplifies the transitions */
     }
       
   if(tl_stats) {
+#ifndef WIN32
 	getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nSimplification of the Buchi automaton - transitions: %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i transitions removed\n", changed);
 
   }
@@ -200,7 +203,9 @@ int simplify_bstates() /* eliminates redundant states */
   BState *s, *s1;
   int changed = 0;
 
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   for (s = bstates->nxt; s != bstates; s = s->nxt) {
     if(s->trans == s->trans->nxt) { /* s has no transitions */
@@ -223,10 +228,12 @@ int simplify_bstates() /* eliminates redundant states */
   retarget_all_btrans();
 
   if(tl_stats) {
+#ifndef WIN32
     getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nSimplification of the Buchi automaton - states: %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i states removed\n", changed);
   }
 
@@ -549,7 +556,9 @@ void mk_buchi()
   BTrans *t1;
   accept = final[0] - 1;
 
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   bstack        = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */
   bstack->nxt   = bstack;
@@ -618,10 +627,12 @@ void mk_buchi()
   retarget_all_btrans();
 
   if(tl_stats) {
+#ifndef WIN32
     getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nBuilding the Buchi automaton : %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i states, %i transitions\n", bstate_count, btrans_count);
   }
 

resources/3rdparty/ltl2ba-1.1/generalized.c → resources/3rdparty/ltl2ba-1.1/src/generalized.c

@@ -35,8 +35,10 @@
 
 extern FILE *tl_out;
 extern ATrans **transition;
+#ifndef WIN32
 extern struct rusage tr_debut, tr_fin;
 extern struct timeval t_diff;
+#endif
 extern int tl_verbose, tl_stats, tl_simp_diff, tl_simp_fly, tl_fjtofj,
   tl_simp_scc, *final_set, node_id;
 extern char **sym_table;
@@ -118,7 +120,9 @@ int simplify_gtrans() /* simplifies the transitions */
   GState *s;
   GTrans *t, *t1;
 
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   for(s = gstates->nxt; s != gstates; s = s->nxt) {
     t = s->trans->nxt;
@@ -149,10 +153,12 @@ int simplify_gtrans() /* simplifies the transitions */
   }
   
   if(tl_stats) {
+#ifndef WIN32
 	  getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - transitions: %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i transitions removed\n", changed);
   }
 
@@ -218,8 +224,9 @@ int simplify_gstates() /* eliminates redundant states */
 {
   int changed = 0;
   GState *a, *b;
-
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   for(a = gstates->nxt; a != gstates; a = a->nxt) {
     if(a->trans == a->trans->nxt) { /* a has no transitions */
@@ -242,10 +249,12 @@ int simplify_gstates() /* eliminates redundant states */
   retarget_all_gtrans();
 
   if(tl_stats) {
+#ifndef WIN32
 	getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - states: %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i states removed\n", changed);
   }
 
@@ -571,8 +580,9 @@ void mk_generalized()
   ATrans *t;
   GState *s;
   int i;
-
+#ifndef WIN32
   if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
+#endif
 
   fin = new_set(0);
   bad_scc = 0; /* will be initialized in simplify_gscc */
@@ -616,10 +626,12 @@ void mk_generalized()
   retarget_all_gtrans();
 
   if(tl_stats) {
+#ifndef WIN32
     getrusage(RUSAGE_SELF, &tr_fin);
     timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
     fprintf(tl_out, "\nBuilding the generalized Buchi automaton : %i.%06is",
 		t_diff.tv_sec, t_diff.tv_usec);
+#endif
     fprintf(tl_out, "\n%i states, %i transitions\n", gstate_count, gtrans_count);
   }
 

resources/3rdparty/ltl2ba-1.1/ltl2ba.h → resources/3rdparty/ltl2ba-1.1/src/ltl2ba.h

@@ -33,8 +33,21 @@
 #include <stdio.h>
 #include <string.h>
 #include <stdlib.h>
+#ifdef WIN32
+#	include <time.h>
+#	define NOMINMAX
+
+#	undef TRUE
+#	undef FALSE
+#	undef OR
+#	undef AND
+
+#define unlink _unlink
+
+#else
 #	include <sys/time.h>
 #	include <sys/resource.h>
+#endif
 
 typedef struct Symbol {
 char		*name;
@@ -186,7 +199,9 @@ void	a_stats(void);
 void	addtrans(Graph *, char *, Node *, char *);
 void	cache_stats(void);
 void	dump(Node *);
+#ifndef WIN32
 void	exit(int);
+#endif
 void	Fatal(char *, char *);
 void	fatal(char *, char *);
 void	fsm_print(void);
@@ -225,7 +240,9 @@ int  included_set(int *, int *, int);
 int  in_set(int *, int);
 int  *list_set(int *, int);
 
+#ifndef WIN32
 int timeval_subtract (struct timeval *, struct timeval *, struct timeval *);
+#endif
 
 #define ZN	(Node *)0
 #define ZS	(Symbol *)0
@@ -245,4 +262,6 @@ typedef Node	*Nodeptr;
 
 #define Assert(x, y)	{ if (!(x)) { tl_explain(y); \
 			  Fatal(": assertion failed\n",(char *)0); } }
+#ifndef WIN32
 #	define min(x,y)        ((x<y)?x:y)
+#endif

resources/3rdparty/ltl2ba-1.1/main.c → resources/3rdparty/ltl2ba-1.1/src/main.c

@@ -209,7 +209,7 @@ main(int argc, char *argv[])
 
 /* Subtract the `struct timeval' values X and Y, storing the result X-Y in RESULT.
    Return 1 if the difference is negative, otherwise 0.  */
- 
+#ifndef WIN32
 int
 timeval_subtract (result, x, y)
 struct timeval *result, *x, *y;
@@ -226,6 +226,7 @@ struct timeval *result, *x, *y;
 	/* Return 1 if result is negative. */
 	return x->tv_sec < y->tv_sec;
 }
+#endif
 
 static void
 tl_endstats(void)