/***** tl_spin: tl_main.c *****/ /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories.     *//* All Rights Reserved.  This software is for educational purposes only.  *//* No guarantee whatsoever is expressed or implied by the distribution of *//* this code.  Permission is given to distribute this code provided that  *//* this introductory message is not removed and no monies are exchanged.  *//* Software written by Gerard J. Holzmann.  For tool documentation see:   *//*             http://spinroot.com/                                       *//* Send all bug-reports and/or questions to: bugs@spinroot.com            */ /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, *//* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */ #include "tl.h" extern FILE	*tl_out; int	newstates  = 0;	/* debugging only */int	tl_errs    = 0;int	tl_verbose = 0;int	tl_terse   = 0;int	tl_clutter = 0;int	state_cnt = 0; unsigned long	All_Mem = 0;char	*claim_name; static char	uform[4096];static int	hasuform=0, cnt=0; extern void cache_stats(void);extern void a_stats(void); inttl_Getchar(void){	if (cnt < hasuform)		return uform[cnt++];	cnt++;	return -1;} inttl_peek(int n){	if (cnt+n < hasuform)	{	return uform[cnt+n];	}	return -1;} voidtl_balanced(void){	int i;	int k = 0; 	for (i = 0; i < hasuform; i++)	{	if (uform[i] == '(')		{	k++;		} else if (uform[i] == ')')		{	k--;	}	}	if (k != 0)	{	tl_errs++;		tl_yyerror("parentheses not balanced");	}} voidput_uform(void){	fprintf(tl_out, "%s", uform);} voidtl_UnGetchar(void){	if (cnt > 0) cnt--;} static voidtl_stats(void){	extern int Stack_mx;	printf("total memory used: %9ld\n", All_Mem);	printf("largest stack sze: %9d\n", Stack_mx);	cache_stats();	a_stats();} inttl_main(int argc, char *argv[]){	int i;	extern int /* verbose, */ xspin; 	tl_verbose = 0; /* was: tl_verbose = verbose; */	tl_clutter = 1-xspin;	/* use -X -f to turn off uncluttering */ 	newstates  = 0;	state_cnt  = 0;	tl_errs    = 0;	tl_terse   = 0;	All_Mem = 0;	memset(uform, 0, sizeof(uform));	hasuform=0;	cnt=0;	claim_name = (char *) 0; 	ini_buchi();	ini_cache();	ini_rewrt();	ini_trans(); 	while (argc > 1 && argv[1][0] == '-')	{		switch (argv[1][1]) {		case 'd':	newstates = 1;	/* debugging mode */				break;		case 'f':	argc--; argv++;				for (i = 0; argv[1][i]; i++)				{	if (argv[1][i] == '\t'					||  argv[1][i] == '\"'					||  argv[1][i] == '\n')						argv[1][i] = ' ';				}				strcpy(uform, argv[1]);				hasuform = (int) strlen(uform);				break;		case 'v':	tl_verbose++;				break;		case 'n':	tl_terse = 1;				break;		case 'c':	argc--; argv++;				claim_name = (char *) emalloc(strlen(argv[1])+1);				strcpy(claim_name, argv[1]);				break;		default :	printf("spin -f: saw '-%c'\n", argv[1][1]);				goto nogood;		}		argc--; argv++;	}	if (hasuform == 0)	{nogood:		printf("usage:\tspin [-v] [-n] -f formula\n");		printf("	-v verbose translation\n");		printf("	-n normalize tl formula and exit\n");		exit(1);	}	tl_balanced(); 	if (tl_errs == 0)		tl_parse(); 	if (tl_verbose) tl_stats();	return tl_errs;} #define Binop(a)		\		fprintf(tl_out, "(");	\		dump(n->lft);		\		fprintf(tl_out, a);	\		dump(n->rgt);		\		fprintf(tl_out, ")") voiddump(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;	}} voidtl_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 voidtl_non_fatal(char *s1, char *s2){	extern int tl_yychar;	int i; 	printf("tl_spin: ");	if (s2)		printf(s1, s2);	else		printf(s1);	if (tl_yychar != -1 && tl_yychar != 0)	{	printf(", saw '");		tl_explain(tl_yychar);		printf("'");	}	printf("\ntl_spin: %s\n---------", uform);	for (i = 0; i < cnt; i++)		printf("-");	printf("^\n");	fflush(stdout);	tl_errs++;} voidtl_yyerror(char *s1){	Fatal(s1, (char *) 0);} voidFatal(char *s1, char *s2){	tl_non_fatal(s1, s2);	/* tl_stats(); */	exit(1);}