// File: C:\Documents and Settings\Nick\My Documents\PRISM-March\models\densecod-2-agents-improved.pctl
// Generated by PRISM on Mon Mar 21 15:26:58 GMT 2005

// Labels:
label "protocol_finished" = (bob_step=5);

// Properties:

// 
P>=1 [ true U ("protocol_finished" & (result=msg)) ]