Verum

interface IMotion { in void up(); in void down(); out void stopped();

behaviour { bool moving = false;
on up: moving = true; on down: moving = true; [moving] on inevitable: {moving = false; stopped;} } }

interface IConveyor { in void start(); in void stop(); out void lightBarrierEntry(); out void lightBarrierExit();

behaviour 
{
    bool moving = false;
    on start: moving = true;
    on stop: moving = false;
    [moving] on optional: {lightBarrierExit;} // When moving the sensor will only be activated if an item is on the belt
}

}

interface IMotor { in void up(); in void down(); out void stopped();

behaviour { bool moving = false; on up: {} on down: {} //[moving] on inevitable: {moving = false; stopped;} } }

interface IController { in void test();

behaviour
{
    on test: {}
}

}

component Controller { provides IController controller; requires IMotor cantilever; requires IMotor horizontalAxis; requires IMotor verticalAxis; requires IConveyor conveyor;

behaviour
{
    enum state {INIT, GRAB, MOVE_VER_1, MOVE_HOR_1, MOVE_VER_2, DROP, ON_BELT, FINISH };
    state demoState = state.INIT;
    // Assuming initial state: cantilever module at top-left of warehouse
    on controller.test(): {
        cantilever.up();
    }
    [demoState.INIT] on cantilever.stopped(): {
        demoState = state.GRAB;
        cantilever.down();
    }
    [demoState.GRAB] on cantilever.stopped(): {
        demoState = state.MOVE_VER_1;
        verticalAxis.up();
    }
    [demoState.MOVE_VER_1] on verticalAxis.stopped(): {
        demoState = state.MOVE_HOR_1;
        horizontalAxis.up();
    }
    [demoState.MOVE_HOR_1] on horizontalAxis.stopped(): {
        // Move to same height as conveyor belt
        demoState = state.MOVE_VER_2;
        verticalAxis.down();    // TBD: move pre-specified distance
    }
    [demoState.MOVE_VER_2] on verticalAxis.stopped(): {
        demoState = state.DROP;
        cantilever.up();
    }
    [demoState.DROP] on cantilever.stopped(): {
        // Item has been delivered to the conveyor belt
    }
    [demoState.DROP] on conveyor.lightBarrierEntry(): {
        demoState = state.ON_BELT;
        conveyor.start();
    }
    [demoState.ON_BELT] on conveyor.lightBarrierExit(): {
        demoState = state.FINISH;
        conveyor.stop();
    }
}

}

component HorizontalAxis { provides IMotor imotor; requires IMotion imotion;

behaviour { bool Moving = false;

on imotor.up(): {imotion.up();}
on imotor.down(): {imotion.down();}
on imotion.stopped(): {imotor.stopped();}

} }

component VerticalAxis { provides IMotor imotor; requires IMotion imotion;

behaviour { bool Moving = false;

on imotor.up(): {imotion.up();}
on imotor.down(): {imotion.down();}
on imotion.stopped(): {imotor.stopped();}

} }

component Cantilever { provides IMotor imotor; requires IMotion imotion;

behaviour { bool Moving = false;

on imotor.up(): {imotion.up();}
on imotor.down(): {imotion.down();}
on imotion.stopped(): {imotor.stopped();}

} }

component Conveyor { provides IConveyor conveyor; }