system implementation sys.impl
    parameters
        A0: set of indices;
        A1: set of indices;
        m0_conn_a0: int;
        m0_conn_a1: int;
        m0_present: bool;

    initial
        m0_conn_a0 = 0 and m0_conn_a1 = 0 and forall(x in A0, x > 0) and forall(x in A1, x > 0);

    subcomponents
        a0: set indexed by A0;
        a1: set indexed by A1;
        m0: single if m0_present;

    connections
        a0[x] -> m0 if x = m0_conn_a0 for x in A0;
        m0 -> a0[x] if x = m0_conn_a0 for x in A0;
        a1[x] -> m0 if x = m0_conn_a1 for x in A1;
        m0 -> a1[x] if x = m0_conn_a1 for x in A1;

    reconfigurations
        exists(x not in A0, x > 0 and next(A0) = add(A0, x));
        exists(x not in A1, x > 0 and next(A1) = add(A1, x));
        exists(x in A0, next(A0) = remove(A0, x) and m0_conn_a0 != x);
        exists(x in A1, next(A1) = remove(A1, x) and m0_conn_a1 != x);
        exists(x in A0, m0_conn_a1 = 0 and m0_conn_a0 = 0 and next(m0_conn_a0) = x);
        exists(x in A1, m0_conn_a0 = 0 and m0_conn_a1 = 0 and next(m0_conn_a1) = x);
        next(m0_conn_a0) = 0;
        next(m0_conn_a1) = 0;
        m0_conn_a0 = 0 and m0_conn_a1 = 0 and next(m0_present) = false;
        next(m0_present) = true;
end sys.impl;
