qmaxuse

QMaxUSE: A query-based verification tool for verifying UML class diagrams with extreme size of OCL invariants.


Project maintained by classicwuhao Hosted on GitHub Pages — Theme by mattgraham

Build Your Own QMaxUSE

If you would like to build your own version of QMaxUSE, please see the instructions provided in the following Sections.

1. MSVC Libraries

If you are using Windows, you may need to install Microsoft Visual C++ Redistributable packages on your windows machines.

1.1 Enabling ANSI Colors for Windows (older version: 1511 to 1903)

You need to enable ANSI color mode for Windows 10 to avoid seeing color codes in QMaxUSE

2. Build QMaxUSE

Currently, you can build QMaxUSE on operating systems: Windows 10 (x64), Ubuntu 20.04 (x64) and mac OS Big Sur(x64). In order to build QMaxUSE, you must have Ant installed on your local machine. QMaxUSE uses an Z3 SMT Solver as its solving engine. The following sections introduce instructions for building QMaxUSE with Z3 SMT solver.

2.1 Using pre-built Z3 libraries.

We provide a set of pre-built Z3 libraries under solver directory for Windows (Win10 x64), Linux (Ubuntu 20.04 x64) and Mac OS (Big Sur x64). Everytime when you run QMaxUSE, it will perform a trial run before solving any set of OCL invariants. You could easily update pre-built Z3 libraries with the latest build on your own machine by just simply overwritting library files under solver directory.

2.2 Building Z3 on your own machine.

You can build Z3 on your own machine based on the instructions provided here.

2.2.1 Windows Build