defproc arbiter (bool a, b, u, v) { bool _u, _v; prs { [keeper=0] a & _v -> _u- [keeper=0] ~a | ~_v -> _u+ [keeper=0] b & _u -> _v- [keeper=0] ~b | ~_u -> _v+ [keeper=0] _u => u- [keeper=0] _v => v- } spec { mk_excllo(_u, _v) } } bool Reset; defproc driver(bool r, a) { prs { Reset | a => r- } } defproc test() { driver d1, d2; arbiter a(d1.r, d2.r, d1.a, d2.a); } test t;