Files
@ 10ae3589084a
Branch filter:
Location: CSY/reowolf/examples/eg_protocols.pdl - annotation
10ae3589084a
598 B
text/plain
defined endpoint manager; made explicit its invariants
a286c28bcdcf 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc a286c28bcdcf a286c28bcdcf a286c28bcdcf 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc 1f2d007ac1cc |
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));
}
}
|