Rev 2 | Blame | Compare with Previous | Last modification | View Log | RSS feed
/***** 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;
};
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 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);
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 void
pop_dsts(void)
{
assert(dsts);
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);
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);
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;
}
}