module circuit1 {
    var r1 : boolean;
    output y1 : boolean;

    init {
        r1 = false;
        y1 = false;
    }

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

module circuit2 {
    input x2 : boolean;
    var r2 : boolean;
    output y2 : boolean;

    init {
        r2 = false;
        y2 = false;
    }

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

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

    instance c1 : circuit1(y1, r1);
    instance c2 : circuit2(x2, y2, r2);

    init {
        x2 = false;
    }

    next {
        havoc x2;
        next(c1);
        next(c2);
    }
}
