JBernstein Files

JBernstein (Version 0.3.7)

http://sourceforge.net/projects/jbernstein/


===== Description =====

JBernstein is a tool implemented in Java that enables to check whether a polynomial constraint holds 
for all variables within its domain. It is mainly used in the verification or synthesis of cyber-physical 
systems where the system model is nonlinear.

===== Execution =====

Unzip the file. Visit the folder where JBernstein.jar is located. 
Then type java -jar JBernstein.jar to execute the program (the /lib folder is required).

    * In Windows, users may also double click JBernstein.jar to execute the program.

    * In Linux or Mac OS, users can right click the file, and select "open with JRE as runtime". 
        Might need to set the property so that the file is allowed to be executed as a program.

===== Instructions  =====

    * Load existing examples 
        1. Simply select the combo box to load, and press the "Analyze" button. Most examples in the PVS testsuite are available for selection from the GUI. 
        2. Alternatively, load some other examples from the menu bar using "File -> Load constraint". 
	3. When you load an example, be sure to select appropriate engines, as there are two available options: 
		"simple": handle one polynomial constraint; the sign and the compared value should be selected from the GUI.
		"full": handle generalized constraints in assume-guarantee style

    * Work on your own examples
        1. Lines starting with ## are comments
        2. Specify the number of variables with keyword VAR
        3. Specify the coefficient with keyword COEF
        4. Specify the bound for each variable (the tool assumes that, e.g., given VAR equals 5, variables are named as x0, x1, x2, x3, x4) with keyword BOUND
        5. The value "Recursive expansion depth" specifies the maximum box refinement attempts for each variable to prove/disprove the constraint. 
            (a) For a problem with <5 variables, it's safe to use value > 10 
            (b) For a problem with more variables, all benchmarks can be answered without using values greater than 5. 
            (c) In pre-load examples, these values are set to let users understand how many refinement steps are required. 
            (d) Users may always set the value to 10 or higher. 
	6. For examples in assume-guarantee style, please refer to samples in folder "example/assume-guarantee"
    * Enable error-estimate due to imprecision of double (since 0.2); experimental feature
        1. The solver can check the property by considering the imprecision of double, thereby guaranteeing the correctness of the generated result.
        2. To ativate this feature, on the menu bar, select "Help -> Setting -> Automatic Error Estimation"
    * Enable precise derivation for counter-examples
        1. The solver is able to give instructions how a counter-example is generated. Without using this feature, 
           the solver may print out a counter-example that is represented in double and contain error.
        2. To ativate this feature, on the menu bar, select "Help -> Setting -> Print precise counter-example" 

===== Limitations =====

1. For assume-guarantee properties, recursive deepening (current implementation) is not superior than iterative deepening. 
   This happens when trying to find a counter-example.

===== License and Contact =====

License: LGPL 3.0
Contact: cheng(dot)chihhong(at)gmail(dot)com or visit http://sourceforge.net/projects/jbernstein/