No edit summary |
|||
Line 34: | Line 34: | ||
** 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 [[Eval Console|Eval console]] of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher. | You can experiment with those by using the [[Eval Console|Eval console]] of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher. | ||
Line 54: | Line 55: | ||
You may also want to look at the tutorial page on [[Tutorial_Modeling_Infinite_Datatypes|modeling infinite datatypes]]. | You may also want to look at the tutorial page on [[Tutorial_Modeling_Infinite_Datatypes|modeling infinite datatypes]]. | ||
Currently there are three rules when ProB tries to keep a function such as <tt>f = %x.(PRED|E)</tt> symbolically rather than computing an explicit representation: | |||
* the domain of the function is obviously infinite; this is the case for predicates such as <tt>x:NATURAL</tt> | |||
* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left. | |||
* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>) | |||
* a pragma is used to mark the lambda abstraction as symbolic as follows <tt>f = /*@ symbolic */ %x.(PRED|E)</tt>; this requires ProB version 1.3.5-beta10 or higher. | |||
= Recursive Function Definitions in ProB = | = Recursive Function Definitions in ProB = |
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 tries to represent the function as a finite set of maplets.
There are basically four 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))
parity : INTEGER <-> INTEGER & parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
Note, you have to remove the check parity : (NATURAL --> {0,1}), as this will currently cause expansion of the recursive function. We describe this new scheme in more detail below.
parity : (NATURAL --> {0,1}) & parity = %x.(x:NATURAL|x mod 2)
You can experiment with those by 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.
Currently there are three rules when ProB tries to keep a function such as f = %x.(PRED|E) symbolically rather than computing an explicit representation:
As of version 1.3.5-beta7 ProB now accepts recursively defined functions. For this:
Here is a full example:
MACHINE Parity ABSTRACT_CONSTANTS parity PROPERTIES parity : INTEGER <-> INTEGER & parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1)) END
With such a recursive function you can:
Computing the image of the function (parity[1..10]) or composing it with another function (([1,2] ; parity)) does not work yet. These work for non-recursive infinite functions, as described above. Future versions of ProB will probably allow these constructs for recursive functions as well.
Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check parity : INTEGER <-> INTEGER or parity : INTEGER +-> INTEGER will cause ProB to try and expand the function. Future versions of ProB may overcome this limitation.
There are the following further restrictions: