.js file is generated following the scheme given below. Roughly speaking, it consists of three steps:
- A new frontend (
main_js.ml) is added to the sources of Alt-Ergo. This file contains some glue code that allows the generated
.jsfile to interact with an HTML file (insertion of buttons, modification of DIV contents, …)
- The sources of Alt-Ergo and
main_js.mlare compiled with
ocamlc. The compilation make use of a preprocessor provided by
js_of_ocamlcompiler is used to transform the bytecode generated by
.js file is then plugged into an HTML file that fits with the glue code inserted in
General overview of the HTML interface
The HTML interface is made of four panels:
- The left panel is an editable textarea in which you can write/past/load the formula you want to prove.
- The bottom-left panel is used to display the answer of Alt-Ergo.
- The right panel is used to display different views. The default view (“Options”) allows to control the options of Alt-Ergo. When a formula is proved valid, one may switch to “Statistics” view, thanks to the corresponding button in the middle, to see what are the quantified axioms and predicates that are used/instantiated during the proof. The “Debug” view shows the information received by
main_js.mlfrom the HTML interface. The “Examples” view shows some basic examples in Alt-Ergo’s native input language that can be loaded in the left panel by a simple click.
A step-by-step example
Let us see how “Try Alt-Ergo” works on a formula translated from Atelier-B in the context of the BWare project:
- First, open Try Alt-Ergo in a new tab/window.
- Download the formula try-alt-ergo.why. This formula contains 177 quantified axioms and 132 predicates.
- Click on the “Load a Local File” button of Try alt-ergo’s interface and load the example into the left panel.
- Go to “Options” panel and set the
maximum number of stepsto 1000, the
maximum number of triggersto 1, and deactivate
- Click on “Ask Alt-Ergo” button and wait approximately 60 seconds (depending on your computer). On my laptop, Alt-Ergo given the following answer after, approximately, 40 seconds.
# Alt-Ergo's answer: Valid (37.2260 seconds) (222 steps)
- Now, you can navigate into the “Statistics” panel to see the quantified axioms and predicates that are instantiated during the proof, those that are potentially used, and those that have never been instantiated.
./alt-ergo.byte -nb-triggers 1 -no-Ematching -max-split infinity -save-used-context try-alt-ergo.why File "/home/mi/Bureau/po.why", line 3017, characters 1-2450:Valid (9.3105) (222) ./alt-ergo.opt -nb-triggers 1 -no-Ematching -max-split infinity -save-used-context try-alt-ergo.why File "/home/mi/Bureau/po.why", line 3017, characters 1-2450:Valid (0.8750) (222)
- Currently, the integration of external plugins (such as our miniSAT-based SAT solver) is not supported
- Compared to AltGr-Ergo, statistics and debug information are only shown at the end of the execution.
- “Asking Alt-Ergo” may report “syntax error” on well formed files for Safari and Midori users. The “Load a Local File” button is not working on Opera browser.
[ Acknowledgement: this work is financially supported by the BWare project. ]