From: compudj Date: Wed, 15 Oct 2008 16:20:33 +0000 (+0000) Subject: update verif X-Git-Tag: v0.12.20~378 X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=2eb837fb7fd1c5790db77f9a79de9d556754fbdf;p=lttv.git update verif git-svn-id: http://ltt.polymtl.ca/svn@3111 04897980-b3bd-0310-b5e0-8ef037075253 --- diff --git a/trunk/verif/examples/buffer.spin b/trunk/verif/examples/buffer.spin index 41965dc3..b04b1bb0 100644 --- a/trunk/verif/examples/buffer.spin +++ b/trunk/verif/examples/buffer.spin @@ -1,8 +1,8 @@ -// LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v1 +// LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v2 // Created for the Spin validator. // Mathieu Desnoyers -// June 2008 +// October 2008 // TODO : create test cases that will generate an overflow on the offset and // counter type. Counter types smaller than a byte should be used. @@ -20,7 +20,7 @@ #define NUMPROCS 4 // NUMPROCS 3 : does not cause event loss because buffers are big enough. -//#define NUMPROCS 3 +// #define NUMPROCS 3 // e.g. 3 events, 1 switch, read 1 subbuffer #define NUMSWITCH 1 @@ -34,7 +34,6 @@ byte commit_count[NR_SUBBUFS]; // Reader counters byte read_off = 0; -byte retrieve_count[NR_SUBBUFS]; byte events_lost = 0; byte refcount = 0; @@ -80,8 +79,11 @@ cmpxchg_loop: tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; if - :: tmp_commit % SUBBUF_SIZE == 0 -> deliver = 1 - :: else -> skip + :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE - + tmp_commit + -> deliver = 1 + :: else + -> skip fi; refcount = refcount - 1; } @@ -139,8 +141,11 @@ cmpxchg_loop: tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; if - :: tmp_commit % SUBBUF_SIZE == 0 -> deliver = 1; - :: else -> skip + :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE - + tmp_commit + -> deliver = 1 + :: else + -> skip fi; } atomic { @@ -163,15 +168,13 @@ end: proctype reader() { byte i, j; - byte tmp_retrieve; - byte lwrite_off, lcommit_count; do :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0 && (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) < HALF_UCHAR - && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] - - retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] - == SUBBUF_SIZE -> + && (commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] + - SUBBUF_SIZE - (((read_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + == 0) -> atomic { i = 0; do @@ -184,10 +187,6 @@ proctype reader() } // reading from buffer... - // Since there is only one reader per buffer at any given time, - // we don't care about retrieve_count vs read_off ordering : - // combined use of retrieve_count and read_off are made atomic by a - // mutex. atomic { i = 0; do @@ -196,9 +195,6 @@ proctype reader() i++ :: i >= SUBBUF_SIZE -> break od; - tmp_retrieve = retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] - + SUBBUF_SIZE; - retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] = tmp_retrieve; read_off = read_off + SUBBUF_SIZE; } :: read_off >= (NUMPROCS - events_lost) -> break; @@ -231,7 +227,6 @@ init { do :: i < NR_SUBBUFS -> commit_count[i] = 0; - retrieve_count[i] = 0; i++ :: i >= NR_SUBBUFS -> break od; @@ -272,8 +267,8 @@ init { commit_sum = commit_sum + commit_count[j]; // The commit count of a particular subbuffer must always be higher // or equal to the retrieve_count of this subbuffer. - assert(commit_count[j] - retrieve_count[j] >= 0 && - commit_count[j] - retrieve_count[j] < HALF_UCHAR); + // assert(commit_count[j] - retrieve_count[j] >= 0 && + // commit_count[j] - retrieve_count[j] < HALF_UCHAR); j++ :: j >= NR_SUBBUFS -> break od; diff --git a/trunk/verif/examples/buffer.spin.trail b/trunk/verif/examples/buffer.spin.trail index 93bb3331..bc2446c0 100644 --- a/trunk/verif/examples/buffer.spin.trail +++ b/trunk/verif/examples/buffer.spin.trail @@ -1,102 +1,103 @@ -4:-4:-4 -1:0:120 -2:0:121 -3:0:121 -4:0:125 -5:0:131 -6:0:131 -7:0:131 -8:0:131 -9:0:134 -10:0:139 -11:0:140 -12:0:142 -13:0:144 -14:0:142 -15:0:144 -16:0:142 -17:0:144 -18:0:146 -19:0:152 -20:0:154 -21:0:156 -22:0:160 -23:6:0 -24:6:6 -25:6:7 -26:6:13 -27:6:14 -28:6:18 -29:6:20 -30:6:28 -31:6:29 -32:5:30 -33:5:35 -34:5:36 -35:5:42 -36:5:43 -37:5:47 -38:5:51 -39:5:55 -40:5:57 -41:5:58 -42:5:61 -43:5:70 -44:5:71 -45:5:75 -46:5:77 -47:5:79 -48:4:30 -49:4:35 -50:4:36 -51:4:42 -52:4:43 -53:4:47 -54:4:51 -55:4:55 -56:4:57 -57:4:58 -58:4:61 -59:4:68 -60:4:75 -61:4:77 -62:4:79 -63:3:30 -64:3:33 -65:3:76 -66:3:77 -67:3:79 -68:2:111 -69:2:113 -70:2:117 -71:3:0 -72:3:3 -73:3:28 -74:3:29 -75:2:119 -76:1:80 -77:1:81 -78:1:82 -79:1:82 -80:1:86 -81:1:90 -82:1:92 -83:1:93 -84:1:93 -85:1:96 -86:1:80 -87:1:81 -88:1:82 -89:1:82 -90:1:86 -91:1:90 -92:1:92 -93:1:93 -94:1:93 -95:1:96 -96:1:105 -97:1:110 -98:0:162 -99:0:165 -100:0:165 -101:0:169 +1:0:118 +2:0:119 +3:0:119 +4:0:122 +5:0:128 +6:0:128 +7:0:128 +8:0:128 +9:0:131 +10:0:136 +11:0:137 +12:0:139 +13:0:141 +14:0:139 +15:0:141 +16:0:139 +17:0:141 +18:0:139 +19:0:141 +20:0:143 +21:0:149 +22:0:151 +23:0:153 +24:0:157 +25:7:0 +26:7:3 +27:7:28 +28:7:29 +29:6:30 +30:6:35 +31:6:36 +32:6:42 +33:6:43 +34:6:47 +35:6:51 +36:6:55 +37:6:57 +38:6:58 +39:6:61 +40:6:68 +41:6:75 +42:6:77 +43:6:79 +44:5:30 +45:5:35 +46:5:36 +47:5:42 +48:5:43 +49:5:47 +50:5:51 +51:5:55 +52:5:57 +53:5:58 +54:5:61 +55:5:70 +56:5:71 +57:5:75 +58:5:77 +59:5:79 +60:4:30 +61:4:35 +62:4:36 +63:4:42 +64:4:43 +65:4:47 +66:4:51 +67:4:55 +68:4:57 +69:4:58 +70:4:61 +71:4:68 +72:4:75 +73:4:77 +74:4:79 +75:3:30 +76:3:35 +77:3:36 +78:3:42 +79:3:43 +80:3:47 +81:3:51 +82:3:55 +83:3:57 +84:3:58 +85:3:61 +86:3:70 +87:3:71 +88:3:75 +89:3:77 +90:3:79 +91:2:109 +92:2:111 +93:2:115 +94:3:0 +95:3:3 +96:3:28 +97:3:29 +98:2:117 +99:0:159 +100:0:162 +101:0:162 +102:0:165 diff --git a/trunk/verif/examples/pan b/trunk/verif/examples/pan index a0356c18..c6cf6e59 100755 Binary files a/trunk/verif/examples/pan and b/trunk/verif/examples/pan differ diff --git a/trunk/verif/examples/pan.b b/trunk/verif/examples/pan.b index 8816afb3..1ae73245 100644 --- a/trunk/verif/examples/pan.b +++ b/trunk/verif/examples/pan.b @@ -10,16 +10,15 @@ ; goto R999; - case 4: /* STATE 5 */ + case 4: /* STATE 4 */ ; - ((P4 *)this)->i = trpt->bup.ovals[2]; - now.retrieve_count[ Index(((P4 *)this)->i, 2) ] = trpt->bup.ovals[1]; + ((P4 *)this)->i = trpt->bup.ovals[1]; now.commit_count[ Index(((P4 *)this)->i, 2) ] = trpt->bup.ovals[0]; ; - ungrab_ints(trpt->bup.ovals, 3); + ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 5: /* STATE 11 */ + case 5: /* STATE 10 */ ; ((P4 *)this)->i = trpt->bup.ovals[1]; /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0]; @@ -28,13 +27,13 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 6: /* STATE 11 */ + case 6: /* STATE 10 */ ; ((P4 *)this)->i = trpt->bup.oval; ; goto R999; - case 7: /* STATE 14 */ + case 7: /* STATE 13 */ ; ((P4 *)this)->i = trpt->bup.ovals[1]; now.buffer_use[ Index(((P4 *)this)->i, 4) ] = trpt->bup.ovals[0]; @@ -42,21 +41,21 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 8: /* STATE 15 */ + case 8: /* STATE 14 */ ; /* 0 */ ((P4 *)this)->i = trpt->bup.oval; ; ; goto R999; - case 9: /* STATE 20 */ + case 9: /* STATE 19 */ ; ; delproc(0, now._nr_pr-1); ; goto R999; - case 10: /* STATE 22 */ + case 10: /* STATE 21 */ ; ((P4 *)this)->i = trpt->bup.oval; ; @@ -64,13 +63,13 @@ ; goto R999; - case 11: /* STATE 24 */ + case 11: /* STATE 23 */ ; now.refcount = trpt->bup.oval; ; goto R999; - case 12: /* STATE 26 */ + case 12: /* STATE 25 */ ; ((P4 *)this)->i = trpt->bup.oval; ; @@ -78,7 +77,7 @@ ; goto R999; - case 13: /* STATE 32 */ + case 13: /* STATE 31 */ ; ((P4 *)this)->i = trpt->bup.ovals[1]; /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0]; @@ -87,19 +86,19 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 14: /* STATE 32 */ + case 14: /* STATE 31 */ ; ((P4 *)this)->i = trpt->bup.oval; ; goto R999; - case 15: /* STATE 34 */ + case 15: /* STATE 33 */ ; now.refcount = trpt->bup.oval; ; goto R999; - case 16: /* STATE 36 */ + case 16: /* STATE 35 */ ; ((P4 *)this)->i = trpt->bup.oval; ; @@ -107,14 +106,14 @@ ; goto R999; - case 17: /* STATE 37 */ + case 17: /* STATE 36 */ ; /* 0 */ ((P4 *)this)->i = trpt->bup.oval; ; ; goto R999; - case 18: /* STATE 45 */ + case 18: /* STATE 44 */ ; ((P4 *)this)->commit_sum = trpt->bup.ovals[1]; ((P4 *)this)->j = trpt->bup.ovals[0]; @@ -122,7 +121,7 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 19: /* STATE 49 */ + case 19: /* STATE 47 */ ; ((P4 *)this)->j = trpt->bup.ovals[1]; ((P4 *)this)->commit_sum = trpt->bup.ovals[0]; @@ -130,7 +129,7 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 20: /* STATE 50 */ + case 20: /* STATE 48 */ ; /* 0 */ ((P4 *)this)->j = trpt->bup.oval; ; @@ -138,10 +137,10 @@ goto R999; ; - case 21: /* STATE 55 */ + case 21: /* STATE 53 */ goto R999; - case 22: /* STATE 58 */ + case 22: /* STATE 56 */ ; p_restor(II); ; @@ -203,29 +202,22 @@ ungrab_ints(trpt->bup.ovals, 2); goto R999; - case 31: /* STATE 24 */ + case 31: /* STATE 17 */ ; - now.read_off = trpt->bup.ovals[3]; - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = trpt->bup.ovals[2]; - ((P2 *)this)->tmp_retrieve = trpt->bup.ovals[1]; - /* 0 */ ((P2 *)this)->i = trpt->bup.ovals[0]; + /* 0 */ ((P2 *)this)->i = trpt->bup.oval; ; ; - ungrab_ints(trpt->bup.ovals, 4); goto R999; - case 32: /* STATE 24 */ + case 32: /* STATE 22 */ ; - now.read_off = trpt->bup.ovals[2]; - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = trpt->bup.ovals[1]; - ((P2 *)this)->tmp_retrieve = trpt->bup.ovals[0]; + now.read_off = trpt->bup.oval; ; - ungrab_ints(trpt->bup.ovals, 3); goto R999; ; ; - case 34: /* STATE 31 */ + case 34: /* STATE 29 */ ; p_restor(II); ; @@ -323,11 +315,12 @@ case 47: /* STATE 40 */ ; - deliver = trpt->bup.ovals[1]; - /* 0 */ ((P1 *)this)->tmp_commit = trpt->bup.ovals[0]; + deliver = trpt->bup.ovals[2]; + /* 1 */ ((P1 *)this)->tmp_commit = trpt->bup.ovals[1]; + /* 0 */ ((P1 *)this)->prev_off = trpt->bup.ovals[0]; ; ; - ungrab_ints(trpt->bup.ovals, 2); + ungrab_ints(trpt->bup.ovals, 3); goto R999; ; @@ -409,12 +402,13 @@ case 60: /* STATE 27 */ ; - now.refcount = trpt->bup.ovals[2]; - deliver = trpt->bup.ovals[1]; - /* 0 */ ((P0 *)this)->tmp_commit = trpt->bup.ovals[0]; + now.refcount = trpt->bup.ovals[3]; + deliver = trpt->bup.ovals[2]; + /* 1 */ ((P0 *)this)->tmp_commit = trpt->bup.ovals[1]; + /* 0 */ ((P0 *)this)->prev_off = trpt->bup.ovals[0]; ; ; - ungrab_ints(trpt->bup.ovals, 3); + ungrab_ints(trpt->bup.ovals, 4); goto R999; case 61: /* STATE 27 */ diff --git a/trunk/verif/examples/pan.c b/trunk/verif/examples/pan.c index 928afc4e..2c12633e 100644 --- a/trunk/verif/examples/pan.c +++ b/trunk/verif/examples/pan.c @@ -478,7 +478,7 @@ addproc(int n) break; case 4: /* :init: */ ((P4 *)pptr(h))->_t = 4; - ((P4 *)pptr(h))->_p = 42; reached4[42]=1; + ((P4 *)pptr(h))->_p = 41; reached4[41]=1; /* params: */ /* locals: */ ((P4 *)pptr(h))->i = 0; @@ -508,20 +508,14 @@ addproc(int n) break; case 2: /* reader */ ((P2 *)pptr(h))->_t = 2; - ((P2 *)pptr(h))->_p = 28; reached2[28]=1; + ((P2 *)pptr(h))->_p = 26; reached2[26]=1; /* params: */ /* locals: */ ((P2 *)pptr(h))->i = 0; ((P2 *)pptr(h))->j = 0; - ((P2 *)pptr(h))->tmp_retrieve = 0; - ((P2 *)pptr(h))->lwrite_off = 0; - ((P2 *)pptr(h))->lcommit_count = 0; #ifdef VAR_RANGES logval("reader:i", ((P2 *)pptr(h))->i); logval("reader:j", ((P2 *)pptr(h))->j); - logval("reader:tmp_retrieve", ((P2 *)pptr(h))->tmp_retrieve); - logval("reader:lwrite_off", ((P2 *)pptr(h))->lwrite_off); - logval("reader:lcommit_count", ((P2 *)pptr(h))->lcommit_count); #endif #ifdef HAS_CODE locinit2(h); @@ -9835,12 +9829,6 @@ iniglobals(void) } } now.read_off = 0; - { int l_in; - for (l_in = 0; l_in < 2; l_in++) - { - now.retrieve_count[l_in] = 0; - } - } now.events_lost = 0; now.refcount = 0; #ifdef VAR_RANGES @@ -9858,12 +9846,6 @@ iniglobals(void) } } logval("read_off", now.read_off); - { int l_in; - for (l_in = 0; l_in < 2; l_in++) - { - logval("retrieve_count[l_in]", now.retrieve_count[l_in]); - } - } logval("events_lost", now.events_lost); logval("refcount", now.refcount); #endif @@ -11464,12 +11446,6 @@ c_globals(void) } } printf(" byte read_off: %d\n", now.read_off); - { int l_in; - for (l_in = 0; l_in < 2; l_in++) - { - printf(" byte retrieve_count[%d]: %d\n", l_in, now.retrieve_count[l_in]); - } - } printf(" byte events_lost: %d\n", now.events_lost); printf(" byte refcount: %d\n", now.refcount); { int l_in; @@ -11497,9 +11473,6 @@ c_locals(int pid, int tp) printf("local vars proc %d (reader):\n", pid); printf(" byte i: %d\n", ((P2 *)pptr(pid))->i); printf(" byte j: %d\n", ((P2 *)pptr(pid))->j); - printf(" byte tmp_retrieve: %d\n", ((P2 *)pptr(pid))->tmp_retrieve); - printf(" byte lwrite_off: %d\n", ((P2 *)pptr(pid))->lwrite_off); - printf(" byte lcommit_count: %d\n", ((P2 *)pptr(pid))->lcommit_count); break; case 1: printf("local vars proc %d (tracer):\n", pid); diff --git a/trunk/verif/examples/pan.h b/trunk/verif/examples/pan.h index 0dcc8a8b..e4ec3cd1 100644 --- a/trunk/verif/examples/pan.h +++ b/trunk/verif/examples/pan.h @@ -23,6 +23,9 @@ char *trailfilename; #ifndef uint #define uint unsigned int #endif +#ifndef HASH32 +#define HASH64 +#endif #define DELTA 500 #ifdef MA #if NCORE>1 && !defined(SEP_STATE) @@ -53,38 +56,38 @@ typedef struct S_F_MAP { char *fnm; int from; int upto; } S_F_MAP; -#define nstates4 59 /* :init: */ -#define endstate4 58 +#define nstates4 57 /* :init: */ +#define endstate4 56 short src_ln4 [] = { - 0, 225, 227, 228, 229, 230, 231, 231, - 226, 233, 226, 233, 235, 236, 237, 238, - 238, 234, 240, 234, 240, 241, 242, 244, - 245, 246, 247, 248, 248, 243, 250, 243, - 250, 252, 253, 254, 255, 256, 256, 251, - 258, 251, 224, 262, 263, 264, 266, 267, - 271, 272, 273, 273, 265, 278, 265, 278, - 282, 260, 284, 0, }; + 0, 226, 228, 229, 230, 231, 231, 227, + 233, 227, 233, 235, 236, 237, 238, 238, + 234, 240, 234, 240, 241, 242, 244, 245, + 246, 247, 248, 248, 243, 250, 243, 250, + 252, 253, 254, 255, 256, 256, 251, 258, + 251, 225, 262, 263, 264, 266, 267, 272, + 273, 273, 265, 278, 265, 278, 282, 260, + 284, 0, }; S_F_MAP src_file4 [] = { { "-", 0, 0 }, - { "buffer.spin", 1, 58 }, - { "-", 59, 60 } + { "buffer.spin", 1, 56 }, + { "-", 57, 58 } }; uchar reached4 [] = { - 0, 1, 1, 0, 0, 0, 1, 1, - 0, 1, 1, 0, 1, 0, 0, 1, - 1, 0, 1, 1, 0, 0, 0, 1, - 0, 0, 0, 1, 1, 0, 1, 1, - 0, 1, 0, 0, 0, 1, 1, 0, - 1, 1, 0, 1, 0, 0, 1, 0, + 0, 1, 1, 0, 0, 1, 1, 0, + 1, 1, 0, 1, 0, 0, 1, 1, + 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, - 0, 0, 0, 0, }; + 1, 0, 0, 0, 1, 1, 0, 1, + 1, 0, 1, 0, 0, 1, 0, 0, + 1, 1, 0, 1, 1, 0, 0, 0, + 0, 0, }; uchar *loopstate4; #define nstates3 10 /* cleaner */ #define endstate3 9 short src_ln3 [] = { - 0, 210, 211, 212, 213, 209, 215, 209, - 208, 216, 0, }; + 0, 211, 212, 213, 214, 210, 216, 210, + 209, 217, 0, }; S_F_MAP src_file3 [] = { { "-", 0, 0 }, { "buffer.spin", 1, 9 }, @@ -95,37 +98,35 @@ uchar reached3 [] = { 0, 0, 0, }; uchar *loopstate3; -#define nstates2 32 /* reader */ -#define endstate2 31 +#define nstates2 30 /* reader */ +#define endstate2 29 short src_ln2 [] = { - 0, 169, 171, 173, 174, 175, 176, 177, - 177, 172, 179, 172, 170, 187, 189, 190, - 191, 192, 192, 188, 194, 188, 194, 196, - 197, 186, 199, 199, 164, 201, 164, 201, - 0, }; + 0, 177, 179, 181, 182, 183, 184, 185, + 185, 180, 187, 180, 178, 191, 193, 194, + 195, 196, 196, 192, 198, 192, 198, 190, + 200, 200, 172, 202, 172, 202, 0, }; S_F_MAP src_file2 [] = { { "-", 0, 0 }, - { "buffer.spin", 1, 31 }, - { "-", 32, 33 } + { "buffer.spin", 1, 29 }, + { "-", 30, 31 } }; uchar reached2 [] = { 0, 1, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, - 0, 0, 1, 1, 0, 1, 1, 0, - 0, }; + 1, 1, 0, 1, 1, 0, 0, }; uchar *loopstate2; #define nstates1 51 /* tracer */ #define endstate1 50 short src_ln1 [] = { - 0, 99, 100, 98, 104, 105, 106, 106, - 103, 108, 102, 111, 111, 112, 112, 110, - 114, 114, 116, 117, 118, 119, 120, 120, - 115, 122, 115, 109, 127, 129, 130, 131, - 132, 132, 128, 134, 128, 134, 135, 137, - 137, 138, 138, 136, 140, 126, 142, 144, - 146, 141, 148, 0, }; + 0, 106, 107, 105, 111, 112, 113, 113, + 110, 115, 109, 118, 118, 119, 119, 117, + 121, 121, 123, 124, 125, 126, 127, 127, + 122, 129, 122, 116, 134, 136, 137, 138, + 139, 139, 135, 141, 135, 141, 142, 145, + 146, 147, 148, 143, 150, 133, 152, 154, + 156, 151, 158, 0, }; S_F_MAP src_file1 [] = { { "-", 0, 0 }, { "buffer.spin", 1, 50 }, @@ -144,10 +145,10 @@ uchar *loopstate1; #define nstates0 31 /* switcher */ #define endstate0 30 short src_ln0 [] = { - 0, 56, 57, 58, 61, 62, 63, 64, - 64, 59, 66, 55, 69, 69, 70, 70, - 68, 72, 67, 75, 76, 78, 78, 79, - 79, 77, 81, 81, 74, 84, 85, 0, }; + 0, 60, 61, 62, 65, 66, 67, 68, + 68, 63, 70, 59, 73, 73, 74, 74, + 72, 76, 71, 79, 80, 83, 84, 85, + 86, 81, 88, 88, 78, 91, 92, 0, }; S_F_MAP src_file0 [] = { { "-", 0, 0 }, { "buffer.spin", 1, 30 }, @@ -224,11 +225,8 @@ typedef struct P2 { /* reader */ unsigned _p : 7; /* state */ uchar i; uchar j; - uchar tmp_retrieve; - uchar lwrite_off; - uchar lcommit_count; } P2; -#define Air2 (sizeof(P2) - Offsetof(P2, lcommit_count) - 1*sizeof(uchar)) +#define Air2 (sizeof(P2) - Offsetof(P2, j) - 1*sizeof(uchar)) #define Ptracer ((P1 *)this) typedef struct P1 { /* tracer */ unsigned _pid : 8; /* 0..255 */ @@ -453,7 +451,6 @@ typedef struct State { uchar write_off; uchar commit_count[2]; uchar read_off; - uchar retrieve_count[2]; uchar events_lost; uchar refcount; uchar sv[VECTORSZ]; @@ -473,9 +470,9 @@ uchar *loopstate5; /* np_ */ #define endstate5 2 /* np_ */ #define start5 0 /* np_ */ -#define start4 42 +#define start4 41 #define start3 8 -#define start2 28 +#define start2 26 #define start1 3 #define start0 11 #ifdef NP diff --git a/trunk/verif/examples/pan.m b/trunk/verif/examples/pan.m index 5d40303e..357708ae 100644 --- a/trunk/verif/examples/pan.m +++ b/trunk/verif/examples/pan.m @@ -15,7 +15,7 @@ _m = 3; goto P999; /* PROC :init: */ - case 3: /* STATE 1 - line 225 "buffer.spin" - [i = 0] (0:0:1 - 1) */ + case 3: /* STATE 1 - line 226 "buffer.spin" - [i = 0] (0:0:1 - 1) */ IfNotBlocked reached[4][1] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); @@ -25,43 +25,35 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 4: /* STATE 2 - line 227 "buffer.spin" - [((i<2))] (8:0:3 - 1) */ + case 4: /* STATE 2 - line 228 "buffer.spin" - [((i<2))] (7:0:2 - 1) */ IfNotBlocked reached[4][2] = 1; if (!((((int)((P4 *)this)->i)<2))) continue; - /* merge: commit_count[i] = 0(8, 3, 8) */ + /* merge: commit_count[i] = 0(7, 3, 7) */ reached[4][3] = 1; - (trpt+1)->bup.ovals = grab_ints(3); + (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ]); now.commit_count[ Index(((P4 *)this)->i, 2) ] = 0; #ifdef VAR_RANGES logval("commit_count[:init::i]", ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ])); #endif ; - /* merge: retrieve_count[i] = 0(8, 4, 8) */ + /* merge: i = (i+1)(7, 4, 7) */ reached[4][4] = 1; - (trpt+1)->bup.ovals[1] = ((int)now.retrieve_count[ Index(((int)((P4 *)this)->i), 2) ]); - now.retrieve_count[ Index(((P4 *)this)->i, 2) ] = 0; -#ifdef VAR_RANGES - logval("retrieve_count[:init::i]", ((int)now.retrieve_count[ Index(((int)((P4 *)this)->i), 2) ])); -#endif - ; - /* merge: i = (i+1)(8, 5, 8) */ - reached[4][5] = 1; - (trpt+1)->bup.ovals[2] = ((int)((P4 *)this)->i); + (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 9, 8) */ - reached[4][9] = 1; + /* merge: .(goto)(0, 8, 7) */ + reached[4][8] = 1; ; - _m = 3; goto P999; /* 4 */ - case 5: /* STATE 6 - line 231 "buffer.spin" - [((i>=2))] (17:0:2 - 1) */ + _m = 3; goto P999; /* 3 */ + case 5: /* STATE 5 - line 231 "buffer.spin" - [((i>=2))] (16:0:2 - 1) */ IfNotBlocked - reached[4][6] = 1; + reached[4][5] = 1; if (!((((int)((P4 *)this)->i)>=2))) continue; /* dead 1: i */ (trpt+1)->bup.ovals = grab_ints(2); @@ -70,41 +62,41 @@ if (!readtrail) #endif ((P4 *)this)->i = 0; - /* merge: goto :b6(17, 7, 17) */ - reached[4][7] = 1; + /* merge: goto :b6(16, 6, 16) */ + reached[4][6] = 1; ; - /* merge: i = 0(17, 11, 17) */ - reached[4][11] = 1; + /* merge: i = 0(16, 10, 16) */ + reached[4][10] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 18, 17) */ - reached[4][18] = 1; + /* merge: .(goto)(0, 17, 16) */ + reached[4][17] = 1; ; _m = 3; goto P999; /* 3 */ - case 6: /* STATE 11 - line 233 "buffer.spin" - [i = 0] (0:17:1 - 3) */ + case 6: /* STATE 10 - line 233 "buffer.spin" - [i = 0] (0:16:1 - 3) */ IfNotBlocked - reached[4][11] = 1; + reached[4][10] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 18, 17) */ - reached[4][18] = 1; + /* merge: .(goto)(0, 17, 16) */ + reached[4][17] = 1; ; _m = 3; goto P999; /* 1 */ - case 7: /* STATE 12 - line 235 "buffer.spin" - [((i<4))] (17:0:2 - 1) */ + case 7: /* STATE 11 - line 235 "buffer.spin" - [((i<4))] (16:0:2 - 1) */ IfNotBlocked - reached[4][12] = 1; + reached[4][11] = 1; if (!((((int)((P4 *)this)->i)<4))) continue; - /* merge: buffer_use[i] = 0(17, 13, 17) */ - reached[4][13] = 1; + /* merge: buffer_use[i] = 0(16, 12, 16) */ + reached[4][12] = 1; (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 4) ]); now.buffer_use[ Index(((P4 *)this)->i, 4) ] = 0; @@ -112,21 +104,21 @@ logval("buffer_use[:init::i]", ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 4) ])); #endif ; - /* merge: i = (i+1)(17, 14, 17) */ - reached[4][14] = 1; + /* merge: i = (i+1)(16, 13, 16) */ + reached[4][13] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 18, 17) */ - reached[4][18] = 1; + /* merge: .(goto)(0, 17, 16) */ + reached[4][17] = 1; ; _m = 3; goto P999; /* 3 */ - case 8: /* STATE 15 - line 238 "buffer.spin" - [((i>=4))] (0:0:1 - 1) */ + case 8: /* STATE 14 - line 238 "buffer.spin" - [((i>=4))] (0:0:1 - 1) */ IfNotBlocked - reached[4][15] = 1; + reached[4][14] = 1; if (!((((int)((P4 *)this)->i)>=4))) continue; /* dead 1: i */ (trpt+1)->bup.oval = ((P4 *)this)->i; @@ -135,36 +127,36 @@ #endif ((P4 *)this)->i = 0; _m = 3; goto P999; /* 0 */ - case 9: /* STATE 20 - line 240 "buffer.spin" - [(run reader())] (0:0:0 - 3) */ + case 9: /* STATE 19 - line 240 "buffer.spin" - [(run reader())] (0:0:0 - 3) */ IfNotBlocked - reached[4][20] = 1; + reached[4][19] = 1; if (!(addproc(2))) continue; _m = 3; goto P999; /* 0 */ - case 10: /* STATE 21 - line 241 "buffer.spin" - [(run cleaner())] (29:0:1 - 1) */ + case 10: /* STATE 20 - line 241 "buffer.spin" - [(run cleaner())] (28:0:1 - 1) */ IfNotBlocked - reached[4][21] = 1; + reached[4][20] = 1; if (!(addproc(3))) continue; - /* merge: i = 0(0, 22, 29) */ - reached[4][22] = 1; + /* merge: i = 0(0, 21, 28) */ + reached[4][21] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 30, 29) */ - reached[4][30] = 1; + /* merge: .(goto)(0, 29, 28) */ + reached[4][29] = 1; ; _m = 3; goto P999; /* 2 */ - case 11: /* STATE 23 - line 244 "buffer.spin" - [((i<4))] (25:0:1 - 1) */ + case 11: /* STATE 22 - line 244 "buffer.spin" - [((i<4))] (24:0:1 - 1) */ IfNotBlocked - reached[4][23] = 1; + reached[4][22] = 1; if (!((((int)((P4 *)this)->i)<4))) continue; - /* merge: refcount = (refcount+1)(0, 24, 25) */ - reached[4][24] = 1; + /* merge: refcount = (refcount+1)(0, 23, 24) */ + reached[4][23] = 1; (trpt+1)->bup.oval = ((int)now.refcount); now.refcount = (((int)now.refcount)+1); #ifdef VAR_RANGES @@ -172,26 +164,26 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 12: /* STATE 25 - line 246 "buffer.spin" - [(run tracer())] (29:0:1 - 1) */ + case 12: /* STATE 24 - line 246 "buffer.spin" - [(run tracer())] (28:0:1 - 1) */ IfNotBlocked - reached[4][25] = 1; + reached[4][24] = 1; if (!(addproc(1))) continue; - /* merge: i = (i+1)(0, 26, 29) */ - reached[4][26] = 1; + /* merge: i = (i+1)(0, 25, 28) */ + reached[4][25] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 30, 29) */ - reached[4][30] = 1; + /* merge: .(goto)(0, 29, 28) */ + reached[4][29] = 1; ; _m = 3; goto P999; /* 2 */ - case 13: /* STATE 27 - line 248 "buffer.spin" - [((i>=4))] (39:0:2 - 1) */ + case 13: /* STATE 26 - line 248 "buffer.spin" - [((i>=4))] (38:0:2 - 1) */ IfNotBlocked - reached[4][27] = 1; + reached[4][26] = 1; if (!((((int)((P4 *)this)->i)>=4))) continue; /* dead 1: i */ (trpt+1)->bup.ovals = grab_ints(2); @@ -200,41 +192,41 @@ if (!readtrail) #endif ((P4 *)this)->i = 0; - /* merge: goto :b8(39, 28, 39) */ - reached[4][28] = 1; + /* merge: goto :b8(38, 27, 38) */ + reached[4][27] = 1; ; - /* merge: i = 0(39, 32, 39) */ - reached[4][32] = 1; + /* merge: i = 0(38, 31, 38) */ + reached[4][31] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 40, 39) */ - reached[4][40] = 1; + /* merge: .(goto)(0, 39, 38) */ + reached[4][39] = 1; ; _m = 3; goto P999; /* 3 */ - case 14: /* STATE 32 - line 250 "buffer.spin" - [i = 0] (0:39:1 - 3) */ + case 14: /* STATE 31 - line 250 "buffer.spin" - [i = 0] (0:38:1 - 3) */ IfNotBlocked - reached[4][32] = 1; + reached[4][31] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = 0; #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 40, 39) */ - reached[4][40] = 1; + /* merge: .(goto)(0, 39, 38) */ + reached[4][39] = 1; ; _m = 3; goto P999; /* 1 */ - case 15: /* STATE 33 - line 252 "buffer.spin" - [((i<1))] (35:0:1 - 1) */ + case 15: /* STATE 32 - line 252 "buffer.spin" - [((i<1))] (34:0:1 - 1) */ IfNotBlocked - reached[4][33] = 1; + reached[4][32] = 1; if (!((((int)((P4 *)this)->i)<1))) continue; - /* merge: refcount = (refcount+1)(0, 34, 35) */ - reached[4][34] = 1; + /* merge: refcount = (refcount+1)(0, 33, 34) */ + reached[4][33] = 1; (trpt+1)->bup.oval = ((int)now.refcount); now.refcount = (((int)now.refcount)+1); #ifdef VAR_RANGES @@ -242,26 +234,26 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 16: /* STATE 35 - line 254 "buffer.spin" - [(run switcher())] (39:0:1 - 1) */ + case 16: /* STATE 34 - line 254 "buffer.spin" - [(run switcher())] (38:0:1 - 1) */ IfNotBlocked - reached[4][35] = 1; + reached[4][34] = 1; if (!(addproc(0))) continue; - /* merge: i = (i+1)(0, 36, 39) */ - reached[4][36] = 1; + /* merge: i = (i+1)(0, 35, 38) */ + reached[4][35] = 1; (trpt+1)->bup.oval = ((int)((P4 *)this)->i); ((P4 *)this)->i = (((int)((P4 *)this)->i)+1); #ifdef VAR_RANGES logval(":init::i", ((int)((P4 *)this)->i)); #endif ; - /* merge: .(goto)(0, 40, 39) */ - reached[4][40] = 1; + /* merge: .(goto)(0, 39, 38) */ + reached[4][39] = 1; ; _m = 3; goto P999; /* 2 */ - case 17: /* STATE 37 - line 256 "buffer.spin" - [((i>=1))] (41:0:1 - 1) */ + case 17: /* STATE 36 - line 256 "buffer.spin" - [((i>=1))] (40:0:1 - 1) */ IfNotBlocked - reached[4][37] = 1; + reached[4][36] = 1; if (!((((int)((P4 *)this)->i)>=1))) continue; /* dead 1: i */ (trpt+1)->bup.oval = ((P4 *)this)->i; @@ -269,16 +261,16 @@ if (!readtrail) #endif ((P4 *)this)->i = 0; - /* merge: goto :b9(0, 38, 41) */ - reached[4][38] = 1; + /* merge: goto :b9(0, 37, 40) */ + reached[4][37] = 1; ; _m = 3; goto P999; /* 1 */ - case 18: /* STATE 43 - line 262 "buffer.spin" - [assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))] (0:52:2 - 1) */ + case 18: /* STATE 42 - line 262 "buffer.spin" - [assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))] (0:50:2 - 1) */ IfNotBlocked - reached[4][43] = 1; + reached[4][42] = 1; assert((((((int)now.write_off)-((int)now.read_off))>=0)&&((((int)now.write_off)-((int)now.read_off))<(255/2))), "(((write_off-read_off)>=0)&&((write_off-read_off)<(255/2)))", II, tt, t); - /* merge: j = 0(52, 44, 52) */ - reached[4][44] = 1; + /* merge: j = 0(50, 43, 50) */ + reached[4][43] = 1; (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)((P4 *)this)->j); ((P4 *)this)->j = 0; @@ -286,25 +278,25 @@ logval(":init::j", ((int)((P4 *)this)->j)); #endif ; - /* merge: commit_sum = 0(52, 45, 52) */ - reached[4][45] = 1; + /* merge: commit_sum = 0(50, 44, 50) */ + reached[4][44] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->commit_sum); ((P4 *)this)->commit_sum = 0; #ifdef VAR_RANGES logval(":init::commit_sum", ((int)((P4 *)this)->commit_sum)); #endif ; - /* merge: .(goto)(0, 53, 52) */ - reached[4][53] = 1; + /* merge: .(goto)(0, 51, 50) */ + reached[4][51] = 1; ; _m = 3; goto P999; /* 3 */ - case 19: /* STATE 46 - line 266 "buffer.spin" - [((j<2))] (52:0:2 - 1) */ + case 19: /* STATE 45 - line 266 "buffer.spin" - [((j<2))] (50:0:2 - 1) */ IfNotBlocked - reached[4][46] = 1; + reached[4][45] = 1; if (!((((int)((P4 *)this)->j)<2))) continue; - /* merge: commit_sum = (commit_sum+commit_count[j])(52, 47, 52) */ - reached[4][47] = 1; + /* merge: commit_sum = (commit_sum+commit_count[j])(50, 46, 50) */ + reached[4][46] = 1; (trpt+1)->bup.ovals = grab_ints(2); (trpt+1)->bup.ovals[0] = ((int)((P4 *)this)->commit_sum); ((P4 *)this)->commit_sum = (((int)((P4 *)this)->commit_sum)+((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])); @@ -312,24 +304,21 @@ logval(":init::commit_sum", ((int)((P4 *)this)->commit_sum)); #endif ; - /* merge: assert((((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2))))(52, 48, 52) */ - reached[4][48] = 1; - assert((((((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])-((int)now.retrieve_count[ Index(((int)((P4 *)this)->j), 2) ]))>=0)&&((((int)now.commit_count[ Index(((int)((P4 *)this)->j), 2) ])-((int)now.retrieve_count[ Index(((int)((P4 *)this)->j), 2) ]))<(255/2))), "(((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2)))", II, tt, t); - /* merge: j = (j+1)(52, 49, 52) */ - reached[4][49] = 1; + /* merge: j = (j+1)(50, 47, 50) */ + reached[4][47] = 1; (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->j); ((P4 *)this)->j = (((int)((P4 *)this)->j)+1); #ifdef VAR_RANGES logval(":init::j", ((int)((P4 *)this)->j)); #endif ; - /* merge: .(goto)(0, 53, 52) */ - reached[4][53] = 1; + /* merge: .(goto)(0, 51, 50) */ + reached[4][51] = 1; ; - _m = 3; goto P999; /* 4 */ - case 20: /* STATE 50 - line 273 "buffer.spin" - [((j>=2))] (58:0:1 - 1) */ + _m = 3; goto P999; /* 3 */ + case 20: /* STATE 48 - line 273 "buffer.spin" - [((j>=2))] (56:0:1 - 1) */ IfNotBlocked - reached[4][50] = 1; + reached[4][48] = 1; if (!((((int)((P4 *)this)->j)>=2))) continue; /* dead 1: j */ (trpt+1)->bup.oval = ((P4 *)this)->j; @@ -337,32 +326,32 @@ if (!readtrail) #endif ((P4 *)this)->j = 0; - /* merge: goto :b10(58, 51, 58) */ - reached[4][51] = 1; + /* merge: goto :b10(56, 49, 56) */ + reached[4][49] = 1; ; - /* merge: assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))(58, 55, 58) */ - reached[4][55] = 1; + /* merge: assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))(56, 53, 56) */ + reached[4][53] = 1; assert((((((int)now.write_off)-((int)((P4 *)this)->commit_sum))>=0)&&((((int)now.write_off)-((int)((P4 *)this)->commit_sum))<(255/2))), "(((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2)))", II, tt, t); - /* merge: assert((((4+1)>4)||(events_lost==0)))(58, 56, 58) */ - reached[4][56] = 1; + /* merge: assert((((4+1)>4)||(events_lost==0)))(56, 54, 56) */ + reached[4][54] = 1; assert((((4+1)>4)||(((int)now.events_lost)==0)), "(((4+1)>4)||(events_lost==0))", II, tt, t); _m = 3; goto P999; /* 3 */ - case 21: /* STATE 55 - line 278 "buffer.spin" - [assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))] (0:58:0 - 3) */ + case 21: /* STATE 53 - line 278 "buffer.spin" - [assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))] (0:56:0 - 3) */ IfNotBlocked - reached[4][55] = 1; + reached[4][53] = 1; assert((((((int)now.write_off)-((int)((P4 *)this)->commit_sum))>=0)&&((((int)now.write_off)-((int)((P4 *)this)->commit_sum))<(255/2))), "(((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2)))", II, tt, t); - /* merge: assert((((4+1)>4)||(events_lost==0)))(58, 56, 58) */ - reached[4][56] = 1; + /* merge: assert((((4+1)>4)||(events_lost==0)))(56, 54, 56) */ + reached[4][54] = 1; assert((((4+1)>4)||(((int)now.events_lost)==0)), "(((4+1)>4)||(events_lost==0))", II, tt, t); _m = 3; goto P999; /* 1 */ - case 22: /* STATE 58 - line 284 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 22: /* STATE 56 - line 284 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked - reached[4][58] = 1; + reached[4][56] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC cleaner */ - case 23: /* STATE 1 - line 210 "buffer.spin" - [((refcount==0))] (3:0:1 - 1) */ + case 23: /* STATE 1 - line 211 "buffer.spin" - [((refcount==0))] (3:0:1 - 1) */ IfNotBlocked reached[3][1] = 1; if (!((((int)now.refcount)==0))) @@ -376,7 +365,7 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 24: /* STATE 3 - line 212 "buffer.spin" - [(run switcher())] (7:0:0 - 1) */ + case 24: /* STATE 3 - line 213 "buffer.spin" - [(run switcher())] (7:0:0 - 1) */ IfNotBlocked reached[3][3] = 1; if (!(addproc(0))) @@ -385,20 +374,20 @@ reached[3][4] = 1; ; _m = 3; goto P999; /* 1 */ - case 25: /* STATE 9 - line 216 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 25: /* STATE 9 - line 217 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked reached[3][9] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC reader */ - case 26: /* STATE 1 - line 169 "buffer.spin" - [((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&((commit_count[((read_off%4)/(4/2))]-retrieve_count[((read_off%4)/(4/2))])==(4/2))))] (0:0:0 - 1) */ + case 26: /* STATE 1 - line 177 "buffer.spin" - [((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&(((commit_count[((read_off%4)/(4/2))]-(4/2))-(((read_off/4)*4)/2))==0)))] (0:0:0 - 1) */ IfNotBlocked reached[2][1] = 1; - if (!((((((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))>0)&&(((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))<(255/2)))&&((((int)now.commit_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])-((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]))==(4/2))))) + if (!((((((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))>0)&&(((((int)now.write_off)/(4/2))-(((int)now.read_off)/(4/2)))<(255/2)))&&(((((int)now.commit_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])-(4/2))-(((((int)now.read_off)/4)*4)/2))==0)))) continue; _m = 3; goto P999; /* 0 */ - case 27: /* STATE 2 - line 171 "buffer.spin" - [i = 0] (0:0:1 - 1) */ + case 27: /* STATE 2 - line 179 "buffer.spin" - [i = 0] (0:0:1 - 1) */ IfNotBlocked reached[2][2] = 1; (trpt+1)->bup.oval = ((int)((P2 *)this)->i); @@ -408,7 +397,7 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 28: /* STATE 3 - line 173 "buffer.spin" - [((i<(4/2)))] (9:0:2 - 1) */ + case 28: /* STATE 3 - line 181 "buffer.spin" - [((i<(4/2)))] (9:0:2 - 1) */ IfNotBlocked reached[2][3] = 1; if (!((((int)((P2 *)this)->i)<(4/2)))) @@ -437,7 +426,7 @@ reached[2][10] = 1; ; _m = 3; goto P999; /* 4 */ - case 29: /* STATE 7 - line 177 "buffer.spin" - [((i>=(4/2)))] (11:0:1 - 1) */ + case 29: /* STATE 7 - line 185 "buffer.spin" - [((i>=(4/2)))] (11:0:1 - 1) */ IfNotBlocked reached[2][7] = 1; if (!((((int)((P2 *)this)->i)>=(4/2)))) @@ -451,8 +440,8 @@ reached[2][8] = 1; ; _m = 3; goto P999; /* 1 */ -/* STATE 13 - line 187 "buffer.spin" - [i = 0] (0:0 - 1) same as 27 (0:0 - 1) */ - case 30: /* STATE 14 - line 189 "buffer.spin" - [((i<(4/2)))] (19:0:2 - 1) */ +/* STATE 13 - line 191 "buffer.spin" - [i = 0] (0:0 - 1) same as 27 (0:0 - 1) */ + case 30: /* STATE 14 - line 193 "buffer.spin" - [((i<(4/2)))] (19:0:2 - 1) */ IfNotBlocked reached[2][14] = 1; if (!((((int)((P2 *)this)->i)<(4/2)))) @@ -478,92 +467,41 @@ reached[2][20] = 1; ; _m = 3; goto P999; /* 3 */ - case 31: /* STATE 17 - line 192 "buffer.spin" - [((i>=(4/2)))] (28:0:4 - 1) */ + case 31: /* STATE 17 - line 196 "buffer.spin" - [((i>=(4/2)))] (0:0:1 - 1) */ IfNotBlocked reached[2][17] = 1; if (!((((int)((P2 *)this)->i)>=(4/2)))) continue; - /* dead 1: i */ (trpt+1)->bup.ovals = grab_ints(4); - (trpt+1)->bup.ovals[0] = ((P2 *)this)->i; + /* dead 1: i */ (trpt+1)->bup.oval = ((P2 *)this)->i; #ifdef HAS_CODE if (!readtrail) #endif ((P2 *)this)->i = 0; - /* merge: goto :b4(28, 18, 28) */ - reached[2][18] = 1; - ; - /* merge: tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))(28, 22, 28) */ - reached[2][22] = 1; - (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->tmp_retrieve); - ((P2 *)this)->tmp_retrieve = (((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])+(4/2)); -#ifdef VAR_RANGES - logval("reader:tmp_retrieve", ((int)((P2 *)this)->tmp_retrieve)); -#endif - ; - /* merge: retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve(28, 23, 28) */ - reached[2][23] = 1; - (trpt+1)->bup.ovals[2] = ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]); - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = ((int)((P2 *)this)->tmp_retrieve); -#ifdef VAR_RANGES - logval("retrieve_count[((read_off%4)/(4/2))]", ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])); -#endif - ; - /* merge: read_off = (read_off+(4/2))(28, 24, 28) */ - reached[2][24] = 1; - (trpt+1)->bup.ovals[3] = ((int)now.read_off); - now.read_off = (((int)now.read_off)+(4/2)); -#ifdef VAR_RANGES - logval("read_off", ((int)now.read_off)); -#endif - ; - /* merge: .(goto)(0, 29, 28) */ - reached[2][29] = 1; - ; - _m = 3; goto P999; /* 5 */ - case 32: /* STATE 22 - line 194 "buffer.spin" - [tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))] (0:28:3 - 3) */ + _m = 3; goto P999; /* 0 */ + case 32: /* STATE 22 - line 198 "buffer.spin" - [read_off = (read_off+(4/2))] (0:0:1 - 1) */ IfNotBlocked reached[2][22] = 1; - (trpt+1)->bup.ovals = grab_ints(3); - (trpt+1)->bup.ovals[0] = ((int)((P2 *)this)->tmp_retrieve); - ((P2 *)this)->tmp_retrieve = (((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])+(4/2)); -#ifdef VAR_RANGES - logval("reader:tmp_retrieve", ((int)((P2 *)this)->tmp_retrieve)); -#endif - ; - /* merge: retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve(28, 23, 28) */ - reached[2][23] = 1; - (trpt+1)->bup.ovals[1] = ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ]); - now.retrieve_count[ Index(((now.read_off%4)/(4/2)), 2) ] = ((int)((P2 *)this)->tmp_retrieve); -#ifdef VAR_RANGES - logval("retrieve_count[((read_off%4)/(4/2))]", ((int)now.retrieve_count[ Index(((((int)now.read_off)%4)/(4/2)), 2) ])); -#endif - ; - /* merge: read_off = (read_off+(4/2))(28, 24, 28) */ - reached[2][24] = 1; - (trpt+1)->bup.ovals[2] = ((int)now.read_off); + (trpt+1)->bup.oval = ((int)now.read_off); now.read_off = (((int)now.read_off)+(4/2)); #ifdef VAR_RANGES logval("read_off", ((int)now.read_off)); #endif ; - /* merge: .(goto)(0, 29, 28) */ - reached[2][29] = 1; - ; - _m = 3; goto P999; /* 3 */ - case 33: /* STATE 26 - line 199 "buffer.spin" - [((read_off>=(4-events_lost)))] (0:0:0 - 1) */ + _m = 3; goto P999; /* 0 */ + case 33: /* STATE 24 - line 200 "buffer.spin" - [((read_off>=(4-events_lost)))] (0:0:0 - 1) */ IfNotBlocked - reached[2][26] = 1; + reached[2][24] = 1; if (!((((int)now.read_off)>=(4-((int)now.events_lost))))) continue; _m = 3; goto P999; /* 0 */ - case 34: /* STATE 31 - line 201 "buffer.spin" - [-end-] (0:0:0 - 3) */ + case 34: /* STATE 29 - line 202 "buffer.spin" - [-end-] (0:0:0 - 3) */ IfNotBlocked - reached[2][31] = 1; + reached[2][29] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC tracer */ - case 35: /* STATE 1 - line 99 "buffer.spin" - [prev_off = write_off] (0:10:2 - 1) */ + case 35: /* STATE 1 - line 106 "buffer.spin" - [prev_off = write_off] (0:10:2 - 1) */ IfNotBlocked reached[1][1] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -582,7 +520,7 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 36: /* STATE 4 - line 104 "buffer.spin" - [((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))] (0:0:1 - 1) */ + case 36: /* STATE 4 - line 111 "buffer.spin" - [((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))] (0:0:1 - 1) */ IfNotBlocked reached[1][4] = 1; if (!((((((int)((P1 *)this)->new_off)-((int)now.read_off))>4)&&((((int)((P1 *)this)->new_off)-((int)now.read_off))<(255/2))))) @@ -593,7 +531,7 @@ #endif ((P1 *)this)->new_off = 0; _m = 3; goto P999; /* 0 */ - case 37: /* STATE 7 - line 106 "buffer.spin" - [(1)] (27:0:0 - 1) */ + case 37: /* STATE 7 - line 113 "buffer.spin" - [(1)] (27:0:0 - 1) */ IfNotBlocked reached[1][7] = 1; if (!(1)) @@ -602,7 +540,7 @@ reached[1][9] = 1; ; _m = 3; goto P999; /* 1 */ - case 38: /* STATE 11 - line 111 "buffer.spin" - [((prev_off!=write_off))] (3:0:1 - 1) */ + case 38: /* STATE 11 - line 118 "buffer.spin" - [((prev_off!=write_off))] (3:0:1 - 1) */ IfNotBlocked reached[1][11] = 1; if (!((((int)((P1 *)this)->prev_off)!=((int)now.write_off)))) @@ -616,7 +554,7 @@ reached[1][12] = 1; ; _m = 3; goto P999; /* 1 */ - case 39: /* STATE 14 - line 112 "buffer.spin" - [write_off = new_off] (0:24:2 - 1) */ + case 39: /* STATE 14 - line 119 "buffer.spin" - [write_off = new_off] (0:24:2 - 1) */ IfNotBlocked reached[1][14] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -641,7 +579,7 @@ reached[1][25] = 1; ; _m = 3; goto P999; /* 3 */ - case 40: /* STATE 17 - line 114 "buffer.spin" - [i = 0] (0:24:1 - 2) */ + case 40: /* STATE 17 - line 121 "buffer.spin" - [i = 0] (0:24:1 - 2) */ IfNotBlocked reached[1][17] = 1; (trpt+1)->bup.oval = ((int)((P1 *)this)->i); @@ -654,7 +592,7 @@ reached[1][25] = 1; ; _m = 3; goto P999; /* 1 */ - case 41: /* STATE 18 - line 116 "buffer.spin" - [((ii)<((int)((P1 *)this)->size)))) @@ -683,7 +621,7 @@ reached[1][25] = 1; ; _m = 3; goto P999; /* 4 */ - case 42: /* STATE 22 - line 120 "buffer.spin" - [((i>=size))] (26:0:1 - 1) */ + case 42: /* STATE 22 - line 127 "buffer.spin" - [((i>=size))] (26:0:1 - 1) */ IfNotBlocked reached[1][22] = 1; if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size)))) @@ -697,7 +635,7 @@ reached[1][23] = 1; ; _m = 3; goto P999; /* 1 */ - case 43: /* STATE 28 - line 127 "buffer.spin" - [i = 0] (0:0:1 - 1) */ + case 43: /* STATE 28 - line 134 "buffer.spin" - [i = 0] (0:0:1 - 1) */ IfNotBlocked reached[1][28] = 1; (trpt+1)->bup.oval = ((int)((P1 *)this)->i); @@ -707,7 +645,7 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 44: /* STATE 29 - line 129 "buffer.spin" - [((ii)<((int)((P1 *)this)->size)))) @@ -733,7 +671,7 @@ reached[1][35] = 1; ; _m = 3; goto P999; /* 3 */ - case 45: /* STATE 32 - line 132 "buffer.spin" - [((i>=size))] (43:0:3 - 1) */ + case 45: /* STATE 32 - line 139 "buffer.spin" - [((i>=size))] (43:0:3 - 1) */ IfNotBlocked reached[1][32] = 1; if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size)))) @@ -764,7 +702,7 @@ #endif ; _m = 3; goto P999; /* 3 */ - case 46: /* STATE 37 - line 134 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:43:2 - 3) */ + case 46: /* STATE 37 - line 141 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:43:2 - 3) */ IfNotBlocked reached[1][37] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -783,20 +721,25 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 47: /* STATE 39 - line 137 "buffer.spin" - [(((tmp_commit%(4/2))==0))] (49:0:2 - 1) */ + case 47: /* STATE 39 - line 145 "buffer.spin" - [((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))] (49:0:3 - 1) */ IfNotBlocked reached[1][39] = 1; - if (!(((((int)((P1 *)this)->tmp_commit)%(4/2))==0))) + if (!((((((((int)((P1 *)this)->prev_off)/4)*4)/2)+(4/2))-((int)((P1 *)this)->tmp_commit)))) continue; - /* dead 1: tmp_commit */ (trpt+1)->bup.ovals = grab_ints(2); - (trpt+1)->bup.ovals[0] = ((P1 *)this)->tmp_commit; + /* dead 1: prev_off */ (trpt+1)->bup.ovals = grab_ints(3); + (trpt+1)->bup.ovals[0] = ((P1 *)this)->prev_off; +#ifdef HAS_CODE + if (!readtrail) +#endif + ((P1 *)this)->prev_off = 0; + /* dead 1: tmp_commit */ (trpt+1)->bup.ovals[1] = ((P1 *)this)->tmp_commit; #ifdef HAS_CODE if (!readtrail) #endif ((P1 *)this)->tmp_commit = 0; /* merge: deliver = 1(49, 40, 49) */ reached[1][40] = 1; - (trpt+1)->bup.ovals[1] = ((int)deliver); + (trpt+1)->bup.ovals[2] = ((int)deliver); deliver = 1; #ifdef VAR_RANGES logval("deliver", ((int)deliver)); @@ -806,12 +749,12 @@ reached[1][44] = 1; ; _m = 3; goto P999; /* 2 */ - case 48: /* STATE 44 - line 140 "buffer.spin" - [.(goto)] (0:49:0 - 2) */ + case 48: /* STATE 44 - line 150 "buffer.spin" - [.(goto)] (0:49:0 - 2) */ IfNotBlocked reached[1][44] = 1; ; _m = 3; goto P999; /* 0 */ - case 49: /* STATE 42 - line 138 "buffer.spin" - [(1)] (49:0:0 - 1) */ + case 49: /* STATE 42 - line 148 "buffer.spin" - [(1)] (49:0:0 - 1) */ IfNotBlocked reached[1][42] = 1; if (!(1)) @@ -820,7 +763,7 @@ reached[1][44] = 1; ; _m = 3; goto P999; /* 1 */ - case 50: /* STATE 47 - line 144 "buffer.spin" - [events_lost = (events_lost+1)] (0:0:1 - 2) */ + case 50: /* STATE 47 - line 154 "buffer.spin" - [events_lost = (events_lost+1)] (0:0:1 - 2) */ IfNotBlocked reached[1][47] = 1; (trpt+1)->bup.oval = ((int)now.events_lost); @@ -830,7 +773,7 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 51: /* STATE 48 - line 146 "buffer.spin" - [refcount = (refcount-1)] (0:0:1 - 2) */ + case 51: /* STATE 48 - line 156 "buffer.spin" - [refcount = (refcount-1)] (0:0:1 - 2) */ IfNotBlocked reached[1][48] = 1; (trpt+1)->bup.oval = ((int)now.refcount); @@ -840,14 +783,14 @@ #endif ; _m = 3; goto P999; /* 0 */ - case 52: /* STATE 50 - line 148 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 52: /* STATE 50 - line 158 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked reached[1][50] = 1; if (!delproc(1, II)) continue; _m = 3; goto P999; /* 0 */ /* PROC switcher */ - case 53: /* STATE 1 - line 56 "buffer.spin" - [prev_off = write_off] (0:9:3 - 1) */ + case 53: /* STATE 1 - line 60 "buffer.spin" - [prev_off = write_off] (0:9:3 - 1) */ IfNotBlocked reached[0][1] = 1; (trpt+1)->bup.ovals = grab_ints(3); @@ -874,7 +817,7 @@ #endif ; _m = 3; goto P999; /* 2 */ - case 54: /* STATE 4 - line 61 "buffer.spin" - [(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))] (29:0:3 - 1) */ + case 54: /* STATE 4 - line 65 "buffer.spin" - [(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))] (29:0:3 - 1) */ IfNotBlocked reached[0][4] = 1; if (!(((((((int)((P0 *)this)->new_off)-((int)now.read_off))>4)&&((((int)((P0 *)this)->new_off)-((int)now.read_off))<(255/2)))||(((int)((P0 *)this)->size)==(4/2))))) @@ -902,7 +845,7 @@ reached[0][6] = 1; ; _m = 3; goto P999; /* 2 */ - case 55: /* STATE 8 - line 64 "buffer.spin" - [(1)] (18:0:0 - 1) */ + case 55: /* STATE 8 - line 68 "buffer.spin" - [(1)] (18:0:0 - 1) */ IfNotBlocked reached[0][8] = 1; if (!(1)) @@ -911,7 +854,7 @@ reached[0][10] = 1; ; _m = 3; goto P999; /* 1 */ - case 56: /* STATE 12 - line 69 "buffer.spin" - [((prev_off!=write_off))] (11:0:1 - 1) */ + case 56: /* STATE 12 - line 73 "buffer.spin" - [((prev_off!=write_off))] (11:0:1 - 1) */ IfNotBlocked reached[0][12] = 1; if (!((((int)((P0 *)this)->prev_off)!=((int)now.write_off)))) @@ -925,12 +868,12 @@ reached[0][13] = 1; ; _m = 3; goto P999; /* 1 */ - case 57: /* STATE 17 - line 72 "buffer.spin" - [.(goto)] (0:28:0 - 1) */ + case 57: /* STATE 17 - line 76 "buffer.spin" - [.(goto)] (0:28:0 - 1) */ IfNotBlocked reached[0][17] = 1; ; _m = 3; goto P999; /* 0 */ - case 58: /* STATE 15 - line 70 "buffer.spin" - [write_off = new_off] (0:28:1 - 1) */ + case 58: /* STATE 15 - line 74 "buffer.spin" - [write_off = new_off] (0:28:1 - 1) */ IfNotBlocked reached[0][15] = 1; (trpt+1)->bup.oval = ((int)now.write_off); @@ -943,7 +886,7 @@ reached[0][17] = 1; ; _m = 3; goto P999; /* 1 */ - case 59: /* STATE 19 - line 75 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:25:2 - 1) */ + case 59: /* STATE 19 - line 79 "buffer.spin" - [tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)] (0:25:2 - 1) */ IfNotBlocked reached[0][19] = 1; (trpt+1)->bup.ovals = grab_ints(2); @@ -962,20 +905,25 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 60: /* STATE 21 - line 78 "buffer.spin" - [(((tmp_commit%(4/2))==0))] (29:0:3 - 1) */ + case 60: /* STATE 21 - line 83 "buffer.spin" - [((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))] (29:0:4 - 1) */ IfNotBlocked reached[0][21] = 1; - if (!(((((int)((P0 *)this)->tmp_commit)%(4/2))==0))) + if (!((((((((int)((P0 *)this)->prev_off)/4)*4)/2)+(4/2))-((int)((P0 *)this)->tmp_commit)))) continue; - /* dead 1: tmp_commit */ (trpt+1)->bup.ovals = grab_ints(3); - (trpt+1)->bup.ovals[0] = ((P0 *)this)->tmp_commit; + /* dead 1: prev_off */ (trpt+1)->bup.ovals = grab_ints(4); + (trpt+1)->bup.ovals[0] = ((P0 *)this)->prev_off; +#ifdef HAS_CODE + if (!readtrail) +#endif + ((P0 *)this)->prev_off = 0; + /* dead 1: tmp_commit */ (trpt+1)->bup.ovals[1] = ((P0 *)this)->tmp_commit; #ifdef HAS_CODE if (!readtrail) #endif ((P0 *)this)->tmp_commit = 0; /* merge: deliver = 1(29, 22, 29) */ reached[0][22] = 1; - (trpt+1)->bup.ovals[1] = ((int)deliver); + (trpt+1)->bup.ovals[2] = ((int)deliver); deliver = 1; #ifdef VAR_RANGES logval("deliver", ((int)deliver)); @@ -986,14 +934,14 @@ ; /* merge: refcount = (refcount-1)(29, 27, 29) */ reached[0][27] = 1; - (trpt+1)->bup.ovals[2] = ((int)now.refcount); + (trpt+1)->bup.ovals[3] = ((int)now.refcount); now.refcount = (((int)now.refcount)-1); #ifdef VAR_RANGES logval("refcount", ((int)now.refcount)); #endif ; _m = 3; goto P999; /* 3 */ - case 61: /* STATE 26 - line 81 "buffer.spin" - [.(goto)] (0:29:1 - 2) */ + case 61: /* STATE 26 - line 88 "buffer.spin" - [.(goto)] (0:29:1 - 2) */ IfNotBlocked reached[0][26] = 1; ; @@ -1006,7 +954,7 @@ #endif ; _m = 3; goto P999; /* 1 */ - case 62: /* STATE 24 - line 79 "buffer.spin" - [(1)] (29:0:1 - 1) */ + case 62: /* STATE 24 - line 86 "buffer.spin" - [(1)] (29:0:1 - 1) */ IfNotBlocked reached[0][24] = 1; if (!(1)) @@ -1023,7 +971,7 @@ #endif ; _m = 3; goto P999; /* 2 */ - case 63: /* STATE 30 - line 85 "buffer.spin" - [-end-] (0:0:0 - 1) */ + case 63: /* STATE 30 - line 92 "buffer.spin" - [-end-] (0:0:0 - 1) */ IfNotBlocked reached[0][30] = 1; if (!delproc(1, II)) continue; diff --git a/trunk/verif/examples/pan.t b/trunk/verif/examples/pan.t index 4dc0dfa0..217eaf43 100644 --- a/trunk/verif/examples/pan.t +++ b/trunk/verif/examples/pan.t @@ -26,123 +26,121 @@ settable(void) /* proctype 4: :init: */ - trans[4] = (Trans **) emalloc(59*sizeof(Trans *)); - - T = trans[ 4][42] = settr(161,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(161,2,1,0,0,"ATOMIC", 1, 2, 0); - trans[4][1] = settr(120,2,8,3,3,"i = 0", 1, 2, 0); - trans[4][9] = settr(128,2,8,1,0,".(goto)", 1, 2, 0); - T = trans[4][8] = settr(127,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(127,2,2,0,0,"DO", 1, 2, 0); - T->nxt = settr(127,2,6,0,0,"DO", 1, 2, 0); - trans[4][2] = settr(121,2,8,4,4,"((i<2))", 1, 2, 0); /* m: 3 -> 8,0 */ + trans[4] = (Trans **) emalloc(57*sizeof(Trans *)); + + T = trans[ 4][41] = settr(158,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(158,2,1,0,0,"ATOMIC", 1, 2, 0); + trans[4][1] = settr(118,2,7,3,3,"i = 0", 1, 2, 0); + trans[4][8] = settr(125,2,7,1,0,".(goto)", 1, 2, 0); + T = trans[4][7] = settr(124,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(124,2,2,0,0,"DO", 1, 2, 0); + T->nxt = settr(124,2,5,0,0,"DO", 1, 2, 0); + trans[4][2] = settr(119,2,7,4,4,"((i<2))", 1, 2, 0); /* m: 3 -> 7,0 */ reached4[3] = 1; trans[4][3] = settr(0,0,0,0,0,"commit_count[i] = 0",0,0,0); - trans[4][4] = settr(0,0,0,0,0,"retrieve_count[i] = 0",0,0,0); - trans[4][5] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][6] = settr(125,2,17,5,5,"((i>=2))", 1, 2, 0); /* m: 11 -> 17,0 */ - reached4[11] = 1; - trans[4][7] = settr(126,2,11,1,0,"goto :b6", 1, 2, 0); /* m: 11 -> 0,17 */ - reached4[11] = 1; - trans[4][10] = settr(129,2,11,1,0,"break", 1, 2, 0); - trans[4][11] = settr(130,2,17,6,6,"i = 0", 1, 2, 0); - trans[4][18] = settr(137,2,17,1,0,".(goto)", 1, 2, 0); - T = trans[4][17] = settr(136,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(136,2,12,0,0,"DO", 1, 2, 0); - T->nxt = settr(136,2,15,0,0,"DO", 1, 2, 0); - trans[4][12] = settr(131,2,17,7,7,"((i<4))", 1, 2, 0); /* m: 13 -> 17,0 */ - reached4[13] = 1; - trans[4][13] = settr(0,0,0,0,0,"buffer_use[i] = 0",0,0,0); - trans[4][14] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][15] = settr(134,2,20,8,8,"((i>=4))", 1, 2, 0); - trans[4][16] = settr(135,2,20,1,0,"goto :b7", 1, 2, 0); - trans[4][19] = settr(138,2,20,1,0,"break", 1, 2, 0); - trans[4][20] = settr(139,2,21,9,9,"(run reader())", 1, 2, 0); - trans[4][21] = settr(140,2,29,10,10,"(run cleaner())", 1, 2, 0); /* m: 22 -> 29,0 */ - reached4[22] = 1; - trans[4][22] = settr(0,0,0,0,0,"i = 0",0,0,0); - trans[4][30] = settr(149,2,29,1,0,".(goto)", 1, 2, 0); - T = trans[4][29] = settr(148,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(148,2,23,0,0,"DO", 1, 2, 0); - T->nxt = settr(148,2,27,0,0,"DO", 1, 2, 0); - trans[4][23] = settr(142,2,25,11,11,"((i<4))", 1, 2, 0); /* m: 24 -> 25,0 */ - reached4[24] = 1; - trans[4][24] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); - trans[4][25] = settr(144,2,29,12,12,"(run tracer())", 1, 2, 0); /* m: 26 -> 29,0 */ - reached4[26] = 1; - trans[4][26] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][27] = settr(146,2,39,13,13,"((i>=4))", 1, 2, 0); /* m: 32 -> 39,0 */ - reached4[32] = 1; - trans[4][28] = settr(147,2,32,1,0,"goto :b8", 1, 2, 0); /* m: 32 -> 0,39 */ - reached4[32] = 1; - trans[4][31] = settr(150,2,32,1,0,"break", 1, 2, 0); - trans[4][32] = settr(151,2,39,14,14,"i = 0", 1, 2, 0); - trans[4][40] = settr(159,2,39,1,0,".(goto)", 1, 2, 0); - T = trans[4][39] = settr(158,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(158,2,33,0,0,"DO", 1, 2, 0); - T->nxt = settr(158,2,37,0,0,"DO", 1, 2, 0); - trans[4][33] = settr(152,2,35,15,15,"((i<1))", 1, 2, 0); /* m: 34 -> 35,0 */ - reached4[34] = 1; - trans[4][34] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); - trans[4][35] = settr(154,2,39,16,16,"(run switcher())", 1, 2, 0); /* m: 36 -> 39,0 */ - reached4[36] = 1; - trans[4][36] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[4][37] = settr(156,2,41,17,17,"((i>=1))", 1, 2, 0); /* m: 38 -> 41,0 */ - reached4[38] = 1; - trans[4][38] = settr(157,2,41,1,0,"goto :b9", 1, 2, 0); - trans[4][41] = settr(160,0,57,1,0,"break", 1, 2, 0); - T = trans[ 4][57] = settr(176,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(176,2,43,0,0,"ATOMIC", 1, 2, 0); - trans[4][43] = settr(162,2,52,18,18,"assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))", 1, 2, 0); /* m: 44 -> 0,52 */ - reached4[44] = 1; - trans[4][44] = settr(0,0,0,0,0,"j = 0",0,0,0); - trans[4][45] = settr(0,0,0,0,0,"commit_sum = 0",0,0,0); - trans[4][53] = settr(172,2,52,1,0,".(goto)", 1, 2, 0); - T = trans[4][52] = settr(171,2,0,0,0,"DO", 1, 2, 0); - T = T->nxt = settr(171,2,46,0,0,"DO", 1, 2, 0); - T->nxt = settr(171,2,50,0,0,"DO", 1, 2, 0); - trans[4][46] = settr(165,2,52,19,19,"((j<2))", 1, 2, 0); /* m: 47 -> 52,0 */ - reached4[47] = 1; - trans[4][47] = settr(0,0,0,0,0,"commit_sum = (commit_sum+commit_count[j])",0,0,0); - trans[4][48] = settr(0,0,0,0,0,"assert((((commit_count[j]-retrieve_count[j])>=0)&&((commit_count[j]-retrieve_count[j])<(255/2))))",0,0,0); - trans[4][49] = settr(0,0,0,0,0,"j = (j+1)",0,0,0); - trans[4][50] = settr(169,4,58,20,20,"((j>=2))", 1, 2, 0); /* m: 55 -> 58,0 */ - reached4[55] = 1; - trans[4][51] = settr(170,2,55,1,0,"goto :b10", 1, 2, 0); /* m: 55 -> 0,58 */ - reached4[55] = 1; - trans[4][54] = settr(173,2,55,1,0,"break", 1, 2, 0); - trans[4][55] = settr(174,4,58,21,21,"assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))", 1, 2, 0); /* m: 56 -> 0,58 */ - reached4[56] = 1; - trans[4][56] = settr(0,0,0,0,0,"assert((((4+1)>4)||(events_lost==0)))",0,0,0); - trans[4][58] = settr(177,0,0,22,22,"-end-", 0, 3500, 0); + trans[4][4] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][5] = settr(122,2,16,5,5,"((i>=2))", 1, 2, 0); /* m: 10 -> 16,0 */ + reached4[10] = 1; + trans[4][6] = settr(123,2,10,1,0,"goto :b6", 1, 2, 0); /* m: 10 -> 0,16 */ + reached4[10] = 1; + trans[4][9] = settr(126,2,10,1,0,"break", 1, 2, 0); + trans[4][10] = settr(127,2,16,6,6,"i = 0", 1, 2, 0); + trans[4][17] = settr(134,2,16,1,0,".(goto)", 1, 2, 0); + T = trans[4][16] = settr(133,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(133,2,11,0,0,"DO", 1, 2, 0); + T->nxt = settr(133,2,14,0,0,"DO", 1, 2, 0); + trans[4][11] = settr(128,2,16,7,7,"((i<4))", 1, 2, 0); /* m: 12 -> 16,0 */ + reached4[12] = 1; + trans[4][12] = settr(0,0,0,0,0,"buffer_use[i] = 0",0,0,0); + trans[4][13] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][14] = settr(131,2,19,8,8,"((i>=4))", 1, 2, 0); + trans[4][15] = settr(132,2,19,1,0,"goto :b7", 1, 2, 0); + trans[4][18] = settr(135,2,19,1,0,"break", 1, 2, 0); + trans[4][19] = settr(136,2,20,9,9,"(run reader())", 1, 2, 0); + trans[4][20] = settr(137,2,28,10,10,"(run cleaner())", 1, 2, 0); /* m: 21 -> 28,0 */ + reached4[21] = 1; + trans[4][21] = settr(0,0,0,0,0,"i = 0",0,0,0); + trans[4][29] = settr(146,2,28,1,0,".(goto)", 1, 2, 0); + T = trans[4][28] = settr(145,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(145,2,22,0,0,"DO", 1, 2, 0); + T->nxt = settr(145,2,26,0,0,"DO", 1, 2, 0); + trans[4][22] = settr(139,2,24,11,11,"((i<4))", 1, 2, 0); /* m: 23 -> 24,0 */ + reached4[23] = 1; + trans[4][23] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); + trans[4][24] = settr(141,2,28,12,12,"(run tracer())", 1, 2, 0); /* m: 25 -> 28,0 */ + reached4[25] = 1; + trans[4][25] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][26] = settr(143,2,38,13,13,"((i>=4))", 1, 2, 0); /* m: 31 -> 38,0 */ + reached4[31] = 1; + trans[4][27] = settr(144,2,31,1,0,"goto :b8", 1, 2, 0); /* m: 31 -> 0,38 */ + reached4[31] = 1; + trans[4][30] = settr(147,2,31,1,0,"break", 1, 2, 0); + trans[4][31] = settr(148,2,38,14,14,"i = 0", 1, 2, 0); + trans[4][39] = settr(156,2,38,1,0,".(goto)", 1, 2, 0); + T = trans[4][38] = settr(155,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(155,2,32,0,0,"DO", 1, 2, 0); + T->nxt = settr(155,2,36,0,0,"DO", 1, 2, 0); + trans[4][32] = settr(149,2,34,15,15,"((i<1))", 1, 2, 0); /* m: 33 -> 34,0 */ + reached4[33] = 1; + trans[4][33] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); + trans[4][34] = settr(151,2,38,16,16,"(run switcher())", 1, 2, 0); /* m: 35 -> 38,0 */ + reached4[35] = 1; + trans[4][35] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); + trans[4][36] = settr(153,2,40,17,17,"((i>=1))", 1, 2, 0); /* m: 37 -> 40,0 */ + reached4[37] = 1; + trans[4][37] = settr(154,2,40,1,0,"goto :b9", 1, 2, 0); + trans[4][40] = settr(157,0,55,1,0,"break", 1, 2, 0); + T = trans[ 4][55] = settr(172,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(172,2,42,0,0,"ATOMIC", 1, 2, 0); + trans[4][42] = settr(159,2,50,18,18,"assert((((write_off-read_off)>=0)&&((write_off-read_off)<(255/2))))", 1, 2, 0); /* m: 43 -> 0,50 */ + reached4[43] = 1; + trans[4][43] = settr(0,0,0,0,0,"j = 0",0,0,0); + trans[4][44] = settr(0,0,0,0,0,"commit_sum = 0",0,0,0); + trans[4][51] = settr(168,2,50,1,0,".(goto)", 1, 2, 0); + T = trans[4][50] = settr(167,2,0,0,0,"DO", 1, 2, 0); + T = T->nxt = settr(167,2,45,0,0,"DO", 1, 2, 0); + T->nxt = settr(167,2,48,0,0,"DO", 1, 2, 0); + trans[4][45] = settr(162,2,50,19,19,"((j<2))", 1, 2, 0); /* m: 46 -> 50,0 */ + reached4[46] = 1; + trans[4][46] = settr(0,0,0,0,0,"commit_sum = (commit_sum+commit_count[j])",0,0,0); + trans[4][47] = settr(0,0,0,0,0,"j = (j+1)",0,0,0); + trans[4][48] = settr(165,4,56,20,20,"((j>=2))", 1, 2, 0); /* m: 53 -> 56,0 */ + reached4[53] = 1; + trans[4][49] = settr(166,2,53,1,0,"goto :b10", 1, 2, 0); /* m: 53 -> 0,56 */ + reached4[53] = 1; + trans[4][52] = settr(169,2,53,1,0,"break", 1, 2, 0); + trans[4][53] = settr(170,4,56,21,21,"assert((((write_off-commit_sum)>=0)&&((write_off-commit_sum)<(255/2))))", 1, 2, 0); /* m: 54 -> 0,56 */ + reached4[54] = 1; + trans[4][54] = settr(0,0,0,0,0,"assert((((4+1)>4)||(events_lost==0)))",0,0,0); + trans[4][56] = settr(173,0,0,22,22,"-end-", 0, 3500, 0); /* proctype 3: cleaner */ trans[3] = (Trans **) emalloc(10*sizeof(Trans *)); - T = trans[ 3][8] = settr(118,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(118,2,5,0,0,"ATOMIC", 1, 2, 0); - trans[3][6] = settr(116,2,5,1,0,".(goto)", 1, 2, 0); - T = trans[3][5] = settr(115,2,0,0,0,"DO", 1, 2, 0); - T->nxt = settr(115,2,1,0,0,"DO", 1, 2, 0); - trans[3][1] = settr(111,2,3,23,23,"((refcount==0))", 1, 2, 0); /* m: 2 -> 3,0 */ + T = trans[ 3][8] = settr(116,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(116,2,5,0,0,"ATOMIC", 1, 2, 0); + trans[3][6] = settr(114,2,5,1,0,".(goto)", 1, 2, 0); + T = trans[3][5] = settr(113,2,0,0,0,"DO", 1, 2, 0); + T->nxt = settr(113,2,1,0,0,"DO", 1, 2, 0); + trans[3][1] = settr(109,2,3,23,23,"((refcount==0))", 1, 2, 0); /* m: 2 -> 3,0 */ reached3[2] = 1; trans[3][2] = settr(0,0,0,0,0,"refcount = (refcount+1)",0,0,0); - trans[3][3] = settr(113,2,7,24,24,"(run switcher())", 1, 2, 0); /* m: 4 -> 7,0 */ + trans[3][3] = settr(111,2,7,24,24,"(run switcher())", 1, 2, 0); /* m: 4 -> 7,0 */ reached3[4] = 1; - trans[3][4] = settr(114,2,7,1,0,"goto :b5", 1, 2, 0); - trans[3][7] = settr(117,0,9,1,0,"break", 1, 2, 0); - trans[3][9] = settr(119,0,0,25,25,"-end-", 0, 3500, 0); + trans[3][4] = settr(112,2,7,1,0,"goto :b5", 1, 2, 0); + trans[3][7] = settr(115,0,9,1,0,"break", 1, 2, 0); + trans[3][9] = settr(117,0,0,25,25,"-end-", 0, 3500, 0); /* proctype 2: reader */ - trans[2] = (Trans **) emalloc(32*sizeof(Trans *)); + trans[2] = (Trans **) emalloc(30*sizeof(Trans *)); - trans[2][29] = settr(108,0,28,1,0,".(goto)", 0, 2, 0); - T = trans[2][28] = settr(107,0,0,0,0,"DO", 0, 2, 0); - T = T->nxt = settr(107,0,1,0,0,"DO", 0, 2, 0); - T->nxt = settr(107,0,26,0,0,"DO", 0, 2, 0); - trans[2][1] = settr(80,0,12,26,0,"((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&((commit_count[((read_off%4)/(4/2))]-retrieve_count[((read_off%4)/(4/2))])==(4/2))))", 1, 2, 0); + trans[2][27] = settr(106,0,26,1,0,".(goto)", 0, 2, 0); + T = trans[2][26] = settr(105,0,0,0,0,"DO", 0, 2, 0); + T = T->nxt = settr(105,0,1,0,0,"DO", 0, 2, 0); + T->nxt = settr(105,0,24,0,0,"DO", 0, 2, 0); + trans[2][1] = settr(80,0,12,26,0,"((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&(((commit_count[((read_off%4)/(4/2))]-(4/2))-(((read_off/4)*4)/2))==0)))", 1, 2, 0); T = trans[ 2][12] = settr(91,2,0,0,0,"ATOMIC", 1, 2, 0); T->nxt = settr(91,2,2,0,0,"ATOMIC", 1, 2, 0); trans[2][2] = settr(81,2,9,27,27,"i = 0", 1, 2, 0); @@ -158,9 +156,9 @@ settable(void) trans[2][7] = settr(86,2,11,29,29,"((i>=(4/2)))", 1, 2, 0); /* m: 8 -> 11,0 */ reached2[8] = 1; trans[2][8] = settr(87,2,11,1,0,"goto :b3", 1, 2, 0); - trans[2][11] = settr(90,0,25,1,0,"break", 1, 2, 0); - T = trans[ 2][25] = settr(104,2,0,0,0,"ATOMIC", 1, 2, 0); - T->nxt = settr(104,2,13,0,0,"ATOMIC", 1, 2, 0); + trans[2][11] = settr(90,0,23,1,0,"break", 1, 2, 0); + T = trans[ 2][23] = settr(102,2,0,0,0,"ATOMIC", 1, 2, 0); + T->nxt = settr(102,2,13,0,0,"ATOMIC", 1, 2, 0); trans[2][13] = /* c */ settr(92,2,19,27,27,"i = 0", 1, 2, 0); trans[2][20] = settr(99,2,19,1,0,".(goto)", 1, 2, 0); T = trans[2][19] = settr(98,2,0,0,0,"DO", 1, 2, 0); @@ -170,19 +168,14 @@ settable(void) reached2[15] = 1; trans[2][15] = settr(0,0,0,0,0,"buffer_use[((read_off+i)%4)] = 0",0,0,0); trans[2][16] = settr(0,0,0,0,0,"i = (i+1)",0,0,0); - trans[2][17] = settr(96,0,28,31,31,"((i>=(4/2)))", 1, 2, 0); /* m: 22 -> 28,0 */ - reached2[22] = 1; - trans[2][18] = settr(97,2,22,1,0,"goto :b4", 1, 2, 0); /* m: 22 -> 0,28 */ - reached2[22] = 1; + trans[2][17] = settr(96,2,21,31,31,"((i>=(4/2)))", 1, 2, 0); + trans[2][18] = settr(97,2,21,1,0,"goto :b4", 1, 2, 0); trans[2][21] = settr(100,2,22,1,0,"break", 1, 2, 0); - trans[2][22] = settr(101,0,28,32,32,"tmp_retrieve = (retrieve_count[((read_off%4)/(4/2))]+(4/2))", 1, 2, 0); /* m: 23 -> 0,28 */ - reached2[23] = 1; - trans[2][23] = settr(0,0,0,0,0,"retrieve_count[((read_off%4)/(4/2))] = tmp_retrieve",0,0,0); - trans[2][24] = settr(0,0,0,0,0,"read_off = (read_off+(4/2))",0,0,0); - trans[2][26] = settr(105,0,31,33,0,"((read_off>=(4-events_lost)))", 1, 2, 0); - trans[2][27] = settr(106,0,31,1,0,"goto :b2", 0, 2, 0); - trans[2][30] = settr(109,0,31,1,0,"break", 0, 2, 0); - trans[2][31] = settr(110,0,0,34,34,"-end-", 0, 3500, 0); + trans[2][22] = settr(101,0,26,32,32,"read_off = (read_off+(4/2))", 1, 2, 0); + trans[2][24] = settr(103,0,29,33,0,"((read_off>=(4-events_lost)))", 1, 2, 0); + trans[2][25] = settr(104,0,29,1,0,"goto :b2", 0, 2, 0); + trans[2][28] = settr(107,0,29,1,0,"break", 0, 2, 0); + trans[2][29] = settr(108,0,0,34,34,"-end-", 0, 3500, 0); /* proctype 1: tracer */ @@ -253,7 +246,7 @@ settable(void) T = trans[1][43] = settr(72,2,0,0,0,"IF", 1, 2, 0); T = T->nxt = settr(72,2,39,0,0,"IF", 1, 2, 0); T->nxt = settr(72,2,41,0,0,"IF", 1, 2, 0); - trans[1][39] = settr(68,4,49,47,47,"(((tmp_commit%(4/2))==0))", 1, 2, 0); /* m: 40 -> 49,0 */ + trans[1][39] = settr(68,4,49,47,47,"((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))", 1, 2, 0); /* m: 40 -> 49,0 */ reached1[40] = 1; trans[1][40] = settr(0,0,0,0,0,"deliver = 1",0,0,0); trans[1][44] = settr(73,0,49,48,48,".(goto)", 1, 2, 0); @@ -308,7 +301,7 @@ settable(void) T = trans[0][25] = settr(24,2,0,0,0,"IF", 1, 2, 0); T = T->nxt = settr(24,2,21,0,0,"IF", 1, 2, 0); T->nxt = settr(24,2,23,0,0,"IF", 1, 2, 0); - trans[0][21] = settr(20,4,29,60,60,"(((tmp_commit%(4/2))==0))", 1, 2, 0); /* m: 22 -> 29,0 */ + trans[0][21] = settr(20,4,29,60,60,"((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))", 1, 2, 0); /* m: 22 -> 29,0 */ reached0[22] = 1; trans[0][22] = settr(0,0,0,0,0,"deliver = 1",0,0,0); trans[0][26] = settr(25,4,29,61,61,".(goto)", 1, 2, 0); /* m: 27 -> 0,29 */ diff --git a/trunk/verif/examples/run b/trunk/verif/examples/run index 5a47e644..8a2cf840 100755 --- a/trunk/verif/examples/run +++ b/trunk/verif/examples/run @@ -1,5 +1,8 @@ #!/bin/bash +#avail. mem +MEM=15360 + ../Spin/Src5.1.6/spin -a buffer.spin -cc -DSAFETY -o pan pan.c +cc -DMEMLIM=${MEM} -DSAFETY -o pan pan.c ./pan diff --git a/trunk/verif/examples/run3 b/trunk/verif/examples/run3 index 69ac0915..2dcc2cc6 100755 --- a/trunk/verif/examples/run3 +++ b/trunk/verif/examples/run3 @@ -1,5 +1,8 @@ #!/bin/bash +#avail. mem +MEM=15360 + ../Spin/Src5.1.6/spin -a buffer.spin -cc -o pan pan.c +cc -DMEMLIM=${MEM} -o pan pan.c ./pan