module main {
    // Define variables for Circuit C1
    var y1 : boolean;
    var r1 : boolean;

    // Define variables for Circuit C2
    input x2 : boolean;
    var y2 : boolean;
    var r2 : boolean;

    // Initial states of the circuits
    init {
        y1 = false;
        r1 = false;
        y2 = false;
        r2 = false;
    }

    // Transition functions for both circuits
    next {
        // Transitions for Circuit C1
        y1' = r1;
        r1' = !r1;

        // Transitions for Circuit C2
        y2' = x2' | r2;
        r2' = x2' | r2;
    }

    // Control block to run and check the model
    control {
        // Run the model for a number of steps to observe behavior
        v = simulate 10;
        v.print_trace;
    }
}
