program QuantumCoinFlipping; var AtoB, BtoA: channel of qubit;
    A2B, B2A: channel of bool;

process Alice; var x, b, g, result: bool; q: qubit; begin
    q := newqubit;
    {Choose one of the four BB84 states and prepare qubit q}
    if
    :: true -> x:=false; b:=false;
    :: true -> x:=false; b:=true; had q;
    :: true -> x:=true; b:=false; X q;
    :: true -> x:=true; b:=true; X q; had q;
    fi
    AtoB!q;
    B2A?g;
    A2B!b;
    A2B!x;
    result := ((not (b and g)) and (b or g));
end;

process Bob; var g, x_hat, b_hat, x, b, result: bool; rq: qubit;
    abort: bool;        {Bob aborts the protocol}
    dontknow: bool;     {Bob cannot determine Alice's honesty}
begin
    AtoB?rq;
    if
    :: true -> g:=false; B2A!g;
    :: true -> g:=true; B2A!g;
    fi
    {Select random measurement basis and measure}
    if
    :: true -> b_hat:=false;
    :: true -> b_hat:=true; had rq;
    fi
    x_hat:=meas rq;
    {Receive original b and x}
    A2B?b;
    A2B?x;
    {Compare bases and bits}
    if
    :: ((b=b_hat) and (not (x=x_hat))) -> abort:=true;
    :: (not (b=b_hat)) -> dontknow:=true;
    fi
    result := ((not (b and g)) and (b or g));
end;
endprogram.

finalstateproperty (Alice.result == Bob.result);

property (AG (((b==b_hat) and (x==x_hat)) imp (abort==false)))