Differences

This shows you the differences between two versions of the page.

--- svmranker:usage [2020/11/17 22:15] – merlin
+++ svmranker:usage [Unknown date] (current) – removed - external edit (Unknown date) 127.0.0.1
@@ Line 1: / Line 1: @@
- **[[svmranker:main| Main ]]** ||  **[[svmranker:main| Tool ]]** ||  **[[svmranker:usage| Usage & Case Study ]] **
-====== 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 ./CLIMain.py --help
-You should be able to see the following output.
-  SVMRanker --- Version 1.0
-  Usage: CLIMain.py [OPTIONS] COMMAND [ARGS]...
-    "python3 CLIMain.py COMMAND --help" for more details
-  Options:
-    --help  Show this message and exit.
-  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 ./CLIMain.py lmulti --help
-The output is the following.
-  SVMRanker --- Version 1.0
-Usage: CLIMain.py lmulti [OPTIONS] SOURCE
-Options:
- <code>
-SVMRanker --- Version 1.0
-Usage: CLIMain.py lmulti [OPTIONS] SOURCE
-Options:
-  --depth_bound INTEGER           depth bound default set to 2
-  --filetype [C|BOOGIE]           --file C: input is c file.
-                                  --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
-  --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                          Show this message and exit
-</code>