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);
}