def __init__(self, name: str, menv: msat_env, enc: LTLEncoder, in_c, x_in_c, out_c, x_out_c, delta):
    super().__init__(name, menv, enc)
    bool_type = msat_get_bool_type(menv)
    (loc, x_loc) = self._symb('l', bool_type)
    self.wait = loc
    self.work = msat_make_not(menv, loc)
    self.x_wait = x_loc
    self.x_work = msat_make_not(menv, x_loc)
    self.symb2next = {loc: x_loc}
    zero = msat_make_number(menv, '0')
    self.init = self.wait
    lhs = msat_make_gt(menv, delta, zero)
    rhs = msat_make_and(menv, msat_make_iff(menv, x_loc, loc), msat_make_equal(menv, x_out_c, out_c))
    self.trans = msat_make_impl(menv, lhs, rhs)
    disc_t = msat_make_equal(menv, delta, zero)
    lhs = msat_make_and(menv, disc_t, self.wait)
    rhs = msat_make_iff(menv, self.x_wait, msat_make_equal(menv, in_c, out_c))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, msat_make_and(menv, self.wait, self.x_wait))
    rhs = msat_make_equal(menv, x_out_c, out_c)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, msat_make_and(menv, self.wait, self.x_work))
    rhs = msat_make_equal(menv, x_out_c, in_c)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, self.work)
    rhs = msat_make_equal(menv, x_out_c, out_c)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
def __init__(self, name: str, menv: msat_env, enc: LTLEncoder, in_c, x_in_c, out_c, x_out_c, delta):
    super().__init__(name, menv, enc)
    bool_type = msat_get_bool_type(menv)
    (loc, x_loc) = self._symb('l', bool_type)
    self.wait = loc
    self.work = msat_make_not(menv, loc)
    self.x_wait = x_loc
    self.x_work = msat_make_not(menv, x_loc)
    self.symb2next = {loc: x_loc}
    zero = msat_make_number(menv, '0')
    self.init = self.wait
    lhs = msat_make_gt(menv, delta, zero)
    rhs = msat_make_and(menv, msat_make_iff(menv, x_loc, loc), msat_make_equal(menv, x_out_c, out_c))
    self.trans = msat_make_impl(menv, lhs, rhs)
    disc_t = msat_make_equal(menv, delta, zero)
    lhs = msat_make_and(menv, disc_t, self.wait)
    rhs = msat_make_iff(menv, self.x_wait, msat_make_equal(menv, in_c, out_c))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, msat_make_and(menv, self.wait, self.x_wait))
    rhs = msat_make_equal(menv, x_out_c, out_c)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, msat_make_and(menv, self.wait, self.x_work))
    rhs = msat_make_equal(menv, x_out_c, in_c)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, self.work)
    rhs = msat_make_equal(menv, x_out_c, out_c)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))