module circuitC1 {
    var y1: boolean;
    var r1: boolean;

    init {
        y1 = false;
        r1 = false;
    }

    next {
        y1' = r1;
        r1' = !r1;
    }
}

module circuitC2 {
    input x2: boolean;
    var y2: boolean;
    var r2: boolean;

    init {
        y2 = false;
        r2 = false;
    }

    next {
        y2' = x2' | r2;
        r2' = x2' | r2;
    }
}

module main {
    input x2: boolean;
    var y1, r1, y2, r2: boolean;

    instance c1: circuitC1(y1: y1, r1: r1);
    instance c2: circuitC2(x2: x2, y2: y2, r2: r2);

    init {
        c1.init;
        c2.init;
    }

    next {
        c1.next;
        c2.next;
    }

    control {
        v = unroll(5);
        check;
        print_results;
    }
}
