The FiniteSat Detection Method

FiniteSat detection method is a linear programming based method for detecting finite satisfiability problems in class diagrams with multiplicity constraints, class hierarchies and generalization set constraints. The algorithm transforms class diagram constraints into an inequality system and returns true if the inequality system is solvable (the class diagram is finitely satisfiable)  and false if otherwise.

The algorithm


Limitation: The FiniteSat algorithm is sound and complete if class hierarchy cycles (i.e. the undirected graph of the class hierarchy is cyclic) do not include disjoint or complete constraints. Otherwise, FiniteSat is sound but incomplete. For example, consider the following four class diagrams below. The class diagram in Figures a and b are non finitely satisfiable. However, the FiniteSat algorithm returns a positive answer for both. The class diagrams in Figures c1 and c2 are semantically equivalent however their inequality systems are not.

Warning Method: Due to the limitation of the FiniteSat algorithm, positive answers of FiniteSatUSE tool’s detection-method triggers an application that provides a warning if the class diagram includes class hierarchy cycles with disjoint or complete constraints (called problematic cycles) , and singles out all such cycles. The FiniteSatUSE tool suggests activating the propagation method if the class diagram includes problematic cycles followed by reactivation the detection method.