********Verification Result******** The Assertion (P() deadlockfree) is VALID. ********Verification Setting******** Admissible Behavior: All Search Engine: First Witness Trace using Depth First Search System Abstraction: False ********Verification Statistics******** Visited States:8 Total Transitions:13 Time Used:0,0545211s Estimated Memory Used:8583,272KB