
module BCR
{
  type BCR_state_t = enum { 0, 1 };
  var BCR_state : BCR_state_t;

  init {
    BCR_state = 0;
  }

  transition {
    case
      BCR_state == 0 : { BCR_state := 1; }
      BCR_state == 1 : { BCR_state := 0; }
    esac
  }
}

module BP
{
  type BP_state_t = enum { 0, 1 };
  var BP_state : BP_state_t;

  init {
    BP_state = 0;
  }

  transition {
    case
      BP_state == 0 : { BP_state := 1; }
      BP_state == 1 : { BP_state := 0; }
    esac
  }
}

module Printer
{
  type Printer_state_t = enum { 0, 1 };
  var Printer_state : Printer_state_t;

  init {
    Printer_state = 0;
  }

  transition {
    case
      Printer_state == 0 : { Printer_state := 1; }
      Printer_state == 1 : { Printer_state := 0; }
    esac
  }
}

module main
{
  var bcr : BCR;
  var bp : BP;
  var printer : Printer;

  init {
    bcr.BCR_state = 0;
    bp.BP_state = 0;
    printer.Printer_state = 0;
  }

  transition {
    next(bcr);
    next(bp);
    next(printer);
  }
}
