model - Promela 同时随机选择两个元素
问题描述
最近我开始学习 Promela,我想从有 10 个黑球和 4 个白球的盒子中挑选两个球进行建模,我可以将盒子建模为数组,但我不知道如何同时选择 2 个球。从剩下的那些中挑选一个然后另一个改变概率。你有什么想法?
解决方案
当您只需要从连续的数字区间中提取一对值时idx
,您可以通过以下方式轻松解决保证问题:idy
[LOW, UPP]
N = UPP - LOW + 1
idx != idy
- 挑选
idx
_[LOW, UPP]
- 挑选
idy
_[LOW, UPP - 1]
调整
idy
wrt 的值。的值idx
如下:idy = LOW + (((idx - LOW) + 1 + (idy - LOW)) % N)
也就是说,您将其解释idy
为固定位移。idx
. 请注意,这种方法不会影响概率分布,特别是从概率的角度来看idy
,它不会idy
依赖于。idx
例子:
#define BLACK_BALLS 4
#define WHITE_BALLS 10
#define TOTAL_BALLS 14
bool box[TOTAL_BALLS];
inline my_select(var, upper) {
if
:: 0 <= upper -> var = 0;
:: 1 <= upper -> var = 1;
:: 2 <= upper -> var = 2;
:: 3 <= upper -> var = 3;
:: 4 <= upper -> var = 4;
:: 5 <= upper -> var = 5;
:: 6 <= upper -> var = 6;
:: 7 <= upper -> var = 7;
:: 8 <= upper -> var = 8;
:: 9 <= upper -> var = 9;
:: 10 <= upper -> var = 10;
:: 11 <= upper -> var = 11;
:: 12 <= upper -> var = 12;
:: 13 <= upper -> var = 13;
fi;
}
proctype pick_two_balls() {
byte idx;
byte idy;
my_select(idx, TOTAL_BALLS - 1);
my_select(idy, TOTAL_BALLS - 2);
printf("Initial picks:\n")
printf("\tpicked %d in [0, %d]\n", idx, TOTAL_BALLS - 1);
printf("\tpicked %d in [0, %d]\n", idy, TOTAL_BALLS - 2);
idy = ((idx + 1) + idy) % (TOTAL_BALLS);
printf("Adjusted picks:\n");
printf("\tball #01 at index %d\n", idx);
printf("\tball #02 at index %d\n", idy);
printf("Final Balls:\n");
if
:: box[idx] -> printf("\tbox[%d] = black\n", idx);
:: !box[idx] -> printf("\tbox[%d] = white\n", idx);
fi;
if
:: box[idy] -> printf("\tbox[%d] = black\n", idy);
:: !box[idy] -> printf("\tbox[%d] = white\n", idy);
fi;
}
init {
byte idx = 0;
byte todo = BLACK_BALLS;
do // not guaranteed to terminate!
:: todo > 0 ->
my_select(idx, TOTAL_BALLS - 1) ->
if
:: box[idx] ->
skip;
:: else ->
box[idx] = true;
todo = todo - 1;
fi;
:: else ->
break;
od;
for (idx: 0 .. TOTAL_BALLS - 1) {
if
:: box[idx] ->
printf("box[%d] = black\n", idx);
:: !box[idx] ->
printf("box[%d] = white\n", idx);
fi;
}
run pick_two_balls();
}
输出:
~$ spin p.pml
box[0] = white
box[1] = black
box[2] = white
box[3] = white
box[4] = white
box[5] = white
box[6] = white
box[7] = white
box[8] = white
box[9] = white
box[10] = white
box[11] = black
box[12] = black
box[13] = black
Initial picks:
picked 9 in [0, 13]
picked 7 in [0, 12]
Adjusted picks:
ball #01 at index 9
ball #02 at index 3
Final Balls:
box[9] = white
box[3] = white
2 processes created
注意#1:在正常情况下,我会使用该select
语句而不是编写自己的my_select(var, upper)
函数。但是,select
不能保证分配给的值var
是通过均匀分布选取的,我认为这对您来说可能是个问题。
注意#2:当您需要提取多个索引时,上面的数学表达式没有帮助。但是,您可以在机械意义上应用相同的原则:维护used_indexes
为 bool 的支持数组,其中位置k
是true
如果它被某个索引使用。每次选择一个新的 indexi
时,都会从数组的开头开始计算空单元格,然后减i
一。一旦i = 0
你有了应该在原始数组中使用的“真实索引” ,你就将该位置标记为在.j
used_indexes
推荐阅读
- google-apps-script - Google Apps Script : Approval workflow with html, google sheet, pdf
- three.js - Theejs - Change texture on collada element with uses ShaderMaterial
- python - GDAL Intersection return value
- jquery - jquery loading gif loads after ajax call
- ios - 安装配置文件时出现问题
- excel - Download .csv from an indirect Asana link
- excel - Pulling multiple names that are listed from a different sheet to another
- love2d - How can you make the updates/second constant?
- python - 逻辑回归完全是关于统计数据?
- c# - '输入结束时的语法错误' - 尝试从数据库启动存储过程