Exactly how do state1 and startTiling relate? It seems startTiling(x) is equals to state1(x) == SOME_CONSTANT_FOR_StartTiling. Is that the case?

Exactly how do state1 and startTiling relate? It seems startTiling(x) is equals to state1(x) == SOME_CONSTANT_FOR_StartTiling. Is that the case?

Internally, the states are encoded as an uninterpreted function with integer values

@StateSet("startTiling, explicitTiling, setTiling")
// internally, create state1( _ )
//                                == 0 : startTiling
//                                == 1 : explicitTiling
//                                == 2 : setTiling

Then this is very helpful when the state does not change in a function invocation we add to the context something like

state1(x1) == state1(x2)

but this means nothing to the user, so we want to show this using the developer facing states. So we need to apply the equality resolution before we do the state changes from state1( _ ) == 0 : startTiling
Does that make sense?

Yes, it does!

I think my concern is whether knowing that the state of x1 and x2 must be the same is important to understand the error message (instead of x1 being in state A and x2 also need to be in state A), since the error would persist even if it was state B.

I think we can maybe just simplify when both sides are instances of the same variable.
Also, we should probably allow the click expand for these cases as well

@rcosta358 when running the cli with the ImageWriteParam case I still get the previous error, can you check it?

We need to merge main first