-// 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 <mathieu.desnoyers@polymtl.ca>
-// 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.
#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
// Reader counters
byte read_off = 0;
-byte retrieve_count[NR_SUBBUFS];
byte events_lost = 0;
byte refcount = 0;
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;
}
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 {
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
}
// 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
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;
do
:: i < NR_SUBBUFS ->
commit_count[i] = 0;
- retrieve_count[i] = 0;
i++
:: i >= NR_SUBBUFS -> break
od;
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;
-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
;
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];
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];
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;
;
;
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;
;
;
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];
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;
;
;
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];
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];
ungrab_ints(trpt->bup.ovals, 2);
goto R999;
- case 20: /* STATE 50 */
+ case 20: /* STATE 48 */
;
/* 0 */ ((P4 *)this)->j = trpt->bup.oval;
;
goto R999;
;
- case 21: /* STATE 55 */
+ case 21: /* STATE 53 */
goto R999;
- case 22: /* STATE 58 */
+ case 22: /* STATE 56 */
;
p_restor(II);
;
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);
;
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;
;
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 */
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;
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);
}
}
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
}
}
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
}
}
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;
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);
#ifndef uint
#define uint unsigned int
#endif
+#ifndef HASH32
+#define HASH64
+#endif
#define DELTA 500
#ifdef MA
#if NCORE>1 && !defined(SEP_STATE)
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 },
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 },
#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 },
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 */
uchar write_off;
uchar commit_count[2];
uchar read_off;
- uchar retrieve_count[2];
uchar events_lost;
uchar refcount;
uchar sv[VECTORSZ];
#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
_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);
#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);
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;
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;
#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
#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);
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
#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;
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;
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) ]));
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;
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)))
#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)))
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);
#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))))
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))))
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))))
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);
#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)))))
#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))
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))))
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);
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);
reached[1][25] = 1;
;
_m = 3; goto P999; /* 1 */
- case 41: /* STATE 18 - line 116 "buffer.spin" - [((i<size))] (24:0:2 - 1) */
+ case 41: /* STATE 18 - line 123 "buffer.spin" - [((i<size))] (24:0:2 - 1) */
IfNotBlocked
reached[1][18] = 1;
if (!((((int)((P1 *)this)->i)<((int)((P1 *)this)->size))))
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))))
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);
#endif
;
_m = 3; goto P999; /* 0 */
- case 44: /* STATE 29 - line 129 "buffer.spin" - [((i<size))] (34:0:2 - 1) */
+ case 44: /* STATE 29 - line 136 "buffer.spin" - [((i<size))] (34:0:2 - 1) */
IfNotBlocked
reached[1][29] = 1;
if (!((((int)((P1 *)this)->i)<((int)((P1 *)this)->size))))
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))))
#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);
#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));
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))
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);
#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);
#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);
#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)))))
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))
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))))
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);
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);
#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));
;
/* 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;
;
#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))
#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;
/* 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);
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);
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 */
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);
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 */
#!/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
#!/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
projects / lttv.git / commitdiff
