/***** 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 PC
extern 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;
};

static SQueue	*sq, *sd, *render;	/* states move from sq to sd to render to holding */
static SQueue	*holding, *lasthold;
static State_Stack *dsts;

static int nst;		/* max nr of states in claims */
static int *Ist;	/* initial states */
static int *Nacc;	/* number of accept states in claim */
static int *Nst;	/* next states */
static int **reached;	/* n claims x states */
static int unfolding;	/* to make sure all accept states are reached */
static int is_accept;	/* remember if the current state is accepting in any claim */
static int not_printing; /* set during explore_product */

static Element ****matrix;	/* n x two-dimensional arrays state x state */
static 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 int
same_state(int *a, int *b)
{	int i;

	for (i = 0; i < nclaims; i++)
	{	if (a[i] != b[i])
		{	return 0;
	}	}
	return 1;
}

static int
in_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 void
to_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 void
wrap_text(char *pre, Lextok *t, char *post)
{
	printf(pre, (char *) 0);
	comment(stdout, t, 0);
	printf(post, (char *) 0);
}

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 void
pop_dsts(void)
{
	assert(dsts != NULL);
	dsts = dsts->nxt;
}

static void
complete_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 void
state_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 != NULL);
						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 void
elim_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 int
claim_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 void
prune_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 void
mk_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 void
check_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 int
render_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 void
explore_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 void
print_product(void)
{	SQueue *q;
	int cnt;

	if (unfolding == 0)
	{	printf("never Product {\n");	/* name expected by iSpin */
		q = find_state(Ist);	/* should find it in the holding q */
		assert(q != NULL);
		q->nxt = holding;	/* put it at the front */
		holding = q;
	}
	render = holding;
	holding = lasthold = 0;

	printf("/* ============= U%d ============= */\n", unfolding);
	cnt = 0;
	do {
		q = render;
		render = render->nxt;
		q->nxt = 0;
		if (verbose&64)
		{	print_state_nm("print: ", q->state.combo, "\n");
		}
		cnt += render_state(q);

		if (lasthold)
		{	lasthold->nxt = q;
			lasthold = q;
		} else
		{	holding = lasthold = q;
		}
	} while (render);
	assert(!dsts);

	if (cnt == 0)
	{	printf("	0;\n");
	}

	if (unfolding == nclaims-1)
	{	printf("}\n");
	}
}

static void
prune_dead(void)
{	Succ_List *sl, *last;
	SQueue *q;
	int cnt;

	do {	cnt = 0;
		for (q = sd; q; q = q->nxt)
		{	/* if successor is deadend, remove it
			 * unless it's a move to the end-state of the claim
			 */
			last = (Succ_List *) 0;
			for (sl = q->state.succ; sl; last = sl, sl = sl->nxt)
			{	if (!sl->s->state.succ)	/* no successor */
				{	if (!last)
					{	q->state.succ = sl->nxt;
					} else
					{	last->nxt = sl->nxt;
					}
					cnt++;
		}	}	}
	} while (cnt > 0);
}

static void
print_raw(void)
{	int i, j, n;

	printf("#if 0\n");
	for (n = 0; n < nclaims; n++)
	{	printf("C%d:\n", n);
		for (i = 0; i < nst; i++)
		{	if (reached[n][i])
			for (j = 0; j < nst; j++)
			{	if (matrix[n][i][j])
				{	if (reached[n][i] & 2) printf("+");
					if (i == Ist[n]) printf("*");
					printf("\t%d", i);
					wrap_text(" -[", matrix[n][i][j]->n, "]->\t");
					printf("%d\n", j);
	}	}	}	}
	printf("#endif\n\n");
	fflush(stdout);
}

