include "globals.mzn";

int : n_intervals;
int : n_operations;
int : n_locations;
int : n_moving_obj;

array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_status;
array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_start;
array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_fin;

% 0 - локация не определена.
array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_locations : m_obj_loc; % Moving object location.

array [1..n_moving_obj, 1..n_locations] of set of 1..n_operations : arrival_op;
array [1..n_moving_obj, 1..n_locations] of set of 1..n_operations : departure_op;

% Определение m_obj_loc.
constraint forall (i in 1..n_moving_obj, j in 1..(n_intervals + 1))
    ((m_obj_loc[i, j] != 0) -> (
        (m_obj_loc[i, j] == m_obj_loc[i, j - 1] /\ (forall (k in departure_op[i, m_obj_loc[i, j]]) (op_status[k, j - 1] == 0)))
            \/
        (not (forall (k in arrival_op[i, m_obj_loc[i, j]]) (op_fin[i, j - 1] == 0)))
    ));

% Начальное состояние.
array [1..n_moving_obj] of var 0..n_locations : initial_m_obj_loc;
constraint forall (i in 1..n_moving_obj) (m_obj_loc[i, 0] = initial_m_obj_loc[i]);

% Конечное состояние.
array [1..n_moving_obj] of var 0..n_locations : final_m_obj_loc;
constraint forall (i in 1..n_moving_obj) (
    (final_m_obj_loc[i] != 0) ->
        (m_obj_loc[i, n_intervals + 1] = final_m_obj_loc[i])
);

constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i, j] == 0); % Краевые значения.

% Определение op_start и op_fin.
constraint forall (i in 1..n_operations) (op_start[i, 0] == 0 /\ op_fin[i, n_intervals + 1] == 0);
constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] = op_status[i, j] /\ not op_status[i, j - 1]);
constraint forall (i in 1..n_operations, j in 1..n_intervals      ) (op_fin  [i, j] = op_status[i, j] /\ not op_status[i, j + 1]);

% Непрерывность перемещения.
array [1..n_operations] of var int : operations_duration;
array [1..n_operations] of var bool : is_moving_operation;

constraint forall (i in 1..n_operations) (
    if (is_moving_operation[i]) then (
        forall (j in 1..n_intervals) (
            if (j + operations_duration[i] > n_intervals + 1) then
                op_start[i, j] = 0
            else (
                (op_start[i, j] == 1) -> (
                    (forall (k in 1..(operations_duration[i] - 1))
                        (op_status[i, j + k] == 1)
                    ) /\
                    (op_status[i, j + operations_duration[i]] == 0)
                )
            )
            endif
        )
    ) else true
    endif
);

% Наличие всех ресурсов на месте.
array [1..n_operations] of set of 1..n_moving_obj : operations_resources;
array [1..n_operations] of 0..n_locations : operations_start_loc;

constraint forall (op in 1..n_operations, j in 1..n_intervals) (
    forall (obj in operations_resources[op]) (
        (op_start[op, j]) -> (m_obj_loc[obj, j] == operations_start_loc[op])
    )
);

solve satisfy;

output ["op_status = ", show(op_status), "\n"];