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)
    int_type = msat_get_integer_type(menv)
    real_type = msat_get_rational_type(menv)
    (loc, x_loc) = self._symb('l', bool_type)
    (evt, x_evt) = self._symb('evt', bool_type)
    (msg_id, x_msg_id) = self._symb('msg_id', int_type)
    (timeout, x_timeout) = self._symb('timeout', real_type)
    (c, x_c) = self._symb('c', real_type)
    self.move = evt
    self.stutter = msat_make_not(menv, evt)
    self.x_move = x_evt
    self.x_stutter = msat_make_not(menv, x_evt)
    self.send = loc
    self.wait_ack = msat_make_not(menv, loc)
    self.x_send = x_loc
    self.x_wait_ack = msat_make_not(menv, x_loc)
    self.symb2next = {loc: x_loc, evt: x_evt, msg_id: x_msg_id, timeout: x_timeout, c: x_c}
    zero = msat_make_number(menv, '0')
    one = msat_make_number(menv, '1')
    base_timeout = one
    self.init = msat_make_and(menv, msat_make_and(menv, self.send, msat_make_equal(menv, c, zero)), msat_make_equal(menv, msg_id, zero))
    self.init = msat_make_and(menv, self.init, msat_make_impl(menv, self.wait_ack, msat_make_leq(menv, c, timeout)))
    self.trans = msat_make_impl(menv, self.x_wait_ack, msat_make_leq(menv, x_c, x_timeout))
    lhs = msat_make_or(menv, msat_make_gt(menv, delta, zero), self.stutter)
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_iff(menv, x_loc, loc), msat_make_equal(menv, x_msg_id, msg_id)), msat_make_and(menv, msat_make_equal(menv, x_timeout, timeout), msat_make_equal(menv, x_c, msat_make_plus(menv, c, delta))))
    rhs = msat_make_and(menv, rhs, msat_make_equal(menv, x_out_c, out_c))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    disc_t = msat_make_and(menv, self.move, msat_make_equal(menv, delta, zero))
    lhs = msat_make_and(menv, disc_t, msat_make_and(menv, self.send, self.x_send))
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_equal(menv, x_msg_id, msg_id), msat_make_equal(menv, x_timeout, base_timeout)), msat_make_and(menv, msat_make_equal(menv, x_c, zero), 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.send, self.x_wait_ack))
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_equal(menv, x_msg_id, msat_make_plus(menv, msg_id, one)), msat_make_equal(menv, x_timeout, base_timeout)), msat_make_and(menv, msat_make_equal(menv, x_c, zero), 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, self.wait_ack)
    rhs_iff = msat_make_and(menv, msat_make_not(menv, msat_make_equal(menv, in_c, msg_id)), msat_make_geq(menv, c, timeout))
    rhs_iff = msat_make_iff(menv, self.x_wait_ack, rhs_iff)
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_equal(menv, x_c, zero), msat_make_equal(menv, x_out_c, out_c)), rhs_iff)
    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_ack, self.x_wait_ack))
    rhs = msat_make_gt(menv, x_timeout, timeout)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, self.wait_ack)
    rhs = msat_make_iff(menv, self.x_send, msat_make_and(menv, msat_make_equal(menv, in_c, msg_id), msat_make_lt(menv, c, timeout)))
    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_ack, self.x_send))
    rhs = msat_make_equal(menv, x_timeout, base_timeout)
    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)
    int_type = msat_get_integer_type(menv)
    real_type = msat_get_rational_type(menv)
    (loc, x_loc) = self._symb('l', bool_type)
    (evt, x_evt) = self._symb('evt', bool_type)
    (msg_id, x_msg_id) = self._symb('msg_id', int_type)
    (timeout, x_timeout) = self._symb('timeout', real_type)
    (c, x_c) = self._symb('c', real_type)
    self.move = evt
    self.stutter = msat_make_not(menv, evt)
    self.x_move = x_evt
    self.x_stutter = msat_make_not(menv, x_evt)
    self.send = loc
    self.wait_ack = msat_make_not(menv, loc)
    self.x_send = x_loc
    self.x_wait_ack = msat_make_not(menv, x_loc)
    self.symb2next = {loc: x_loc, evt: x_evt, msg_id: x_msg_id, timeout: x_timeout, c: x_c}
    zero = msat_make_number(menv, '0')
    one = msat_make_number(menv, '1')
    base_timeout = one
    self.init = msat_make_and(menv, msat_make_and(menv, self.send, msat_make_equal(menv, c, zero)), msat_make_equal(menv, msg_id, zero))
    self.init = msat_make_and(menv, self.init, msat_make_impl(menv, self.wait_ack, msat_make_leq(menv, c, timeout)))
    self.trans = msat_make_impl(menv, self.x_wait_ack, msat_make_leq(menv, x_c, x_timeout))
    lhs = msat_make_or(menv, msat_make_gt(menv, delta, zero), self.stutter)
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_iff(menv, x_loc, loc), msat_make_equal(menv, x_msg_id, msg_id)), msat_make_and(menv, msat_make_equal(menv, x_timeout, timeout), msat_make_equal(menv, x_c, msat_make_plus(menv, c, delta))))
    rhs = msat_make_and(menv, rhs, msat_make_equal(menv, x_out_c, out_c))
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    disc_t = msat_make_and(menv, self.move, msat_make_equal(menv, delta, zero))
    lhs = msat_make_and(menv, disc_t, msat_make_and(menv, self.send, self.x_send))
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_equal(menv, x_msg_id, msg_id), msat_make_equal(menv, x_timeout, base_timeout)), msat_make_and(menv, msat_make_equal(menv, x_c, zero), 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.send, self.x_wait_ack))
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_equal(menv, x_msg_id, msat_make_plus(menv, msg_id, one)), msat_make_equal(menv, x_timeout, base_timeout)), msat_make_and(menv, msat_make_equal(menv, x_c, zero), 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, self.wait_ack)
    rhs_iff = msat_make_and(menv, msat_make_not(menv, msat_make_equal(menv, in_c, msg_id)), msat_make_geq(menv, c, timeout))
    rhs_iff = msat_make_iff(menv, self.x_wait_ack, rhs_iff)
    rhs = msat_make_and(menv, msat_make_and(menv, msat_make_equal(menv, x_c, zero), msat_make_equal(menv, x_out_c, out_c)), rhs_iff)
    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_ack, self.x_wait_ack))
    rhs = msat_make_gt(menv, x_timeout, timeout)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_and(menv, disc_t, self.wait_ack)
    rhs = msat_make_iff(menv, self.x_send, msat_make_and(menv, msat_make_equal(menv, in_c, msg_id), msat_make_lt(menv, c, timeout)))
    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_ack, self.x_send))
    rhs = msat_make_equal(menv, x_timeout, base_timeout)
    self.trans = msat_make_and(menv, self.trans, msat_make_impl(menv, lhs, rhs))