typedef struct {} token_t; place s0 token_t : {}; place s1 token_t; place s2 token_t; place s3 token_t; place s4 token_t; place r0 token_t : {}; place r1 token_t; place r2 token_t; place r3 token_t; place r4 token_t; place d0 token_t : {}; place d1 token_t; place d2 token_t; place a0 token_t : {}; place a1 token_t; place a2 token_t; trans m1 in { place s0 : {}; } out { place s1 : {}; }; trans m2 in { place s0 : {}; } out { place s2 : {}; }; trans send1 in { place s1 : {}; place d0 : {}; } out { place s3 : {}; place d1 : {}; }; trans send2 in { place s2 : {}; place d0 : {}; } out { place s4 : {}; place d2 : {}; }; trans tout1 in { place s3 : {}; } out { place s1 : {}; }; trans tout2 in { place s4 : {}; } out { place s2 : {}; }; trans ack1 in { place s3 : {}; place a1 : {}; } out { place s0 : {}; place a0 : {}; }; trans ack2 in { place s4 : {}; place a2 : {}; } out { place s0 : {}; place a0 : {}; }; trans lose1 in { place d1 : {}; } out { place d0 : {}; }; trans lose2 in { place d2 : {}; } out { place d0 : {}; }; trans rec1 in { place r0 : {}; place d1 : {}; } out { place r1 : {}; place d0 : {}; }; trans rec2 in { place r0 : {}; place d2 : {}; } out { place r2 : {}; place d0 : {}; }; trans a1 in { place r1 : {}; place a0 : {}; } out { place r3 : {}; place a1 : {}; }; trans a2 in { place r2 : {}; place a0 : {}; } out { place r4 : {}; place a2 : {}; }; trans r1 in { place r3 : {}; } out { place r0 : {}; }; trans r2 in { place r4 : {}; } out { place r0 : {}; }; deadlock true;