From f796e5ca6fba1c8c545dc3e8bd39a5739acc6c9a Mon Sep 17 00:00:00 2001 From: Michael Weber Date: Sun, 28 Nov 2010 21:46:18 +0100 Subject: [PATCH] Make libltl2ba.la self-contained Moved all globals accessed outside of main.c to util.c. Library must be initialized by calling ltl2ba_init(). Fixed bug: appending never claim to a file --- Makefile.am | 1 + ltl2ba.h | 21 +++++ main.c | 229 ++++++---------------------------------------------- util.c | 216 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 263 insertions(+), 204 deletions(-) create mode 100644 util.c diff --git a/Makefile.am b/Makefile.am index c75bf9d..4b606d8 100644 --- a/Makefile.am +++ b/Makefile.am @@ -18,6 +18,7 @@ libltl2ba_la_SOURCES += rewrt.c libltl2ba_la_SOURCES += cache.c libltl2ba_la_SOURCES += alternating.c libltl2ba_la_SOURCES += generalized.c +libltl2ba_la_SOURCES += util.c libltl2ba_la_SOURCES += ltl2ba.h # make diff --git a/ltl2ba.h b/ltl2ba.h index 0987643..6479d9d 100644 --- a/ltl2ba.h +++ b/ltl2ba.h @@ -246,3 +246,24 @@ typedef Node *Nodeptr; #define Assert(x, y) { if (!(x)) { tl_explain(y); \ Fatal(": assertion failed\n",(char *)0); } } #define min(x,y) ((x +#include +#include + #include "ltl2ba.h" -FILE *tl_out; - -int tl_stats = 0; /* time and size stats */ -int tl_simp_log = 1; /* logical simplification */ -int tl_simp_diff = 1; /* automata simplification */ -int tl_simp_fly = 1; /* on the fly simplification */ -int tl_simp_scc = 1; /* use scc simplification */ -int tl_fjtofj = 1; /* 2eme fj */ -int tl_errs = 0; -int tl_verbose = 0; -int tl_terse = 0; -unsigned long All_Mem = 0; - -static char uform[4096]; -static int hasuform=0, cnt=0; static char **ltl_file = (char **)0; static char **add_ltl = (char **)0; -static char out1[64]; static void tl_endstats(void); -static void non_fatal(char *, char *); +static const char *outfile; void -alldone(int estatus) +cleanup() { - if (strlen(out1) > 0) - (void) unlink((const char *)out1); - exit(estatus); + if (outfile != NULL) { + unlink (outfile); + } } FILE * -cpyfile(char *src, char *tgt) +cpyfile(const char *src, const char *tgt) { FILE *inp, *out; char buf[1024]; @@ -79,37 +68,6 @@ cpyfile(char *src, char *tgt) return out; } -char * -emalloc(int n) -{ char *tmp; - - if (!(tmp = (char *) malloc(n))) - fatal("not enough memory", (char *)0); - memset(tmp, 0, n); - return tmp; -} - -int -tl_Getchar(void) -{ - if (cnt < hasuform) - return uform[cnt++]; - cnt++; - return -1; -} - -void -put_uform(void) -{ - fprintf(tl_out, "%s", uform); -} - -void -tl_UnGetchar(void) -{ - if (cnt > 0) cnt--; -} - void usage(void) { @@ -133,6 +91,7 @@ usage(void) int tl_main(int argc, char *argv[]) { int i; + int hasuform = 0; while (argc > 1 && argv[1][0] == '-') { switch (argv[1][1]) { case 'f': argc--; argv++; @@ -142,8 +101,7 @@ tl_main(int argc, char *argv[]) || argv[1][i] == '\n') argv[1][i] = ' '; } - strcpy(uform, argv[1]); - hasuform = strlen(uform); + hasuform = set_uform(argv[1]); break; default : usage(); } @@ -157,9 +115,9 @@ tl_main(int argc, char *argv[]) int main(int argc, char *argv[]) -{ int i; - tl_out = stdout; - +{ ltl2ba_init(); + tl_out = stdout; + atexit(cleanup); while (argc > 1 && argv[1][0] == '-') { switch (argv[1][1]) { case 'F': ltl_file = (char **) (argv+2); @@ -193,164 +151,27 @@ main(int argc, char *argv[]) *ltl_file = (char *) formula; } if (argc > 1) - { char cmd[128], out2[64]; - strcpy(out1, "_tmp1_"); - strcpy(out2, "_tmp2_"); - tl_out = cpyfile(argv[1], out2); + { outfile = "_tmp2_"; + tl_out = cpyfile(argv[1], outfile); tl_main(2, add_ltl); fclose(tl_out); + if (rename(outfile, argv[1]) != 0) { + perror("rename"); + alldone(1); + } + outfile = NULL; } else { if (argc > 0) exit(tl_main(2, add_ltl)); usage(); } -} - -/* Subtract the `struct timeval' values X and Y, storing the result X-Y in RESULT. - Return 1 if the difference is negative, otherwise 0. */ - -int -timeval_subtract (result, x, y) -struct timeval *result, *x, *y; -{ - if (x->tv_usec < y->tv_usec) { - x->tv_usec += 1000000; - x->tv_sec--; - } - - /* Compute the time remaining to wait. tv_usec is certainly positive. */ - result->tv_sec = x->tv_sec - y->tv_sec; - result->tv_usec = x->tv_usec - y->tv_usec; - - /* Return 1 if result is negative. */ - return x->tv_sec < y->tv_sec; + exit (EXIT_SUCCESS); } static void tl_endstats(void) -{ extern int Stack_mx; - printf("\ntotal memory used: %9ld\n", All_Mem); - /*printf("largest stack sze: %9d\n", Stack_mx);*/ +{ printf("\ntotal memory used: %9ld\n", All_Mem); /*cache_stats();*/ a_stats(); } - -#define Binop(a) \ - fprintf(tl_out, "("); \ - dump(n->lft); \ - fprintf(tl_out, a); \ - dump(n->rgt); \ - fprintf(tl_out, ")") - -void -dump(Node *n) -{ - if (!n) return; - - switch(n->ntyp) { - case OR: Binop(" || "); break; - case AND: Binop(" && "); break; - case U_OPER: Binop(" U "); break; - case V_OPER: Binop(" V "); break; -#ifdef NXT - case NEXT: - fprintf(tl_out, "X"); - fprintf(tl_out, " ("); - dump(n->lft); - fprintf(tl_out, ")"); - break; -#endif - case NOT: - fprintf(tl_out, "!"); - fprintf(tl_out, " ("); - dump(n->lft); - fprintf(tl_out, ")"); - break; - case FALSE: - fprintf(tl_out, "false"); - break; - case TRUE: - fprintf(tl_out, "true"); - break; - case PREDICATE: - fprintf(tl_out, "(%s)", n->sym->name); - break; - case -1: - fprintf(tl_out, " D "); - break; - default: - printf("Unknown token: "); - tl_explain(n->ntyp); - break; - } -} - -void -tl_explain(int n) -{ - switch (n) { - case ALWAYS: printf("[]"); break; - case EVENTUALLY: printf("<>"); break; - case IMPLIES: printf("->"); break; - case EQUIV: printf("<->"); break; - case PREDICATE: printf("predicate"); break; - case OR: printf("||"); break; - case AND: printf("&&"); break; - case NOT: printf("!"); break; - case U_OPER: printf("U"); break; - case V_OPER: printf("V"); break; -#ifdef NXT - case NEXT: printf("X"); break; -#endif - case TRUE: printf("true"); break; - case FALSE: printf("false"); break; - case ';': printf("end of formula"); break; - default: printf("%c", n); break; - } -} - -static void -non_fatal(char *s1, char *s2) -{ extern int tl_yychar; - int i; - - printf("ltl2ba: "); - if (s2) - printf(s1, s2); - else - printf(s1); - if (tl_yychar != -1 && tl_yychar != 0) - { printf(", saw '"); - tl_explain(tl_yychar); - printf("'"); - } - printf("\nltl2ba: %s\n---------", uform); - for (i = 0; i < cnt; i++) - printf("-"); - printf("^\n"); - fflush(stdout); - tl_errs++; -} - -void -tl_yyerror(char *s1) -{ - Fatal(s1, (char *) 0); -} - -void -Fatal(char *s1, char *s2) -{ - non_fatal(s1, s2); - alldone(1); -} - -void -fatal(char *s1, char *s2) -{ - non_fatal(s1, s2); - alldone(1); -} - - diff --git a/util.c b/util.c new file mode 100644 index 0000000..b846800 --- /dev/null +++ b/util.c @@ -0,0 +1,216 @@ +#include "ltl2ba.h" + +FILE *tl_out = NULL; + +int tl_stats = 0; +int tl_simp_log = 1; +int tl_simp_diff = 1; +int tl_simp_fly = 1; +int tl_simp_scc = 1; +int tl_fjtofj = 1; +int tl_errs = 0; +int tl_verbose = 0; +int tl_terse = 0; +unsigned long All_Mem = 0; + + +static char uform[4096]; +static int hasuform=0, cnt=0; + +int +ltl2ba_init() +{ + tl_out = stderr; + return 0; +} + +int +tl_Getchar(void) +{ + if (cnt < hasuform) + return uform[cnt++]; + cnt++; + return -1; +} + +int +set_uform(const char *arg) +{ + strcpy(uform, arg); + hasuform = strlen(uform); + return hasuform; +} + +void +append_uform(const char *arg) +{ + strncat(uform, arg, sizeof uform); +} + +void +put_uform(void) +{ + fprintf(tl_out, "%s", uform); +} + +void +tl_UnGetchar(void) +{ + if (cnt > 0) cnt--; +} + + +static void +non_fatal(char *s1, char *s2) +{ extern int tl_yychar; + int i; + + printf("ltl2ba: "); + if (s2) + printf(s1, s2); + else + printf(s1); + if (tl_yychar != -1 && tl_yychar != 0) + { printf(", saw '"); + tl_explain(tl_yychar); + printf("'"); + } + printf("\nltl2ba: %s\n---------", uform); + for (i = 0; i < cnt; i++) + printf("-"); + printf("^\n"); + fflush(stdout); + tl_errs++; +} + + +char * +emalloc(int n) +{ char *tmp; + + if (!(tmp = (char *) malloc(n))) + fatal("not enough memory", (char *)0); + memset(tmp, 0, n); + return tmp; +} + +void +alldone(int estatus) +{ + exit(estatus); +} + +void +tl_yyerror(char *s1) +{ + Fatal(s1, (char *) 0); +} + +void +Fatal(char *s1, char *s2) +{ + non_fatal(s1, s2); + alldone(1); +} + +void +fatal(char *s1, char *s2) +{ + non_fatal(s1, s2); + alldone(1); +} + + +/* Subtract the `struct timeval' values X and Y, storing the result X-Y in RESULT. + Return 1 if the difference is negative, otherwise 0. */ + +int +timeval_subtract (result, x, y) +struct timeval *result, *x, *y; +{ + if (x->tv_usec < y->tv_usec) { + x->tv_usec += 1000000; + x->tv_sec--; + } + + /* Compute the time remaining to wait. tv_usec is certainly positive. */ + result->tv_sec = x->tv_sec - y->tv_sec; + result->tv_usec = x->tv_usec - y->tv_usec; + + /* Return 1 if result is negative. */ + return x->tv_sec < y->tv_sec; +} + +#define Binop(a) \ + fprintf(tl_out, "("); \ + dump(n->lft); \ + fprintf(tl_out, a); \ + dump(n->rgt); \ + fprintf(tl_out, ")") + +void +dump(Node *n) +{ + if (!n) return; + + switch(n->ntyp) { + case OR: Binop(" || "); break; + case AND: Binop(" && "); break; + case U_OPER: Binop(" U "); break; + case V_OPER: Binop(" V "); break; +#ifdef NXT + case NEXT: + fprintf(tl_out, "X"); + fprintf(tl_out, " ("); + dump(n->lft); + fprintf(tl_out, ")"); + break; +#endif + case NOT: + fprintf(tl_out, "!"); + fprintf(tl_out, " ("); + dump(n->lft); + fprintf(tl_out, ")"); + break; + case FALSE: + fprintf(tl_out, "false"); + break; + case TRUE: + fprintf(tl_out, "true"); + break; + case PREDICATE: + fprintf(tl_out, "(%s)", n->sym->name); + break; + case -1: + fprintf(tl_out, " D "); + break; + default: + printf("Unknown token: "); + tl_explain(n->ntyp); + break; + } +} + +void +tl_explain(int n) +{ + switch (n) { + case ALWAYS: printf("[]"); break; + case EVENTUALLY: printf("<>"); break; + case IMPLIES: printf("->"); break; + case EQUIV: printf("<->"); break; + case PREDICATE: printf("predicate"); break; + case OR: printf("||"); break; + case AND: printf("&&"); break; + case NOT: printf("!"); break; + case U_OPER: printf("U"); break; + case V_OPER: printf("V"); break; +#ifdef NXT + case NEXT: printf("X"); break; +#endif + case TRUE: printf("true"); break; + case FALSE: printf("false"); break; + case ';': printf("end of formula"); break; + default: printf("%c", n); break; + } +}