CodeTools[ProgramAnalysis] - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Programming : CodeTools : Program Analysis : CodeTools/ProgramAnalysis/TrajectoryPoints

CodeTools[ProgramAnalysis]

  

TrajectoryPoints

  

generate points from a WhileLoop

 

Calling Sequence

Parameters

Description

Examples

Compatibility

Calling Sequence

TrajectoryPoints(loop, seedpoints, n, p, trajectorytype)

Parameters

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

Description

• 

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.

Examples

withCodeTools[ProgramAnalysis]:

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:

loopCreateLoopp

loopRecordWhileLoop&comma;variables&equals;n&comma;parameters&equals;a&comma;initialization&equals;1&comma;transitions&equals;&comma;n&plus;1&comma;guard&equals;n<a&comma;precondition&equals;&comma;postcondition&equals;&comma;returnvalue&equals;n

(1)
• 

Ask for 20 trajectory points to be generated, starting with n&equals;1 and taking a&equals;10:

trajcetory_points_1TrajectoryPointsloop&comma;1&comma;10&comma;20

trajcetory_points_110&comma;10&comma;5&comma;10&comma;2&comma;10&comma;3&comma;10&comma;1&comma;10&comma;4&comma;10&comma;9&comma;10&comma;6&comma;10&comma;8&comma;10&comma;7&comma;10

(2)
• 

Fewer than 20 points were generated in counting from 1 to 10:

numelemstrajcetory_points_1

10

(3)
• 

Additional seed points can be given to generate more trajectory points:

trajcetory_points_2TrajectoryPointsloop&comma;1&comma;10&comma;1&comma;20&comma;20

trajcetory_points_29&comma;20&comma;10&comma;10&comma;7&comma;20&comma;5&comma;10&comma;8&comma;20&comma;2&comma;10&comma;3&comma;10&comma;6&comma;20&comma;1&comma;10&comma;11&comma;20&comma;1&comma;20&comma;4&comma;10&comma;10&comma;20&comma;9&comma;10&comma;6&comma;10&comma;8&comma;10&comma;3&comma;20&comma;2&comma;20&comma;7&comma;10&comma;5&comma;20&comma;4&comma;20

(4)

numelemstrajcetory_points_2

21

(5)

Compatibility

• 

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]

CodeTools[ProgramAnalysis]