No edit summary |
No edit summary |
||
Line 49: | Line 49: | ||
OPERATIONS | OPERATIONS | ||
Inc = BEGIN c:=c+1 END; | Inc = BEGIN c:=c+1 END; | ||
r <-- Parity = BEGIN r:= parity(c) 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 | 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; r <-- ParityImage = BEGIN r:= parity[0..c] END; r <-- ParityHistory = BEGIN r:= (%i.(i:1..c+1|i-1) ; parity) END END