Files
@ a6f53f74e58c
Branch filter:
Location: CSY/reowolf/examples/old/eg_protocols.pdl - annotation
a6f53f74e58c
598 B
text/plain
fixed bug: failed to restore !sync_batches.is_empty() invariant when the native is immediately inconsistent
1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e 1ae65b0b574e |
primitive forward(in i, out o) {
while(true) synchronous {
put(o, get(i));
}
}
composite dynamic(in i, out o) {
new forward(i, o);
}
primitive sync(in i, out o) {
while(true) synchronous {
if(fires(i)) {
put(o, get(i));
}
}
}
primitive sync_two(in ia, in ib, out oa, out ob) {
while(true) synchronous {
if (fires(ia)) {
put(oa, get(ia));
put(ob, get(ib));
}
}
}
primitive xor_three(in ai, out ao, in bi, out bo, in ci, out co) {
synchronous {
if (fires(ai)) put(ao, get(ai));
else if (fires(bi)) put(bo, get(bi));
else put(co, get(ci));
}
}
|