3

私は、CBMC (C 境界モデル チェッカー) で「正確に 1 回」のプロパティを記述するためのより良い解決策を思いつくために一生懸命努力しています。つまり、行内の 1 つの要素の位置が値 1 (またはブール値 true としてチェックできる任意の正の数) を持つ必要があり、残りはすべてゼロでなければなりません。

M = 4 の場合

for(i=0;i<M;i++){
__CPROVER_assume( (update[i][0]) ?  
    ( !(update[i][1]) && !(update[i][2])  &&!(update[i][3]) ) :         
     ((update[i][1]) ?  (!(update[i][2])  && !(update[i][3]) ) :                  
     ((update[i][2]) ? !update[i][3] : update[i][3] )) )   ;
}`

それ以上のMは大問題です。M = 8 としましょう。次のようなことをしなければなりません:

for(i=0;i<M;i++){
   __CPROVER_assume( (update[i][0]) ?  ( !(update[i][1]) && !(update[i][2])  && !(update[i][3]) && (update[i][4]) && !(update[i][5])  && !(update[i][6]) && !(update[i][7]) )  :
           ((update[i][1]) ?  (!(update[i][2])  && !(update[i][3]) && !(update[i][4]) && !(update[i][5])  && !(update[i][6]) && !(update[i][7]) ) :
             ((update[i][2]) ? ((!update[i][3]) && !(update[i][4]) && !(update[i][5])  && !(update[i][6]) && !(update[i][7]))  :
                   ((update[i][3]) ? (!(update[i][4]) && !(update[i][5])  && !(update[i][6]) && !(update[i][7]))  : 
                   ((update[i][4]) ? (!(update[i][5])  && !(update[i][6]) && !(update[i][7])) : 
                      ((update[i][5]) ? (!(update[i][6]) && !(update[i][7])) :  
                         ((update[i][6]) ? !(update[i][7]) : (update[i][7])))))))) ;
}

違反を 1 回だけチェックするのは簡単ですが、それを述べるのは簡単ではありません。もう 1 つのオプションがあります。2 次元配列の問題を 1 次元のビットベクトルの問題に記述してから、スマート xor を実行することです。しかし、私は現在それについて確信が持てません。

誰にも問題のより良い解決策がありますか?

4

1 に答える 1

3

真の値の数を数えて、その数を確認してみてはどうでしょうか。

for (i = 0; i < M; i++) {
    int n_true = 0;
    int j;

    for (j = 0; j < M; j++) {
        n_true += (update[i][j] ? 1 : 0);
    }

    __CPROVER_assume(n_true == 1);
}
于 2015-03-09T15:41:13.107 に答える