No edit summary |
No edit summary |
||
Line 35: | Line 35: | ||
** 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 | You can experiment with those by using the [[Eval Console|Tutorial on using the Eval Console]] of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher. | ||
MACHINE InfiniteParityFunction | MACHINE InfiniteParityFunction |
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))
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 is currently being re-developed for ProB 1.3.5.
parity : (NATURAL --> {0,1}) & parity = %x.(x:NATURAL|x mod 2)
You can experiment with those by using the Tutorial on using the Eval Console 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 --> INTEGER & 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; r <-- ParityImage = BEGIN r:= parity[0..c] END; r <-- ParityHistory = BEGIN r:= (%i.(i:1..c+1|i-1) ; parity) END END
You may also want to look at the tutorial page on modeling infinite datatypes.