********Verification Result********
The Assertion (Jobshop() deadlockfree) is NOT valid.
The following trace leads to a deadlock situation.
<init -> [ifb((m3 == 0))] -> b1 -> [Wait[d13]] -> b1 -> [ifb((m1 == 0))] -> b1 -> [Wait[d11]] -> b1 -> [ifb((m2 == 0))] -> b1 -> [Wait[d12]] -> b1 -> [ifb((m4 == 0))] -> b1 -> [Wait[d14]] -> fin1>

********Verification Setting********
Admissible Behavior: All
Search Engine: First Witness Trace using Depth First Search
System Abstraction: False

********Verification Statistics********
Visited States:27
Total Transitions:26
Time Used:0,0684184s
Estimated Memory Used:8618,08KB