The current folder contains examples to run invariant verification for
non-linear hybrid automata.

The curent status of this analysis is quite experimental and is not
integrated with the all the model checking algorihtms.
The only commands that support non-linear arithmetic is
hycomp_check_invar_nonlinear.

hycomp currently DOES NOT integrate a SMT solver for non-linear real
arithmetic (NRA) (mathsat does not support NRA).
At the current stage, the tool offers two possible scenarios:
1. Call an SMT solver via pipe
2. dump the VMT format file

1. Call via PIPE a SMT solver that supports the NRA theory.
hycomp can actually call z3 and hysat.

Note that, in this case, the tool will call mathsat on a linear
relaxation of the problem before calling the non-linear solver.
If mathsat returns UNSAT, then the result is correct.

1.1. Call z3 (you need  the perl interpreter as pre requisite)
  - set the path to z3 in the variable Z3PATH inside the script z3fixer.pl
    E.g. my $Z3PATH="/usr/bin/z3";
  - make the z3fixer.pl script executable
    $> chmod +x z3fixer.pl
  - change the path to the z3fixer.pl setting the environment
    variable Z3_PATH in the command file nonlinear_bmc.cmd.
    E.g. set Z3_PATH "./z3fixer.pl"
  - change the path that will be used to write the smt2 file in the
    environment variable Z3_FILE_NAME_PATH in the commmand file
    nonlinear_bmc.cmd
    e.g. set Z3_FILE_NAME_PATH "/tmp/z3.app"

  - Run hycomp
    ../../hycomp -pre cpp -source nonlinear_bmc.cmd ball_count_1d_plain.hydi

1.2. Call hysat (in this case counterexamples are not constructed in hycomp)
A copy of the executable for isat can be obtained from http://isat.gforge.avacs.org/

  - set the path to the hysat executable in the nonlinear_bmc.cmd file
    Example
    set HY_SAT_PATH "~/hysat/isat_1.0r1322_64bit_static" 
  - change the path that will be used to write the hysat file in the
    environment variable HY_SAT_FILE_NAME_PATH in the commmand file
    nonlinear_bmc.cmd
    Example:
    set HY_SAT_FILE_NAME_PATH "/tmp/tmp.hys"
  - set the hysat parameters (always in the nonlinear_bmc.cmd) to be
    used in every check (refer to the hysat manual for their description)
    Example

    # Heuristic ("" means random)
    set HY_SAT_HEU ""
    # minimal splitting width. HySAT will not split an interval if 
    # the difference is less than this value
    # It is called Minimal splitting width
    set HY_SAT_MSW "0.1"
    # absolute progress. HySAT will not make a decision on a lower/upper
    # bound if the difference with the new lower/upper bound is less than
    # this value
    # it is called 
    set HY_SAT_PRABS "0.01"
    # deduction are not done if the relative progress is below PRREL parameter
    set HY_SAT_PRREL "0"
    set HY_SAT_RESTART "1"
    set HY_SAT_IDV "2"
    set HY_SAT_CH_SAT_OFTEN "0"
    set HY_SAT_PSPL "0"
    set HY_SAT_PURIFICATION "0"
    set HY_SAT_PDPOS "100"

  - change the type of smt solver in the command file nonlinear_bmc.cmd:
    E.g.
    hycomp_check_invar_nonlinear -n 0 -s hysat

  - Run hycomp
    ../../hycomp -pre cpp -source nonlinear_bmc.cmd ball_count_1d_plain.hydi

2. Dump the VMT (verification modulo theory) problem corresponding to
discrete transition system encoding of the invariant verification
problem.

See the example in the dumpvmt folder.

REFERENCE

Alessandro Cimatti, Sergio Mover, Stefano Tonetta: A quantifier-free SMT encoding of non-linear hybrid automata. FMCAD 2012: 187-195
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: Quantier-free encoding of invariants for Hybrid Systems, FMSD (DOI 10.1007/s10703-013-0202-8)
