previous up next
Go up to Top
Go forward to Correctness Proof
RISC-Linz logo

Source Code

The source code implementing the program is included below. The assertion NumberOfMessages states that, as soon as node 0 has signalled by its variable sent the initialization of the network, there must be exactly two messages in the network. A message may be either contained in some channel out(j), or, in a program's local variable msg.

// --------------------------------------------------------------------------
// $Id: algorithm.tex,v 1.2 1997/11/06 14:37:28 schreine Exp schreine $
// a trivial test application
//
// (c) 1997, Wolfgang Schreiner <Wolfgang.Schreiner@risc.uni-linz.ac.at>
// http://www.risc.uni-linz.ac.at/software/daj
// --------------------------------------------------------------------------
import daj.*;

// ----------------------------------------------------------------------------
//
// the application itself
//
// ----------------------------------------------------------------------------
public class Main extends Application
{
  // --------------------------------------------------------------------------
  // main function of application
  // --------------------------------------------------------------------------
  public static void main(String[] args)
  {
    new Main().run();
  }

  // --------------------------------------------------------------------------
  // constructor for application
  // --------------------------------------------------------------------------
  public Main()
  {
    super("A Trivial Program", 400, 300);
  }

  // --------------------------------------------------------------------------
  // construction of network
  // --------------------------------------------------------------------------
  public void construct()
  {
    Node node0 = node(new Prog(0), "0", 100, 100);
    Node node1 = node(new Prog(1), "1", 150, 200);
    Node node2 = node(new Prog(2), "2", 300, 150);
    link(node0, node1);
    link(node1, node2);
    link(node2, node0);
    link(node0, node2);
    link(node2, node1);
    link(node1, node0);
  }

  // --------------------------------------------------------------------------
  // informative message
  // --------------------------------------------------------------------------
  public String getText()
  {
    return "A Trivial Program\n \n" +
      "2 messages circling bidirectionally\n" +
      "through a ring of three nodes";
  }
}

// ----------------------------------------------------------------------------
//
// a program class
//
// ----------------------------------------------------------------------------
class Prog extends Program
{
  private int number;
  public int index;
  public Message msg;
  public boolean sent;

  // --------------------------------------------------------------------------
  // called for	initialization of program
  // --------------------------------------------------------------------------
  public Prog(int i)
  { 
    number = i;	
    msg = null;
    sent = false;
  } 
 
  // --------------------------------------------------------------------------
  // called for	 execution of program
  // --------------------------------------------------------------------------
  public void main()
  { 
    if (number == 0)
      {
	out(0).send(new Msg(0));
	out(1).send(new Msg(1));
	sent = true;
      }
    GlobalAssertion assertion = new NumberOfMessages();
    for (int i = 0; i < 5; i++)
      {
	assert(assertion);
	index = in().select();
	msg = in(index).receive();
	out(index).send(msg);
	msg = null;
      }
  }

  // --------------------------------------------------------------------------
  // called for	display of program state
  // --------------------------------------------------------------------------
  public String getText()
  {
    String msgString;
    if (msg == null)
      msgString = "(null)";
    else
      msgString = msg.getText();
    return 
      "sent: " + String.valueOf(sent) +
      "\nmsg: " + msgString;
  }
}

// ----------------------------------------------------------------------------
//
// a message class
//
// ----------------------------------------------------------------------------
class Msg extends Message
{
  int val;
  public Msg(int i)
  {
    val = i;
  }
  public int value()
  {
    return val;
  }
  public String getText()
  {
    return "content = " + String.valueOf(val);
  }
}

// ----------------------------------------------------------------------------
//
// global assertion stating that two messages are floating around
//
// ----------------------------------------------------------------------------
class NumberOfMessages extends GlobalAssertion
{
  int count;

  public String getText()
  {
    return "invalid count of messages: " + 
      String.valueOf(count);
  }

  public boolean assert(Program prog[])
  {
    if (!((Prog)prog[0]).sent) return true;
    count = 0;
    for (int j = 0; j < prog.length; j++)
      {
	Prog program = (Prog)prog[j];
	count += getMessages(program.out(0)).length;
	count += getMessages(program.out(1)).length;
	if (program.msg != null) count++;
      }
    return count == 2;
  }
}

Maintained by: Wolfgang Schreiner
Last Modification: November 14, 1997

previous up next