system implementation sys.impl
    parameters
        A0: set of indices;
        A1: set of indices;
        A2: set of indices;
        m0_conn_a0: int;
        m0_taint_a0: bool;
        m0_conn_a1: int;
        m0_taint_a1: bool;
        m0_present: bool;
        m1_conn_a1: int;
        m1_taint_a1: bool;
        m1_conn_a2: int;
        m1_taint_a2: bool;
        m1_present: bool;

    initial
        m0_conn_a0 = 0 and m0_conn_a1 = 0 and m1_conn_a1 = 0 and m1_conn_a2 = 0 and m0_taint_a0 = false and m0_taint_a1 = false and m1_taint_a1 = false and m1_taint_a2 = false and forall(x in A0, x > 0) and forall(x in A1, x > 0) and forall(x in A2, x > 0);

    subcomponents
        a0: set indexed by A0;
        a1: set indexed by A1;
        a2: set indexed by A2;
        m0: single if m0_present;
        m1: single if m1_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;
        a1[x] -> m1 if x = m1_conn_a1 for x in A1;
        m1 -> a1[x] if x = m1_conn_a1 for x in A1;
        a2[x] -> m1 if x = m1_conn_a2 for x in A2;
        m1 -> a2[x] if x = m1_conn_a2 for x in A2;

    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 not in A2, x > 0 and next(A2) = add(A2, 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 and m1_conn_a1 != x);
        exists(x in A2, next(A2) = remove(A2, x) and m1_conn_a2 != x);
        exists(x in A0, not m0_taint_a1 and m0_conn_a0 = 0 and next(m0_conn_a0) = x and next(m0_taint_a0) = true);
        exists(x in A1, not m0_taint_a0 and m0_conn_a1 = 0 and next(m0_conn_a1) = x and next(m0_taint_a1) = true);
        exists(x in A1, not m1_taint_a2 and m1_conn_a1 = 0 and next(m1_conn_a1) = x and next(m1_taint_a1) = true);
        exists(x in A2, not m1_taint_a1 and m1_conn_a2 = 0 and next(m1_conn_a2) = x and next(m1_taint_a2) = true);
        next(m0_conn_a0) = 0;
        next(m0_conn_a1) = 0;
        next(m1_conn_a1) = 0;
        next(m1_conn_a2) = 0;
        m0_conn_a0 = 0 and m0_conn_a1 = 0 and next(m0_present) = false and next(m0_taint_a0) = false and next(m0_taint_a1) = false;
        m1_conn_a1 = 0 and m1_conn_a2 = 0 and next(m1_present) = false and next(m1_taint_a1) = false and next(m1_taint_a2) = false;
        next(m0_present) = true;
        next(m1_present) = true;
end sys.impl;
