// Parameter K for coins
const int K;

// Max probability of component (coins) violating assumption property (checked separately)
const double p_coin_fail = 
N=2 ? (
 K=2 ? 0.10833260973166493 :
 K=12 ? 0.04164301267240658 :
 K=20 ? 0.01249126244810821 :
0 ) :
N=3 ? ( 
 K=2 ? 0.22908875545788154 :
 K=4 ? 0.12450138796380239 :
 K=8 ? 0.06248479880890645 :
 K=12 ? 0.04164365757451993 :
 K=16 ? 0.031218839562495382 :
 K=20 ? 0.024960596483605935 :
0 ) : 0;

// Probability bound for assumption, derived from above
const double p_one_coin_ok = 1 - pow(p_coin_fail, MAX-2);

// Assume-guarantee check via multi-objective (using ASYM rule)
"num_ag": multi(Pmax=? [ F "one_proc_err" ], P>=p_one_coin_ok [ G "one_coin_ok" ])

// Pareto query for assume-guarantee check
"pareto": multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ])