1 /***** spin: guided.c *****/
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
13 #include <sys/types.h>
17 extern RunList
*run
, *X
;
18 extern Element
*Al_El
;
19 extern Symbol
*Fname
, *oFname
;
20 extern int verbose
, lineno
, xspin
, jumpsteps
, depth
, merger
, cutoff
;
21 extern int nproc
, nstop
, Tval
, ntrail
, columns
;
22 extern short Have_claim
, Skip_claim
;
23 extern void ana_src(int, int);
27 static int lastclaim
= -1;
29 static void lost_trail(void);
35 for (oX
= run
; oX
; oX
= oX
->nxt
)
37 { printf("(%s) ", oX
->n
->name
);
43 newer(char *f1
, char *f2
)
45 #if defined(WIN32) || defined(WIN64)
51 if (stat(f1
, (struct stat
*)&x
) < 0) return 0;
52 if (stat(f2
, (struct stat
*)&y
) < 0) return 1;
53 if (x
.st_mtime
< y
.st_mtime
) return 0;
62 for (e
= Al_El
; e
; e
= e
->Nxt
)
64 && (e
->n
->ntyp
== ATOMIC
65 || e
->n
->ntyp
== NON_ATOMIC
66 || e
->n
->ntyp
== D_STEP
))
73 return (!Have_claim
|| !X
|| X
->pid
!= 0);
83 * if source model name is leader.pml
84 * look for the trail file under these names:
92 sprintf(snap
, "%s%d.trail", oFname
->name
, ntrail
);
94 sprintf(snap
, "%s.trail", oFname
->name
);
96 if ((fd
= fopen(snap
, "r")) == NULL
)
97 { snap
[strlen(snap
)-2] = '\0'; /* .tra */
98 if ((fd
= fopen(snap
, "r")) == NULL
)
99 { if ((q
= strchr(oFname
->name
, '.')) != NULL
)
102 sprintf(snap
, "%s%d.trail",
103 oFname
->name
, ntrail
);
105 sprintf(snap
, "%s.trail",
109 if ((fd
= fopen(snap
, "r")) != NULL
)
112 snap
[strlen(snap
)-2] = '\0'; /* last try */
113 if ((fd
= fopen(snap
, "r")) != NULL
)
116 printf("spin: cannot find trail file\n");
120 if (xspin
== 0 && newer(oFname
->name
, snap
))
121 printf("spin: warning, \"%s\" is newer than %s\n",
127 * sets Tval because timeouts may be part of trail
128 * this used to also set m_loss to 1, but that is
129 * better handled with the runtime -m flag
134 while (fscanf(fd
, "%d:%d:%d\n", &depth
, &pno
, &nst
) == 3)
135 { if (depth
== -2) { start_claim(pno
); continue; }
136 if (depth
== -4) { merger
= 1; ana_src(0, 1); continue; }
140 dotag(stdout
, " CYCLE>\n");
142 dotag(stdout
, "<<<<<START OF CYCLE>>>>>\n");
147 if (cutoff
> 0 && depth
>= cutoff
)
148 { printf("-------------\n");
149 printf("depth-limit (-u%d steps) reached\n", cutoff
);
153 if (Skip_claim
&& pno
== 0) continue;
155 for (dothis
= Al_El
; dothis
; dothis
= dothis
->Nxt
)
156 { if (dothis
->Seqno
== nst
)
160 { printf("%3d: proc %d, no matching stmnt %d\n",
161 depth
, pno
- Have_claim
, nst
);
165 i
= nproc
- nstop
+ Skip_claim
;
167 if (dothis
->n
->ntyp
== '@')
173 { dotag(stdout
, "<end>\n");
176 if (Have_claim
&& pno
== 0)
177 printf("%3d: claim terminates\n",
180 printf("%3d: proc %d terminates\n",
181 depth
, pno
- Have_claim
);
185 if (pno
<= 1) continue; /* init dies before never */
186 printf("%3d: stop error, ", depth
);
187 printf("proc %d (i=%d) trans %d, %c\n",
188 pno
- Have_claim
, i
, nst
, dothis
->n
->ntyp
);
192 if (!xspin
&& (verbose
&32))
193 { printf("i=%d pno %d\n", i
, pno
);
196 for (X
= run
; X
; X
= X
->nxt
)
203 { printf("%3d: no process %d (step %d)\n", depth
, pno
- Have_claim
, nst
);
204 printf(" max %d (%d - %d + %d) claim %d",
205 nproc
- nstop
+ Skip_claim
,
206 nproc
, nstop
, Skip_claim
, Have_claim
);
207 printf("active processes:\n");
208 for (X
= run
; X
; X
= X
->nxt
)
209 { printf("\tpid %d\tproctype %s\n", X
->pid
, X
->n
->name
);
214 { printf("%3d:\tproc %d (?) ", depth
, pno
);
221 lineno
= dothis
->n
->ln
;
222 Fname
= dothis
->n
->fn
;
224 if (dothis
->n
->ntyp
== D_STEP
)
225 { Element
*g
, *og
= dothis
;
228 if (g
&& depth
>= jumpsteps
229 && ((verbose
&32) || ((verbose
&4) && not_claim())))
233 if (og
->n
->ntyp
== D_STEP
)
234 og
= og
->n
->sl
->this->frst
;
237 comment(stdout
, og
->n
, 0);
240 if (verbose
&1) dumpglobals();
241 if (verbose
&2) dumplocal(X
);
242 if (xspin
) printf("\n");
245 } while (g
&& g
!= dothis
->nxt
);
247 { X
->pc
= g
?huntele(g
, 0, -1):g
;
251 keepgoing
: if (dothis
->merge_start
)
252 a
= dothis
->merge_start
;
257 { X
->pc
= eval_sub(dothis
);
258 if (X
->pc
) X
->pc
= huntele(X
->pc
, 0, a
);
261 if (depth
>= jumpsteps
262 && ((verbose
&32) || ((verbose
&4) && not_claim()))) /* -v or -p */
266 if (dothis
->n
->ntyp
== D_STEP
)
267 dothis
= dothis
->n
->sl
->this->frst
;
270 comment(stdout
, dothis
->n
, 0);
272 if (a
&& (verbose
&32))
273 printf("\t<merge %d now @%d>",
275 (X
&& X
->pc
)?X
->pc
->seqno
:-1);
278 if (verbose
&1) dumpglobals();
279 if (verbose
&2) dumplocal(X
);
280 if (xspin
) printf("\n");
284 printf("\ttransition failed\n");
285 a
= 0; /* avoid inf loop */
288 if (a
&& X
&& X
->pc
&& X
->pc
->seqno
!= a
)
293 if (Have_claim
&& X
&& X
->pid
== 0
295 && lastclaim
!= dothis
->n
->ln
)
296 { lastclaim
= dothis
->n
->ln
;
299 sprintf(t
, "#%d", lastclaim
);
303 printf("Never claim moves to line %d\t[", lastclaim
);
304 comment(stdout
, dothis
->n
, 0);
307 printf("spin: trail ends after %d steps\n", depth
);
315 while (fscanf(fd
, "%d:%d:%d:%d\n", &d
, &p
, &n
, &l
) == 4)
316 { printf("step %d: proc %d ", d
, p
); whichproc(p
);
317 printf("(state %d) - d %d\n", n
, l
);
319 wrapup(1); /* no return */
324 { int i
= nproc
- nstop
;
328 for (Y
= run
; Y
; Y
= Y
->nxt
)
This page took 0.063971 seconds and 5 git commands to generate.