:orphan:

-------------------------------------
Tutorial code trace (bufferSize == 2)
-------------------------------------

.. code:: shell

   USER% ./mcmini -q -m28 -f ./subtle 2
   
   About to exec into ./subtle
   TraceId 31, *** DEADLOCK DETECTED ***
   THREAD BACKTRACE
    1. thread 0: starts
    2. thread 0: pthread_mutex_init(mut:1, _)
    3. thread 0: pthread_mutex_init(mut:2, _)
    4. thread 0: pthread_mutex_init(mut:3, _)
    5. thread 0: pthread_mutex_init(mut:4, _)
    6. thread 0: pthread_cond_init(cond:1, _)
    7. thread 0: pthread_cond_init(cond:2, _)
    8. thread 0: pthread_create(thr:1, _, _, _)
    9. thread 0: pthread_create(thr:2, _, _, _)
   10. thread 1: starts
   11. thread 1: pthread_mutex_lock(mut:1)
   12. thread 1: pthread_mutex_unlock(mut:1)
   13. thread 1: pthread_mutex_lock(mut:3)
   14. thread 1: pthread_mutex_unlock(mut:3)
   15. thread 1: pthread_mutex_lock(mut:4)
   16. thread 1: pthread_mutex_unlock(mut:4)
   17. thread 1: pthread_mutex_lock(mut:1)
   18. thread 1: pthread_mutex_unlock(mut:1)
   19. thread 1: pthread_mutex_lock(mut:2)
   20. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ]
   21. thread 1: pthread_mutex_unlock(mut:2)
   22. thread 1: pthread_mutex_lock(mut:1)
   23. thread 1: pthread_mutex_unlock(mut:1)
   24. thread 1: pthread_mutex_lock(mut:3)
   25. thread 1: pthread_mutex_unlock(mut:3)
   26. thread 1: pthread_mutex_lock(mut:4)
   27. thread 1: pthread_mutex_unlock(mut:4)
   28. thread 1: pthread_mutex_lock(mut:1)
   29. thread 1: pthread_mutex_unlock(mut:1)
   30. thread 1: pthread_mutex_lock(mut:2)
   31. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ]
   32. thread 1: pthread_mutex_unlock(mut:2)
   33. thread 1: pthread_mutex_lock(mut:1)
   34. thread 1: pthread_mutex_unlock(mut:1)
   35. thread 1: pthread_mutex_lock(mut:3)
   36. thread 1: pthread_mutex_unlock(mut:3)
   37. thread 2: starts
   38. thread 2: pthread_mutex_lock(mut:3)
   39. thread 2: pthread_mutex_unlock(mut:3)
   40. thread 2: pthread_mutex_lock(mut:1)
   41. thread 2: pthread_mutex_unlock(mut:1)
   42. thread 2: pthread_mutex_lock(mut:2)
   43. thread 2: pthread_mutex_unlock(mut:2)
   44. thread 2: pthread_mutex_lock(mut:3)
   45. thread 2: pthread_mutex_unlock(mut:3)
   46. thread 2: pthread_mutex_lock(mut:4)
   47. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ]
   48. thread 2: pthread_mutex_unlock(mut:4)
   49. thread 2: pthread_mutex_lock(mut:3)
   50. thread 2: pthread_mutex_unlock(mut:3)
   51. thread 2: pthread_mutex_lock(mut:1)
   52. thread 2: pthread_mutex_unlock(mut:1)
   53. thread 2: pthread_mutex_lock(mut:2)
   54. thread 2: pthread_mutex_unlock(mut:2)
   55. thread 2: pthread_mutex_lock(mut:3)
   56. thread 2: pthread_mutex_unlock(mut:3)
   57. thread 2: pthread_mutex_lock(mut:4)
   58. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ]
   59. thread 2: pthread_mutex_unlock(mut:4)
   60. thread 1: pthread_mutex_lock(mut:4)
   61. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep)
   62. thread 2: pthread_mutex_lock(mut:3)
   63. thread 2: pthread_mutex_unlock(mut:3)
   64. thread 2: pthread_mutex_lock(mut:1)
   65. thread 2: pthread_mutex_unlock(mut:1)
   66. thread 2: pthread_mutex_lock(mut:2)
   67. thread 2: pthread_cond_wait(cond:1, mut:2) (awake -> asleep)
   0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 2, 2, 2, 2, 2, 2,
   END
   THREAD PENDING OPERATIONS
    * thread 0: pthread_join(thr:1, _) [ Blocked ]
      thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) [ Blocked ]
      thread 2: pthread_cond_wait(cond:1, mut:2) (asleep -> awake) [ Blocked ]
   END
   ***** Model checking completed! *****
   *** DEADLOCK DETECTED ***
     (Trace number (traceId): 31)
   Number of traces: 32
   Total number of transitions: 224
   Elapsed time: 1 seconds