/*  -*- Mode:C -*- */
/* Björn Victor 2002 */

/* Number of trains on each track:
   indexed by signalist id (0,1) for the opinion of each end */
/* TA is trains on "my" track (where trains normally come in)
   TB is "his" track
*/
byte TA[2], TB[2];

/*
Message types:
   tont: "trains on my primary track is n"
   toutB: "train came out backwards, n trains left" (on my primary track)
   toutF: "train came out forwards, n trains left" (on your primary track)
For trains:
   trainIn:  a train wants to come in this end
   trainOut: a train comes out this end forwards
   trainBack: ...backwards
   trainGA:  tell the train to go ahead
   trainNO:  ... to stay there and wait
For semaphores (i.e., Dijkstra semaphores, not train semaphores!)
   p: wait (proberen)
   v: signal (verhoegen)
*/
mtype = { tont, toutB, toutF, howmany,
	  trainIn, trainOut, trainBack, trainGA, trainNO,
	  p, v };

/* Messages between signalists are synchronous, and consist of
   (type,n) where n is insignificant for the "howmany" message */
chan tsig[2] = [0] of { mtype, byte };

/* Trains also signal when they arrive - asynchrounously! */
chan track[2] = [3] of { mtype };

/* Semaphore (Dijkstra type) for handling message timing: when a train enters
   the tunnel, the message sent by the signalist to the other end
   *always* gets sent before the train exits (one end or the other),
   and similarly on exit.  This avoids two trains entering/exiting at
   the same time. */
chan sigsem = [0] of { mtype };

/* Binary semaphore process */
proctype Semaphore(chan s) {
end:  do
    :: s?p -> s!v
  od
}

/* A tunnel end:
   i is the id (0,1)
   me is the telegraph channel from the other end,
   he is the telegraph channel TO the other end,
   a, b are the tracks, where train signals come.
      a is the primary track, b is the other end's primary track.
 */
proctype TunnelEnd(byte i; chan me; chan he; chan a; chan b) {
  byte n;
  do
    /* Other end tells us things, or asks us */
    /* there are n trains on his track: trust him */
    :: me?tont(n) -> TB[i] = n;
    /* a train came backing out his, count down */
    :: me?toutB(n) -> TB[i]--;
       assert(TB[i] <= TA[(i+1)%2]); /* more may have come which we don't know about */
    /* a train came out forwards mine, count down */
    :: me?toutF(n) -> TA[i]--;
       assert(TA[i] == TB[(i+1)%2]); /* at this point we should be agreed */
    /* Trains coming or going */
       /* went in our track */
    :: a?trainIn  ->
	 if
	   :: (TB[i] == 0) ->
/* only let him in if there's noone going in the other direction */
	      TA[i]++;
	      he!tont(TA[i]);
	      a!trainGA
	   :: else -> a!trainNO
         fi
       /* out our track */
    :: a?trainBack ->
	 TA[i]--;
	 he!toutB(TA[i]);
	 a!trainGA
       /* out his track */
    :: b?trainOut ->
	 TB[i]--;
	 he!toutF(TB[i]);
	 b!trainGA
  od
}

/* A train goes in at one end, out the same or other */
proctype Train(chan a,sem) {
  do
    :: sem!p -> a!trainIn;	/* try to go in */
       if
	 :: a?trainGA -> sem?v;	/* was OK, */
progress:   sem!p -> 
	    if			/* now go out forwards or backwards */
	      :: a!trainOut; a?trainGA; sem?v
	      :: a!trainBack; a?trainGA; sem?v
	    fi
	 :: a?trainNO -> sem?v;	/* we weren't allowed, try again */
       fi
  od
}

init /* Initially (this is like "main" in a C program) */
{
  TA[0] = 0; TA[1] = 0;		/* no trains in tunnel */
  TB[0] = 0; TB[1] = 0;
  atomic {			/* Start the protocol entities */
    run TunnelEnd(0,tsig[0],tsig[1],track[0],track[1]);
    run Train(track[0],sigsem);
    run Train(track[1],sigsem);
    run TunnelEnd(1,tsig[1],tsig[0],track[1],track[0]);
    run Semaphore(sigsem);
  }
  /* Check that there are always only trains on one of the tracks */
  assert(((TA[0] >= 0) && (TB[0] == 0)) || ((TA[0] == 0) && (TB[0] >= 0)));
  assert(((TA[1] >= 0) && (TB[1] == 0)) || ((TA[1] == 0) && (TB[1] >= 0)));

}