svmranker:usage
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionLast revisionBoth sides next revision | ||
svmranker:usage [2020/11/17 22:38] – merlin | svmranker:usage [2020/11/20 14:10] – merlin | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | **[[svmranker: | + | {{: |
====== Usage ====== | ====== Usage ====== | ||
In the following, we assume that current directory is SVMRanker. | In the following, we assume that current directory is SVMRanker. | ||
Line 9: | Line 9: | ||
Usage: CLIMain.py [OPTIONS] COMMAND [ARGS]... | Usage: CLIMain.py [OPTIONS] COMMAND [ARGS]... | ||
" | " | ||
- | | + | |
Options: | Options: | ||
--help | --help | ||
- | | + | |
Commands: | Commands: | ||
lmulti | lmulti | ||
lnested | lnested | ||
- | | + | parseboogie |
- | parsectoboogie | + | |
- | parsectopy | + | |
- | As we can see, SVMRanker provides five commands. The first two commands allow for proving termination of a given program while the remaining three can be used for parsing the input file and translate it to a different format. In the remaining part of the section we focus on the details for the use of the lmulti and lnested commands. | + | As we can see, SVMRanker provides five commands. The first two commands allow for proving termination of a given program while the remaining three can be used for parsing the input file and translate it to a different format. In the remaining part of the section we focus on the details for the use of the **lmulti** and **lnested** commands. |
- | lmulti, short for learning multiphase ranking function, instructs SVMRanker to learn a multiphase ranking function for the given program. To get the detailed usage information for this command, one can use the following command. | + | **lmulti**, short for learning multiphase ranking function, instructs SVMRanker to learn a multiphase ranking function for the given program. To get the detailed usage information for this command, one can use the following command. |
python3 ./ | python3 ./ | ||
- | | ||
- | The output is the following. | ||
- | SVMRanker --- Version 1.0 | + | The output is the following. |
- | Usage: CLIMain.py lmulti [OPTIONS] SOURCE | + | |
- | Options: | + | |
- | + | < | |
- | < | + | |
SVMRanker --- Version 1.0 | SVMRanker --- Version 1.0 | ||
Usage: CLIMain.py lmulti [OPTIONS] SOURCE | Usage: CLIMain.py lmulti [OPTIONS] SOURCE | ||
Options: | Options: | ||
- | | + | --depth_bound INTEGER |
- | --filetype [C|BOOGIE] | + | |
- | --file BOOGIE: | + | |
- | + | | |
- | --sample_strategy [ENLARGE|CONSTRAINT] | + | |
- | --sample_strategy ENLARGE: enlarge the sample zone when sample num not enough. | + | |
- | --sample_strategy CONSTRAINT: find feasible points by constraint if sample | + | |
- | num not enough default set to ENLARGE | + | |
- | | + | --cutting_strategy [NEG|MINI|POS] |
- | use f(x) < b to cut | + | |
- | --cutting_strategy POS: b is a postive number | + | |
- | --cutting_strategy NEG: b is a negative number | + | |
- | --cutting_strategy MINI: b is the minimum value of sampled points | + | |
- | | + | default set to MINI |
- | | + | --template_strategy [SINGLEFULL|FULL] |
- | templates used for learning | + | |
- | --template_strategy SINGLEFULL: templates are either single variable | + | |
- | or combination of all variables | + | |
- | --template_strategy FULL: template is combination of all variables | + | |
- | default set to SINGLEFULL | + | |
- | | + | --print_level [DEBUG|INFO|NONE] |
- | --print_level DEBUG: print all the information of the learning and debugging | + | |
- | --print_level INFO: print the information of the learning | + | |
- | --print_level NONE: only print the result information of the learning | + | |
- | default set to NONE | + | |
- | | + | --help |
- | </ | + | </ |
As the help shows, there are several options available to tune the execution of lmulti; we present their usage by means of a couple of examples. \\ | As the help shows, there are several options available to tune the execution of lmulti; we present their usage by means of a couple of examples. \\ | ||
<code c Example1.c> | <code c Example1.c> | ||
- | | + | int main() { |
- | int x, y; | + | |
- | while(x > 0 || y > 0) { | + | |
- | x = x + y - 1; | + | |
- | y = y - 1; | + | |
- | } | + | |
- | } | + | } |
</ | </ | ||
- | The is the first C program we consider here; see the file src/ | + | The is the first C program we consider here; see the file src/ |
- | python3 ./ | + | python3 ./ |
- | SVMRanker completes the analysis by returning a 2-multiphase ranking function for the Example1.c program, as shown below. | + | SVMRanker completes the analysis by returning a 2-multiphase ranking function for the **Example1.c** program, as shown below. |
< | < | ||
SVMRanker --- Version 1.0 | SVMRanker --- Version 1.0 | ||
- | example/ | + | example/**Example1.c** |
--------------------LEARNING MULTIPHASE SUMMARY------------------- | --------------------LEARNING MULTIPHASE SUMMARY------------------- | ||
MULTIPHASE DEPTH: | MULTIPHASE DEPTH: | ||
Line 94: | Line 90: | ||
0.0796 * x^1 + 0.482 * 1 + 0.482 * 1 | 0.0796 * x^1 + 0.482 * 1 + 0.482 * 1 | ||
</ | </ | ||
- | Notice that we used the option --filetype to specify the type of the input program, given that SVMRanker supports both Boogie programs and C programs as input file, with the former being the default format. Furthermore, | + | Notice that we used the option |
<code c Example2.c> | <code c Example2.c> | ||
- | | + | int main() { |
- | int x, y; | + | |
- | while(x > 0) { | + | |
- | x = x + y; | + | |
- | y = y + z; | + | |
- | z = z - 1; | + | |
- | } | + | |
- | } | + | } |
</ | </ | ||
- | If we run SVMRanker on Example2.c with the default value of 2 for --depth_bound, | + | If we run SVMRanker on **Example2.c** with the default value of 2 for **--depth_bound**, we obtain |
- | python3 ./ | + | |
- | With the help of --depth_bound, | + | With the help of **--depth_bound**, SVMRanker produces the result shown below. |
< | < | ||
SVMRanker --- Version 1.0 | SVMRanker --- Version 1.0 | ||
Line 122: | Line 118: | ||
We now present the other options that let SVMRanker use different strategies in the process of learning a multiphase ranking function; different strategies regarding how program data points are sampled, how the state space is cut, and what templates are used, influence the running time of SVMRanker and possibly the final result. | We now present the other options that let SVMRanker use different strategies in the process of learning a multiphase ranking function; different strategies regarding how program data points are sampled, how the state space is cut, and what templates are used, influence the running time of SVMRanker and possibly the final result. | ||
- | | + | * - -sample_strategy This option controls the strategy SVMRanker uses to sample program data points. Possible values are CONSTRAINT and ENLARGE (the default): CONSTRAINT samples randomly the points satisfying the loop condition/ |
- | | + | * - -cutting_strategy This option controls the bound $b$ of the constraint f(x) < b that is used to cut the program state space in two parts for the current phase' |
- | | + | * - -template_strategy This option controls what templates are used in the learning procedure. Possible values are FULL and SINGLEFULL (the default): FULL uses as templates the linear combinations of all program variables; SINGLEFULL extends FULL with templates using only one variable at a time. |
- | | + | * - -print_level This option controls the verbosity of the SVMRanker output. |
- | The SVMRanker command lnested, short for learning nested ranking function, is used for learning a nested ranking function for a given program. The usage information of lnested can be obtained by the following command, with the output below. | + | The SVMRanker command |
- | python3 ./ | + | python3 ./ |
The output is the following. | The output is the following. | ||
< | < | ||
SVMRanker --- Version 1.0 | SVMRanker --- Version 1.0 | ||
- | Usage: CLIMain.py lnested [OPTIONS] SOURCE | + | Usage: CLIMain.py |
Options: | Options: | ||
- | | + | --depth_bound INTEGER |
- | --filetype [C|BOOGIE] | + | |
- | --file BOOGIE: input is boogie file. default set to BOOGIE | + | |
- | | + | --sample_strategy [ENLARGE|CONSTRAINT] |
- | --sample_strategy ENLARGE: enlarge the sample zone when sample num not enough. | + | |
- | --sample_strategy CONSTRAINT: find feasible points by constraint | + | |
- | | + | if sample num not enough default set to ENLARGE |
- | | + | |
- | --print_level [DEBUG|INFO|NONE] | + | |
- | --print_level DEBUG: print all the information of the learning and debugging | + | |
- | --print_level INFO: print the information of the learning | + | |
- | --print_level NONE: only print the result information of the learning | + | |
- | default set to NONE | + | |
- | + | | |
- | --help | + | |
+ | </ | ||
+ | As we can see, the options of ****lnested**** are also the ones of lmulti; also the use of **lnested** is similar to the one of **lmulti**, just the outcome can be different. | ||
+ | |||
+ | For instance, we can prove termination of ****Example2.c**** by means of a learned nested ranking function by running SVMRanker as follows. | ||
+ | python3 ./ | ||
+ | The output is shown below. | ||
+ | < | ||
+ | SVMRanker --- Version 1.0 | ||
+ | example/ | ||
+ | --------------------LEARNING NESTED SUMMARY------------------- | ||
+ | NESTED DEPTH: | ||
+ | LEARNING RESULT: | ||
+ | -----------RANKING FUNCTIONS---------- | ||
+ | 1.0 * z^1.0 + 0.9 * 1; 1.0 * y^1.0 + 0.9 * 1; 1.0 * x^1.0 + 0.7 * 1 | ||
</ | </ |