Take the following function:
CONSTANTS parity PROPERTIES parity : (NATURAL --> {0,1}) & parity(0) = 0 & !x.(x:NATURAL => parity(x+1) = 1 - parity(x))
Here, ProB will complain that it cannot find a solution for parity. The reason is that parity is a function over an infinite domain, but ProB has to represent the function as a finite set of maplets.
There are basically three solutions to this problem:
parity : (NAT --> {0,1}) & parity(0) = 0 & !x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x))
of parity greater than x: parity : (NATURAL --> {0,1}) & parity(0) = 0 & !x.(x:NATURAL1 => parity(x) = 1 - parity(x-1))
You then need to rewrite your function using set comprehension or lambdas. Also, you are only allowed to apply the function, you cannot use any other set/function operation (otherwise the function will be expanded). Note: this only works in version 1.2.7 of ProB; this feature has not yet been enabled in 1.3.0.