You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
27 lines
865 B
27 lines
865 B
// 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" ])
|