move everything out of trunk

[lttv.git] / trunk / verif / Spin / Src5.1.6 / reprosrc.c

diff --git a/trunk/verif/Spin/Src5.1.6/reprosrc.c b/trunk/verif/Spin/Src5.1.6/reprosrc.c
deleted file mode 100755 (executable)
index 0d4ba6b..0000000
--- a/trunk/verif/Spin/Src5.1.6/reprosrc.c
+++ /dev/null
@@ -1,136 +0,0 @@
-/***** spin: reprosrc.c *****/
-
-/* Copyright (c) 2002-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            */
-
-#include <stdio.h>
-#include "spin.h"
-#include "y.tab.h"
-
-static int indent = 1;
-
-extern ProcList        *rdy;
-void repro_seq(Sequence *);
-
-void
-doindent(void)
-{      int i;
-       for (i = 0; i < indent; i++)
-               printf("   ");
-}
-
-void
-repro_sub(Element *e)
-{
-       doindent();
-       switch (e->n->ntyp) {
-       case D_STEP:
-               printf("d_step {\n");
-               break;
-       case ATOMIC:
-               printf("atomic {\n");
-               break;
-       case NON_ATOMIC:
-               printf(" {\n");
-               break;
-       }
-       indent++;
-       repro_seq(e->n->sl->this);
-       indent--;
-
-       doindent();
-       printf(" };\n");
-}
-
-void
-repro_seq(Sequence *s)
-{      Element *e;
-       Symbol *v;
-       SeqList *h;
-
-       for (e = s->frst; e; e = e->nxt)
-       {
-               v = has_lab(e, 0);
-               if (v) printf("%s:\n", v->name);
-
-               if (e->n->ntyp == UNLESS)
-               {       printf("/* normal */ {\n");
-                       repro_seq(e->n->sl->this);
-                       doindent();
-                       printf("} unless {\n");
-                       repro_seq(e->n->sl->nxt->this);
-                       doindent();
-                       printf("}; /* end unless */\n");
-               } else if (e->sub)
-               {
-                       switch (e->n->ntyp) {
-                       case DO: doindent(); printf("do\n"); indent++; break;
-                       case IF: doindent(); printf("if\n"); indent++; break;
-                       }
-
-                       for (h = e->sub; h; h = h->nxt)
-                       {       indent--; doindent(); indent++; printf("::\n");
-                               repro_seq(h->this);
-                               printf("\n");
-                       }
-
-                       switch (e->n->ntyp) {
-                       case DO: indent--; doindent(); printf("od;\n"); break;
-                       case IF: indent--; doindent(); printf("fi;\n"); break;
-                       }
-               } else
-               {       if (e->n->ntyp == ATOMIC
-                       ||  e->n->ntyp == D_STEP
-                       ||  e->n->ntyp == NON_ATOMIC)
-                               repro_sub(e);
-                       else if (e->n->ntyp != '.'
-                            &&  e->n->ntyp != '@'
-                            &&  e->n->ntyp != BREAK)
-                       {
-                               doindent();
-                               if (e->n->ntyp == C_CODE)
-                               {       printf("c_code ");
-                                       plunk_inline(stdout, e->n->sym->name, 1);
-                               } else if (e->n->ntyp == 'c'
-                                      &&  e->n->lft->ntyp == C_EXPR)
-                               {       printf("c_expr { ");
-                                       plunk_expr(stdout, e->n->lft->sym->name);
-                                       printf("} ->\n");
-                               } else
-                               {       comment(stdout, e->n, 0);
-                                       printf(";\n");
-                       }       }
-               }
-               if (e == s->last)
-                       break;
-       }
-}
-
-void
-repro_proc(ProcList *p)
-{
-       if (!p) return;
-       if (p->nxt) repro_proc(p->nxt);
-
-       if (p->det) printf("D");        /* deterministic */
-       printf("proctype %s()", p->n->name);
-       if (p->prov)
-       {       printf(" provided ");
-               comment(stdout, p->prov, 0);
-       }
-       printf("\n{\n");
-       repro_seq(p->s);
-       printf("}\n");
-}
-
-void
-repro_src(void)
-{
-       repro_proc(rdy);
-}