
module BCR
{
  type state_t = enum { S0, S1 };
  var BCR_state : state_t;

  init {
    BCR_state = S0;
  }

  next {
    if (BCR_state == S0) {
      havoc BCR_state;
      assume(BCR_state == S1);
    } else {
      havoc BCR_state;
      assume(BCR_state == S0);
    }
  }
}

module BP
{
  type state_t = enum { S0, S1 };
  var BP_state : state_t;

  init {
    BP_state = S0;
  }

  next {
    if (BP_state == S0) {
      havoc BP_state;
      assume(BP_state == S1);
    } else {
      havoc BP_state;
      assume(BP_state == S0);
    }
  }
}

module Printer
{
  type state_t = enum { S0, S1 };
  var Printer_state : state_t;

  init {
    Printer_state = S0;
  }

  next {
    if (Printer_state == S0) {
      havoc Printer_state;
      assume(Printer_state == S1);
    } else {
      havoc Printer_state;
      assume(Printer_state == S0);
    }
  }
}

module main
{
  var BCR_state : BCR.state_t;
  var BP_state : BP.state_t;
  var Printer_state : Printer.state_t;

  init {
    BCR.init();
    BP.init();
    Printer.init();
  }

  next {
    BCR.next();
    BP.next();
    Printer.next();
  }
}
