This section shortly summarises the main options for the resource analysis. A full discussion is given in the ART3 Manual.
The --help option gives an up-to-date list of all available options.
--listRK: List all known resource metrics and exit
--infoRK p1..pn: List detailed information about a given resource metric and exit Use this option to obtain more information about the particular sub-metric codes reported by option --listRK. The output given when using this function is also stored inside the files constraints.lp and constraints.solved.
--RK p1..pn}: Analyse for specified cost metric, with given parameters. If parsing your model does not work correctly, specify option \texttt{--end} directly afterwards as a delimiter.
-H, --RKH: Analyse for default heap-space metric, HumeHeapBoxed.
-S, --RKS: Analyse for default stack-space metric, HumeStackBoxed.
-T, --RKT: Analyse for default time metric, HumeTimeM32.
--end: Ignored option. Useful as a delimiter after options taking parameters.
--retlab p1..pn: Specifies number of return labels in HAM code. Default: 50. \textbf{WARNING: Affects time costs! This value must be correct!} It can be gleaned from the .c file, the number of cases in the switch statement found under ``\verb+_KY16_humeReturn+''. In the future, this number is supposed to be transmitted by the phamc-ann in the .art3 file.
-z: Attribute cost of zero everywhere, unless inline signal received. This option is only useful in conjunction with signals, described in Section~\ref{signals}. The cost metric is replaced by an all-zero metric, and signals can be used to apply the specified metric to certain code fragments to analyse the cost of the fragment on its own, but within the surrounding context. For example, if all input is wired into box A and all output is wired from box C, but we are only interested in the costs of box B inbetween, then using signals and \texttt{-z} can be used to express the cost of running box B in the terms of the input of A and the leftover potential in terms of the output of box C; except for all scheduling costs.
--nnp: Do not assign potential to numeric values (default) The opposite of option --nnp, see comment there.
--ap: Assign potential to numeric values (experimental)
Assigning potential to numerical types is sometimes needed to successfully analyse some programs that cannot be analysed otherwise.
The easiest examples that benefit from this option would be repeat :: A -> Int -> [A]+ and \verb+length :: [A] -> Int.
However, the numeric potential is still experimental and not yet fully tested.
--bb: One big box, i.e. a matching potential must be transmitted on each internal wire. This is useful if more than one box run is to be considered.
--igbo: Ignore all box declarations
--igex: Ignore main expression
--jfun: Analyse functions only. Equivalent to --igbo and --igex. This is highly useful to understand why the LP for an entire program is infeasible. Each global function definition is analysed on its own (together with all called functions, which are individually re-analysed in each step to yield the best possible typing; ``best'' still being best by some heuristic guess, since there is no clear definition of ``best'').
--sim: Simultaneously solve all constraints in a single LP-solver call, i.e. all common variables must have the same value.
--nosim: Solve all constraint set individual with separate LP-solver calls (default). This means that each function/box receives its best type, regardless of the call graph. Be aware that function that uses another function might require a worse type for that subfunction than the one printed for that subfunction (harmless, but might cause confusion in understanding).
--trcmerge: Produce only one merged tracefile for all traces
--ngw: Disable ghost-variable warnings
--nsl: Do not insert slack variables, allows faster feasibility test for LP \textbf{RECOMMENDATION:} Use this option by default, as it will speed up the analysis significantly. Whether or not the analysis is able to determine an annotated typing, is not at all affected by this option, as the constraints fed to the LP-solver are essentially the same (mainly the objective functions is changed). However, the particular result reported will usually be of lesser quality and only occasionally better than without this option.
-X: Enable miscellaneous experimental features
--zeroes: Shows "<0>" within annotated types; otherwise suppressed
--nocon: Suppresses constructor names within annotated types
--nodupwarn, --ndw: Suppress immediately repeated identical warning messages
-v, -V: Verbose messages
-h, -?: Print a short help message
--help: Print an extended help message listing all options
--version: Print version info
As an experimental feature through option --ap, we support potential for numeric values. This means that the potential depends on the actual numeric runtime value, which requires a value range analysis. The included value range analysis is very primitive. It does not work across boxes nor function calls. It is incomplete, which means in particular that it is not safe to use. In order to ensure safety, the user has to investigate that all values that were assigned a positive potential never reach a value below zero at any time during execution. Otherwise the analysis' result is meaningless!
However, the analysis allows the manual insertion of pragmas (signals, see Sction Section 5.3) to help guiding the value range analysis. Signal 9000 can be used to deny potential to an expression of a numeric type. This is always safe to do, so numeric variables, especially function arguments, which cannot be expected to be non-negative. The disadvantage is of course, that the analysis may not succeed anymore due to super-linear costs.
Signals 6000 and 7000 can be used to manually set the bounds for a numeric type. This should be done very carefully, as the validity of the result depends on the correctness of the specified bounds. Note that a numeric value with a negative lower bound can never be assigned any potential, hence a negative value attached to signal 6000 or 7000 will automatically trigger 9000.
Another pitfall lies in increasing the upper bound for a value that already has potential assigned to it, for an increase in value would mean an unjustified increase in potential,
rendering the entire analysis useless.
However, the analysis will allow it and issue a warning in this case.
This can again be avoided by first sending the signal 9000, i.e.
<>7000,"45.5"<><>9000,"nopot"<>.
Signals are expressions within the Schopenhauer sourecode, which may influence the analysis.
A signal is always written in this manner:
<>code;string<>expression
A signal must always precede a normal art3-expression and comes into effect before and/or after the expression
it is bound to is examined by the analysis.
A table of available signals, together with examples of their use, is given in the ART3 Manual.