
module BCR
{
    type state_t = enum { 0, 1 };

    var BCR_state : state_t;

    init {
        BCR_state = 0;
    }

    next {
        if (BCR_state == 0) {
            BCR_state' = 1;
        } else {
            BCR_state' = 0;
        }
    }
}

module BP
{
    type state_t = enum { 0, 1 };

    var BP_state : state_t;

    init {
        BP_state = 0;
    }

    next {
        if (BP_state == 0) {
            BP_state' = 1;
        } else {
            BP_state' = 0;
        }
    }
}

module Printer
{
    type state_t = enum { 0, 1 };

    var Printer_state : state_t;

    init {
        Printer_state = 0;
    }

    next {
        if (Printer_state == 0) {
            Printer_state' = 1;
        } else {
            Printer_state' = 0;
        }
    }
}

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

    init {
        BCR_state = BCR.BCR_state;
        BP_state = BP.BP_state;
        Printer_state = Printer.Printer_state;
    }

    next {
        BCR.BCR_state' = BCR_state;
        BP.BP_state' = BP_state;
        Printer.Printer_state' = Printer_state;
    }
}
