def check_ltl(menv: msat_env, enc: LTLEncoder) -> (Iterable, msat_term, msat_term, msat_term):
    assert menv
    assert isinstance(menv, msat_env)
    assert enc
    assert isinstance(enc, LTLEncoder)
    real_type = msat_get_rational_type(menv)
    (delta, x_delta) = decl_consts(menv, delta_name, real_type)
    (transm_time, x_transm_time) = decl_consts(menv, 'tot_transm_time', real_type)
    curr2next = {delta: x_delta, transm_time: x_transm_time}
    mgr = TokenManager('mgr', menv, enc, delta)
    stations = [Station('st{}'.format(i), menv, enc, mgr, delta) for i in range(num_procs)]
    for (s, x_s) in mgr.symb2next.items():
        curr2next[s] = x_s
    for comp in stations:
        for (s, x_s) in comp.symb2next.items():
            assert (s not in curr2next.keys())
            curr2next[s] = x_s
    zero = msat_make_number(menv, '0')
    init = msat_make_equal(menv, transm_time, zero)
    init = msat_make_and(menv, init, msat_make_geq(menv, delta, zero))
    trans = msat_make_geq(menv, x_delta, zero)
    for (s0, s1) in combinations(stations, 2):
        trans = msat_make_and(menv, trans, msat_make_or(menv, s0.stutter, s1.stutter))
    st_acquire = stations[0].acquire
    for st in stations[1:]:
        st_acquire = msat_make_or(menv, st_acquire, st.acquire)
    trans = msat_make_and(menv, trans, msat_make_iff(menv, mgr.acquire, st_acquire))
    st_release = stations[0].release
    for st in stations[1:]:
        st_release = msat_make_or(menv, st_release, st.release)
    trans = msat_make_and(menv, trans, msat_make_iff(menv, mgr.release, st_release))
    lhs = msat_make_and(menv, mgr.counting, mgr.x_idle)
    rhs = msat_make_equal(menv, x_transm_time, msat_make_plus(menv, transm_time, mgr.c))
    trans = msat_make_and(menv, trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_not(menv, lhs)
    rhs = msat_make_equal(menv, x_transm_time, transm_time)
    trans = msat_make_and(menv, trans, msat_make_impl(menv, lhs, rhs))
    init = msat_make_and(menv, init, mgr.init)
    trans = msat_make_and(menv, trans, mgr.trans)
    for s in stations:
        init = msat_make_and(menv, init, s.init)
        trans = msat_make_and(menv, trans, s.trans)
    lhs = enc.make_G(enc.make_F(msat_make_and(menv, mgr.counting, enc.make_X(mgr.idle))))
    rhs = msat_make_lt(menv, transm_time, msat_make_number(menv, '10'))
    rhs = enc.make_G(enc.make_F(rhs))
    ltl = msat_make_impl(menv, lhs, rhs)
    return (TermMap(curr2next), init, trans, ltl)
def check_ltl(menv: msat_env, enc: LTLEncoder) -> (Iterable, msat_term, msat_term, msat_term):
    assert menv
    assert isinstance(menv, msat_env)
    assert enc
    assert isinstance(enc, LTLEncoder)
    real_type = msat_get_rational_type(menv)
    (delta, x_delta) = decl_consts(menv, delta_name, real_type)
    (transm_time, x_transm_time) = decl_consts(menv, 'tot_transm_time', real_type)
    curr2next = {delta: x_delta, transm_time: x_transm_time}
    mgr = TokenManager('mgr', menv, enc, delta)
    stations = [Station('st{}'.format(i), menv, enc, mgr, delta) for i in range(num_procs)]
    for (s, x_s) in mgr.symb2next.items():
        curr2next[s] = x_s
    for comp in stations:
        for (s, x_s) in comp.symb2next.items():
            assert (s not in curr2next.keys())
            curr2next[s] = x_s
    zero = msat_make_number(menv, '0')
    init = msat_make_equal(menv, transm_time, zero)
    init = msat_make_and(menv, init, msat_make_geq(menv, delta, zero))
    trans = msat_make_geq(menv, x_delta, zero)
    for (s0, s1) in combinations(stations, 2):
        trans = msat_make_and(menv, trans, msat_make_or(menv, s0.stutter, s1.stutter))
    st_acquire = stations[0].acquire
    for st in stations[1:]:
        st_acquire = msat_make_or(menv, st_acquire, st.acquire)
    trans = msat_make_and(menv, trans, msat_make_iff(menv, mgr.acquire, st_acquire))
    st_release = stations[0].release
    for st in stations[1:]:
        st_release = msat_make_or(menv, st_release, st.release)
    trans = msat_make_and(menv, trans, msat_make_iff(menv, mgr.release, st_release))
    lhs = msat_make_and(menv, mgr.counting, mgr.x_idle)
    rhs = msat_make_equal(menv, x_transm_time, msat_make_plus(menv, transm_time, mgr.c))
    trans = msat_make_and(menv, trans, msat_make_impl(menv, lhs, rhs))
    lhs = msat_make_not(menv, lhs)
    rhs = msat_make_equal(menv, x_transm_time, transm_time)
    trans = msat_make_and(menv, trans, msat_make_impl(menv, lhs, rhs))
    init = msat_make_and(menv, init, mgr.init)
    trans = msat_make_and(menv, trans, mgr.trans)
    for s in stations:
        init = msat_make_and(menv, init, s.init)
        trans = msat_make_and(menv, trans, s.trans)
    lhs = enc.make_G(enc.make_F(msat_make_and(menv, mgr.counting, enc.make_X(mgr.idle))))
    rhs = msat_make_lt(menv, transm_time, msat_make_number(menv, '10'))
    rhs = enc.make_G(enc.make_F(rhs))
    ltl = msat_make_impl(menv, lhs, rhs)
    return (TermMap(curr2next), init, trans, ltl)