/***** spin: pangen7.c *****/ /* Copyright (c) 1989-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            *//* pangen7.c: Version 5.3.0 2010, synchronous product of never claims     */ #include <stdlib.h>#include "spin.h"#include "y.tab.h"#include <assert.h>#ifdef PCextern int unlink(const char *);#else#include <unistd.h>#endif extern ProcList	*rdy;extern Element *Al_El;extern int nclaims, verbose, Strict; typedef struct Succ_List Succ_List;typedef struct SQueue SQueue;typedef struct OneState OneState;typedef struct State_Stack State_Stack;typedef struct Guard Guard; struct Succ_List {	SQueue	*s;	Succ_List *nxt;}; struct OneState {	int	*combo;	/* the combination of claim states */	Succ_List	*succ;	/* list of ptrs to immediate successor states */}; struct SQueue {	OneState	state;	SQueue	*nxt;}; struct State_Stack {	int *n;	State_Stack *nxt;}; struct Guard {	Lextok *t;	Guard *nxt;}; SQueue	*sq, *sd, *render;	/* states move from sq to sd to render to holding */SQueue	*holding, *lasthold;State_Stack *dsts; int nst;		/* max nr of states in claims */int *Ist;		/* initial states */int *Nacc;		/* number of accept states in claim */int *Nst;		/* next states */int **reached;		/* n claims x states */int unfolding;		/* to make sure all accept states are reached */int is_accept;		/* remember if the current state is accepting in any claim */int not_printing;	/* set during explore_product */ Element ****matrix;	/* n x two-dimensional arrays state x state */Element **Selfs;	/* self-loop states at end of claims */ static void get_seq(int, Sequence *);static void set_el(int n, Element *e);static void gen_product(void);static void print_state_nm(char *, int *, char *);static SQueue *find_state(int *);static SQueue *retrieve_state(int *); static intsame_state(int *a, int *b){	int i; 	for (i = 0; i < nclaims; i++)	{	if (a[i] != b[i])		{	return 0;	}	}	return 1;} static intin_stack(SQueue *s, SQueue *in){	SQueue *q; 	for (q = in; q; q = q->nxt)	{	if (same_state(q->state.combo, s->state.combo))		{	return 1;	}	}	return 0;} static voidto_render(SQueue *s){	SQueue *a, *q, *last; /* find in sd/sq and move to render, if not already there */	int n; 	for (n = 0; n < nclaims; n++)	{	reached[n][ s->state.combo[n] ] |= 2;	} 	for (q = render; q; q = q->nxt)	{	if (same_state(q->state.combo, s->state.combo))		{	return;	}	}	for (q = holding; q; q = q->nxt)	{	if (same_state(q->state.combo, s->state.combo))		{	return;	}	} 	a = sd;more:	for (q = a, last = 0; q; last = q, q = q->nxt)	{	if (same_state(q->state.combo, s->state.combo))		{	if (!last)			{	if (a == sd)				{	sd = q->nxt;				} else if (a == sq)				{	sq = q->nxt;				} else				{	holding = q->nxt;				}			} else			{	last->nxt = q->nxt;			}			q->nxt = render;			render = q;			return;	}	}	if (verbose)	{	print_state_nm("looking for: ", s->state.combo, "\n");	}	(void) find_state(s->state.combo);	/* creates it in sq */	if (a != sq)	{	a = sq;		goto more;	}	fatal("cannot happen, to_render", 0);} static voidwrap_text(char *pre, Lextok *t, char *post){	printf(pre);	comment(stdout, t, 0);	printf(post);} static State_Stack *push_dsts(int *n){	State_Stack *s;	int i; 	for (s = dsts; s; s = s->nxt)	{	if (same_state(s->n, n))		{	if (verbose&64)			{	printf("\n");				for (s = dsts; s; s = s->nxt)				{	print_state_nm("\t", s->n, "\n");				}				print_state_nm("\t", n, "\n");			}			return s;	}	} 	s = (State_Stack *) emalloc(sizeof(State_Stack));	s->n = (int *) emalloc(nclaims * sizeof(int));	for (i = 0; i < nclaims; i++)		s->n[i] = n[i];	s->nxt = dsts;	dsts = s;	return 0;} static voidpop_dsts(void){	assert(dsts);	dsts = dsts->nxt;} static voidcomplete_transition(Succ_List *sl, Guard *g){	Guard *w;	int cnt = 0; 	printf("	:: ");	for (w = g; w; w = w->nxt)	{	if (w->t->ntyp == CONST		&&  w->t->val == 1)		{	continue;		} else if (w->t->ntyp == 'c'		&&  w->t->lft->ntyp == CONST		&&  w->t->lft->val == 1)		{	continue; /* 'true' */		} 		if (cnt > 0)		{	printf(" && ");		}		wrap_text("", w->t, "");		cnt++;	}	if (cnt == 0)	{	printf("true");	}	print_state_nm(" -> goto ", sl->s->state.combo, ""); 	if (is_accept > 0)	{	printf("_U%d\n", (unfolding+1)%nclaims);	} else	{	printf("_U%d\n", unfolding);	}} static voidstate_body(OneState *s, Guard *guard){	Succ_List *sl;	State_Stack *y;	Guard *g;	int i, once; 	for (sl = s->succ; sl; sl = sl->nxt)	{	once = 0; 		for (i = 0; i < nclaims; i++)		{	Element *e;			e = matrix[i][s->combo[i]][sl->s->state.combo[i]]; 			/* if one of the claims has a DO or IF move			   then pull its target state forward, once			 */ 			if (!e			|| e->n->ntyp == NON_ATOMIC			||  e->n->ntyp == DO			||  e->n->ntyp == IF)			{	s = &(sl->s->state);				y = push_dsts(s->combo);				if (!y)				{	if (once++ == 0)					{	assert(s->succ);						state_body(s, guard);					}					pop_dsts();				} else if (!y->nxt)	/* self-loop transition */				{	if (!not_printing) printf(" /* self-loop */\n");				} else				{	/* non_fatal("loop in state body", 0); ** maybe ok */				}				continue;			} else			{	g = (Guard *) emalloc(sizeof(Guard));				g->t = e->n;				g->nxt = guard;				guard = g;		}	} 		if (guard && !once)		{	if (!not_printing) complete_transition(sl, guard);			to_render(sl->s);	}	}} static struct X {	char *s;	int n;} spl[] = {	{"end",		3 },	{"accept",	6 },	{0,		0 },}; static int slcnt;extern Label *labtab; static ProcList *locate_claim(int n){	ProcList *p;	int i; 	for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */	{	if (i == n)		{	break;	}	}	assert(p && p->b == N_CLAIM); 	return p;} static voidelim_lab(Element *e){	Label *l, *lst; 	for (l = labtab, lst = NULL; l; lst = l, l = l->nxt)	{	if (l->e == e)		{	if (lst)			{	lst->nxt = l->nxt;			} else			{	labtab = l->nxt;			}			break;	}	}} static intclaim_has_accept(ProcList *p){	Label *l; 	for (l = labtab; l; l = l->nxt)	{	if (strcmp(l->c->name, p->n->name) == 0		&&  strncmp(l->s->name, "accept", 6) == 0)		{	return 1;	}	}	return 0;} static voidprune_accept(void){	int n; 	for (n = 0; n < nclaims; n++)	{	if ((reached[n][Selfs[n]->seqno] & 2) == 0)		{	if (verbose)			{	printf("claim %d: selfloop not reachable\n", n);			}			elim_lab(Selfs[n]);			Nacc[n] = claim_has_accept(locate_claim(n));	}	}} static voidmk_accepting(int n, Element *e){	ProcList *p;	Label *l;	int i; 	assert(!Selfs[n]);	Selfs[n] = e; 	l = (Label *) emalloc(sizeof(Label));	l->s = (Symbol *) emalloc(sizeof(Symbol));	l->s->name = "accept00";	l->c = (Symbol *) emalloc(sizeof(Symbol));	l->uiid = 0;	/* this is not in an inline */ 	for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */	{	if (i == n)		{	l->c->name = p->n->name;			break;	}	}	assert(p && p->b == N_CLAIM);	Nacc[n] = 1; 	l->e = e;	l->nxt = labtab;	labtab = l;} static voidcheck_special(int *nrs){	ProcList *p;	Label *l;	int i, j, nmatches;	int any_accepts = 0; 	for (i = 0; i < nclaims; i++)	{	any_accepts += Nacc[i];	} 	is_accept = 0;	for (j = 0; spl[j].n; j++) /* 2 special label prefixes */	{	nmatches = 0;		for (p = rdy, i = 0; p; p = p->nxt, i++) /* check each claim */		{	if (p->b != N_CLAIM)			{	continue;			}			/* claim i in state nrs[i], type p->tn, name p->n->name			 * either the state has an accept label, or the claim has none,			 * so that all its states should be considered accepting			 * --- but only if other claims do have accept states!			 */			if (Strict == 0 && j == 1 && Nacc[i] == 0 && any_accepts > 0)			{	if ((verbose&32) && i == unfolding)				{	printf("	/* claim %d pseudo-accept */\n", i);				}				goto is_accepting;			}			for (l = labtab; l; l = l->nxt)	/* check its labels */			{	if (strcmp(l->c->name, p->n->name) == 0  /* right claim */				&&  l->e->seqno == nrs[i]		 /* right state */				&&  strncmp(l->s->name, spl[j].s, spl[j].n) == 0)				{	if (j == 1)	/* accept state */					{	char buf[32];is_accepting:					if (strchr(p->n->name, ':'))						{	sprintf(buf, "N%d", i);						} else						{	strcpy(buf, p->n->name);						}						if (unfolding == 0 && i == 0)						{	if (!not_printing)							printf("%s_%s_%d:\n",	/* true accept */								spl[j].s, buf, slcnt++);						} else if (verbose&32)						{	if (!not_printing)							printf("%s_%s%d:\n",								buf, spl[j].s, slcnt++);						}						if (i == unfolding)						{	is_accept++; /* move to next unfolding */						}					} else					{	nmatches++;					}					break;		}	}	}		if (j == 0 && nmatches == nclaims)	/* end-state */		{	if (!not_printing)			{	printf("%s%d:\n", spl[j].s, slcnt++);	}	}	}} static intrender_state(SQueue *q){	if (!q || !q->state.succ)	{	if (verbose&64)		{	printf("	no exit\n");		}		return 0;	} 	check_special(q->state.combo); /* accept or end-state labels */ 	dsts = (State_Stack *) 0;	push_dsts(q->state.combo);	/* to detect loops */ 	if (!not_printing)	{	print_state_nm("", q->state.combo, "");	/* the name */		printf("_U%d:\n\tdo\n", unfolding);	} 	state_body(&(q->state), (Guard *) 0); 	if (!not_printing)	{	printf("\tod;\n");	}	pop_dsts();	return 1;} static voidexplore_product(void){	SQueue *q; 	/* all states are in the sd queue */ 	q = retrieve_state(Ist);	/* retrieve from the sd q */	q->nxt = render;		/* put in render q */	render = q;	do {		q = render;		render = render->nxt;		q->nxt = 0;		/* remove from render q */ 		if (verbose&64)		{	print_state_nm("explore: ", q->state.combo, "\n");		} 		not_printing = 1;		render_state(q);	/* may add new states */		not_printing = 0; 		if (lasthold)		{	lasthold->nxt = q;			lasthold = q;		} else		{	holding = lasthold = q;		}	} while (render);	assert(!dsts);	} static voidprint_product(void){	SQueue *q;	int cnt; 	if (unfolding == 0)	{	printf("never Product {\n");	/* name expected by iSpin */

Lines 1–500 of 925. Load more