Examples of UML class diagrams annotated with OCL invariants

Collection of 11 UML class diagrams annotated with OCL invariants. This collection is intended as a test suite for tools checking the satisfiability of the constraints in UML/OCL class diagrams. This model dataset has been curated and adapted from example libraries of modeling tools such as Visual Paradigm, Creately and Boardmix. The class diagrams are described using the USE (UML-based Specification Environment) textual format, which describes both the diagrams' elements and the textual OCL constraints. For each model, there is a second ".properties" file that is used buy USE's bounded model finder plug-in to check the finite satisfiability of the constraints in the model.