TVT Examples

This page will eventually hold many examples of systems modelled as LSTSs.

Contents

The Dining Philosophers

The Dining Philosophers problem is a classic problem. The problem consists of N philosophers sitting at a table who do nothing but think and eat. Between each philosopher, there is a single fork. In order to eat, a philosopher must have both forks. A problem can arise if each philosopher grabs the fork on the right, then waits for the fork on the left. In this case a deadlock has occurred, and all philosophers will starve.
This example is presented also in the TVT tutorial.
  • A philosopher as an LSTS
  • A fork as an LSTS
  • Rules for making the generic system
  • The Bankteller machine

    The Bankteller machine is a more extensive and practical example that captures some essential problems in two-way communication where messages may be lost.
  • The Bankteller machine

  • Henri Hansen, hansen@cs.tut.fi.
    Maintained by Timo Erkkilä, timoe@cs.tut.fi.
    Last modifications to this page: Tue Feb 18 19:57:03 EET 2003.