def __init__(self, name: str, menv: msat_env, enc: LTLEncoder, delta):
    super().__init__(name, menv, enc)
    real_type = msat_get_rational_type(menv)
    bool_type = msat_get_bool_type(menv)
    (loc, x_loc) = self._symb('l', bool_type)
    (evt_symbs, evts, x_evts) = self._enum('evt', 3)
    (c, x_c) = self._symb('c', real_type)
    (timeout, x_timeout) = self._symb('timeout', real_type)
    self.timeout = timeout
    self.x_timeout = x_timeout
    self.c = c
    self.idle = loc
    self.counting = msat_make_not(menv, loc)
    self.x_idle = x_loc
    self.x_counting = msat_make_not(menv, x_loc)
    self.acquire = evts[0]
    self.release = evts[1]
    self.stutter = evts[2]
    self.symb2next = {loc: x_loc, c: x_c, timeout: x_timeout}
    for (s, x_s) in evt_symbs:
        assert (s not in self.symb2next)
        self.symb2next[s] = x_s
    zero = msat_make_number(menv, '0')
    bound_evt = evts[0]
    x_bound_evt = x_evts[0]
    for (evt, x_evt) in zip(evts[1:], x_evts[1:]):
        bound_evt = msat_make_or(menv, bound_evt, evt)
        x_bound_evt = msat_make_or(menv, x_bound_evt, x_evt)
    self.init = bound_evt
    self.trans = x_bound_evt
    self.init = msat_make_and(menv, msat_make_and(menv, self.init, self.idle), msat_make_and(menv, msat_make_equal(menv, c, zero), msat_make_equal(menv, timeout, zero)))
    rhs = msat_make_leq(menv, c, timeout)
    self.init = msat_make_and(menv, self.init, msat_make_impl(menv, self.counting, rhs))
    rhs = msat_make_leq(menv, x_c, x_timeout)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, self.x_counting, rhs))
    lhs = msat_make_or(menv, self.stutter, msat_make_gt(menv, delta, zero))
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_iff(menv, x_loc, loc), msat_make_equal(menv, x_c, msat_make_plus(menv, c, delta))), msat_make_equal(menv, x_timeout, timeout))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    disc_t = msat_make_and(menv, msat_make_equal(menv, delta, zero), msat_make_or(menv, self.acquire, self.release))
    lhs = msat_make_and(menv, disc_t, self.idle)
    rhs = msat_make_and(menv, self.acquire, msat_make_and(menv, self.x_counting, msat_make_equal(menv, x_c, zero)))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, self.counting)
    rhs = msat_make_and(menv, msat_make_and(menv, self.x_idle, self.release), msat_make_and(menv, msat_make_equal(menv, x_c, zero), msat_make_equal(menv, x_timeout, zero)))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
def __init__(self, name: str, menv: msat_env, enc: LTLEncoder, delta):
    super().__init__(name, menv, enc)
    real_type = msat_get_rational_type(menv)
    bool_type = msat_get_bool_type(menv)
    (loc, x_loc) = self._symb('l', bool_type)
    (evt_symbs, evts, x_evts) = self._enum('evt', 3)
    (c, x_c) = self._symb('c', real_type)
    (timeout, x_timeout) = self._symb('timeout', real_type)
    self.timeout = timeout
    self.x_timeout = x_timeout
    self.c = c
    self.idle = loc
    self.counting = msat_make_not(menv, loc)
    self.x_idle = x_loc
    self.x_counting = msat_make_not(menv, x_loc)
    self.acquire = evts[0]
    self.release = evts[1]
    self.stutter = evts[2]
    self.symb2next = {loc: x_loc, c: x_c, timeout: x_timeout}
    for (s, x_s) in evt_symbs:
        assert (s not in self.symb2next)
        self.symb2next[s] = x_s
    zero = msat_make_number(menv, '0')
    bound_evt = evts[0]
    x_bound_evt = x_evts[0]
    for (evt, x_evt) in zip(evts[1:], x_evts[1:]):
        bound_evt = msat_make_or(menv, bound_evt, evt)
        x_bound_evt = msat_make_or(menv, x_bound_evt, x_evt)
    self.init = bound_evt
    self.trans = x_bound_evt
    self.init = msat_make_and(menv, msat_make_and(menv, self.init, self.idle), msat_make_and(menv, msat_make_equal(menv, c, zero), msat_make_equal(menv, timeout, zero)))
    rhs = msat_make_leq(menv, c, timeout)
    self.init = msat_make_and(menv, self.init, msat_make_impl(menv, self.counting, rhs))
    rhs = msat_make_leq(menv, x_c, x_timeout)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, self.x_counting, rhs))
    lhs = msat_make_or(menv, self.stutter, msat_make_gt(menv, delta, zero))
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_iff(menv, x_loc, loc), msat_make_equal(menv, x_c, msat_make_plus(menv, c, delta))), msat_make_equal(menv, x_timeout, timeout))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    disc_t = msat_make_and(menv, msat_make_equal(menv, delta, zero), msat_make_or(menv, self.acquire, self.release))
    lhs = msat_make_and(menv, disc_t, self.idle)
    rhs = msat_make_and(menv, self.acquire, msat_make_and(menv, self.x_counting, msat_make_equal(menv, x_c, zero)))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, self.counting)
    rhs = msat_make_and(menv, msat_make_and(menv, self.x_idle, self.release), msat_make_and(menv, msat_make_equal(menv, x_c, zero), msat_make_equal(menv, x_timeout, zero)))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))