CodeTools[ProgramAnalysis]
TrajectoryPoints
generate points from a WhileLoop
Calling Sequence
Parameters
Description
Examples
Compatibility
TrajectoryPoints(loop, seedpoints, n, p, trajectorytype)
loop
-
WhileLoop
seedpoints
list of integers, or a list or a set thereof; initial points for the generated trajectories
n
posint, number of trajectory points to generate per seed point
p
(optional) posint, compute the trajectories modulo this number
trajectorytype
(optional) one of plain (default), inductive, or absolute, the type of trajectory to generate
This command computes loop trajectories for the WhileLoop loop. The trajectories start the point(s) given by seedpoints. These points are formed of loop's parameters and variables, formed as the list loop:−variables,loop:−parameters. The loop is iterated for each of these seed points and new values are computed.
This command operates in three modes depending on the trajectorytype:
trajectorytype = plain (default) : the loop is executed as in the original procedure. loop's guard and branch conditions are evaluated at every iteration, causing a single trajectory to be generate per initial point and terminating as the guard condition evaluates to false or as the requested number of points is reached.
trajectorytype = inductive : the guard condition is ignored while iterating the loop so that the generated trajectories may continue beyond their natural end points.
trajectorytype = absolute : both the guard and branch conditions of the loop are ignored. At each iteration, the trajectory is split so that it follows each branch in the loop's if statement as if the branches were all simultaneously taken.
The loop will be iterated until at least n distinct points are generated, if possible. The number of returned points may be fewer than n if the loop terminates prematurely due to the guard condition or if the trajectories loop back onto themselves and cease to generate new points.
The evaluation of the loop trajectories can optionally be conducted modulo p. By default, the computations are done without modular arithmetic in a characteristic zero field.
with⁡CodeToolsProgramAnalysis:
Generating a Sufficient Number of Points
The following procedure counts up from 1 to a:
p := proc(a) local n: n := 1: while n < a do n := n + 1: end do: return n: end proc:
Create the WhileLoop data structure:
loop≔CreateLoop⁡p
loop≔Record⁡WhileLoop,variables=n,parameters=a,initialization=1,transitions=,n+1,guard=n<a,precondition=,postcondition=,returnvalue=n
Ask for 20 trajectory points to be generated, starting with n=1 and taking a=10:
trajcetory_points_1≔TrajectoryPoints⁡loop,1,10,20
trajcetory_points_1≔8,10,1,10,9,10,5,10,3,10,6,10,2,10,4,10,7,10,10,10
Fewer than 20 points were generated in counting from 1 to 10:
numelems⁡trajcetory_points_1
10
Additional seed points can be given to generate more trajectory points:
trajcetory_points_2≔TrajectoryPoints⁡loop,1,10,1,20,20
trajcetory_points_2≔3,20,8,10,4,20,2,20,1,10,9,10,1,20,5,10,3,10,11,20,6,10,2,10,9,20,4,10,10,20,7,20,8,20,7,10,5,20,6,20,10,10
numelems⁡trajcetory_points_2
21
The CodeTools[ProgramAnalysis][TrajectoryPoints] command was introduced in Maple 2016.
For more information on Maple 2016 changes, see Updates in Maple 2016.
See Also
CodeTools[ProgramAnalysis][LoopInvariant]
CodeTools[ProgramAnalysis][IsLoopInvariant]
Download Help Document