QMaxUSE v1.0.2

QMaxUSE v1.0.2 [14-Mar-2022]

• Changes:
  • Enable verification on abstract classes
  • Add additional axioms for abstract classes selection
  • Add cvc5 support for macOS release

QMaxUSE v1.0.1

v1.0.1 release

Changes:

• Fix bugs of non-empty axioms for non-abstract classes.
• Remove auto-generated smt2 files.
• Add upward and downward modifiers.
• Add cvc5 for ubuntu-release (experimental).
• Enable switch between z3 and cvc5.

New Features:

• Use upward / downward modifier to select all parent/child classes of a specified class.
• Use command set-solver: <solver name> to switch between z3 and cvc5. This applies to a single query and concurrent verification.

QMaxUSE v1.0.0

v1.0.0 release

Changes:

• Fix bugs with implicit selection from an OCL invariant.
• Add solvers for Windows, Ubuntu and MacOS.
• Perform a test run before launching a query or concurrent verification.
• Adjust colorful outputs (For windows color codes, see the following section).

Features:

• A query language (details here)
• A concurrent verification engine (details here)

Notes:

Enabling Windows ANSI Colors

If you are running QMaxUSE in Windows command line. You need to enable ANSI color mode for Windows 10 to avoid seeing color codes in QMaxUSE

• Set the following key to be 1.

   [HKEY_CURRENT_USER\Console]
   VirtualTerminalLevel=dword:00000001
  

  This will enable ANSI colors in Windows terminal. Here is a link about the details.

Microsoft Visual C++ Packages

You may need to install Microsoft Visual C++ Redistributable packages on your windows machines