def transition_system(env: PysmtEnv) -> Tuple[(FrozenSet[FNode], FNode, FNode, FNode)]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    pc = mgr.Symbol('pc', types.INT)
    x = mgr.Symbol('x', types.INT)
    x_pc = symb_to_next(mgr, pc)
    x_x = symb_to_next(mgr, x)
    symbols = frozenset([pc, x])
    m_1 = mgr.Int((- 1))
    n_locs = 3
    max_int = 11
    ints = []
    pcs = []
    x_pcs = []
    for idx in range(n_locs):
        num = mgr.Int(idx)
        ints.append(num)
        pcs.append(mgr.Equals(pc, num))
        x_pcs.append(mgr.Equals(x_pc, num))
    for idx in range(n_locs, max_int):
        num = mgr.Int(idx)
        ints.append(num)
    pcend = mgr.Equals(pc, m_1)
    x_pcend = mgr.Equals(x_pc, m_1)
    init = pcs[0]
    cfg = []
    cond = mgr.LE(x, ints[10])
    cfg.append(mgr.Implies(mgr.And(pcs[0], cond), x_pcs[1]))
    cfg.append(mgr.Implies(mgr.And(pcs[0], mgr.Not(cond)), x_pcend))
    cond = mgr.GT(x, ints[6])
    cfg.append(mgr.Implies(mgr.And(pcs[1], cond), x_pcs[0]))
    cfg.append(mgr.Implies(mgr.And(pcs[1], mgr.Not(cond)), x_pcs[0]))
    cfg.append(mgr.Implies(pcs[2], x_pcs[0]))
    cfg.append(mgr.Implies(pcend, x_pcend))
    trans = []
    same = mgr.Equals(x_x, x)
    trans.append(mgr.Implies(pcs[0], same))
    trans.append(mgr.Implies(pcs[1], same))
    trans.append(mgr.Implies(pcs[2], mgr.Equals(x_x, mgr.Plus(x, ints[2]))))
    trans.append(mgr.Implies(pcend, same))
    trans = mgr.And(*cfg, *trans)
    fairness = mgr.Not(mgr.Equals(pc, m_1))
    return (symbols, init, trans, fairness)
def transition_system(env: PysmtEnv) -> Tuple[(FrozenSet[FNode], FNode, FNode, FNode)]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    pc = mgr.Symbol('pc', types.INT)
    x = mgr.Symbol('x', types.INT)
    x_pc = symb_to_next(mgr, pc)
    x_x = symb_to_next(mgr, x)
    symbols = frozenset([pc, x])
    m_1 = mgr.Int((- 1))
    n_locs = 3
    max_int = 11
    ints = []
    pcs = []
    x_pcs = []
    for idx in range(n_locs):
        num = mgr.Int(idx)
        ints.append(num)
        pcs.append(mgr.Equals(pc, num))
        x_pcs.append(mgr.Equals(x_pc, num))
    for idx in range(n_locs, max_int):
        num = mgr.Int(idx)
        ints.append(num)
    pcend = mgr.Equals(pc, m_1)
    x_pcend = mgr.Equals(x_pc, m_1)
    init = pcs[0]
    cfg = []
    cond = mgr.LE(x, ints[10])
    cfg.append(mgr.Implies(mgr.And(pcs[0], cond), x_pcs[1]))
    cfg.append(mgr.Implies(mgr.And(pcs[0], mgr.Not(cond)), x_pcend))
    cond = mgr.GT(x, ints[6])
    cfg.append(mgr.Implies(mgr.And(pcs[1], cond), x_pcs[0]))
    cfg.append(mgr.Implies(mgr.And(pcs[1], mgr.Not(cond)), x_pcs[0]))
    cfg.append(mgr.Implies(pcs[2], x_pcs[0]))
    cfg.append(mgr.Implies(pcend, x_pcend))
    trans = []
    same = mgr.Equals(x_x, x)
    trans.append(mgr.Implies(pcs[0], same))
    trans.append(mgr.Implies(pcs[1], same))
    trans.append(mgr.Implies(pcs[2], mgr.Equals(x_x, mgr.Plus(x, ints[2]))))
    trans.append(mgr.Implies(pcend, same))
    trans = mgr.And(*cfg, *trans)
    fairness = mgr.Not(mgr.Equals(pc, m_1))
    return (symbols, init, trans, fairness)