probabilistic 

const int INITSTATE = 8; //initialize to 1/sqrt2 (|00>+|11>), which is state=8

// Property: P=? [ true U ((bob_step=5) & (result=msg)) ], Result is 1

module Alice
alice_step : [0..3];
msg : [0..3];
// 1="00", 2="01", 3="10", 4="11"
[initialize]	(bob_step=0)&(alice_step=0) -> (alice_step'=1);	
[]		(bob_step=0)&(alice_step=1) -> 1/4 : (msg'=0) & (alice_step'=2) + 1/4 : (msg'=1) & (alice_step'=2) 
			 	+  1/4 : (msg'=2) & (alice_step'=2) + 1/4 : (msg'=3) & (alice_step'=2); 
[sigma0]	(bob_step=0)&(alice_step=2)&(msg=0) -> (alice_step'=3);
[sigma1]	(bob_step=0)&(alice_step=2)&(msg=1) -> (alice_step'=3);
[sigma3]	(bob_step=0)&(alice_step=2)&(msg=2) -> (alice_step'=3);
[sigma2]	(bob_step=0)&(alice_step=2)&(msg=3) -> (alice_step'=3);
[sendtoBob]	(bob_step=0)&(alice_step=3) -> (alice_step'=3);
endmodule

module Bob
bob_step : [0..5];
result : [0..3];
// 1="00", 2="01", 3="10", 4="11"
[sendtoBob]	(alice_step=3)&(bob_step=0) -> (bob_step'=1);
[cnot]		(alice_step=3)&(bob_step=1) -> (bob_step'=2);
[hadamard1] 	(alice_step=3)&(bob_step=2) -> (bob_step'=3);
[measure]	(alice_step=3)&(bob_step=3) -> (bob_step'=4);
[]		(alice_step=3)&(bob_step=4) -> (result'=outcome) & (bob_step'=5);
[]		(alice_step=3)&(bob_step=5) -> (bob_step'=5); //End of the protocol
endmodule

// PRISM state transition system (model) for generic two-qubit quantum system
// with the operations Pauli I,X,Y,Z, Controlled NOT, and Hadamard-on-first-qubit
// Code generated by PRISMGEN (c) Simon Gay, Nick Papanikolaou 2004
module TwoQubits
state : [0..23];
outcome : [0..3];

[initialize] (state=0) -> (state'=INITSTATE);
// sigma0 +|00> -> +|00>
[sigma0] (state=0) -> (state'=0);
// sigma0 +|01> -> +|01>
[sigma0] (state=1) -> (state'=1);
// sigma0 +|10> -> +|10>
[sigma0] (state=2) -> (state'=2);
// sigma0 +|11> -> +|11>
[sigma0] (state=3) -> (state'=3);
// sigma0 +|00>+|01> -> +|00>+|01>
[sigma0] (state=4) -> (state'=4);
// sigma0 +|00>-|01> -> +|00>-|01>
[sigma0] (state=5) -> (state'=5);
// sigma0 +|00>+|10> -> +|00>+|10>
[sigma0] (state=6) -> (state'=6);
// sigma0 +|00>-|10> -> +|00>-|10>
[sigma0] (state=7) -> (state'=7);
// sigma0 +|00>+|11> -> +|00>+|11>
[sigma0] (state=8) -> (state'=8);
// sigma0 +|00>-|11> -> +|00>-|11>
[sigma0] (state=9) -> (state'=9);
// sigma0 +|01>+|10> -> +|01>+|10>
[sigma0] (state=10) -> (state'=10);
// sigma0 +|01>-|10> -> +|01>-|10>
[sigma0] (state=11) -> (state'=11);
// sigma0 +|01>+|11> -> +|01>+|11>
[sigma0] (state=12) -> (state'=12);
// sigma0 +|01>-|11> -> +|01>-|11>
[sigma0] (state=13) -> (state'=13);
// sigma0 +|10>+|11> -> +|10>+|11>
[sigma0] (state=14) -> (state'=14);
// sigma0 +|10>-|11> -> +|10>-|11>
[sigma0] (state=15) -> (state'=15);
// sigma0 +|00>+|01>+|10>+|11> -> +|00>+|01>+|10>+|11>
[sigma0] (state=16) -> (state'=16);
// sigma0 +|00>+|01>+|10>-|11> -> +|00>+|01>+|10>-|11>
[sigma0] (state=17) -> (state'=17);
// sigma0 +|00>+|01>-|10>+|11> -> +|00>+|01>-|10>+|11>
[sigma0] (state=18) -> (state'=18);
// sigma0 +|00>+|01>-|10>-|11> -> +|00>+|01>-|10>-|11>
[sigma0] (state=19) -> (state'=19);
// sigma0 +|00>-|01>+|10>+|11> -> +|00>-|01>+|10>+|11>
[sigma0] (state=20) -> (state'=20);
// sigma0 +|00>-|01>+|10>-|11> -> +|00>-|01>+|10>-|11>
[sigma0] (state=21) -> (state'=21);
// sigma0 +|00>-|01>-|10>+|11> -> +|00>-|01>-|10>+|11>
[sigma0] (state=22) -> (state'=22);
// sigma0 +|00>-|01>-|10>-|11> -> +|00>-|01>-|10>-|11>
[sigma0] (state=23) -> (state'=23);
// sigma1 +|00> -> +|10>
[sigma1] (state=0) -> (state'=2);
// sigma1 +|01> -> +|11>
[sigma1] (state=1) -> (state'=3);
// sigma1 +|10> -> +|00>
[sigma1] (state=2) -> (state'=0);
// sigma1 +|11> -> +|01>
[sigma1] (state=3) -> (state'=1);
// sigma1 +|00>+|01> -> +|10>+|11>
[sigma1] (state=4) -> (state'=14);
// sigma1 +|00>-|01> -> +|10>-|11>
[sigma1] (state=5) -> (state'=15);
// sigma1 +|00>+|10> -> +|00>+|10>
[sigma1] (state=6) -> (state'=6);
// sigma1 +|00>-|10> -> +|00>-|10>
[sigma1] (state=7) -> (state'=7);
// sigma1 +|00>+|11> -> +|01>+|10>
[sigma1] (state=8) -> (state'=10);
// sigma1 +|00>-|11> -> +|01>-|10>
[sigma1] (state=9) -> (state'=11);
// sigma1 +|01>+|10> -> +|00>+|11>
[sigma1] (state=10) -> (state'=8);
// sigma1 +|01>-|10> -> +|00>-|11>
[sigma1] (state=11) -> (state'=9);
// sigma1 +|01>+|11> -> +|01>+|11>
[sigma1] (state=12) -> (state'=12);
// sigma1 +|01>-|11> -> +|01>-|11>
[sigma1] (state=13) -> (state'=13);
// sigma1 +|10>+|11> -> +|00>+|01>
[sigma1] (state=14) -> (state'=4);
// sigma1 +|10>-|11> -> +|00>-|01>
[sigma1] (state=15) -> (state'=5);
// sigma1 +|00>+|01>+|10>+|11> -> +|00>+|01>+|10>+|11>
[sigma1] (state=16) -> (state'=16);
// sigma1 +|00>+|01>+|10>-|11> -> +|00>-|01>+|10>+|11>
[sigma1] (state=17) -> (state'=20);
// sigma1 +|00>+|01>-|10>+|11> -> +|00>-|01>-|10>-|11>
[sigma1] (state=18) -> (state'=23);
// sigma1 +|00>+|01>-|10>-|11> -> +|00>+|01>-|10>-|11>
[sigma1] (state=19) -> (state'=19);
// sigma1 +|00>-|01>+|10>+|11> -> +|00>+|01>+|10>-|11>
[sigma1] (state=20) -> (state'=17);
// sigma1 +|00>-|01>+|10>-|11> -> +|00>-|01>+|10>-|11>
[sigma1] (state=21) -> (state'=21);
// sigma1 +|00>-|01>-|10>+|11> -> +|00>-|01>-|10>+|11>
[sigma1] (state=22) -> (state'=22);
// sigma1 +|00>-|01>-|10>-|11> -> +|00>+|01>-|10>+|11>
[sigma1] (state=23) -> (state'=18);
// sigma2 +|00> -> +|10>
[sigma2] (state=0) -> (state'=2);
// sigma2 +|01> -> +|11>
[sigma2] (state=1) -> (state'=3);
// sigma2 +|10> -> +|00>
[sigma2] (state=2) -> (state'=0);
// sigma2 +|11> -> +|01>
[sigma2] (state=3) -> (state'=1);
// sigma2 +|00>+|01> -> +|10>+|11>
[sigma2] (state=4) -> (state'=14);
// sigma2 +|00>-|01> -> +|10>-|11>
[sigma2] (state=5) -> (state'=15);
// sigma2 +|00>+|10> -> +|00>-|10>
[sigma2] (state=6) -> (state'=7);
// sigma2 +|00>-|10> -> +|00>+|10>
[sigma2] (state=7) -> (state'=6);
// sigma2 +|00>+|11> -> +|01>-|10>
[sigma2] (state=8) -> (state'=11);
// sigma2 +|00>-|11> -> +|01>+|10>
[sigma2] (state=9) -> (state'=10);
// sigma2 +|01>+|10> -> +|00>-|11>
[sigma2] (state=10) -> (state'=9);
// sigma2 +|01>-|10> -> +|00>+|11>
[sigma2] (state=11) -> (state'=8);
// sigma2 +|01>+|11> -> +|01>-|11>
[sigma2] (state=12) -> (state'=13);
// sigma2 +|01>-|11> -> +|01>+|11>
[sigma2] (state=13) -> (state'=12);
// sigma2 +|10>+|11> -> +|00>+|01>
[sigma2] (state=14) -> (state'=4);
// sigma2 +|10>-|11> -> +|00>-|01>
[sigma2] (state=15) -> (state'=5);
// sigma2 +|00>+|01>+|10>+|11> -> +|00>+|01>-|10>-|11>
[sigma2] (state=16) -> (state'=19);
// sigma2 +|00>+|01>+|10>-|11> -> +|00>-|01>-|10>-|11>
[sigma2] (state=17) -> (state'=23);
// sigma2 +|00>+|01>-|10>+|11> -> +|00>-|01>+|10>+|11>
[sigma2] (state=18) -> (state'=20);
// sigma2 +|00>+|01>-|10>-|11> -> +|00>+|01>+|10>+|11>
[sigma2] (state=19) -> (state'=16);
// sigma2 +|00>-|01>+|10>+|11> -> +|00>+|01>-|10>+|11>
[sigma2] (state=20) -> (state'=18);
// sigma2 +|00>-|01>+|10>-|11> -> +|00>-|01>-|10>+|11>
[sigma2] (state=21) -> (state'=22);
// sigma2 +|00>-|01>-|10>+|11> -> +|00>-|01>+|10>-|11>
[sigma2] (state=22) -> (state'=21);
// sigma2 +|00>-|01>-|10>-|11> -> +|00>+|01>+|10>-|11>
[sigma2] (state=23) -> (state'=17);
// sigma3 +|00> -> +|00>
[sigma3] (state=0) -> (state'=0);
// sigma3 +|01> -> +|01>
[sigma3] (state=1) -> (state'=1);
// sigma3 +|10> -> +|10>
[sigma3] (state=2) -> (state'=2);
// sigma3 +|11> -> +|11>
[sigma3] (state=3) -> (state'=3);
// sigma3 +|00>+|01> -> +|00>+|01>
[sigma3] (state=4) -> (state'=4);
// sigma3 +|00>-|01> -> +|00>-|01>
[sigma3] (state=5) -> (state'=5);
// sigma3 +|00>+|10> -> +|00>-|10>
[sigma3] (state=6) -> (state'=7);
// sigma3 +|00>-|10> -> +|00>+|10>
[sigma3] (state=7) -> (state'=6);
// sigma3 +|00>+|11> -> +|00>-|11>
[sigma3] (state=8) -> (state'=9);
// sigma3 +|00>-|11> -> +|00>+|11>
[sigma3] (state=9) -> (state'=8);
// sigma3 +|01>+|10> -> +|01>-|10>
[sigma3] (state=10) -> (state'=11);
// sigma3 +|01>-|10> -> +|01>+|10>
[sigma3] (state=11) -> (state'=10);
// sigma3 +|01>+|11> -> +|01>-|11>
[sigma3] (state=12) -> (state'=13);
// sigma3 +|01>-|11> -> +|01>+|11>
[sigma3] (state=13) -> (state'=12);
// sigma3 +|10>+|11> -> +|10>+|11>
[sigma3] (state=14) -> (state'=14);
// sigma3 +|10>-|11> -> +|10>-|11>
[sigma3] (state=15) -> (state'=15);
// sigma3 +|00>+|01>+|10>+|11> -> +|00>+|01>-|10>-|11>
[sigma3] (state=16) -> (state'=19);
// sigma3 +|00>+|01>+|10>-|11> -> +|00>+|01>-|10>+|11>
[sigma3] (state=17) -> (state'=18);
// sigma3 +|00>+|01>-|10>+|11> -> +|00>+|01>+|10>-|11>
[sigma3] (state=18) -> (state'=17);
// sigma3 +|00>+|01>-|10>-|11> -> +|00>+|01>+|10>+|11>
[sigma3] (state=19) -> (state'=16);
// sigma3 +|00>-|01>+|10>+|11> -> +|00>-|01>-|10>-|11>
[sigma3] (state=20) -> (state'=23);
// sigma3 +|00>-|01>+|10>-|11> -> +|00>-|01>-|10>+|11>
[sigma3] (state=21) -> (state'=22);
// sigma3 +|00>-|01>-|10>+|11> -> +|00>-|01>+|10>-|11>
[sigma3] (state=22) -> (state'=21);
// sigma3 +|00>-|01>-|10>-|11> -> +|00>-|01>+|10>+|11>
[sigma3] (state=23) -> (state'=20);
// cnot +|00> -> +|00>
[cnot] (state=0) -> (state'=0);
// cnot +|01> -> +|01>
[cnot] (state=1) -> (state'=1);
// cnot +|10> -> +|11>
[cnot] (state=2) -> (state'=3);
// cnot +|11> -> +|10>
[cnot] (state=3) -> (state'=2);
// cnot +|00>+|01> -> +|00>+|01>
[cnot] (state=4) -> (state'=4);
// cnot +|00>-|01> -> +|00>-|01>
[cnot] (state=5) -> (state'=5);
// cnot +|00>+|10> -> +|00>+|11>
[cnot] (state=6) -> (state'=8);
// cnot +|00>-|10> -> +|00>-|11>
[cnot] (state=7) -> (state'=9);
// cnot +|00>+|11> -> +|00>+|10>
[cnot] (state=8) -> (state'=6);
// cnot +|00>-|11> -> +|00>-|10>
[cnot] (state=9) -> (state'=7);
// cnot +|01>+|10> -> +|01>+|11>
[cnot] (state=10) -> (state'=12);
// cnot +|01>-|10> -> +|01>-|11>
[cnot] (state=11) -> (state'=13);
// cnot +|01>+|11> -> +|01>+|10>
[cnot] (state=12) -> (state'=10);
// cnot +|01>-|11> -> +|01>-|10>
[cnot] (state=13) -> (state'=11);
// cnot +|10>+|11> -> +|10>+|11>
[cnot] (state=14) -> (state'=14);
// cnot +|10>-|11> -> +|10>-|11>
[cnot] (state=15) -> (state'=15);
// cnot +|00>+|01>+|10>+|11> -> +|00>+|01>+|10>+|11>
[cnot] (state=16) -> (state'=16);
// cnot +|00>+|01>+|10>-|11> -> +|00>+|01>-|10>+|11>
[cnot] (state=17) -> (state'=18);
// cnot +|00>+|01>-|10>+|11> -> +|00>+|01>+|10>-|11>
[cnot] (state=18) -> (state'=17);
// cnot +|00>+|01>-|10>-|11> -> +|00>+|01>-|10>-|11>
[cnot] (state=19) -> (state'=19);
// cnot +|00>-|01>+|10>+|11> -> +|00>-|01>+|10>+|11>
[cnot] (state=20) -> (state'=20);
// cnot +|00>-|01>+|10>-|11> -> +|00>-|01>-|10>+|11>
[cnot] (state=21) -> (state'=22);
// cnot +|00>-|01>-|10>+|11> -> +|00>-|01>+|10>-|11>
[cnot] (state=22) -> (state'=21);
// cnot +|00>-|01>-|10>-|11> -> +|00>-|01>-|10>-|11>
[cnot] (state=23) -> (state'=23);
// hadamard1 +|00> -> +|00>+|10>
[hadamard1] (state=0) -> (state'=6);
// hadamard1 +|01> -> +|01>+|11>
[hadamard1] (state=1) -> (state'=12);
// hadamard1 +|10> -> +|00>-|10>
[hadamard1] (state=2) -> (state'=7);
// hadamard1 +|11> -> +|01>-|11>
[hadamard1] (state=3) -> (state'=13);
// hadamard1 +|00>+|01> -> +|00>+|01>+|10>+|11>
[hadamard1] (state=4) -> (state'=16);
// hadamard1 +|00>-|01> -> +|00>-|01>+|10>-|11>
[hadamard1] (state=5) -> (state'=21);
// hadamard1 +|00>+|10> -> +|00>
[hadamard1] (state=6) -> (state'=0);
// hadamard1 +|00>-|10> -> +|10>
[hadamard1] (state=7) -> (state'=2);
// hadamard1 +|00>+|11> -> +|00>+|01>+|10>-|11>
[hadamard1] (state=8) -> (state'=17);
// hadamard1 +|00>-|11> -> +|00>-|01>+|10>+|11>
[hadamard1] (state=9) -> (state'=20);
// hadamard1 +|01>+|10> -> +|00>+|01>-|10>+|11>
[hadamard1] (state=10) -> (state'=18);
// hadamard1 +|01>-|10> -> +|00>-|01>-|10>-|11>
[hadamard1] (state=11) -> (state'=23);
// hadamard1 +|01>+|11> -> +|01>
[hadamard1] (state=12) -> (state'=1);
// hadamard1 +|01>-|11> -> +|11>
[hadamard1] (state=13) -> (state'=3);
// hadamard1 +|10>+|11> -> +|00>+|01>-|10>-|11>
[hadamard1] (state=14) -> (state'=19);
// hadamard1 +|10>-|11> -> +|00>-|01>-|10>+|11>
[hadamard1] (state=15) -> (state'=22);
// hadamard1 +|00>+|01>+|10>+|11> -> +|00>+|01>
[hadamard1] (state=16) -> (state'=4);
// hadamard1 +|00>+|01>+|10>-|11> -> +|00>+|11>
[hadamard1] (state=17) -> (state'=8);
// hadamard1 +|00>+|01>-|10>+|11> -> +|01>+|10>
[hadamard1] (state=18) -> (state'=10);
// hadamard1 +|00>+|01>-|10>-|11> -> +|10>+|11>
[hadamard1] (state=19) -> (state'=14);
// hadamard1 +|00>-|01>+|10>+|11> -> +|00>-|11>
[hadamard1] (state=20) -> (state'=9);
// hadamard1 +|00>-|01>+|10>-|11> -> +|00>-|01>
[hadamard1] (state=21) -> (state'=5);
// hadamard1 +|00>-|01>-|10>+|11> -> +|10>-|11>
[hadamard1] (state=22) -> (state'=15);
// hadamard1 +|00>-|01>-|10>-|11> -> +|01>-|10>
[hadamard1] (state=23) -> (state'=11);
[measure] (state=0) -> (state'=state) & (outcome'=state);
[measure] (state=1) -> (state'=state) & (outcome'=state);
[measure] (state=2) -> (state'=state) & (outcome'=state);
[measure] (state=3) -> (state'=state) & (outcome'=state);
[measure] (state=4) -> 1/2 : (state'=0) & (outcome'=0) + 1/2 : (state'=1) & (outcome'=1);
[measure] (state=5) -> 1/2 : (state'=0) & (outcome'=0) + 1/2 : (state'=1) & (outcome'=1);
[measure] (state=6) -> 1/2 : (state'=0) & (outcome'=0) + 1/2 : (state'=2) & (outcome'=2);
[measure] (state=7) -> 1/2 : (state'=0) & (outcome'=0) + 1/2 : (state'=2) & (outcome'=2);
[measure] (state=8) -> 1/2 : (state'=0) & (outcome'=0) + 1/2 : (state'=3) & (outcome'=3);
[measure] (state=9) -> 1/2 : (state'=0) & (outcome'=0) + 1/2 : (state'=3) & (outcome'=3);
[measure] (state=10) -> 1/2 : (state'=1) & (outcome'=1) + 1/2 : (state'=2) & (outcome'=2);
[measure] (state=11) -> 1/2 : (state'=1) & (outcome'=1) + 1/2 : (state'=2) & (outcome'=2);
[measure] (state=12) -> 1/2 : (state'=1) & (outcome'=1) + 1/2 : (state'=3) & (outcome'=3);
[measure] (state=13) -> 1/2 : (state'=1) & (outcome'=1) + 1/2 : (state'=3) & (outcome'=3);
[measure] (state=14) -> 1/2 : (state'=2) & (outcome'=2) + 1/2 : (state'=3) & (outcome'=3);
[measure] (state=15) -> 1/2 : (state'=2) & (outcome'=2) + 1/2 : (state'=3) & (outcome'=3);
[measure] (state=16) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=17) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=18) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=19) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=20) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=21) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=22) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
[measure] (state=23) -> 1/4 : (state'=0) & (outcome'=0) + 1/4 : (state'=1) & (outcome'=1) + 1/4 : (state'=2) & (outcome'=2) + 1/4 : (state'=3) & (outcome'=3);
endmodule

//system
//	((Alice || Bob) |[initialize,sigma0,sigma1,sigma2,sigma3,cnot,hadamard1,measure]| TwoQubits)
//endsystem