bool P;

proctype autome1(){

    if
        ::P && true -> P=false;
        ::P && true -> skip;
        ::!P -> skip;
    fi;
}

proctype automa2(){

    bool Q = true;

    if
        ::P && Q->
            if
                ::true -> P=false;
                ::true -> Q=false;
                ::else -> skip;
            fi;
        ::!P && Q ->
            if
                ::true -> P=!P; Q=!Q;
                ::else -> skip;
            fi;
        ::P && !Q -> Q=!Q;
    fi;
}

init{

atomic{

    if
        ::true -> P=false;
    else -> P=true;

    run automa1();
    run automa2();

}


}