COMP3153/9153 Algorithmic Verification Term 1, 2020

Code (Homework 2)

Table of Contents

1 Tank Model

/* Level of the individual tanks */
int level[2];

/* Model of Pump */
active proctype Pump() { 
  do
  :: level[0]<level[1] -> level[1]--;skip;level[0]++; 
  :: level[1]<level[0] -> level[0]--;skip;level[1]++; 
  :: else -> break;
  od
}

/* set initial water levels */
init { 
  level[0]=5; 
  level[1]=49;
}

2020-05-15 Fri 00:10

Announcements RSS