No edit summary |
No edit summary |
||
Line 35: | Line 35: | ||
** sometimes compute the domain of the function, here, <tt>dom(parity)</tt> is determined to be <tt>NATURAL</tt>. But this only works for simple infinite functions represented. | ** sometimes compute the domain of the function, here, <tt>dom(parity)</tt> is determined to be <tt>NATURAL</tt>. But this only works for simple infinite functions represented. | ||
** sometimes check that you have a total function, e.g., <tt>parity: NATURAL --> INTEGER</tt> can be checked by ProB. However, if you change the range (say from <tt>INTEGER</tt> to <tt>0..1</tt>), then ProB will try to expand the function. | ** sometimes check that you have a total function, e.g., <tt>parity: NATURAL --> INTEGER</tt> can be checked by ProB. However, if you change the range (say from <tt>INTEGER</tt> to <tt>0..1</tt>), then ProB will try to expand the function. | ||
You can experiment with those by using the <tt>Eval...</tt> window of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher. | |||
MACHINE InfiniteParityFunction | |||
CONSTANTS parity | |||
PROPERTIES | |||
parity : (NATURAL --> {0,1}) & | |||
parity = %x.(x:NATURAL|x mod 2) | |||
VARIABLES c | |||
INVARIANT | |||
c: NATURAL | |||
INITIALISATION c:=0 | |||
OPERATIONS | |||
Inc = BEGIN c:=c+1 END; | |||
r <-- Parity = BEGIN r:= parity(c) END | |||
END |
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))
Note: this only works in version 1.2.7 of ProB; this feature has not yet been enabled in 1.3.0.
parity : (NATURAL --> {0,1}) & parity = %x.(x:NATURAL|x mod 2)
You can experiment with those by using the Eval... window of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher.
MACHINE InfiniteParityFunction CONSTANTS parity PROPERTIES parity : (NATURAL --> {0,1}) & parity = %x.(x:NATURAL|x mod 2) VARIABLES c INVARIANT c: NATURAL INITIALISATION c:=0 OPERATIONS Inc = BEGIN c:=c+1 END; r <-- Parity = BEGIN r:= parity(c) END END