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:

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
  

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.

<file java>

int main() {
  	int x, y;
  	while(x > 0 || y > 0) {
  		x = x + y - 1;
  		y = y - 1;
  	}
}

</file>