c
module BCR
{
  type state_t = enum { S0, S1 };

  var BCR_state : state_t;

  init {
    BCR_state = S0;
  }

  transition {
    case
      BCR_state == S0 : BCR_state' = S1;
      BCR_state == S1 : BCR_state' = S0;
    esac
  }
}

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

  var BP_state : state_t;

  init {
    BP_state = S0;
  }

  transition {
    case
      BP_state == S0 : BP_state' = S1;
      BP_state == S1 : BP_state' = S0;
    esac
  }
}

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

  var Printer_state : state_t;

  init {
    Printer_state = S0;
  }

  transition {
    case
      Printer_state == S0 : Printer_state' = S1;
      Printer_state == S1 : Printer_state' = S0;
    esac
  }
}

module main
{
  instance bcr : BCR(BCR_state);
  instance bp : BP(BP_state);
  instance printer : Printer(Printer_state);

  control {
    havoc bcr.BCR_state;
    havoc bp.BP_state;
    havoc printer.Printer_state;

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