svmranker:usage
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
svmranker:usage [2020/11/17 22:25] – merlin | svmranker:usage [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1 | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | | ||
- | ====== Usage ====== | ||
- | In the following, we assume that current directory is SVMRanker. | ||
- | |||
- | After having installed the required software, SVMRanker can be used by entering the src/ directory and then calling SVMRanker as follows: | ||
- | python3 ./ | ||
- | You should be able to see the following output. | ||
- | SVMRanker --- Version 1.0 | ||
- | Usage: CLIMain.py [OPTIONS] COMMAND [ARGS]... | ||
- | " | ||
- | | ||
- | Options: | ||
- | --help | ||
- | | ||
- | Commands: | ||
- | lmulti | ||
- | 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. | ||
- | |||
- | 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 ./ | ||
- | | ||
- | The output is the following. | ||
- | |||
- | SVMRanker --- Version 1.0 | ||
- | Usage: CLIMain.py lmulti [OPTIONS] SOURCE | ||
- | |||
- | Options: | ||
- | | ||
- | < | ||
- | SVMRanker --- Version 1.0 | ||
- | Usage: CLIMain.py lmulti [OPTIONS] SOURCE | ||
- | |||
- | 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 | ||
- | | ||
- | |||
- | --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. \\ | ||
- | |||
- | <code java> | ||
- | int main() { | ||
- | int x, y; | ||
- | while(x > 0 || y > 0) { | ||
- | x = x + y - 1; | ||
- | y = y - 1; | ||
- | } | ||
- | } | ||
- | </ | ||
- | |||