-- Version 1
-- simple 3-bit counter counting from 0 to 7
-- contains only one process
-- transition relation expressed in digital logic terms
MODULE main
VAR
  b0 : boolean;
  b1 : boolean;
  b2 : boolean;
ASSIGN
  init(b0) := FALSE;
  init(b1) := FALSE;
  init(b2) := FALSE;

  next(b0) := !b0;
  next(b1) := (b0 | b1) & !(b0 & b1);
  next(b2) := ((b0 & b1) | b2) & !(b0 & b1 & b2);

-- bit b2 is set infinitely often
-- true
SPEC
  AG AF b2

----------------------------------------------------------
-- Version 2
-- simple 3-bit counter counting from 0 to 7
-- contains only one process
-- transition relation expressed in mathematical terms
MODULE main
VAR
  b0 : boolean;
  b1 : boolean;
  b2 : boolean;
ASSIGN
  init(b0) := FALSE;
  init(b1) := FALSE;
  init(b2) := FALSE;

  next(b0) := !b0;
  next(b1) := 
    case 
      b0 : !b1;
      TRUE : b1;
    esac;
  next(b2) := 
    case 
      b0 & b1 : !b2;
      TRUE : b2;
    esac;

-- bit b2 is set infinitely often
-- true
SPEC
  AG AF b2

----------------------------------------------------------
-- Version 3
-- simple 3-bit counter counting from 0 to 7
-- contains 3 processes, one for each bit
-- brings out that calculation for each bit is the same
-- carry-in modeled as by-value parameter
MODULE counter_cell(carry_in)
VAR
  b : boolean;
ASSIGN
  init(b) := FALSE;
  next(b) := b xor carry_in;
DEFINE
  carry_out := b & carry_in;

MODULE main
VAR
  p0 : counter_cell(TRUE);
  p1 : counter_cell(p0.carry_out);
  p2 : counter_cell(p1.carry_out);

-- bit b2 is set infinitely often
-- true
SPEC
  AG AF p2.b