# UCLAONT: Ontology-Based UML Class Models Verification Tool updates
## 3 Running Example
### Ontology-Based Finite Satisfiability  
There are two techniques for verifying satisfiability of static model: (1) linear inequalities; and (2) detection graph. In the first technique, a class model is transformed into linear inequalities, and the satisfiability problem is solved by finding the solution of inequalities. In the second technique, a class model is converted into a directed graph, and satisfiability is checked through the detection of the critical cycle. Ontology is also based on graph-theoretic structure and has concepts like vertices and edges of the graph. In this work ontology-based technique is used for finding critical cycles in the ontology graph of the class model. Figure 2 shows how an ontology graph of Figure 1 (Monopoly Game class model) will be built.  
Figure 1: Running Example of Monopoly Game.  
In graph-based representation, many cycles are not important for checking the class model's satisfiability, such as balance or greater. In the balance cycle, the same quantities are involved for the division and multiplication for calculating cycle weight. Therefore, quantity 1 is always produced. In the greater cycle, a smaller quantity for the division and a larger quantity is involved for multiplication. Therefore, a quantity greater than 1 is always produced. Both balance and greater cycles are not crucial for determining satisfiability. Therefore, they should not be part of the search. Furthermore, one critical cycle is enough for proving the unsatisfiability of the class model. As per the above investigation, this work proposes an ontology-based technique that minimizes the search space for finding a critical cycle in the ontology graph of the ontology-based representation of the UML class model. In this proposed tool, the object property is used for traversing the graph. In the proposed method, an arbitrary object is selected for traversing and step forward to the next object property until and unless the next selected object property range becomes equal to the domain of the first selected object property where the traversing was started. Further details can be found in [27].  
UML classes connect to each other with different relationships; one of them is the dependency relationship. The dependency relationships specify the object of class effects on the object of another class such as in initiate dependency when an object of a class is created, it also creates an object of another class. The dependency relationships are not only used in the class diagram they can also be used in package diagrams, component diagrams, and so forth. The dependency relationships which impact the correctness of the class model only those are considered in this work such as create/Initiate, drive, call and use. In the proposed solution, the dependency relationship is transformed into object property and some additional restrictions are also applied on them such as use and calls are annotated as transitive, and drive and create/initiate are annotated as transitive and asymmetric. Sometimes a class model can become incorrect due to some concealed aspects of the dependency such as a class model presented in Figure 3. According to the model, Class A initiates the object of Class B, when the Class B object is initiated, it initiates the object of Class C. Furthermore, Class C has a generalization relationship with Class D, and the Class C object will also be considered a Class D object due to inheritance. ultimately, there will be a cycle of objects initialization that will never end and the model will not be finitely satisfiable.  
Figure 2: Ontology Graph of Monopoly Game Class Model.