N = 4m for non-zero m

[benbrastmckie]

Seems to produce a type error in print_str += elem in print.py. I presume that this is because the bitvector are all hexadecimals. I wonder if there is a function that converts from hexadecimal to bitvectors of the desired kind.

[mbuit82]

Yeah I suspect it is the hexadecimal/binary issue, since all multiples of 4 are hexadecimal (I previously thought it was powers of 2, but it's actually mults of 4). I can make a function to "manually" convert the values to binary. I'll play around w the BVOR function also to see if hexadecimal behave the same was as binary BVs for that (I'll add all this to my TODO)

[benbrastmckie]

I showed the model checker to Graham last night and I think he found the error we're getting for N=4m. In the definition of bitvec_to_substates it looks for a character b, and doesn't find one for the hexadecimals. Rather than changing this definition, I think converting values to binary makes sense. Here is what ChatGPT came up with:

def hex_to_z3_bitvector(hex_str, size):
    # Convert hexadecimal string to Z3 bit-vector
    return BitVecVal(int(hex_str, 16), size)

hex_value = "1A"  # Hexadecimal string
bit_vector_size = 8  # Size of the bit-vector

z3_bitvector = hex_to_z3_bitvector(hex_value, bit_vector_size)

print(z3_bitvector)

This seems to work, though I'm a little confused about the relationship between 16 and size included in the function. But perhaps this will help to convert from hex to bv.

As for where this converter should go, I'm thinking it is probably best to put it as far upstream as possible. So perhaps at the definition of all_bits? There are two places all_bits is defined (inside other functions) so perhaps this could be abstracted into its own function which checks for hex values. I also noticed poss_bits is also defined twice, so perhaps could be included int the helper function. This leads to a broader issue about reorganizing print.py which I'll open separately.

[mbuit82]

Awesome—I'm curious what else Graham thought about the model too (like overall and other stuff)!

I was playing around with bitvectors with N = 4m and it seems they act 'normally' (like binary BVs) wrt BVOR, until it comes time to print. The issue with the function ChatGPT gave is that if we make a BV with bit_vector_size 8 (ie, 4m), it'll still be hexadecimal when it comes time to print. If we instead make it size 4m+1, it'll effectively look like we're adding a state to the model in the printing. I think the best solution might be to make a function that only converts these to binary when it comes time to print (which parts of ChatGPT's function would be good for). Let me know if that's what you had in mind

[benbrastmckie]

That makes sense! As long as all the functions on bitvectors continue to work when they are hexadecimals, converting before printing is a great strategy.

[mbuit82]

I just implemented that and pushed—let me know if the output makes sense for some of them (to check that hexadecimal BVs do in fact work as binary BVs before printing)!

[benbrastmckie]

It looks like it is breaking some of the print functions:

There is a model of:
A, B, ~(A => B)

States:
  #x0 = □ (possible)
  #x1 = a (possible)
  #x2 = b (world)
  #x3 = a.b (impossible)

The evaluation world is b:
  A, B  (true in b)

Propositions:
  |A| = < {b}, ∅ >
  There are no A-alternatives to b

  |B| = < {b}, ∅ >
  There are no B-alternatives to b

Are you able to run and test the files to get the same output? Unless you split off a branch to work on, it would be good to make sure everything runs before pushing. We can go over the branch workflow next time so that pushing changes doesn't break the master branch.

As for what is breaking, I haven't been able to take a look, but seems like the hexs must be making other trouble for the print functions. It does look like the conversion definitions are working though (it is printing 'a', 'b', etc. for states) and no longer throwing errors. So probably just a few small tweaks to get it to print everything.

[mbuit82]

Which file was this for? And also, is the issue that it still prints e.g. #x2? (And lastly what was the N value for these?)

[benbrastmckie]

Oh my bad! I had made some changes to crimson that I forgot about. It's working great. But yes, the hex codes in the states print function should converted to bitvectors. Otherwise I think this issue is resolved.

[mbuit82]

No worries—I think I found a couple problems in there always (and fixed the hex code printing issue); before, the states would only print to twice as big as the maximum state necessarily found in the model. However, now it should more definitively explore the entire state space. This also seems to fix the issue I was talking about in N>4 where it wouldn't print out the whole state space (just tried it for the example that was previously not being explored completely at N=15, and now it's printing the complete exploration). Though in reality, I think this does bring up a good point: if a model only explores up to the 2^5 and there N=10, then the states which have a 1 in the 2^6 to 2^10 positions are all impossible (because they are not going to be in the extension of possible). So is it even worth printing those out? I think that's why they weren't being printed out before

[benbrastmckie]

I turned off printing for impossible states since it wasn't adding much. But maybe there is a better way to do this. But printing states seems to be working well. I'm going to close the issue.