Farkas Calculator online demonstrator

Input

fkcc script

#
# Polynomial product, parametrized delay
#

parameters := {inv_eps,eps};

iterations := [] -> { [i,j,N]: 0 <= i and i <= N  and 0 <= j and j <= N};
theta := positive_on iterations;

dependence := [] -> { [is,js,id,jd,N]: 0 <= is and is <= N  and 0 <= js and js <= N and 0 <= id and id <= N  and 0 <= jd and jd <= N and is+js = id+jd and is<id};

#
# Correctness: s -> t ==> theta(s) <= theta(t) + eps, 0 <= eps <= 1
#
causality := positive_on dependence;
to_target := {[is,js,id,jd,N]->[id,jd,N]};
to_source := {[is,js,id,jd,N]->[is,js,N]};

theta_correct := solve (theta . to_target) - (theta . to_source) - causality + {[is,js,id,jd,N] -> -1*eps} = 0;

theta_def := define theta with theta;
eps_correct := [] -> {[i]: 0 <= eps and eps <= 1 and inv_eps = 1-eps};

#
# Efficiency: theta(s) <= latency(N), then min latency(N)
#

# L(N) >= 0 on the parameter domain
latency := positive_on ([] -> {[N]: N >= 0});

# theta(i) <= L(N) \forall i,N
bound_theta := positive_on ([] -> {[i,j,N]: 0 <= i and i <= N  and 0 <= j and j <= N});
theta_bounded := solve (latency . {[i,j,N] -> [N]}) - theta- bound_theta = 0;
bound_def := define latency with latency;

# Display the result
D := keep inv_eps,latency_0,latency_1,theta_0,theta_1,theta_2,theta_3,eps in theta_correct*theta_def*eps_correct*theta_bounded*bound_def;

set D;
D;

lexmin D;

Output format