Ограничения в OPL.

src/constraints/conversion_2.mod

+using CP;
+
+int n_intervals  = ...;
+int n_operations = ...;
+int n_locations  = ...;
+int n_moving_obj = ...;
+
+dvar boolean op_status[0..n_operations][0..(n_intervals + 1)];
+dvar boolean op_start[0..n_operations][0..(n_intervals + 1)];
+
+int moving_op_of_obj[0..n_moving_obj][0..n_operations] = ...;
+
+// Текущая операция операция перемещения, в которой задействован данный объект.
+dvar int current_moving_operation[0..n_moving_obj][0..(n_intervals + 1)] in 0..n_operations;
+
+// Является ли данная операция операцией перемещения.
+int is_moving_operation[0..n_operations] = ...;
+
+// Главный объект (субъект) операции.
+int main_obj_of_operation[0..n_operations] = ...;
+
+
+// Объект, пришвартованный к данной локации.
+dvar int current_moored_obj[0..n_locations, 0..(n_intervals + 1)] in 0..n_moving_obj;
+
+// Операции с условной швартовкой.
+int op_with_nominally_mooring_max_size = ...;
+int op_with_nominally_mooring_sizes[0..n_locations, 0..n_moving_obj] = ...;
+int op_with_nominally_mooring[0..n_locations, 0..n_moving_obj, 1..op_with_nominally_mooring_max_size] = ...;
+	
+
+// Местоположение объекта или пункт назначения (если объект движется) перед началом определённого интервала.
+dvar int m_obj_loc[0..n_moving_obj, 0..(n_intervals + 1)] in 0..n_locations;
+
+int twin_location[1..n_locations];
+int main_location[1..n_locations];
+
+execute initializeArray {
+	for(var i = 1; i <= n_locations; i++) {
+		twin_location[i] = i - 1 + (i % 2) * 2;
+		main_location[i] = i - ((i + 1) % 2);
+	}
+}
+
+int operations_destination[0..n_operations] = ...; // Локация в которой окажется объект после завершения операции.
+
+// Является ли операция швартовкой/отшвартовкой.
+int is_mooring_op[0..n_operations] = ...;
+
+int initial_m_obj_loc[0..n_moving_obj] = ...;
+int final_m_obj_loc[0..n_moving_obj] = ...;
+
+// Операции, которые могут задействовать данный объект как ресурс.
+{int} operations_that_used_obj_as_resource [0..n_moving_obj] = ...;
+
+// Операция, в которой участвует данный объект как ресурс.
+dvar int participation_as_resource[0..n_moving_obj, 0..(n_intervals + 1)] in 0..n_operations;
+
+int n_resources_types = ...; // Количество различных типов ресурсов.
+{int} objects_of_type[1..n_resources_types] = ...; // Все объекты конкретного типа.
+
+int n_resources_counters = ...; // Количество счётчиков ресурсов.
+// Счётчик ресурсов.
+dvar int resources_counter[1..n_resources_counters , 1..n_intervals];
+int counter_type[1..n_resources_counters] = ...; // Типы ресурсов, за которыми следят счётчики.
+int operation_of_counter[1..n_resources_counters] = ...; // Операция, которой принадлежит данный счётчик.
+int required_counter_values[1..n_resources_counters] = ...; // Необходимые значения на счётчиках ресурсов для выполнения операции.
+{int} counters_of_operation[0..n_operations] = ...; // Счётчики, которые относятся к данной операции.
+
+dvar boolean is_involved_in_cargo_op[0..n_moving_obj, 0..n_intervals];
+
+// Операции погрузки, которые используют этот объект в качестве главного или в качестве бункеровщика.
+{int} related_cargo_op[0..n_moving_obj] = ...;
+
+// Операции отшвартовки, которые используют объект в качестве главного.
+{int} related_unmooring_op[0..n_moving_obj] = ...;
+
+// Требуемое положение конкретных типов объектов в момент начала операций.
+int operations_resources_start_loc[1..n_resources_counters] = ...;
+
+// Требуемое положение главного объекта в момент начала операций.
+int main_obj_start_loc[0..n_operations] = ...;
+// Требуемое положение бункеровщика в момент начала операции.
+int bunker_start_loc[0..n_operations] = ...;
+
+// Бункеровщик, участвующий в операции погрузки (0, если такогого нет или это не погрузка).
+int bunker_of_cargo_op[0..n_operations] = ...;
+
+int operations_duration[0..n_operations] = ...;
+int is_continuous_operation[0..n_operations] = ...;
+
+{int} conflicting_operations[0..n_operations] = ...;
+
+int bad_weather[0..n_operations, 0..n_intervals] = ...;
+
+
+int n_cargo_types = ...;
+int n_all_storage_sections = ...;
+dvar int storage_used_volume[0..n_all_storage_sections, 0..(n_intervals + 1)];
+
+int max_storage_vol[0..n_all_storage_sections] = ...;
+
+int initial_storage_vol[0..n_all_storage_sections] = ...;
+int final_storage_vol[0..n_all_storage_sections] = ...;
+
+int cargo_flows[0..n_all_storage_sections, 0..(n_intervals + 1)] = ...;
+
+int n_loading_op = ...;
+
+int loading_op_delta_of_main_obj[0..n_operations] = ...;
+int loading_op_abs_delta[0..n_operations] = ...;
+int loading_op_direction[0..n_operations] = ...;
+
+int operations_main_stor[0..n_operations] = ...;
+int operations_secondary_stor[0..n_operations] = ...;
+int operations_cargo_t[0..n_operations] = ...;
+
+int loading_op_delta[1..n_loading_op] = ...;
+int loading_op_local_direction[1..n_loading_op] = ...;
+int loading_op_n[1..n_loading_op] = ...; // Номера среди общего списка операций.
+
+{int} involved_operations[1..n_all_storage_sections] = ...;
+{int} sections_of_moving_obj[1..n_moving_obj] = ...;
+int is_sections_of_moving_obj_empty[1..n_moving_obj] = ...;
+
+
+int n_fixed_op = ...;
+int fixed_op[1..n_fixed_op] = ...;
+{int} fixed_op_resources[1..n_fixed_op] = ...;
+int fixed_op_start[1..n_fixed_op] = ...;
+int fixed_op_end[1..n_fixed_op] = ...; // Включительно.
+int fixed_op_intensity[1..n_fixed_op] = ...;
+
+int is_fixed[0..n_operations, 0..n_intervals] = ...;
+int is_obj_involved_in_fixed_op[0..n_moving_obj, 0..(n_intervals + 1)] = ...;
+
+
+int min_positive_cargo_val[1..n_all_storage_sections, 1..n_locations] = ...; // Объём максимальной положительной операции, которая может быть произведена с этой секцией в этом хранилище. Если в локации таковой нет, то это значение объёма хранилища + 1.
+int max_negative_cargo_val[1..n_all_storage_sections, 1..n_locations] = ...;
+
+int can_obj_leave_loc_only_alone[1..n_moving_obj, 1..n_locations] = ...;
+int is_fixed_op_planned_in_future[1..n_moving_obj, 1..n_locations, 1..n_intervals] = ...;
+
+
+dvar boolean is_not_terminated[1..(n_intervals + 1)];
+
+minimize sum (i in 1..(n_intervals + 1)) is_not_terminated[i];
+
+subject to {
+    forall (t in 0..(n_intervals + 1)) (op_status[0, t] == 0); // Фиктивная операция.
+    forall (t in 0..(n_intervals + 1)) ( op_start[0, t] == 0); // Фиктивная операция.
+    
+    // Определение current_moving_operation.
+	    forall (t in 0..(n_intervals + 1)) (current_moving_operation[0, t] == 0); // Фиктивный объект.
+    	
+    	// Крайние значения.
+	    forall (obj in 1..n_moving_obj, t in {0, n_intervals + 1}) (
+	        current_moving_operation[obj, t] == 0
+	    );
+	    
+	    // Текущая операция лежит в множестве тех, которые затрагивают данный объект.
+	    forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	        (current_moving_operation[obj, t] != 0) => (moving_op_of_obj[obj, current_moving_operation[obj, t]] != 0)
+	    );
+	    // Если операция, затрагивающая данный объект в качестве главного, выполняется - то именно она текущая операция перемещения для этого объекта.
+	    forall (op in 1..n_operations, t in 1..n_intervals : (is_moving_operation[op] == 1)) (
+	        (op_status[op, t] == 1) => (current_moving_operation[main_obj_of_operation[op], t] == op)
+	    );
+	    // Связь current_moving_operation c op_status.
+	    forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	        (current_moving_operation[obj, t] != 0) => (op_status[current_moving_operation[obj, t], t] == 1)
+	    );
+
+	    
+	// Определение current_moored_obj.
+	    forall (t in 0..(n_intervals + 1)) (current_moored_obj[0, t] == 0); // Фиктивная локация.
+	
+	    // Фиксирование неиспользуемых значений.
+	    forall (loc in 1..n_locations, t in 0..(n_intervals + 1) : loc mod 2 == 1) (
+	        current_moored_obj[loc, t] == 0
+	    );
+	
+	    // Крайние значения.
+	    forall (loc in 1..n_locations, t in {0, n_intervals + 1}) (
+	        current_moored_obj[loc, t] == 0
+	    );
+	
+	
+	    // current_moored_obj соответствуе какому-либо реально пришвартованному объекту.
+	    forall (loc in 1..n_locations, t in 1..n_intervals : loc mod 2 == 0) (
+	        (current_moored_obj[loc, t] != 0) => ((m_obj_loc[current_moored_obj[loc, t], t] == loc) ||
+	                       (
+//	                       (sum (id in 1..op_with_nominally_mooring_sizes[loc, current_moored_obj[loc, t]])
+//	                         op_status[op_with_nominally_mooring[loc, current_moored_obj[loc, t], id], t]
+//	                        ) > 0
+							(sum (id in 1..op_with_nominally_mooring_max_size) // new!!!
+	                         op_status[op_with_nominally_mooring[loc, current_moored_obj[loc, t], id], t]
+	                        ) > 0
+	                      ))
+	    );
+	
+	    // Если объект пришвартован или швартуется, то current_moored_obj об это знает.
+	    forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	        (m_obj_loc[obj, t] mod 2 == 0) => (current_moored_obj[m_obj_loc[obj, t], t] == obj)
+	    );
+	
+	    // Если выполняется операция, где судно условно пришвартовано, то current_moored_obj знает об этом.
+	    forall (loc in 1..n_locations,
+	                       obj in 1..n_moving_obj,
+	                       op_id in 1..op_with_nominally_mooring_sizes[loc, obj],
+	                       t in 1..n_intervals) (
+	        (op_status[op_with_nominally_mooring[loc, obj, op_id], t] == 1) => (current_moored_obj[loc, t] == obj)
+	    );
+	  
+	    
+	// Определение m_obj_loc.
+	    forall (t in 0..(n_intervals + 1)) (m_obj_loc[0, t] == 0); // Фиктивный объект.
+	
+	    // За фиктивный нулевой интервал объект не успевает ничего сделать с начальным положением.
+	    forall (obj in 1..n_moving_obj) (
+	        m_obj_loc[obj, 1] == m_obj_loc[obj, 0]
+	    );
+	
+	    // Направление движения/местоположение объекта может измениться только если перед этим началась операция перемещения, и он не вспомогательный при операции швартовки.
+	        forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) (
+	            ((current_moving_operation[obj, t - 1] != current_moving_operation[obj, t - 2]) &&
+	             (current_moving_operation[obj, t - 1] != 0) &&
+	             ((obj == main_obj_of_operation[current_moving_operation[obj, t - 1]])
+	                  ||
+	              (is_mooring_op[current_moving_operation[obj, t - 1]] == 0)
+	             )
+	            ) => (m_obj_loc[obj, t] == operations_destination[current_moving_operation[obj, t - 1]])
+	        );
+	        forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) (
+	            ((current_moving_operation[obj, t - 1] == current_moving_operation[obj, t - 2]) ||
+	             (current_moving_operation[obj, t - 1] == 0) ||
+	             ((obj != main_obj_of_operation[current_moving_operation[obj, t - 1]])
+	                  &&
+	              (    is_mooring_op[current_moving_operation[obj, t - 1]] == 1)
+	             )
+	            ) => (m_obj_loc[obj, t] == m_obj_loc[obj, t - 1])
+	        );
+	        
+	        
+	// Начальное состояние.
+	    forall (i in 1..n_moving_obj) (m_obj_loc[i, 0] == initial_m_obj_loc[i]);
+	
+	// Конечное состояние.
+	    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])
+	    );
+
+
+	// Определение op_status, op_start.
+	    forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i, j] == 0); // Краевые значения.
+	
+	    forall (op in 1..n_operations, j in {0, n_intervals + 1}) (op_start[op, j] == 0);
+	    forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] == ((op_status[i, j] == 1) && (op_status[i, j - 1] == 0)));
+
+
+	// Связь ресурсов с операцией и основным объектом.	
+	    forall (t in 0..(n_intervals + 1)) (participation_as_resource[0, t] == 0); // Фиктивный объект.
+	
+	        // Граничные значения.
+	        forall (obj in 1..n_moving_obj) (participation_as_resource[obj, 0] == 0);
+	        forall (obj in 1..n_moving_obj) (participation_as_resource[obj, n_intervals + 1] == 0);
+	
+	        // Только те операции, которые затрагивают данный объект.
+	        forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	            (participation_as_resource[obj, t] != 0)
+	                => participation_as_resource[obj, t] in operations_that_used_obj_as_resource[obj]
+	        );
+	
+	        // Связь с текущими операциями перемещения.
+	            // Если объект задействован в операции перемещения, которая использует его как ресурс,
+	            // то participation_as_resource должен указывать на эту операцию.
+	            forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	                 (current_moving_operation[obj, t] in operations_that_used_obj_as_resource[obj])
+	                    =>
+	                 (participation_as_resource[obj, t] == current_moving_operation[obj, t])
+	            );
+	            // Если объект участвует как ресурс в операции перемещения, то это согласованно с current_moving_operation.
+	            forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	                ((participation_as_resource[obj, t] != 0) &&
+	                 (is_moving_operation[participation_as_resource[obj, t]] == 1)
+	                ) => (participation_as_resource[obj, t] == current_moving_operation[obj, t])
+	            );
+	
+	        // { Объект участвует где-то в качестве ресурса - соответствующая операция обязана быть активной. }
+	        forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	            (participation_as_resource[obj, t] != 0) => (op_status[participation_as_resource[obj, t], t] == 1)
+	        );
+	
+	        // От начала операции и до конца её ресурсы не могут измениться (в том числе и для погрузки).
+	        forall (obj in 1..n_moving_obj, t in 1..(n_intervals - 1)) (
+	            ((participation_as_resource[obj, t] != 0) &&
+	             (op_status[participation_as_resource[obj, t], t + 1] == 1)
+	            ) => (participation_as_resource[obj, t + 1] == participation_as_resource[obj, t])
+	        );
+	
+	
+	    // Участие всех необходимых ресурсов в операции.
+	    forall (t in 1..n_intervals, op in 1..n_operations, counter in counters_of_operation[op]) (
+	        (op_status[op, t] == 1) => (resources_counter[counter, t] == required_counter_values[counter])
+	    );
+	
+	    // Определение resources_counter.
+	    forall (counter in 1..n_resources_counters, t in 1..n_intervals) (
+	        resources_counter[counter, t] == sum (obj in objects_of_type[counter_type[counter]]) (
+	            participation_as_resource[obj, t] == operation_of_counter[counter]
+	        )
+	    );
+
+
+	// Участие объекта в операциях грузообработки.
+	    forall (t in 1..n_intervals) (is_involved_in_cargo_op[0, t] == 0); // Фиктивный объект.
+	    forall (obj in 1..n_moving_obj) (is_involved_in_cargo_op[obj, 0] == 0);
+	
+	    // Определение is_involved_in_cargo_op.
+	    forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	        is_involved_in_cargo_op[obj, t] == (
+	                ((sum (op in related_cargo_op[obj]) (op_status[op, t])
+	                 ) > 0
+	                )
+	                    ||
+	                ((participation_as_resource[obj, t] != 0) && (is_moving_operation[participation_as_resource[obj, t]] == 0))
+	            )
+	    );
+	    // Операции перемещения исключают операции грузообработки и наоборот.
+	    forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+	        (is_involved_in_cargo_op[obj, t] == 1) => (current_moving_operation[obj, t] == 0)
+	    );
+
+
+
+	// Наличие всех объектов на месте во время начала операции перемещения + готовность к началу.
+	    // Наличие на месте всех ресурсов.
+	    forall (
+	        op      in 1..n_operations,
+	        t       in 1..n_intervals,
+	        counter in counters_of_operation[op],
+	        obj     in objects_of_type[counter_type[counter]]) (
+	            ((participation_as_resource[obj, t] == op) && (op_start[op, t] == 1)
+	            ) => (m_obj_loc[obj, t] == operations_resources_start_loc[counter])
+	    );
+	
+	    // Наличие главных объектов на месте.
+	    forall (op in 1..n_operations, t in 1..n_intervals) (
+	        (op_start[op, t] == 1) => (m_obj_loc[main_obj_of_operation[op], t] == main_obj_start_loc[op])
+	    );
+	
+	    // Наличие бункеровщиков на месте.
+	    forall (op in 1..n_operations,
+	                       t in 1..n_intervals
+	                        : bunker_of_cargo_op[op] != 0) (
+	        (op_start[op, t] == 1) => (m_obj_loc[bunker_of_cargo_op[op], t] == bunker_start_loc[op])
+	    );
+
+	// Непрерывность перемещения и швартовки.
+	    forall (i in 1..n_operations : is_continuous_operation[i] == 1) 
+	        forall (j in 1..(n_intervals - operations_duration[i] + 1))
+	        	forall (k in 1..(operations_duration[i] - 1))
+		            (op_start[i, j] == 1) => (
+		                (op_status[i, j + k] == 1)
+		                    &&
+		                (op_status[i, j + operations_duration[i]] == 0)
+		            )
+	        ;
+	    
+	    forall (i in 1..n_operations : is_continuous_operation[i] == 1)
+	        forall (j in (n_intervals - operations_duration[i] + 2)..(n_intervals + 1)) (op_start[i, j] == 0)
+	    ;
+	
+	// Конфликтующие операции.
+	        forall (op in 1..n_operations, t in 0..(n_intervals + 1), conf_op in conflicting_operations[op]) (
+	            (op_status[op, t] == 1) => (op_status[conf_op, t] == 0)
+	        );
+	
+	// Окна непогоды.
+	    forall (op in 1..n_operations, t in 1..n_intervals) (
+	        (bad_weather[op, t] == 1) => (op_status[op, t] == 0)
+	    );
+
+
+	// Грузообработка.
+	    forall (t in 0..(n_intervals + 1)) (storage_used_volume[0, t] == 0); // Фиктивный объект.
+	
+	    // Ограничения на вместимость.
+	        // Максимальный объём.
+	        forall (storage in 1..n_all_storage_sections, t in 0..(n_intervals + 1)) (
+	            (storage_used_volume[storage, t]) <= max_storage_vol[storage]
+	        );
+	        // Неотрицательность объёма.
+	        forall (storage in 1..n_all_storage_sections, t in 0..(n_intervals + 1)) (
+	            0 <= storage_used_volume[storage, t]
+	        );
+	
+	    // Ограничения на граничные значения.
+	        forall (storage in 1..n_all_storage_sections) ( // Initial values.
+	            storage_used_volume[storage, 0] == initial_storage_vol[storage]
+	        );
+	
+	        forall (storage in 1..n_all_storage_sections // Final values.
+	                            : final_storage_vol[storage] >= 0) (
+	                storage_used_volume[storage, n_intervals + 1] == final_storage_vol[storage]
+	        );
+	
+	    // Изменение грузов в хранилищах.
+	        
+	
+	        forall (storage in 1..n_all_storage_sections, t in 1..(n_intervals + 1)) (
+	            storage_used_volume[storage, t] == (
+	                storage_used_volume[storage, t - 1] +
+	                cargo_flows[storage, t] +
+	                sum (inv_op in involved_operations[storage]) (
+	                    loading_op_delta[inv_op] *
+	                    op_status[loading_op_n[inv_op], t]
+	                )
+	            )
+	        );
+
+
+	// Фиксированные операции.	
+	    forall (no in 1..n_fixed_op)
+	        forall (t in fixed_op_start[no]..fixed_op_end[no])
+	            (op_status[fixed_op[no], t] == 1)
+	    ;
+	    
+	    forall (no in 1..n_fixed_op)
+	        forall (t in fixed_op_start[no]..fixed_op_end[no])
+	            forall (obj in fixed_op_resources[no]) (
+	                participation_as_resource[obj, t] == fixed_op[no]
+	            
+	        )
+	    ;
+
+
+
+//	// Оптимизация - сдвиг в начало.
+//	    // Возможно ли начать операцию в данный интервал (если предположить, что операция длится 1 интервал).
+//	    array [0..n_operations, 1..n_intervals] of var bool : is_op_possible;
+//	
+//	    forall (t in 1..n_intervals) (is_op_possible[0, t] == false); // Фиктивный объект.
+//	
+//	    // Счётчик ресурсов, которые могут быть потенциально задействованы в операции.
+//	    array [1..n_resources_counters , 1..n_intervals] of var int : possible_resources_counter;
+//	
+//	    // Определение possible_resources_counter.
+//	        forall (counter in 1..n_resources_counters, t in 1..n_intervals) (
+//	            possible_resources_counter[counter, t] == sum (obj in objects_of_type[counter_type[counter]]) (
+//	                (participation_as_resource[obj, t] == 0) &&
+//	                (current_moving_operation[obj, t] == 0)  &&
+//	                (m_obj_loc[obj, t] == operations_resources_start_loc[counter])
+//	            )
+//	        );
+//	
+//	    // Достаточно ли свободных ресурсов для операции.
+//	    array [0..n_operations, 1..n_intervals] of var bool : is_enough_free_resources;
+//	
+//	        forall (t in 1..n_intervals) (is_enough_free_resources[0, t] == false); // Фиктивный объект.
+//	
+//	        forall (op in 1..n_operations, t in 1..n_intervals) (
+//	            is_enough_free_resources[op, t] == forall (counter in counters_of_operation[op]) (
+//	                possible_resources_counter[counter, t] >= required_counter_values[counter]
+//	            )
+//	        );
+//	
+//	    // Определение is_op_possible.
+//	        forall (op in 1..n_operations, t in 1..n_intervals) (
+//	            is_op_possible[op, t] == (
+//	                (bad_weather[op, t] == false) &&                  // Погода не мешает.
+//	                (m_obj_loc[main_obj_of_operation[op], t] == main_obj_start_loc[op])
+//	                                                              && // Главный объект на месте.
+//	                (current_moving_operation[main_obj_of_operation[op], t] == 0)
+//	                                                              && // Главный объект не участвует в операции перемещеня.
+//	                (is_enough_free_resources[op, t] == true)      && // Достаточно свободных ресурсов на нужном месте.
+//	                (forall (conf_op in conflicting_operations[op]) (op_status[conf_op, t] == false))
+//	                                                              && // Не выполняется ни одной конфликтующей операции.
+//	                (is_moving_operation[op] -> not is_involved_in_cargo_op[main_obj_of_operation[op], t])
+//	                                                              && // Если это операция перемещения, то главный объект
+//	                                                                 // не участвует в операциях погрузки.
+//	                ((is_mooring_op[op] && (operations_destination[op] mod 2 = 0)) -> (
+//	                    current_moored_obj[operations_destination[op], t] = 0)
+//	                )                                             && // Если это операция пришвартовки, то в этот интервал
+//	                                                                 // причал должен быть свободным.
+//	                ((not is_moving_operation[op]) -> (
+//	                    let {1..n_all_storage_sections : m_stor = operations_main_stor[op];
+//	                         1..n_all_storage_sections : s_stor = operations_secondary_stor[op];
+//	                         int                       : delta = loading_op_delta_of_main_obj[op];
+//	                        } in
+//	                    (storage_used_volume[m_stor, t] + delta >= 0) /\
+//	                    (storage_used_volume[m_stor, t] + delta <= max_storage_vol[m_stor]) /\
+//	                    (storage_used_volume[s_stor, t] - delta >= 0) /\
+//	                    (storage_used_volume[s_stor, t] - delta <= max_storage_vol[s_stor])
+//	                ))                                            /\ // Если это операция грузообработки, то она не выведет
+//	                                                                 // объём берегового хранилища и хранилища судна за
+//	                                                                 // границы дозволенного.
+//	                (((not is_moving_operation[op]) /\ (main_obj_start_loc[op] mod 2 = 1)) ->
+//	                    ((current_moored_obj[twin_location[main_obj_start_loc[op]], t] = 0) \/
+//	                     (current_moored_obj[twin_location[main_obj_start_loc[op]], t] = main_obj_of_operation[op]))
+//	                )                                             /\ // Если это операция грузообработки без пришвартовки,
+//	                                                                 // то причал должен быть свободен в этот интервал, либо
+//	                                                                 // главный объект должен быть уже условно пришвартован.
+//	                (((bunker_of_cargo_op[op] != 0) /\ (op_status[op, t])) ->
+//	                    ((m_obj_loc[bunker_of_cargo_op[op], t] = bunker_start_loc[op]) /\
+//	                     (current_moving_operation[bunker_of_cargo_op[op], t] = 0))
+//	                )                                                // Бункеровщик (если есть) находится в нужной локации
+//	                                                                 // и не участвует в операциях перемещения.
+//	            )
+//	        );
+//	
+//	    // Сам критерий оптимизации - если если операцию можно было начать на 1 интервал раньше, то её нужно начать раньше.
+//	        forall (op in 1..n_operations, t in 2..n_intervals) (
+//	            (op_start[op, t] /\ (not is_fixed[op, t])) -> not is_op_possible[op, t - 1]
+//	        );
+	
+	// Оптимизация - судно возвращается откуда перед этим пришло -> оно сделало или делает что-то "полезное".
+//	    array [0..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : prev_m_obj_loc;
+//	    array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_involved_in_useful_operation;
+//	
+//	    constraint forall (t in 0..(n_intervals + 1)) (prev_m_obj_loc[0, t] = 1);
+//	    constraint forall (t in 0..(n_intervals + 1)) (is_obj_involved_in_useful_operation[0, t] = false);
+//	
+//	    // Определение prev_m_obj_loc
+//	        constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
+//	            (m_obj_loc[obj, t - 1] != m_obj_loc[obj, t]) -> (prev_m_obj_loc[obj, t] = m_obj_loc[obj, t - 1])
+//	        );
+//	        constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
+//	            (m_obj_loc[obj, t - 1] == m_obj_loc[obj, t]) -> (prev_m_obj_loc[obj, t] = prev_m_obj_loc[obj, t - 1])
+//	        );
+//	        constraint forall (obj in 1..n_moving_obj) (prev_m_obj_loc[obj, 0] = m_obj_loc[obj, 0]);
+//	
+//	    // Определение is_obj_involved_in_useful_operation
+//	        constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
+//	            is_obj_involved_in_useful_operation[obj, t] = (
+//	                   (participation_as_resource[obj, t] != 0)
+//	                \/ (exists (op in related_cargo_op[obj]) (op_status[op, t]))
+//	                \/ (is_obj_involved_in_fixed_op[obj, t])
+//	                \/ (exists (op in related_unmooring_op[obj]) (op_status[op, t]))
+//	            )
+//	        );
+//	        constraint forall (obj in 1..n_moving_obj) (is_obj_involved_in_useful_operation[obj, 0] = false);
+//	
+//	    // Успел ли объект поучаствовать в полезной операции к концу данного интервала.
+//	    array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_attended_useful_op_in_cur_loc;
+//	    // Определение is_attended_useful_op_in_cur_loc
+//	        constraint forall (t in 0..(n_intervals + 1)) (is_attended_useful_op_in_cur_loc[0, t] = false);
+//	
+//	        constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
+//	            is_attended_useful_op_in_cur_loc[obj, t] = (
+//	                (is_attended_useful_op_in_cur_loc[obj, t - 1] /\ (m_obj_loc[obj, t - 1] == m_obj_loc[obj, t])) // Предыдущее значение в текущей локации.
+//	                    \/
+//	                is_obj_involved_in_useful_operation[obj, t]
+//	                    \/
+//	                is_obj_involved_in_useful_operation[obj, t - 1] // Учитывает случай когда операция перемещения, из-за которой объект попал в локацию была нужна.
+//	            )
+//	        );
+//	
+//	    // Сама оптимизация - если объект
+//	    constraint forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) (
+//	        ((m_obj_loc[obj, t - 1] != m_obj_loc[obj, t]) /\ (prev_m_obj_loc[obj, t - 1] == m_obj_loc[obj, t])
+//	        ) -> is_attended_useful_op_in_cur_loc[obj, t - 1]
+//	    );
+	
+//	// Оптимизация - если объект не может совершить в данной локации операции без выхода за границы хранилища, а так же если он
+//	// может уйти только своим ходом, то он либо уходит немедленно, либо остаётся на месте навсегда.
+//	
+//	    array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : can_obj_theoretically_use_cargo_op;
+//	    // Определение can_obj_theoretically_use_cargo_op.
+//	        constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
+//	            can_obj_theoretically_use_cargo_op[obj, t] = (
+//	                is_sections_of_moving_obj_empty[obj]
+//	                    \/
+//	                exists (section in sections_of_moving_obj[obj]) (
+//	                       (storage_used_volume[section, t - 1] + min_positive_cargo_val[section, main_location[m_obj_loc[obj, t]]] <= max_storage_vol[section])
+//	                    \/ (storage_used_volume[section, t - 1] + max_negative_cargo_val[section, main_location[m_obj_loc[obj, t]]] >= 0)
+//	                )
+//	            )
+//	        );
+//	        constraint forall (t in 0..(n_intervals + 1)) (can_obj_theoretically_use_cargo_op[0, t] = false);
+//	        constraint forall (obj in 1..n_moving_obj) (can_obj_theoretically_use_cargo_op[obj, 0] = false);
+//	
+//	    // Остановился ли объект окончательно, начиная с данного интервала.
+//	    array [0..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_totally_terminated;
+//	    constraint forall (obj in 1..n_moving_obj) (is_obj_totally_terminated[obj, n_intervals + 1] = true);
+//	    constraint forall (t in 0..(n_intervals + 1)) (is_obj_totally_terminated[0, t] = true);
+//	
+//	    constraint forall (obj in 1..n_moving_obj, t in 0..n_intervals) (
+//	        is_obj_totally_terminated[obj, t] = (
+//	               (current_moving_operation[obj, t] = 0)
+//	            /\ (not is_involved_in_cargo_op[obj, t])
+//	            /\ (is_obj_totally_terminated[obj, t + 1])
+//	        )
+//	    );
+//	
+//	    // Само ограничение.
+//	    constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) (
+//	        (   (can_obj_leave_loc_only_alone[obj, m_obj_loc[obj, t]])
+//	         /\ (not can_obj_theoretically_use_cargo_op[obj, t])
+//	         /\ (not is_fixed_op_planned_in_future[obj, m_obj_loc[obj, t], t])
+//	        ) ->
+//	        (is_obj_totally_terminated[obj, t] \/ (current_moving_operation[obj, t] != 0))
+//	    );
+
+	// Критерий оптимизации
+	    // В конце всё остановится.
+	    (is_not_terminated[n_intervals + 1] == 0);
+	
+	    // Действия ещё не остановились, если в текущий интервал что-нибудь происходит или они не остановятся в следующий интервал.
+	    forall (t in 1..n_intervals) (
+	        is_not_terminated[t] == (
+		        ((sum (op in 1..n_operations) (op_status[op, t])
+		         ) > 0)
+	                ||
+	            (is_not_terminated[t + 1] == 1)
+	        )
+	    );
+	    
+}
+
+execute {
+	writeln("op_status = ", op_status, ";");
+	writeln("m_obj_loc = ", m_obj_loc, ";");
+	writeln("op_start = ", op_start, ";");
+	writeln("is_not_terminated = ", is_not_terminated, ";");
+	writeln("storage_used_volume = ", storage_used_volume, ";");
+	
+	writeln("current_moving_operation = ", current_moving_operation, ";");
+	writeln("resources_counter = ", resources_counter, ";");
+	writeln("operation_of_counter = ", operation_of_counter, ";");
+	writeln("participation_as_resource = ", participation_as_resource, ";");
+	
+	writeln("is_involved_in_cargo_op = ", is_involved_in_cargo_op, ";");
+}
+