In reply to priyank87:
Remember that for a property with an antecedent to succeed, all threads of that antecedent must be evaluated; thus the need for a first match.
start |-> ##[1:$] send |-> ##3 ack; // can never succeed
start |-> first_match (##[1:$] send) |-> ##3 ack; // can succeed
start |=> send[->1] |-> ##3 ack; // can succeed
start |-> ##[1:$] send ##3 ack; // can succeed, is more efficient for sims
Ben