No edit summary |
No edit summary |
||
Line 17: | Line 17: | ||
parity(0) = 0 & | parity(0) = 0 & | ||
!x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x)) | !x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x)) | ||
* Rewrite your function so that in the forall you do not refer to values | * Rewrite your function so that in the forall you do not refer to values of parity greater than x: | ||
parity : (NATURAL --> {0,1}) & | parity : (NATURAL --> {0,1}) & | ||
parity(0) = 0 & | parity(0) = 0 & | ||
Line 24: | Line 23: | ||
* Use symbolic animation (turn on Lazy expansion of lambdas & set comprehensions and lazy expansion of Recursive set comprehensions and lambdas in the Animation Preferences). 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). | * Use symbolic animation (turn on Lazy expansion of lambdas & set comprehensions and lazy expansion of Recursive set comprehensions and lambdas in the Animation Preferences). 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 | Note: this only works in version 1.2.7 of ProB; this feature is currently being re-developed for ProB 1.3.5. | ||
* Another solution is try and write your function constructively and non-recursively, ideally using a lambda abstraction: | * Another solution is try and write your function constructively and non-recursively, ideally using a lambda abstraction: |
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 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 --> 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.