void
sync_product(void)
{	ProcList *p;
	Element *e;
	int n, i;

	if (nclaims <= 1) return;

	(void) unlink("pan.pre");

	Ist  = (int *) emalloc(sizeof(int) * nclaims);
	Nacc = (int *) emalloc(sizeof(int) * nclaims);
	Nst  = (int *) emalloc(sizeof(int) * nclaims);
	reached = (int **) emalloc(sizeof(int *) * nclaims);
	Selfs   = (Element **) emalloc(sizeof(Element *) * nclaims);
	matrix  = (Element ****) emalloc(sizeof(Element ***) * nclaims); /* claims */

	for (p = rdy, i = 0; p; p = p->nxt, i++)
	{	if (p->b == N_CLAIM)
		{	nst = max(p->s->maxel, nst);
			Nacc[i] = claim_has_accept(p);
	}	}

	for (n = 0; n < nclaims; n++)
	{	reached[n] = (int *) emalloc(sizeof(int) * nst);
		matrix[n] = (Element ***) emalloc(sizeof(Element **) * nst);	/* rows */
		for (i = 0; i < nst; i++)					/* cols */
		{	matrix[n][i] = (Element **) emalloc(sizeof(Element *) * nst);
	}	}

	for (e = Al_El; e; e = e->Nxt)
	{	e->status &= ~DONE;
	}

	for (p = rdy, n=0; p; p = p->nxt, n++)
	{	if (p->b == N_CLAIM)
		{	/* fill in matrix[n] */
			e = p->s->frst;
			Ist[n] = huntele(e, e->status, -1)->seqno;

			reached[n][Ist[n]] = 1|2;
			get_seq(n, p->s);
	}	}

	if (verbose)	/* show only the input automata */
	{	print_raw();
	}

	gen_product();	/* create product automaton */
}

static int
nxt_trans(int n, int cs, int frst)
{	int j;

	for (j = frst; j < nst; j++)
	{	if (reached[n][cs]
		&&  matrix[n][cs][j])
		{	return j;
	}	}
	return -1;
}

static void
print_state_nm(char *p, int *s, char *a)
{	int i;
	printf("%sP", p);
	for (i = 0; i < nclaims; i++)
	{	printf("_%d", s[i]);
	}
	printf("%s", a);
}

static void
create_transition(OneState *s, SQueue *it)
{	int n, from, upto;
	int *F = s->combo;
	int *T = it->state.combo;
	Succ_List *sl;
	Lextok *t;

	if (verbose&64)
	{	print_state_nm("", F, " ");
		print_state_nm("-> ", T, "\t");
	}

	/* check if any of the claims is blocked */
	/* which makes the state a dead-end */
	for (n = 0; n < nclaims; n++)
	{	from = F[n];
		upto = T[n];
		t = matrix[n][from][upto]->n;
		if (verbose&64)
		{	wrap_text("", t, " ");
		}
		if (t->ntyp == 'c'
		&&  t->lft->ntyp == CONST)
		{	if (t->lft->val == 0)	/* i.e., false */
			{	goto done;
	}	}	}

	sl = (Succ_List *) emalloc(sizeof(Succ_List));
	sl->s = it;
	sl->nxt = s->succ;
	s->succ = sl;
done:
	if (verbose&64)
	{	printf("\n");
	}
}

static SQueue *
find_state(int *cs)
{	SQueue *nq, *a = sq;
	int i;

again:	/* check in nq, sq, and then in the render q */
	for (nq = a; nq; nq = nq->nxt)
	{	if (same_state(nq->state.combo, cs))
		{	return nq;	/* found */
	}	}
	if (a == sq && sd)
	{	a = sd;
		goto again; /* check the other stack too */
	} else if (a == sd && render)
	{	a = render;
		goto again;
	}

	nq = (SQueue *) emalloc(sizeof(SQueue));
	nq->state.combo = (int *) emalloc(nclaims * sizeof(int));
	for (i = 0; i < nclaims; i++)
	{	nq->state.combo[i] = cs[i];
	}
	nq->nxt = sq;	/* add to sq stack */
	sq = nq;

	return nq;
}

static SQueue *
retrieve_state(int *s)
{	SQueue *nq, *last = NULL;

	for (nq = sd; nq; last = nq, nq = nq->nxt)
	{	if (same_state(nq->state.combo, s))
		{	if (last)
			{	last->nxt = nq->nxt;
			} else
			{	sd = nq;
			}
			return nq;	/* found */
	}	}

	fatal("cannot happen: retrieve_state", 0);
	return (SQueue *) 0;
}

static void
all_successors(int n, OneState *cur)
{	int i, j = 0;

	if (n >= nclaims)
	{	create_transition(cur, find_state(Nst));
	} else
	{	i = cur->combo[n];
		for (;;)
		{	j = nxt_trans(n, i, j);
			if (j < 0) break;
			Nst[n] = j;
			all_successors(n+1, cur);
			j++;
	}	}
}

