// Määritellään tietotyyppi jolla on vain yksi mahdollinen arvo
// vastaa P/T-verkon tokenia
typedef unsigned(1) token_t; 

place s0 token_t: 1;
place s1 token_t;
place s2 token_t;

place r0 token_t: 1;
place r1 token_t;
place r2 token_t;

place d0 token_t: 1;
place d1 token_t;

place a0 token_t: 1;
place a1 token_t;

trans send
in {
  place s0 : 1;}
out {
  place s1 : 1;};

trans sdata
in {
  place s1 : 1;
  place d0 : 1;}
out {
  place s2 : 1;
  place d1 : 1;};

trans timeout
in {
  place s2 : 1;}
out {
  place s1 : 1;};
/*
trans ldata
in {
  place d1 : 1;}
out {
  place d0 : 1;};
*/
trans rdata
in {
  place d1 : 1;
  place r0 : 1;}
out {
  place r1 : 1;
  place d0 : 1;};

trans rec
in {
  place r1 : 1;}
out {
  place r2 : 1;};

trans sack
in {
  place r2 : 1;
  place a0 : 1;}
out {
  place a1 : 1;
  place r0 : 1;};
/*
trans lack
in {
  place a1 : 1;}
out {
  place a0 : 1;};
*/
trans rack
in {
  place a1 : 1;
  place s2 : 1;}
out {
  place a0 : 1;
  place s0 : 1;};

deadlock true;