Web application

Our mapping ocl2fol is available at:


User manual

From scratch:

1. Select the DTM-tab, and type-in an ActionGUI data model M in Δ.

2. Select the OCL to FOL-tab, and add as many OCL boolean expressions exp1,..., expn in Η as you want by (repeatedly) clicking on the Add-button and typing-in the desired expression expi.

Notice that you can always modify or remove OCL boolean expressions already typed-in by clicking on the buttons Remove and Modify.

3. Select an SMT solver (currently, either Z3 or Yices).

4. Generate the theory ocl2fol(M) U {ocl2fol_def(M, exp_1),...,ocl2fol_def(M, exp_n)} U {ocl2fol_th(Mexp_1),...,ocl2fol_th(Mexp_n)} with the syntax of the selected SMT solver.  

From a stored project

An OCL2FOL project consists of a data model M in Δ and a set of OCL boolean expressions exp1,..., expn in Η. 

To store the data model and OCL expressions that you have typed in the OCL2FOL web application as an OCL2FOL project, simply click on the button Store and download the generated XML file (by default, memento.xml) to your local disk.

To restore an OCL2FOL project, simply click on the button Restore and upload the project from your local disk.