Program Sample

Contents

Program Sample

/* Enumerated type */
typedef typ = enum { label1,label2, label3 };

/* Global variables */
var flag : bool,    /* Boolean */
    e    : typ,     /* Enumerated */
    ui   : uint[3], /* Bounded unsigned integer encoded on 3 bits */
    si   : sint[4], /* Bounded signed integer encoded on 4 bits */
    x,y  : int,     /* Integer */
    r    : real;    /* Real (maybe treated as floating-point) */
    
/* Initial condition on global variables */
initial not flag and e==label1 and 
        ui==uint[3]0 and si==sint[4]0 and /* bounded integer constants need explicit type */
        x==0 and y==0;

/* a procedure  */
proc incr(a:int) returns (b:int)
var l : int; /* local variable */
begin
  if e==label2 then     /* if-then-else */
    ui = ui + uint[3]1; /* bounded integer constants need explicit type */
    si = si * sint[4]3;
  else
    si = si * sint[4]4;
  endif;
  b = a+1;
end

/* first thread */
thread X:
var l:int; /* local variable */
begin
  l = 0;
  while x<10 do
    l = l+1; x = x+1;
  done;
  flag = true;
end

/* second thread */
thread Y:
var l:int;
begin
  l = 0;
  assume(flag); /* acts like a filter, can emulate active waiting */
  while y<10 do
    l = l+1; x = x+1; y = y +_f 1;
  done;
  if l>=12 then 
    /* This point just before fail is a final point for backward analysis */
    fail;
    /* This point just after fail is never reachable */
  endif;
end

Program Sample

Contents