module main {
    var b1: boolean;
    var b2: boolean;
    var x: 1..2; // x can take values 1 or 2

    process P1 {
        state wait1, crit1;

        init {
            state := wait1;
        }

        transition {
            wait1 -> crit1 {
                b1 := true;
                x := 2;
            }
            crit1 -> wait1 {
                b1 := false;
            }
        }
    }

    process P2 {
        state wait2, crit2;

        init {
            state := wait2;
        }

        transition {
            wait2 -> crit2 {
                b2 := true;
                x := 1;
            }
            crit2 -> wait2 {
                b2 := false;
            }
        }
    }

    init {
        b1 := false;
        b2 := false;
        x := 1; // Initially set x to 1
    }

    transition {
        // Interleaving of P1 and P2
        P1.state = wait1 && P2.state = wait2 && x == 1 -> {
            P1.state' := crit1;
        }
        P1.state = crit1 -> {
            P1.state' := wait1;
        }

        P2.state = wait2 && P1.state = wait1 && x == 2 -> {
            P2.state' := crit2;
        }
        P2.state = crit2 -> {
            P2.state' := wait2;
        }
    }
}
