% dp_check('model_dp1_dp3_4PEperT_10t_10p').

archi_model_spec("model_dp1_dp3_4PEperT_10t_10p",L) :-
L = [ sw_archi(log_upg),
tasks([t0,t1,t2,t3,t4,t5,t6,t7,t8,t9]),
processing_elements([c0,c1,c2,c3,c4,c5,c6,c7,c8,c9]),
a_type(c0,processing),
a_type(c1,processing),
a_type(c2,processing),
a_type(c3,processing),
a_type(c4,processing),
a_type(c5,processing),
a_type(c6,processing),
a_type(c7,processing),
a_type(c8,processing),
a_type(c9,processing),
am_PE_use(c0,[]),
am_PE_use(c1,[]),
am_PE_use(c2,[]),
am_PE_use(c3,[]),
am_PE_use(c4,[]),
am_PE_use(c5,[]),
am_PE_use(c6,[]),
am_PE_use(c7,[]),
am_PE_use(c8,[]),
am_PE_use(c9,[]),
ha_independent(c0),
ha_independent(c1),
ha_independent(c2),
ha_independent(c3),
ha_independent(c4),
ha_independent(c5),
ha_independent(c6),
ha_independent(c7),
ha_independent(c8),
ha_independent(c9),
dm_PE_allowed(t0,[c0,c1,c2,c3]),
dm_PE_allowed(t1,[c0,c1,c2,c3]),
dm_PE_allowed(t2,[c0,c1,c2,c3]),
dm_PE_allowed(t3,[c4,c5,c6,c7]),
dm_PE_allowed(t4,[c4,c5,c6,c7]),
dm_PE_allowed(t5,[c4,c5,c6,c7]),
dm_PE_allowed(t6,[c8,c9]),
dm_PE_allowed(t7,[c8,c9]),
dm_PE_allowed(t8,[c8,c9]),
dm_PE_allowed(t9,[c8,c9]),
dm_PE_scheduling(c0,t0, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c1,t0, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c2,t0, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c3,t0, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c0,t1, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c1,t1, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c2,t1, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c3,t1, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c0,t2, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c1,t2, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c2,t2, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c3,t2, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c4,t3, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c5,t3, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c6,t3, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c7,t3, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c4,t4, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c5,t4, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c6,t4, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c7,t4, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c4,t5, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c5,t5, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c6,t5, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c7,t5, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c8,t6, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c9,t6, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c8,t7, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c9,t7, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c8,t8, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c9,t8, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c8,t9, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
dm_PE_scheduling(c9,t9, sched(proportionate_fair_pf_protocol,preemptive,time_unit_migration_type)),
a_proc_type(c0,processor),
a_proc_type(c1,processor),
a_proc_type(c2,processor),
a_proc_type(c3,processor),
a_proc_type(c4,processor),
a_proc_type(c5,processor),
a_proc_type(c6,processor),
a_proc_type(c7,processor),
a_proc_type(c8,processor),
a_proc_type(c9,processor),
a_proc_isa(c0,i386),
a_proc_isa(c1,i386),
a_proc_isa(c2,i386),
a_proc_isa(c3,i386),
a_proc_isa(c4,i386),
a_proc_isa(c5,i386),
a_proc_isa(c6,i386),
a_proc_isa(c7,i386),
a_proc_isa(c8,i386),
a_proc_isa(c9,i386),
a_proc_speed(c0, 100000000),
a_proc_speed(c1, 100000000),
a_proc_speed(c2, 100000000),
a_proc_speed(c3, 100000000),
a_proc_speed(c4, 100000000),
a_proc_speed(c5, 100000000),
a_proc_speed(c6, 100000000),
a_proc_speed(c7, 100000000),
a_proc_speed(c8, 100000000),
a_proc_speed(c9, 100000000),
end_with_success ].