static void
gen_product(void)
{	OneState *cur_st;
	SQueue *q;

	find_state(Ist);	/* create initial state */

	while (sq)
	{	if (in_stack(sq, sd))
		{	sq = sq->nxt;
			continue;
		}
		cur_st = &(sq->state);

		q = sq;
		sq = sq->nxt;	/* delete from sq stack */
		q->nxt = sd;	/* and move to done stack */
		sd = q;

		all_successors(0, cur_st);
	}
	/* all states are in the sd queue now */
	prune_dead();
	explore_product();	/* check if added accept-self-loops are reachable */
	prune_accept();

	if (verbose)
	{	print_raw();
	}

	/* PM: merge states with identical successor lists */

	/* all outgoing transitions from accept-states
	   from claim n in copy n connect to states in copy (n+1)%nclaims
	   only accept states from claim 0 in copy 0 are true accept states
	   in the product

	   PM: what about claims that have no accept states (e.g., restrictions)
	*/

	for (unfolding = 0; unfolding < nclaims; unfolding++)
	{	print_product();
	}
}

static void
t_record(int n, Element *e, Element *g)
{	int from = e->seqno, upto = g?g->seqno:0;

	assert(from >= 0 && from < nst);
	assert(upto >= 0 && upto < nst);

	matrix[n][from][upto] = e;
	reached[n][upto] |= 1;
}

static void
get_sub(int n, Element *e)
{
	if (e->n->ntyp == D_STEP
	||  e->n->ntyp == ATOMIC)
	{	fatal("atomic or d_step in never claim product", 0);
	} 
	/* NON_ATOMIC */
	e->n->sl->this->last->nxt = e->nxt;
	get_seq(n, e->n->sl->this);

	t_record(n, e, e->n->sl->this->frst);

}

static void
set_el(int n, Element *e)
{	Element *g;

	if (e->n->ntyp == '@')	/* change to self-loop */
	{	e->n->ntyp = CONST;
		e->n->val = 1;	/* true */
		e->nxt = e;
		g = e;
		mk_accepting(n, e);
	} else

	if (e->n->ntyp == GOTO)
	{	g = get_lab(e->n, 1);
		g = huntele(g, e->status, -1);
	} else if (e->nxt)
	{	g = huntele(e->nxt, e->status, -1);
	} else
	{	g = NULL;
	}

	t_record(n, e, g);
}

static void
get_seq(int n, Sequence *s)
{	SeqList *h;
	Element *e;

	e = huntele(s->frst, s->frst->status, -1);
	for ( ; e; e = e->nxt)
	{	if (e->status & DONE)
		{	goto checklast;
		}
		e->status |= DONE;

		if (e->n->ntyp == UNLESS)
		{	fatal("unless stmnt in never claim product", 0);
		}

		if (e->sub)	/* IF or DO */
		{	Lextok *x = NULL;
			Lextok *y = NULL;
			Lextok *haselse = NULL;

			for (h = e->sub; h; h = h->nxt)
			{	Lextok *t = h->this->frst->n;
				if (t->ntyp == ELSE)
				{	if (verbose&64) printf("else at line %d\n", t->ln);
					haselse = t;
					continue;
				}
				if (t->ntyp != 'c')
				{	fatal("product, 'else' combined with non-condition", 0);
				}

				if (t->lft->ntyp == CONST	/* true */
				&&  t->lft->val == 1
				&&  y == NULL)
				{	y = nn(ZN, CONST, ZN, ZN);
					y->val = 0;
				} else
				{	if (!x)
						x = t;
					else
						x = nn(ZN, OR, x, t);
					if (verbose&64)
					{	wrap_text(" [", x, "]\n");
			}	}	}
			if (haselse)
			{	if (!y)
				{	y = nn(ZN, '!', x, ZN);
				}
				if (verbose&64)
				{	wrap_text(" [else: ", y, "]\n");
				}
				haselse->ntyp = 'c';	/* replace else */
				haselse->lft = y;
			}

			for (h = e->sub; h; h = h->nxt)
			{	t_record(n, e, h->this->frst);
				get_seq(n, h->this);
			}
		} else
		{	if (e->n->ntyp == ATOMIC
			||  e->n->ntyp == D_STEP
			||  e->n->ntyp == NON_ATOMIC)
			{	get_sub(n, e);
			} else 
			{	set_el(n, e);
			}
		}
checklast:	if (e == s->last)
			break;
	}
}