Primitive Integer Operation

Question

I am trying to compare 2 sets of element related by a binary relation which as an effect that

#set1 = #set0 + 2 

Apparently in this expression the 2 is interpreted as {}, that is what the evaluator tells me, so the expression returns true. The book says that + arithmetic operator is detected automatically. But apparently the problem is more about how to express the 2 in arithmetic. In the book I saw an example which is exactly what I want to do.

Moreover, when I calculate #Set, which contains set1+set0 the evaluator returns me a negative value.

Does someone have an idea about this?

Thanks in advance.

Answer 1

Try this:

sig A {}
sig B {}

pred show{ #A = add[#B, 2]}

run show for 5

As far as I understand there is special function for adding integers. Let me know if I understood you right.