No edit summary |
m grammatical edits, punctuation edits |
||
| Line 22: | Line 22: | ||
parity(0) = 0 & | parity(0) = 0 & | ||
!x.(x:NATURAL1 => parity(x) = 1 - parity(x-1)) | !x.(x:NATURAL1 => parity(x) = 1 - parity(x-1)) | ||
* 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 has not yet been enabled in 1.3.0. | Note: this only works in version 1.2.7 of ProB; this feature has not yet been enabled in 1.3.0. | ||
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.