Subversion Repositories planix.SVN

/***** 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);

int

tl_Getchar(void)

{

	if (cnt < hasuform)

		return uform[cnt++];

	cnt++;

	return -1;

}

int

tl_peek(int n)

{

	if (cnt+n < hasuform)

	{	return uform[cnt+n];

	}

	return -1;

}

void

tl_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");

	}

}

void

put_uform(void)

{

	fprintf(tl_out, "%s", uform);

}

void

tl_UnGetchar(void)

{

	if (cnt > 0) cnt--;

}

static void

tl_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();

}

int

tl_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, ")")

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

tl_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++;

}

void

tl_yyerror(char *s1)

{

	Fatal(s1, (char *) 0);

}

void

Fatal(char *s1, char *s2)

{

	tl_non_fatal(s1, s2);

	/* tl_stats(); */

	exit(1);

}