Import sources from 2011-03-30 iso image

1 files changed, 400 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/tl_parse.c b/sys/src/cmd/spin/tl_parse.c
new file mode 100755
index 000000000..6206a0d99
--- /dev/null
+++ b/sys/src/cmd/spin/tl_parse.c
@@ -0,0 +1,400 @@
+/***** tl_spin: tl_parse.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 int	tl_yylex(void);
+extern int	tl_verbose, tl_errs;
+
+int	tl_yychar = 0;
+YYSTYPE	tl_yylval;
+
+static Node	*tl_formula(void);
+static Node	*tl_factor(void);
+static Node	*tl_level(int);
+
+static int	prec[2][4] = {
+	{ U_OPER,  V_OPER, 0, 0 },	/* left associative */
+	{ OR, AND, IMPLIES, EQUIV, },	/* left associative */
+};
+
+static Node *
+tl_factor(void)
+{	Node *ptr = ZN;
+
+	switch (tl_yychar) {
+	case '(':
+		ptr = tl_formula();
+		if (tl_yychar != ')')
+			tl_yyerror("expected ')'");
+		tl_yychar = tl_yylex();
+		break;
+	case NOT:
+		ptr = tl_yylval;
+		tl_yychar = tl_yylex();
+		ptr->lft = tl_factor();
+		ptr = push_negation(ptr);
+		break;
+	case ALWAYS:
+		tl_yychar = tl_yylex();
+
+		ptr = tl_factor();
+#ifndef NO_OPT
+		if (ptr->ntyp == FALSE
+		||  ptr->ntyp == TRUE)
+			break;	/* [] false == false */
+
+		if (ptr->ntyp == V_OPER)
+		{	if (ptr->lft->ntyp == FALSE)
+				break;	/* [][]p = []p */
+
+			ptr = ptr->rgt;	/* [] (p V q) = [] q */
+		}
+#endif
+		ptr = tl_nn(V_OPER, False, ptr);
+		break;
+#ifdef NXT
+	case NEXT:
+		tl_yychar = tl_yylex();
+		ptr = tl_factor();
+		if (ptr->ntyp == TRUE)
+			break;	/* X true = true */
+		ptr = tl_nn(NEXT, ptr, ZN);
+		break;
+#endif
+	case EVENTUALLY:
+		tl_yychar = tl_yylex();
+
+		ptr = tl_factor();
+#ifndef NO_OPT
+		if (ptr->ntyp == TRUE
+		||  ptr->ntyp == FALSE)
+			break;	/* <> true == true */
+
+		if (ptr->ntyp == U_OPER
+		&&  ptr->lft->ntyp == TRUE)
+			break;	/* <><>p = <>p */
+
+		if (ptr->ntyp == U_OPER)
+		{	/* <> (p U q) = <> q */
+			ptr = ptr->rgt;
+			/* fall thru */
+		}
+#endif
+		ptr = tl_nn(U_OPER, True, ptr);
+
+		break;
+	case PREDICATE:
+		ptr = tl_yylval;
+		tl_yychar = tl_yylex();
+		break;
+	case TRUE:
+	case FALSE:
+		ptr = tl_yylval;
+		tl_yychar = tl_yylex();
+		break;
+	}
+	if (!ptr) tl_yyerror("expected predicate");
+#if 0
+	printf("factor:	");
+	tl_explain(ptr->ntyp);
+	printf("\n");
+#endif
+	return ptr;
+}
+
+static Node *
+bin_simpler(Node *ptr)
+{	Node *a, *b;
+
+	if (ptr)
+	switch (ptr->ntyp) {
+	case U_OPER:
+#ifndef NO_OPT
+		if (ptr->rgt->ntyp == TRUE
+		||  ptr->rgt->ntyp == FALSE
+		||  ptr->lft->ntyp == FALSE)
+		{	ptr = ptr->rgt;
+			break;
+		}
+		if (isequal(ptr->lft, ptr->rgt))
+		{	/* p U p = p */	
+			ptr = ptr->rgt;
+			break;
+		}
+		if (ptr->lft->ntyp == U_OPER
+		&&  isequal(ptr->lft->lft, ptr->rgt))
+		{	/* (p U q) U p = (q U p) */
+			ptr->lft = ptr->lft->rgt;
+			break;
+		}
+		if (ptr->rgt->ntyp == U_OPER
+		&&  ptr->rgt->lft->ntyp == TRUE)
+		{	/* p U (T U q)  = (T U q) */
+			ptr = ptr->rgt;
+			break;
+		}
+#ifdef NXT
+		/* X p U X q == X (p U q) */
+		if (ptr->rgt->ntyp == NEXT
+		&&  ptr->lft->ntyp == NEXT)
+		{	ptr = tl_nn(NEXT,
+				tl_nn(U_OPER,
+					ptr->lft->lft,
+					ptr->rgt->lft), ZN);
+		}
+#endif
+#endif
+		break;
+	case V_OPER:
+#ifndef NO_OPT
+		if (ptr->rgt->ntyp == FALSE
+		||  ptr->rgt->ntyp == TRUE
+		||  ptr->lft->ntyp == TRUE)
+		{	ptr = ptr->rgt;
+			break;
+		}
+		if (isequal(ptr->lft, ptr->rgt))
+		{	/* p V p = p */	
+			ptr = ptr->rgt;
+			break;
+		}
+		/* F V (p V q) == F V q */
+		if (ptr->lft->ntyp == FALSE
+		&&  ptr->rgt->ntyp == V_OPER)
+		{	ptr->rgt = ptr->rgt->rgt;
+			break;
+		}
+		/* p V (F V q) == F V q */
+		if (ptr->rgt->ntyp == V_OPER
+		&&  ptr->rgt->lft->ntyp == FALSE)
+		{	ptr->lft = False;
+			ptr->rgt = ptr->rgt->rgt;
+			break;
+		}
+#endif
+		break;
+	case IMPLIES:
+#ifndef NO_OPT
+		if (isequal(ptr->lft, ptr->rgt))
+		{	ptr = True;
+			break;
+		}
+#endif
+		ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
+		ptr = rewrite(ptr);
+		break;
+	case EQUIV:
+#ifndef NO_OPT
+		if (isequal(ptr->lft, ptr->rgt))
+		{	ptr = True;
+			break;
+		}
+#endif
+		a = rewrite(tl_nn(AND,
+			dupnode(ptr->lft),
+			dupnode(ptr->rgt)));
+		b = rewrite(tl_nn(AND,
+			Not(ptr->lft),
+			Not(ptr->rgt)));
+		ptr = tl_nn(OR, a, b);
+		ptr = rewrite(ptr);
+		break;
+	case AND:
+#ifndef NO_OPT
+		/* p && (q U p) = p */
+		if (ptr->rgt->ntyp == U_OPER
+		&&  isequal(ptr->rgt->rgt, ptr->lft))
+		{	ptr = ptr->lft;
+			break;
+		}
+		if (ptr->lft->ntyp == U_OPER
+		&&  isequal(ptr->lft->rgt, ptr->rgt))
+		{	ptr = ptr->rgt;
+			break;
+		}
+
+		/* p && (q V p) == q V p */
+		if (ptr->rgt->ntyp == V_OPER
+		&&  isequal(ptr->rgt->rgt, ptr->lft))
+		{	ptr = ptr->rgt;
+			break;
+		}
+		if (ptr->lft->ntyp == V_OPER
+		&&  isequal(ptr->lft->rgt, ptr->rgt))
+		{	ptr = ptr->lft;
+			break;
+		}
+
+		/* (p U q) && (r U q) = (p && r) U q*/
+		if (ptr->rgt->ntyp == U_OPER
+		&&  ptr->lft->ntyp == U_OPER
+		&&  isequal(ptr->rgt->rgt, ptr->lft->rgt))
+		{	ptr = tl_nn(U_OPER,
+				tl_nn(AND, ptr->lft->lft, ptr->rgt->lft),
+				ptr->lft->rgt);
+			break;
+		}
+
+		/* (p V q) && (p V r) = p V (q && r) */
+		if (ptr->rgt->ntyp == V_OPER
+		&&  ptr->lft->ntyp == V_OPER
+		&&  isequal(ptr->rgt->lft, ptr->lft->lft))
+		{	ptr = tl_nn(V_OPER,
+				ptr->rgt->lft,
+				tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
+			break;
+		}
+#ifdef NXT
+		/* X p && X q == X (p && q) */
+		if (ptr->rgt->ntyp == NEXT
+		&&  ptr->lft->ntyp == NEXT)
+		{	ptr = tl_nn(NEXT,
+				tl_nn(AND,
+					ptr->rgt->lft,
+					ptr->lft->lft), ZN);
+			break;
+		}
+#endif
+
+		if (isequal(ptr->lft, ptr->rgt)	/* (p && p) == p */
+		||  ptr->rgt->ntyp == FALSE	/* (p && F) == F */
+		||  ptr->lft->ntyp == TRUE)	/* (T && p) == p */
+		{	ptr = ptr->rgt;
+			break;
+		}	
+		if (ptr->rgt->ntyp == TRUE	/* (p && T) == p */
+		||  ptr->lft->ntyp == FALSE)	/* (F && p) == F */
+		{	ptr = ptr->lft;
+			break;
+		}
+
+		/* (p V q) && (r U q) == p V q */
+		if (ptr->rgt->ntyp == U_OPER
+		&&  ptr->lft->ntyp == V_OPER
+		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
+		{	ptr = ptr->lft;
+			break;
+		}
+#endif
+		break;
+
+	case OR:
+#ifndef NO_OPT
+		/* p || (q U p) == q U p */
+		if (ptr->rgt->ntyp == U_OPER
+		&&  isequal(ptr->rgt->rgt, ptr->lft))
+		{	ptr = ptr->rgt;
+			break;
+		}
+
+		/* p || (q V p) == p */
+		if (ptr->rgt->ntyp == V_OPER
+		&&  isequal(ptr->rgt->rgt, ptr->lft))
+		{	ptr = ptr->lft;
+			break;
+		}
+
+		/* (p U q) || (p U r) = p U (q || r) */
+		if (ptr->rgt->ntyp == U_OPER
+		&&  ptr->lft->ntyp == U_OPER
+		&&  isequal(ptr->rgt->lft, ptr->lft->lft))
+		{	ptr = tl_nn(U_OPER,
+				ptr->rgt->lft,
+				tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
+			break;
+		}
+
+		if (isequal(ptr->lft, ptr->rgt)	/* (p || p) == p */
+		||  ptr->rgt->ntyp == FALSE	/* (p || F) == p */
+		||  ptr->lft->ntyp == TRUE)	/* (T || p) == T */
+		{	ptr = ptr->lft;
+			break;
+		}	
+		if (ptr->rgt->ntyp == TRUE	/* (p || T) == T */
+		||  ptr->lft->ntyp == FALSE)	/* (F || p) == p */
+		{	ptr = ptr->rgt;
+			break;
+		}
+
+		/* (p V q) || (r V q) = (p || r) V q */
+		if (ptr->rgt->ntyp == V_OPER
+		&&  ptr->lft->ntyp == V_OPER
+		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
+		{	ptr = tl_nn(V_OPER,
+				tl_nn(OR, ptr->lft->lft, ptr->rgt->lft),
+				ptr->rgt->rgt);
+			break;
+		}
+
+		/* (p V q) || (r U q) == r U q */
+		if (ptr->rgt->ntyp == U_OPER
+		&&  ptr->lft->ntyp == V_OPER
+		&&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
+		{	ptr = ptr->rgt;
+			break;
+		}		
+#endif
+		break;
+	}
+	return ptr;
+}
+
+static Node *
+tl_level(int nr)
+{	int i; Node *ptr = ZN;
+
+	if (nr < 0)
+		return tl_factor();
+
+	ptr = tl_level(nr-1);
+again:
+	for (i = 0; i < 4; i++)
+		if (tl_yychar == prec[nr][i])
+		{	tl_yychar = tl_yylex();
+			ptr = tl_nn(prec[nr][i],
+				ptr, tl_level(nr-1));
+			ptr = bin_simpler(ptr);
+			goto again;
+		}
+	if (!ptr) tl_yyerror("syntax error");
+#if 0
+	printf("level %d:	", nr);
+	tl_explain(ptr->ntyp);
+	printf("\n");
+#endif
+	return ptr;
+}
+
+static Node *
+tl_formula(void)
+{	tl_yychar = tl_yylex();
+	return tl_level(1);	/* 2 precedence levels, 1 and 0 */	
+}
+
+void
+tl_parse(void)
+{	Node *n = tl_formula();
+	if (tl_verbose)
+	{	printf("formula: ");
+		dump(n);
+		printf("\n");
+	}
+	if (tl_Getchar() != -1)
+	{	tl_yyerror("syntax error");
+		tl_errs++;
+		return;
+	}
+	trans(n);
+}