// File: /home/nikos/./qkd-v2.pctl
// Generated by PRISM on Sun Apr 18 22:28:29 CEST 2004

// Properties:

// 
P=? [ true U bob_state=7 { (ch_state=0) & (al_state=0) & (al_index=1) & (bob_state=0) & (eve_state=0) } ]