From d743e222f71d7b0aaea5fb12f9b43ce2caa0f8c5 Mon Sep 17 00:00:00 2001 From: PBerger Date: Fri, 20 Sep 2013 15:55:31 +0200 Subject: [PATCH] Refactored ltl2ba to compile under windows Added a CMakeLists.txt for ltl2ba Former-commit-id: 47a102e0ce7cc1bdbcbce721cb27ee6217af945d --- resources/3rdparty/ltl2ba-1.1/CMakeLists.txt | 20 +++++++++++++++ .../3rdparty/ltl2ba-1.1/{ => src}/LICENSE | 0 .../3rdparty/ltl2ba-1.1/{ => src}/Makefile | 0 .../3rdparty/ltl2ba-1.1/{ => src}/README | 0 .../ltl2ba-1.1/{ => src}/alternating.c | 7 +++++- .../3rdparty/ltl2ba-1.1/{ => src}/buchi.c | 17 ++++++++++--- .../3rdparty/ltl2ba-1.1/{ => src}/cache.c | 0 .../ltl2ba-1.1/{ => src}/generalized.c | 20 ++++++++++++--- resources/3rdparty/ltl2ba-1.1/{ => src}/lex.c | 0 .../3rdparty/ltl2ba-1.1/{ => src}/ltl2ba.h | 25 ++++++++++++++++--- .../3rdparty/ltl2ba-1.1/{ => src}/main.c | 3 ++- resources/3rdparty/ltl2ba-1.1/{ => src}/mem.c | 0 .../3rdparty/ltl2ba-1.1/{ => src}/parse.c | 0 .../3rdparty/ltl2ba-1.1/{ => src}/rewrt.c | 0 resources/3rdparty/ltl2ba-1.1/{ => src}/set.c | 0 .../3rdparty/ltl2ba-1.1/{ => src}/trans.c | 0 16 files changed, 80 insertions(+), 12 deletions(-) create mode 100644 resources/3rdparty/ltl2ba-1.1/CMakeLists.txt rename resources/3rdparty/ltl2ba-1.1/{ => src}/LICENSE (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/Makefile (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/README (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/alternating.c (99%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/buchi.c (99%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/cache.c (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/generalized.c (98%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/lex.c (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/ltl2ba.h (95%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/main.c (99%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/mem.c (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/parse.c (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/rewrt.c (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/set.c (100%) rename resources/3rdparty/ltl2ba-1.1/{ => src}/trans.c (100%) diff --git a/resources/3rdparty/ltl2ba-1.1/CMakeLists.txt b/resources/3rdparty/ltl2ba-1.1/CMakeLists.txt new file mode 100644 index 000000000..0d7c73f99 --- /dev/null +++ b/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}) diff --git a/resources/3rdparty/ltl2ba-1.1/LICENSE b/resources/3rdparty/ltl2ba-1.1/src/LICENSE similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/LICENSE rename to resources/3rdparty/ltl2ba-1.1/src/LICENSE diff --git a/resources/3rdparty/ltl2ba-1.1/Makefile b/resources/3rdparty/ltl2ba-1.1/src/Makefile similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/Makefile rename to resources/3rdparty/ltl2ba-1.1/src/Makefile diff --git a/resources/3rdparty/ltl2ba-1.1/README b/resources/3rdparty/ltl2ba-1.1/src/README similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/README rename to resources/3rdparty/ltl2ba-1.1/src/README diff --git a/resources/3rdparty/ltl2ba-1.1/alternating.c b/resources/3rdparty/ltl2ba-1.1/src/alternating.c similarity index 99% rename from resources/3rdparty/ltl2ba-1.1/alternating.c rename to resources/3rdparty/ltl2ba-1.1/src/alternating.c index 2dc947a53..74025d8ef 100644 --- a/resources/3rdparty/ltl2ba-1.1/alternating.c +++ b/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); } diff --git a/resources/3rdparty/ltl2ba-1.1/buchi.c b/resources/3rdparty/ltl2ba-1.1/src/buchi.c similarity index 99% rename from resources/3rdparty/ltl2ba-1.1/buchi.c rename to resources/3rdparty/ltl2ba-1.1/src/buchi.c index fe1f80ee5..7ef18326e 100644 --- a/resources/3rdparty/ltl2ba-1.1/buchi.c +++ b/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) { - getrusage(RUSAGE_SELF, &tr_fin); +#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); } @@ -548,8 +555,10 @@ void mk_buchi() GTrans *t; 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); } diff --git a/resources/3rdparty/ltl2ba-1.1/cache.c b/resources/3rdparty/ltl2ba-1.1/src/cache.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/cache.c rename to resources/3rdparty/ltl2ba-1.1/src/cache.c diff --git a/resources/3rdparty/ltl2ba-1.1/generalized.c b/resources/3rdparty/ltl2ba-1.1/src/generalized.c similarity index 98% rename from resources/3rdparty/ltl2ba-1.1/generalized.c rename to resources/3rdparty/ltl2ba-1.1/src/generalized.c index 6a37fe23f..8200c4207 100644 --- a/resources/3rdparty/ltl2ba-1.1/generalized.c +++ b/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) { - getrusage(RUSAGE_SELF, &tr_fin); +#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) { - getrusage(RUSAGE_SELF, &tr_fin); +#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); } diff --git a/resources/3rdparty/ltl2ba-1.1/lex.c b/resources/3rdparty/ltl2ba-1.1/src/lex.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/lex.c rename to resources/3rdparty/ltl2ba-1.1/src/lex.c diff --git a/resources/3rdparty/ltl2ba-1.1/ltl2ba.h b/resources/3rdparty/ltl2ba-1.1/src/ltl2ba.h similarity index 95% rename from resources/3rdparty/ltl2ba-1.1/ltl2ba.h rename to resources/3rdparty/ltl2ba-1.1/src/ltl2ba.h index 0987643cb..e28c694e7 100644 --- a/resources/3rdparty/ltl2ba-1.1/ltl2ba.h +++ b/resources/3rdparty/ltl2ba-1.1/src/ltl2ba.h @@ -33,8 +33,21 @@ #include #include #include -#include -#include +#ifdef WIN32 +# include +# define NOMINMAX + +# undef TRUE +# undef FALSE +# undef OR +# undef AND + +#define unlink _unlink + +#else +# include +# include +#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); } } -#define min(x,y) ((xtv_sec < y->tv_sec; } +#endif static void tl_endstats(void) diff --git a/resources/3rdparty/ltl2ba-1.1/mem.c b/resources/3rdparty/ltl2ba-1.1/src/mem.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/mem.c rename to resources/3rdparty/ltl2ba-1.1/src/mem.c diff --git a/resources/3rdparty/ltl2ba-1.1/parse.c b/resources/3rdparty/ltl2ba-1.1/src/parse.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/parse.c rename to resources/3rdparty/ltl2ba-1.1/src/parse.c diff --git a/resources/3rdparty/ltl2ba-1.1/rewrt.c b/resources/3rdparty/ltl2ba-1.1/src/rewrt.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/rewrt.c rename to resources/3rdparty/ltl2ba-1.1/src/rewrt.c diff --git a/resources/3rdparty/ltl2ba-1.1/set.c b/resources/3rdparty/ltl2ba-1.1/src/set.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/set.c rename to resources/3rdparty/ltl2ba-1.1/src/set.c diff --git a/resources/3rdparty/ltl2ba-1.1/trans.c b/resources/3rdparty/ltl2ba-1.1/src/trans.c similarity index 100% rename from resources/3rdparty/ltl2ba-1.1/trans.c rename to resources/3rdparty/ltl2ba-1.1/src/trans.c