Better way to express “exactly once” in CBMC

Question

I'm trying really hard to come up with a better solution to state an “exactly once” property in CBMC (C bounded model checker). I mean exactly one element position in a row should have the value 1 (or any positive number that can be checked as the boolean true), the rest must be all zeros.

For 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] )) )   ;
}`

For M bigger than that It's huge problem. Lets say M = 8 I have to do something like :

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])))))))) ;
}

Checking the violation of exactly once is easy but stating it looks nontrivial. I may have one more option: to state the 2-dimensional array problem into the 1 dimensional bitvector problem and then doing some smart xor. But I'm currently not sure about that.

Does anybody have a better solution for the problem?

http://cs.stackexchange.com/q/13188/755 – D.W. Mar 27 '17 at 16:04 — D.W., Mar 27 '17 at 16:04

score 3 · Accepted Answer · answered Mar 09 '15 at 15:41

3

How about counting the number of true values, and then checking how many there were:

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);
}

answered Mar 09 '15 at 15:41

John Bollinger

160,171
8
81
157

1

Thank you very much : -> John. Started with the same idea . And somehow that do't worked that's why used the complete enumeration . Oh god I used assume rather than __CPROVER_assume and that was the whole problem. – user2754673 Mar 09 '15 at 15:52

Better way to express “exactly once” in CBMC

1 Answers1