QMaxUSE: A query-based verification tool for verifying UML class diagrams with extreme size of OCL invariants.
If you would like to build your own version of QMaxUSE, please see the instructions provided in the following Sections.
If you are using Windows, you may need to install Microsoft Visual C++ Redistributable packages on your windows machines.
You need to enable ANSI color mode for Windows 10 to avoid seeing color codes in QMaxUSE
[HKEY_CURRENT_USER\Console]
VirtualTerminalLevel=dword:00000001
This will enable ANSI colors in Windows terminal. Here is a link about the details.
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.
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.
You can build Z3 on your own machine based on the instructions provided here.