View Javadoc

1   /*
2    wsmo4j - a WSMO API and Reference Implementation
3    Copyright (c) 2005, University of Innsbruck, Austria
4    This library is free software; you can redistribute it and/or modify it under
5    the terms of the GNU Lesser General Public License as published by the Free
6    Software Foundation; either version 2.1 of the License, or (at your option)
7    any later version.
8    This library is distributed in the hope that it will be useful, but WITHOUT
9    ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
10   FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
11   details.
12   You should have received a copy of the GNU Lesser General Public License along
13   with this library; if not, write to the Free Software Foundation, Inc.,
14   59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
15   */
16  package org.deri.wsmo4j.validator;
17  
18  
19  import java.util.*;
20  
21  import org.deri.wsmo4j.io.serializer.wsml.*;
22  import org.deri.wsmo4j.logicalexpression.AttributeValueMoleculeImpl;
23  import org.deri.wsmo4j.logicalexpression.ConstantTransformer;
24  import org.omwg.logicalexpression.*;
25  import org.omwg.logicalexpression.Visitor;
26  import org.omwg.logicalexpression.terms.*;
27  import org.omwg.ontology.*;
28  import org.wsmo.common.*;
29  import org.wsmo.factory.*;
30  import org.wsmo.validator.ValidationError;
31  
32  
33  /**
34   * Checks logical expressions for wsml-dl validity.
35   *
36   * @author nathalie.steinmetz@deri.org
37   */
38  public class WsmlDLExpressionValidator
39          implements Visitor {
40  
41      private WsmlDLValidator validator = null;
42      
43      private LogExprSerializerWSML leSerializer = null;
44      
45      private LogicalExpressionFactory leFactory = null;
46      
47      private Axiom axiom = null;
48      
49      private List <ValidationError> errors = null;
50      
51      private boolean formula;
52      
53      private boolean validDescription;
54      
55      private boolean quantifier;
56      
57      private boolean universalRight;
58      
59      private boolean existential;
60      
61      private boolean bMol;
62      
63      private String error;
64      
65      private Set <Term> variables;
66      
67      private Set <List <Term>> molecules;
68      
69      private Variable root;
70      
71      private int numberOfMolecules;
72      
73      private boolean checkGraph;
74      
75      private boolean checkForRoot;
76      
77      private boolean graph;
78      
79      private boolean noRoot;
80      
81      
82      /**
83       * @param axiom whose logical expression is checked
84       * @param errors list that will be filled with error messages of found variant violations
85       */
86      protected WsmlDLExpressionValidator(Axiom axiom, LogicalExpressionFactory leFactory, List <ValidationError> errors, WsmlDLValidator validator) {
87          this.validator = validator;
88          leSerializer = validator.leSerializer;
89          this.leFactory = leFactory;
90          this.axiom = axiom;
91          this.errors = errors;
92          formula = false;
93          validDescription = false;
94          quantifier = false;
95          universalRight = false;
96          existential = false;
97          bMol = false;
98          graph = false;
99          checkGraph = false;
100         checkForRoot = false;
101         noRoot = false;
102         error = null;
103         variables = new HashSet <Term>();
104         molecules = new HashSet <List <Term>>();
105         root = null;
106         numberOfMolecules = 0;
107     }
108    
109     protected void setup() {
110         formula = false;
111         quantifier = false;
112         universalRight = false;
113         existential = false;
114         bMol = false;
115         variables = new HashSet <Term>();
116         root = null;
117         noRoot = false;
118         
119         setGraph(false);
120     }
121     
122     /**
123      * Checks if an Atom is valid to wsml-dl.
124      * 
125      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitAtom(org.omwg.logicalexpression.Atom)
126      */
127     public void visitAtom(Atom expr) {
128 //        System.out.println("\nAtom in now: " + expr.toString() + existential);
129         if (universalRight) {
130         	quantifier = true;
131             String error = ValidationError.AX_FORMULA_ERR + ":\n" +
132             "The UniversalQuantifier must only contain strong" +
133             " equation builtInAtoms on the right side of" +
134             " implication:\n" + leSerializer.serialize(expr);
135             if (!expr.getIdentifier().toString().equals(Constants.STRONG_EQUAL)) {
136                      addError(expr, error);
137                      validDescription = false;
138             }
139             universalRight = false;
140         }
141         else if (existential) {
142         	quantifier = true;
143             String error = ValidationError.AX_FORMULA_ERR + ":\n" +
144             "The ExistentialQuantifier must only contain strong" +
145             " equation builtInAtoms at negations:\n" +
146             leSerializer.serialize(expr);
147             if (!expr.getIdentifier().toString().equals(Constants.STRONG_EQUAL)) {
148                      addError(expr, error);
149                      validDescription = false;
150             }
151             existential = false;
152         }
153         if ((expr.getIdentifier().toString().equals(Constants.WSML_NAMESPACE + 
154         				Constants.TRUE)) ||
155         		(expr.getIdentifier().toString().equals(Constants.WSML_NAMESPACE + 
156         				Constants.FALSE))) {
157         	noRoot = true;
158         }
159         else if (expr instanceof BuiltInAtom && !quantifier) {
160         	String error = ValidationError.AX_ATOMIC_ERR + ":\n" +
161             "Built-in atoms are not allowed:\n" +
162             leSerializer.serialize(expr);
163         	addError(expr, error);
164         }
165         else if (!(expr.getIdentifier().toString().equals(Constants.NUMERIC_ADD)) && 
166         		!(expr.getIdentifier().toString().equals(Constants.NUMERIC_DIV)) && 
167         		!(expr.getIdentifier().toString().equals(Constants.NUMERIC_MUL)) && 
168         		!(expr.getIdentifier().toString().equals(Constants.NUMERIC_SUB))) {  
169             Molecule molecule = atomToMolecule(expr);
170             if (molecule != null) {
171                 molecule.accept(this);
172             }
173         }
174     }
175     
176     /**
177      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitAttributeContraintMolecule(org.omwg.logicalexpression.AttributeConstraintMolecule)
178      */
179     public void visitAttributeContraintMolecule(AttributeConstraintMolecule expr) {
180 //        System.out.println("\nAttributeConstraintMolecule in now: " + expr.toString());
181         error = "";
182         // check if the molecule is a valid b-molecule in a description
183         if (formula) {
184             isValidBMolecule(expr);
185         }
186         else {
187             // the identifier must be a Concept
188             if (check(expr.getLeftParameter(), false, true, true, true, true)) {
189                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
190                         + "\nThe range identifier must be a Concept, " +
191                         "not a " + error + "\n" + leSerializer.serialize(expr));
192             }
193             // the arguments must be datatypes
194             if (check(expr.getRightParameter(), true, true, true, false, true)) {
195                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
196                         + "\nThe arguments must be " +
197                         "Datatypes, not " + error + "\n"  + leSerializer.serialize(expr));
198             }
199             // the attribute's name must be a Relation with concrete range
200             if ((check(expr.getAttribute(), true, true, false, true, true))
201                     || (!checkConcreteRelations(expr.getAttribute()))){
202                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":" 
203                         + "\nThe name must be a Relation with concrete range, " +
204                         "not a " + error + "\n" + leSerializer.serialize(expr));
205             } 
206         }
207     }
208 
209     /**
210      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitAttributeInferenceMolecule(org.omwg.logicalexpression.AttributeInferenceMolecule)
211      */
212     public void visitAttributeInferenceMolecule(AttributeInferenceMolecule expr) {
213 //        System.out.println("\nAttributeInferenceMolecule in now: " + expr.toString());
214         error = "";
215         // check if the molecule is a valid b-molecule in a description
216         if (formula) {
217             isValidBMolecule(expr);
218         }
219         else {
220             // the identifier must be a Concept
221             if (check(expr.getLeftParameter(), false, true, true, true, true)) {
222                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
223                         + "\nThe range identifier must be a Concept, " +
224                         "not a " + error + "\n" + leSerializer.serialize(expr));
225             }
226             // the arguments of an infering attribute must be datatypes or concepts
227             if (check(expr.getRightParameter(), false, true, true, false, true)) {
228                 addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe arguments " +
229                         "must be Datatypes or Concepts, " +
230                         "not " + error + "\n" + leSerializer.serialize(expr));
231             }    
232             else { 
233                 // if the argument is a datatype, the attribute's name must be a relation with concrete range
234                 if (checkDatatypes(expr.getRightParameter())) {
235                     if (!checkConcreteRelations(expr.getAttribute())) {
236                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
237                                 "must be a relation with concrete range " +
238                                 "(because the argument is a datatype)\n" + leSerializer.serialize(expr));   
239                     }
240                 }
241                 // if the argument is a concept, the attribute's name must be a relation with abstract range
242                 else if (checkConcepts(expr.getRightParameter())) {
243                     if (!checkAbstractRelations(expr.getAttribute())) {
244                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
245                                 "must be a relation with abstract range " +
246                                 "(because the argument is a concept)\n" + leSerializer.serialize(expr));   
247                     }
248                 }
249             }
250         }
251     }
252 
253     /**
254      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitAttributeValueMolecule(org.omwg.logicalexpression.AttributeValueMolecule)
255      */
256     public void visitAttributeValueMolecule(AttributeValueMolecule expr) {
257 //        System.out.println("\nAttributeValueMolecule in now: " + expr.toString());
258         error = "";
259         // check if the molecule is a valid b-molecule in a description
260         if (formula) {
261             isValidBMolecule(expr);
262         }
263         else {
264             // the identifier must be an Instance
265             if (check(expr.getLeftParameter(), true, false, true, true, true)) {
266                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":" 
267                         + "\nThe range identifier must be an Instance, " +
268                         "not a " + error + "\n" + leSerializer.serialize(expr));
269             }
270             // the arguments of a value definition attribute must be DataValues or Instances
271             if (check(expr.getRightParameter(), true, false, true, false, true)) {
272                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":\nThe arguments " +
273                         "must be DataValues or Instances, " +
274                         "not " + error + "\n" + leSerializer.serialize(expr));
275             }
276             else {
277                 // if the argument is a DataValue, the attribute's name must be a relation with concrete range
278                 if (checkDatatypes(expr.getRightParameter())) {
279                     if (!checkConcreteRelations(expr.getAttribute())) {
280                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
281                                 "must be a relation with concrete range " +
282                                 "(because the argument is a DataValue)\n" + leSerializer.serialize(expr));   
283                     }
284                 }
285                 // if the argument is an instance, the attribute's name must be a relation with abstract range
286                 else if (checkInstances(expr.getRightParameter())) {
287                     if (!checkAbstractRelations(expr.getAttribute())) {
288                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
289                                 "must be a relation with abstract range " +
290                                 "(because the argument is an instance)\n" + leSerializer.serialize(expr));   
291                     }
292                 }
293             }
294         }
295     }
296 
297     /**
298      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitCompoundMolecule(org.omwg.logicalexpression.CompoundMolecule)
299      */
300     public void visitCompoundMolecule(CompoundMolecule expr) {
301 //        System.out.println("\nCompoundMolecule in now: " + expr.toString());
302         Iterator i = expr.listOperands().iterator();
303         while(i.hasNext()){
304             ((Molecule)i.next()).accept(this);
305         }
306     }
307 
308     /**
309      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitMemberShipMolecule(org.omwg.logicalexpression.MembershipMolecule)
310      */
311     public void visitMemberShipMolecule(MembershipMolecule expr) {
312 //        System.out.println("\nMembershipMolecule in now: " + expr.toString());
313         error = "";
314         // checks if the molecule is a valid a-molecule in a description
315         if (formula) {
316             if (universalRight) {
317                 addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
318                         "The UniversalQuantifier may not contain a " +
319                         "MembershipMolecule on the right side of" +
320                         " implication:\n" + leSerializer.serialize(expr));
321                 validDescription = false;
322                 universalRight = false;
323             }
324             else {
325                 // the identifier must be a Variable
326                 if (!(expr.getLeftParameter() instanceof Variable)) {    
327                     addError(expr, ValidationError.AX_FORMULA_ERR + ":" 
328                             + "\nThe identifier of an a-molecule must be a Variable\n"
329                             + leSerializer.serialize(expr));
330                     validDescription = false;
331                 }
332                 // the argument must be a Concept
333                 if (check(expr.getRightParameter(), true, false, false, false, false)) {
334                     addError(expr, ValidationError.AX_FORMULA_ERR + ":" 
335                             + "\nThe argument of an a-molecule must be a Concept\n"
336                             + leSerializer.serialize(expr));
337                     validDescription = false;
338                 }
339                 if (graph && (!variables.contains(expr.getLeftParameter()))) {
340 //                	checkGraph = true;
341                     variables.add(expr.getLeftParameter());
342                 }
343             }
344         }
345         else {
346             // the identifier must be an Instance
347             if (check(expr.getLeftParameter(), true, false, true, true, true)) {
348                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":" 
349                         + "\nThe identifier must be an Instance, " +
350                         "not a " + error + "\n" + leSerializer.serialize(expr));
351             }
352             // the arguments must be Concepts
353             if (check(expr.getRightParameter(), false, true, true, true, true)) {
354                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
355                         + "\nThe arguments must be Concepts, " +
356                         "not " + error + "\n" + leSerializer.serialize(expr));
357             }
358         }
359     }
360 
361     /**
362      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitSubConceptMolecule(org.omwg.logicalexpression.SubConceptMolecule)
363      */
364     public void visitSubConceptMolecule(SubConceptMolecule expr) {
365 //        System.out.println("\nSubConceptMolecule in now: " + expr.toString());
366         if (universalRight) {
367             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
368                     "The UniversalQuantifier may not contain a " +
369                     "SubConceptMolecule on the right side of" +
370                     " implication:\n" + leSerializer.serialize(expr));
371             validDescription = false;
372             universalRight = false;
373         }
374         else if (existential) {
375             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
376                     "The ExistentialQuantifier may not contain a " +
377                     "SubConceptMolecule:\n" + leSerializer.serialize(expr));
378             validDescription = false;
379             existential = false;
380         }
381         else {
382             error = "";
383             // the identifier must be a Concept
384             if (check(expr.getLeftParameter(), false, true, true, true, true)) {
385                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
386                         + "\nThe identifier must be a Concept, " +
387                         "not a " + error + "\n" + leSerializer.serialize(expr));
388             }
389             // the arguments must be Concepts
390             if (check(expr.getRightParameter(), false, true, true, true, true)) {
391                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
392                         + "\nThe arguments must be Concepts, " +
393                         "not " + error + "\n" + leSerializer.serialize(expr));
394             }
395         }
396     }
397 
398     /**
399      * Checks if a Negation is valid to wsml-dl.
400      * 
401      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitNegation(org.omwg.logicalexpression.Negation)
402      */
403     public void visitNegation(Negation expr) {
404 //        System.out.println("\nNegation in now: " + expr.toString());
405         // if the method is called from a formula
406         if (formula) {
407             if (universalRight || existential) {
408                 if (!(expr.getOperand() instanceof BuiltInAtom)) {
409                     addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
410                             "The negation in a quantifier must contain a Built-In" +
411                             " Atom:\n" + leSerializer.serialize(expr));
412                     validDescription = false;
413                     existential = false;
414                     universalRight = false;
415                     return;
416                 }
417             }
418             expr.getOperand().accept(this);
419         }   
420         else {
421             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
422                  "Negation is not allowed:\n" + leSerializer.serialize(expr));
423         }
424     }
425 
426     /**
427      * Checks if a NegationAsFailure is valid to wsml-dl.
428      * 
429      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitNegationAsFailure(org.omwg.logicalexpression.NegationAsFailure)
430      */
431     public void visitNegationAsFailure(NegationAsFailure expr) {
432 //        System.out.println("\nNegationAsFailure in now: " + expr.toString() + universalRight);
433         if (universalRight) {
434             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
435                     "The UniversalQuantifier may not contain a " +
436                     "NegationAsFailure on the right side of" +
437                     " implication:\n" + leSerializer.serialize(expr));
438             validDescription = false;
439             universalRight = false;
440         }
441         else if (existential) {
442             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
443                     "The ExistentialQuantifier may not contain a " +
444                     "NegationAsFailure:\n" + leSerializer.serialize(expr));
445             validDescription = false;
446             existential = false;
447         }
448         else if (existential) {
449             expr.accept(this);
450         }
451         else {
452             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
453                     "NegationAsFailure is not allowed:\n" + leSerializer.serialize(expr));
454         }
455     }
456 
457     /**
458      * Checks if a Constraint is valid to wsml-dl.
459      * 
460      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitConstraint(org.omwg.logicalexpression.Constraint)
461      */
462     public void visitConstraint(Constraint expr) {
463 //        System.out.println("\nConstraint in now: " + expr.toString());
464         if (universalRight) {
465             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
466                     "The UniversalQuantifier may not contain a " +
467                     "Constraint on the right side of" +
468                     " implication:\n" + leSerializer.serialize(expr));
469             validDescription = false;
470             universalRight = false;
471         }
472         else if (existential) {
473             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
474                     "The ExistentialQuantifier may not contain a " +
475                     "Constraint:\n" + leSerializer.serialize(expr));
476             validDescription = false;
477             existential = false;
478         }
479         else {
480             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
481                         "Constraint is not allowed:\n" + leSerializer.serialize(expr));
482         }
483     }
484 
485     /**
486      * Checks if a Conjunction is valid to wsml-dl.
487      * 
488      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitConjunction(org.omwg.logicalexpression.Conjunction)
489      */
490     public void visitConjunction(Conjunction expr) {
491 //        System.out.println("existential: " + existential);
492 //        System.out.println("\nConjunction in now: " + expr.toString());
493 //        System.out.println("Left: " + expr.getLeftOperand().toString());
494 //        System.out.println("Right: " + expr.getRightOperand().toString());
495         // if the method is called from a formula
496         if (formula) {
497             if (universalRight) {
498                 addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
499                         "The UniversalQuantifier may not contain a " +
500                         "Conjunction on the right side of" +
501                         " implication:\n" + leSerializer.serialize(expr));
502                 validDescription = false;
503                 universalRight = false;
504             }
505             else {
506                 if (existential && (((!(expr.getLeftOperand() instanceof Negation)) 
507                         && (!(expr.getLeftOperand() instanceof Conjunction))
508                         && (!(expr.getLeftOperand() instanceof AttributeMolecule))
509                         && (!(expr.getLeftOperand() instanceof MembershipMolecule))) 
510                         || ((!(expr.getRightOperand() instanceof Negation)) 
511                         && (!(expr.getRightOperand() instanceof Conjunction))
512                         && (!(expr.getRightOperand() instanceof AttributeMolecule))
513                         && (!(expr.getRightOperand() instanceof MembershipMolecule))))){
514                     addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
515                             "The Conjunction in an ExistentialQuantifier must contain " +
516                             "a Negation or another Conjunction:\n" + leSerializer.serialize(expr));
517                     validDescription = false;
518                     existential = false;
519                     return;
520                 }
521                 else {
522                     expr.getLeftOperand().accept(this);
523                     expr.getRightOperand().accept(this);
524                 }
525             }
526         }
527         else {
528             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
529                     "Conjunction is not allowed:\n" + leSerializer.serialize(expr));
530         }  
531     }
532 
533     /**
534      * Checks if a Disjunction is valid to wsml-dl.
535      * 
536      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitDisjunction(org.omwg.logicalexpression.Disjunction)
537      */
538     public void visitDisjunction(Disjunction expr) {
539 //        System.out.println("\n Disjunction in now: " + expr.toString() + universalRight);
540         // if the method is called from a formula
541         if (formula) {
542             if (universalRight) {
543                 if (((!(expr.getLeftOperand() instanceof Negation)) 
544                         && (!(expr.getLeftOperand() instanceof Disjunction))) 
545                         || ((!(expr.getRightOperand() instanceof Negation)) 
546                         && (!(expr.getRightOperand() instanceof Disjunction)))){
547                     addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
548                             "The Disjunction in a UniversalQuantifier must contain " +
549                             "a Negation or another Disjunction:\n" + leSerializer.serialize(expr));
550                     validDescription = false;
551                     universalRight = false;
552                     return;
553                 }
554             }
555             expr.getLeftOperand().accept(this);
556             expr.getRightOperand().accept(this);
557         }
558         else {
559             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
560                     "Disjunction is not allowed:\n" + leSerializer.serialize(expr));
561         }  
562     }
563 
564     /**
565      * Checks if an InverseImplication is valid to wsml-dl.
566      * 
567      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitInverseImplication(org.omwg.logicalexpression.InverseImplication)
568      */
569     public void visitInverseImplication(InverseImplication expr) {
570 //        System.out.println("\nInverseImplication in now: " + expr.toString());
571         if (universalRight) {
572             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
573                     "The UniversalQuantifier may not contain a " +
574                     "InverseImplication on the right side of" +
575                     " implication:\n" + leSerializer.serialize(expr));
576             validDescription = false;
577             universalRight = false;
578         }
579         else if (existential) {
580             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
581                     "The ExistentialQuantifier may not contain a " +
582                     "InverseImplication:\n" + leSerializer.serialize(expr));
583             validDescription = false;
584             existential = false;
585         }
586         else {
587         	if (formula == true) {
588         		addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
589                         "Nested Implications are not allowed:\n" + 
590                         leSerializer.serialize(expr));
591                 validDescription = false;
592         	}
593         	else {
594 	            formula = true;
595 	            validDescription = true;
596 	            
597 	            expr.getLeftOperand().accept(this);
598 	            expr.getRightOperand().accept(this);
599         	}
600         	
601         	LogicalExpression left = expr.getLeftOperand();    
602             LogicalExpression right = expr.getRightOperand();      	
603             left.accept(this);    
604             right.accept(this);
605             if (!validDescription) {
606                 addError(expr, ValidationError.AX_IMPL_BY_ERR + ":\n" 
607                         + leSerializer.serialize(expr));
608                 return;
609             }
610             
611             // check on transitive attribute structure
612             if (((left instanceof Atom) || (left instanceof AttributeValueMolecule)) && 
613                     (right instanceof Conjunction)) {
614                 LogicalExpression leftConjunction = ((Conjunction) right).getLeftOperand();
615                 LogicalExpression rightConjunction = ((Conjunction) right).getRightOperand();
616                 if (((leftConjunction instanceof Atom) 
617                         || (leftConjunction instanceof AttributeValueMolecule)) 
618                         && ((rightConjunction instanceof Atom) 
619                         || (rightConjunction instanceof AttributeValueMolecule))) {
620                     if (isValidTransitiveInvImpl(expr)) {
621                     	validDescription = false;
622                     }
623                     return;
624                 }
625             }
626             
627             // check on symmetric, sub-attribute and inverse attribute structure
628             if (((left instanceof Atom) || (left instanceof AttributeValueMolecule)) && 
629                     ((right instanceof Atom) || (right instanceof AttributeValueMolecule))) {
630                 if (isValidInverseImplication(expr)) {
631                 	validDescription = false;
632                 }
633                 return;
634             }
635             
636             if (validDescription) {
637 //                existential = false;
638             	
639             	checkForRoot = true;
640             	new Graph(expr, this);
641             	checkForRoot = false;
642         
643             	new Graph(expr.getLeftOperand(), this);
644             	new Graph(expr.getRightOperand(), this);
645 
646             }
647         }
648     }
649 
650     /**
651      * Checks if an Implication is valid to wsml-dl.
652      * 
653      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitImplication(org.omwg.logicalexpression.Implication)
654      */
655     public void visitImplication(Implication expr) {
656 //        System.out.println("\nImplication in now: " + expr.toString());
657         if (universalRight) {
658             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
659                     "The UniversalQuantifier may not contain a " +
660                     "Implication on the right side of" +
661                     " implication:\n" + leSerializer.serialize(expr));
662             validDescription = false;
663             universalRight = false;
664         }
665         else if (existential) {
666             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
667                     "The ExistentialQuantifier may not contain a " +
668                     "Implication:\n" + leSerializer.serialize(expr));
669             validDescription = false;
670             existential = false;
671         }
672         else {
673         	if (formula == true) {
674         		addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
675                         "Nested Implications are not allowed:\n" + 
676                         leSerializer.serialize(expr));
677                 validDescription = false;
678         	}
679         	else {
680         		formula = true;
681 	            validDescription = true;
682 	
683 	            expr.getLeftOperand().accept(this);
684 	            expr.getRightOperand().accept(this);
685         	}
686         	
687             if (!validDescription) {
688                 addError(expr, ValidationError.AX_IMP_ERR + ":\n" +
689                         leSerializer.serialize(expr));
690             }
691             else {
692 //                existential = false;
693             	
694             	checkForRoot = true;
695             	new Graph(expr, this);
696             	checkForRoot = false;
697         
698             	new Graph(expr.getLeftOperand(), this);
699             	new Graph(expr.getRightOperand(), this);
700             }
701         }
702     }
703 
704     /**
705      * Checks if an Equivalence is valid to wsml-dl.
706      * 
707      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitEquivalence(org.omwg.logicalexpression.Equivalence)
708      */
709     public void visitEquivalence(Equivalence expr) {
710 //        System.out.println("\nEquivalence in now: " + expr.toString());
711         if (universalRight) {
712             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
713                     "The UniversalQuantifier may not contain a " +
714                     "Equivalence on the right side of" +
715                     " implication:\n" + leSerializer.serialize(expr));
716             validDescription = false;
717             universalRight = false;
718         }
719         else if (existential) {
720             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
721                     "The ExistentialQuantifier may not contain a " +
722                     "Equivalence:\n" + leSerializer.serialize(expr));
723             validDescription = false;
724             existential = false;
725         }
726         else {
727         	if (formula == true) {
728         		addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
729                         "Nested Implications are not allowed:\n" + 
730                         leSerializer.serialize(expr));
731                 validDescription = false;
732                 existential = false;
733         	}
734         	else {
735 	            formula = true;
736 	            validDescription = true;
737 	            expr.getLeftOperand().accept(this);
738 	            expr.getRightOperand().accept(this); 
739         	}
740         	
741             if (!validDescription) {
742                 addError(expr, ValidationError.AX_EQUIV_ERR + ":\n" +
743                         "Invalid Equivalence Formula:\n" +
744                         leSerializer.serialize(expr));
745             }
746             else {
747 //                existential = false;
748 
749             	checkForRoot = true;
750             	new Graph(expr, this);
751             	checkForRoot = false;
752             	
753             	new Graph(expr.getLeftOperand(), this);
754             	new Graph(expr.getRightOperand(), this);
755             }
756         }
757     }
758 
759     /**
760      * Checks if a LogicProgrammingRule is valid to wsml-dl.
761      * 
762      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitLogicProgrammingRule(org.omwg.logicalexpression.LogicProgrammingRule)
763      */
764     public void visitLogicProgrammingRule(LogicProgrammingRule expr) {
765 //        System.out.println("\nLogicProgrammingRule in now: " + expr.toString());
766         if (universalRight) {
767             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
768                     "The UniversalQuantifier may not contain a " +
769                     "LogicProgrammingRule on the right side of" +
770                     " implication:\n" + leSerializer.serialize(expr));
771             validDescription = false;
772             universalRight = false;
773         }
774         else if (existential) {
775             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
776                     "The ExistentialQuantifier may not contain a " +
777                     "LogicProgrammingRule:\n" + leSerializer.serialize(expr));
778             validDescription = false;
779             existential = false;
780         }
781         else {
782             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
783                         "LogicProgrammingRule is not allowed:\n" + leSerializer.serialize(expr));
784         }
785     }
786 
787     /**
788      * Checks if a UniversalQuantification is valid to wsml-dl.
789      * 
790      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitUniversalQuantification(org.omwg.logicalexpression.UniversalQuantification)
791      */
792     public void visitUniversalQuantification(UniversalQuantification expr) {
793 //        System.out.println("\nUniversalQuantification in now: " + expr.toString());
794         if (universalRight) {
795             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
796                     "The UniversalQuantifier may not contain a " +
797                     "UniversalQuantification on the right side of" +
798                     " implication:\n" + leSerializer.serialize(expr));
799             validDescription = false;
800             universalRight = false;
801         }
802         else {
803             // if the method is called from a formula
804             if (formula) {
805                 Vector operands = (Vector) expr.listOperands();
806                 if ((operands.size() == 1) && (operands.get(0) instanceof Implication)) {
807                     Implication imp = (Implication) operands.get(0);
808                     if (expr.listVariables().size() == 1) {
809                         isValidBMolecule(imp.getLeftOperand());
810                         imp.getRightOperand().accept(this);    
811                     }
812                     else {
813                         if ((imp.getLeftOperand() instanceof Conjunction) 
814                                 || (imp.getLeftOperand() instanceof Negation)
815                                 || (imp.getLeftOperand() instanceof AttributeMolecule)
816                                 || (imp.getLeftOperand() instanceof MembershipMolecule)) {
817                             imp.getLeftOperand().accept(this);  
818                         }
819                         else {
820                             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
821                                     "The UniversalQuantifier must have a Molecule " +
822                                     "or a Conjunction on the left side of implication:\n" +
823                                     leSerializer.serialize(expr));
824                             validDescription = false;
825                             return;
826                         }
827                         if ((imp.getRightOperand() instanceof Disjunction)
828                                 || (imp.getRightOperand() instanceof Negation)
829                                 || (imp.getRightOperand() instanceof BuiltInAtom)) {
830                             universalRight = true;
831                             imp.getRightOperand().accept(this);    
832                         }
833                         else {
834                             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
835                                     "The UniversalQuantifier must have a Negation, a Strong Equality " +
836                                     "BuiltInAtom or a Disjunction on the right side of implication:\n" +
837                                     leSerializer.serialize(expr));
838                             validDescription = false;
839                             return;
840                         }
841                     }
842                 }
843                 else {
844                     addError (expr, ValidationError.AX_FORMULA_ERR + ":\n" +
845                             "UniversalQuantification is only allowed with an " +
846                             "implication as operand:\n" + leSerializer.serialize(expr));
847                     validDescription = false;
848                 }
849                 if (graph) {
850                     checkGraph = true;
851                     Set <Variable> vs = expr.listVariables();
852                     Iterator it = vs.iterator();
853                     while (it.hasNext()) {
854                         Variable v = (Variable) it.next();
855                         if (!variables.contains(v)) {
856                             variables.add(v);
857                         }  
858                     }
859                 }
860             }
861             else {
862                 addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
863                         "UniversalQuantification is not allowed:\n" + leSerializer.serialize(expr));
864                 validDescription = false;
865             }
866         }
867     }
868     
869     /**
870      * Checks if an ExistentialQuantification is valid to wsml-dl.
871      * 
872      * @see org.deri.wsmo4j.validator.WsmlFullExpressionValidator#visitExistentialQuantification(org.omwg.logicalexpression.ExistentialQuantification)
873      */
874     public void visitExistentialQuantification(ExistentialQuantification expr) {
875 //        System.out.println("\nExistentialQuantification in now: " + expr.toString());
876         if (universalRight) {
877             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
878                     "The UniversalQuantifier may not contain a " +
879                     "ExistentialQuantification on the right side of" +
880                     " implication:\n" + leSerializer.serialize(expr));
881             validDescription = false;
882             universalRight = false;
883         }
884         else {
885             //  if the method is called from a formula
886             if (formula) {
887                 Vector operands = (Vector) expr.listOperands();
888                 int size = operands.size();
889                 for (int i=0; i<size; i++) {
890                     if (!(operands.get(i) instanceof Conjunction) && 
891                     		!(operands.get(i) instanceof AttributeValueMoleculeImpl)) {
892                         addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
893                                 "ExistentialQuantifier is only allowed with " +
894                                 "conjunctions as operands:\n" + leSerializer.serialize(expr));
895                         validDescription = false;
896                         return;
897                     }
898                 }
899                 if (expr.listVariables().size() == 1) {
900 //                    isValidBMolecule(((Conjunction) operands.get(0)).getLeftOperand());
901                 	bMol = false;
902                 	if (operands.get(0) instanceof Conjunction) {
903                 		((Conjunction) operands.get(0)).getLeftOperand().accept(this);
904                 	}
905                 	else {
906                 		((LogicalExpression) operands.get(0)).accept(this);
907                 	}
908                     if (!graph && !bMol) {
909                     	addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
910                                 "ExistentialQuantifier is only allowed with " +
911                                 "an AttributeValueMolecule as left operand of a conjunction:\n" + 
912                                 leSerializer.serialize(expr));
913                     }
914                     if (operands.get(0) instanceof Conjunction) {
915                     	((Conjunction) operands.get(0)).getRightOperand().accept(this);
916                     }
917                 }  
918                 else {
919                     existential = true;
920                     for (int i=0; i<size; i++) {
921                         ((Conjunction) operands.get(i)).getLeftOperand().accept(this);
922                         ((Conjunction) operands.get(i)).getRightOperand().accept(this);
923                     }
924                 }
925                 if (graph) {
926                     checkGraph = true;
927                     Set <Variable> vs = expr.listVariables();
928                     Iterator it = vs.iterator();
929                     while (it.hasNext()) {
930                         Variable v = (Variable) it.next();
931                         if (!variables.contains(v)) {
932                             variables.add(v);
933                         }  
934                     }
935                 }
936             }
937             else {
938                 addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
939                         "ExistentialQuantifier is not allowed:\n" + leSerializer.serialize(expr));
940                 validDescription = false;
941             }  
942         }
943     }
944     
945     /*
946      * Gets an atom and transforms it into a value definition molecule
947      */
948     private Molecule atomToMolecule(Atom expr) {
949         Molecule molecule = null;
950         // the atom must be a binary atom
951         if (expr.getArity() != 2) {
952             addError(expr, ValidationError.AX_ATOMIC_ERR + ":\nThe atom must " +
953                     "be a binary atom\n" + leSerializer.serialize(expr));
954             return molecule;
955         }
956         else {
957             molecule = leFactory.createAttributeValue(
958                     expr.getParameter(0), expr.getIdentifier(), expr.getParameter(1));
959             return molecule;
960         }
961     }
962     
963     /*
964      * Checks if a specified molecule is a valid b-molecule
965      */
966     private void isValidBMolecule(LogicalExpression le) {
967         if (universalRight) {
968             addError(le, ValidationError.AX_FORMULA_ERR + ":\n" +
969                     "The UniversalQuantifier may not contain a " +
970                     "Molecule on the right side of" +
971                     " implication:\n" + leSerializer.serialize(le));
972             validDescription = false;
973             universalRight = false;
974         }
975         else {
976             AttributeValueMolecule expr = null;
977             if (le instanceof Atom) {
978                 le = atomToMolecule((Atom) le);
979                 if (le == null) {
980                     validDescription = false;
981                 }
982             }
983             if (le instanceof AttributeValueMolecule) {
984                 expr = (AttributeValueMolecule) le;
985                 
986                 // the argument of the attribute value molecule must be a Variable
987                 if (!(expr.getLeftParameter() instanceof Variable)) {    
988                     addError(expr, ValidationError.AX_FORMULA_ERR + ":" 
989                             + "\nThe argument must be a Variable\n"
990                             + leSerializer.serialize(expr));
991                     validDescription = false;
992                 } 
993                 // the name of the attribute must be a relation
994                 if (check(expr.getAttribute(), true, true, false, true, true)) {
995                     addError(expr, ValidationError.AX_FORMULA_ERR + ": The " +
996                             "attribute name must be a relation\n" + leSerializer.serialize(expr));
997                     validDescription = false;  
998                 }
999                 // the arguments of the attribute must be variables
1000                 if (!(expr.getRightParameter() instanceof Variable)) {
1001                     addError(expr, ValidationError.AX_FORMULA_ERR + ": The " +
1002                             "attribute's arguments must be variables\n" + leSerializer.serialize(expr));
1003                     validDescription = false;                
1004                 }
1005                 // put the variables and molecules into Sets to be able to check if the expression is a valid graph
1006                 if (graph) {
1007                     checkGraph = true;
1008                     if (!variables.contains(expr.getLeftParameter())) {
1009                         variables.add(expr.getLeftParameter());
1010                     }
1011                     if (!variables.contains(expr.getRightParameter())) {
1012                         variables.add(expr.getRightParameter());
1013                     }
1014                     List <Term> list = new Vector <Term> ();
1015                     list.add(expr.getLeftParameter());
1016                     if (!expr.getLeftParameter().equals(expr.getRightParameter())) {
1017                         list.add(expr.getRightParameter());
1018                     }
1019                     Iterator it = molecules.iterator();
1020                     while (it.hasNext()) {
1021                         List l = (List) it.next();
1022                         if ((l.get(0).equals(expr.getLeftParameter())) && 
1023                                 (l.get(1).equals(expr.getRightParameter()))) {
1024                             return;
1025                         }
1026                     }
1027                     numberOfMolecules = numberOfMolecules + 1;
1028                     molecules.add(list);
1029                 }
1030                 bMol = true;
1031             }
1032             else {
1033                 addError(le, ValidationError.AX_FORMULA_ERR + ": This b-molecule" +
1034                         " must be an atom or an AttributeValueMolecule" +
1035                         leSerializer.serialize(le));
1036                 validDescription = false;
1037             }
1038         }
1039     }
1040     
1041     /*
1042      * Checks if a specified InverseImplication, containing a molecule and a 
1043      * conjunction as operands, is a valid transitive construction
1044      */
1045     private boolean isValidTransitiveInvImpl(InverseImplication expr) {
1046         AttributeValueMolecule left, conjunctionLeft, conjunctionRight;
1047         
1048         // Atoms can be used interchangeably with attribute value molecules
1049         if (expr.getLeftOperand() instanceof Atom) {
1050             left = (AttributeValueMolecule) atomToMolecule((Atom) expr.getLeftOperand());
1051         }
1052         else {
1053             left = (AttributeValueMolecule) expr.getLeftOperand();
1054         }
1055         if (((Conjunction) expr.getRightOperand()).getLeftOperand() instanceof Atom) {
1056             conjunctionLeft = (AttributeValueMolecule) atomToMolecule((Atom) 
1057                     ((Conjunction) expr.getRightOperand()).getLeftOperand());
1058         }
1059         else {
1060             conjunctionLeft = (AttributeValueMolecule) (
1061                     (Conjunction) expr.getRightOperand()).getLeftOperand();
1062         }
1063         if (((Conjunction) expr.getRightOperand()).getRightOperand() instanceof Atom) {
1064             conjunctionRight = (AttributeValueMolecule) atomToMolecule((Atom) 
1065                     ((Conjunction) expr.getRightOperand()).getRightOperand());
1066         }
1067         else {
1068             conjunctionRight = (AttributeValueMolecule) ((Conjunction) expr.getRightOperand()).getRightOperand();
1069         } 
1070               
1071         Variable leftVariable = (Variable) left.getLeftParameter();
1072         Variable conjunctionLeftVariable = (Variable) conjunctionLeft.getLeftParameter();
1073         Variable conjunctionRightVariable = (Variable) conjunctionRight.getLeftParameter();
1074         Term leftRelation = left.getAttribute();
1075         Term conjunctionLeftRelation = conjunctionLeft.getAttribute();
1076         Term conjunctionRightRelation = conjunctionRight.getAttribute();     
1077         Variable leftArgument = (Variable) left.getRightParameter();
1078         Variable conjunctionLeftArgument = (Variable) conjunctionLeft.getRightParameter();
1079         Variable conjunctionRightArgument = (Variable) conjunctionRight.getRightParameter();
1080         
1081         // check on globally transitive attribute/relation
1082         if (leftVariable.equals(conjunctionLeftVariable) 
1083                 && leftVariable.equals(conjunctionRightVariable)) {
1084             return false;
1085         }
1086         else if (!(leftRelation.equals(conjunctionLeftRelation)) 
1087                 || !(leftRelation.equals(conjunctionRightRelation))) {
1088         	return false;
1089         }
1090         else if (leftVariable.equals(conjunctionLeftVariable)) {
1091             if (!(leftArgument.equals(conjunctionRightArgument)) 
1092                     || !(conjunctionLeftArgument.equals(conjunctionRightVariable))) {
1093             	return false;
1094             }
1095         }
1096         else if (leftVariable.equals(conjunctionRightVariable)) {
1097             if (!(leftArgument.equals(conjunctionLeftArgument)) 
1098                     || !(conjunctionRightArgument.equals(conjunctionLeftVariable))) {
1099             	return false;
1100             }
1101         }
1102         return true;
1103     }
1104     
1105     /*
1106      * Checks if an Inverse Implication, containing two molecules as Operands, 
1107      * is a valid construction. Valid constructions are symmetric, sub-attribute 
1108      * and inverse attribute structures
1109      */
1110     private boolean isValidInverseImplication(InverseImplication expr) {
1111         AttributeValueMolecule left = null;
1112         AttributeValueMolecule right = null;
1113         
1114         // Atoms can be used interchangeably with attribute value molecules
1115         if (expr.getLeftOperand() instanceof Atom) {
1116             left = (AttributeValueMolecule) atomToMolecule((Atom) expr.getLeftOperand());
1117         }
1118         else {
1119             left = (AttributeValueMolecule) expr.getLeftOperand();
1120         }
1121         if (expr.getRightOperand() instanceof Atom) {
1122             right = (AttributeValueMolecule) atomToMolecule((Atom) expr.getRightOperand());
1123         }
1124         else {
1125             right = (AttributeValueMolecule) expr.getRightOperand();
1126         }
1127         if (left == null || right == null) {
1128             return false;
1129         }
1130         else {
1131             Variable leftVariable = (Variable) left.getLeftParameter();
1132             Variable rightVariable = (Variable) right.getLeftParameter();
1133             Term leftRelation = left.getAttribute();
1134             Term rightRelation = right.getAttribute();       
1135             Variable leftArgument = (Variable) left.getRightParameter();
1136             Variable rightArgument = (Variable) right.getRightParameter();
1137             
1138             // check on globally symmetric and inverse attribute/relation
1139             if (!(leftVariable.equals(rightArgument)) || !(leftArgument.equals(rightVariable))) {
1140                 
1141                 // check on globally sub-attribute/relation
1142                 if (!(leftVariable.equals(rightVariable)) || !(leftArgument.equals(rightArgument)) 
1143                         || leftRelation.equals(rightRelation)) {
1144                     return false;
1145                 }
1146             }
1147             return true;
1148         }
1149     }
1150     
1151     /*
1152      * Check if a specified Molecule's parameter or a term is used in the actual 
1153      * axiom as Instance, Relation or Datatype, or whether it is a Variable
1154      */
1155     private boolean check(Object o, boolean concept, boolean instance, 
1156             boolean relation, boolean datatype, boolean variable) {
1157         if (o instanceof Molecule) {
1158             if (concept && checkConcepts(((Molecule) o).getLeftParameter())) {
1159                 error = "Concept";
1160                 return true;
1161             }
1162             if (instance && checkInstances(((Molecule) o).getLeftParameter())) {
1163                 error = "Instance";
1164                 return true;
1165             }
1166             else if (relation && checkRelations(((Molecule) o).getLeftParameter())) {
1167                 error = "Relation";
1168                 return true;
1169             }
1170             else if (datatype && checkDatatypes(((Molecule) o).getLeftParameter())) {
1171                 error = "Datatype";
1172                 return true;
1173             }
1174             else if (variable && (((Molecule) o).getLeftParameter() instanceof Variable)) {
1175                 error = "Variable";
1176                 return true;
1177             }
1178         }
1179         else if (o instanceof Term) {
1180             if (concept && checkConcepts(o)) {
1181                 error = "Concept";
1182             }
1183             if (instance && checkInstances(o)) {
1184                 error = "Instance";
1185                 return true;
1186             }
1187             else if (relation && checkRelations(o)) {
1188                 error = "Relation";
1189                 return true;
1190             }
1191             else if (datatype && checkDatatypes(o)) {
1192                 error = "Datatype";
1193                 return true;
1194             }
1195             else if (variable && (o instanceof Variable)) {
1196                 error = "Variable";
1197                 return true;
1198             }
1199         }
1200         return false;
1201     }
1202     
1203     /*
1204      * Checks if a specified Term is contained in the concepts vector
1205      */
1206     private boolean checkConcepts(Object o) {
1207         return validator.getIdConcepts().contains(o);
1208     }
1209     
1210     /*
1211      * Checks if a specified Term is contained in the instances vector
1212      */
1213     private boolean checkInstances(Object o) {
1214         return validator.getIdInstances().contains(o);
1215     }
1216     
1217     /*
1218      * Checks if a specified Term is contained in the relations vector
1219      */
1220     private boolean checkRelations(Object o) {
1221         return validator.getIdRelations().contains(o);
1222     }
1223     
1224     /*
1225      * Checks if a specified Term is contained in the abstract relations vector
1226      */
1227     private boolean checkAbstractRelations(Object o) {
1228         return validator.getIdAbstractRelations().contains(o);
1229     }
1230     
1231     /*
1232      * Checks if a specified Term is contained in the concrete relations vector
1233      */
1234     private boolean checkConcreteRelations(Object o) {
1235         return validator.getIdConcreteRelations().contains(o);
1236     }
1237     
1238     /*
1239      * Checks if a specified Term is contained in the datatypes vector
1240      */
1241     private boolean checkDatatypes(Object o) {
1242         return ConstantTransformer.getInstance().isDataType(o.toString());
1243     }
1244     
1245     public Set getMolecules() {
1246         return molecules;
1247     }
1248 
1249     public int getNumberOfMolecules() {
1250         return numberOfMolecules;
1251     }
1252 
1253     public Set getVariables() {
1254         return variables;
1255     }
1256     
1257     public Variable getRoot() {
1258     	return root;
1259     }
1260     
1261     protected void setGraph(boolean graph) {
1262         this.graph = graph;
1263         checkGraph = false;
1264         variables = new HashSet <Term> ();
1265         molecules = new HashSet <List <Term>> ();
1266         numberOfMolecules = 0;
1267     }
1268 
1269     /*
1270      * Adds a new ValidationError to the error list
1271      */
1272     private void addError(LogicalExpression logexp, String msg) {
1273         LogicalExpressionErrorImpl le = new LogicalExpressionErrorImpl(
1274                 axiom, logexp, msg, WSML.WSML_DL);
1275         if (!errors.contains(le)) {
1276             errors.add(le);
1277         }
1278     }
1279    
1280     protected class Graph {
1281       
1282         private WsmlDLExpressionValidator exprVal;
1283         private Map <Variable, List <Term>> listMap = new HashMap <Variable, List <Term>> ();
1284         private List <Variable> connected = new Vector <Variable> ();
1285         private LogicalExpression expr;
1286         private Set <Term> leftVariables = new HashSet <Term> ();
1287         private Set <Term> rightVariables = new HashSet <Term> ();
1288         
1289         public Graph(LogicalExpression expr, WsmlDLExpressionValidator exprVal) {
1290             this.expr = expr;
1291             this.exprVal = exprVal;
1292             if (checkForRoot) {
1293             	root = null;
1294             	leftVariables.clear();
1295             	rightVariables.clear();
1296             	exprVal.setGraph(true);
1297             	hasRootVariable();
1298             }
1299             else if (!quantifier){ 	
1300             	exprVal.setGraph(true);
1301             	isValidGraph();
1302             }
1303         }
1304         
1305         /*
1306          * Checks if the left and right parts of a given logical expression 
1307          * contain a root variable.
1308          */
1309         public boolean hasRootVariable() {
1310         	((Binary) expr).getLeftOperand().accept(exprVal);
1311         	Iterator <Term> it = variables.iterator();
1312         	while (it.hasNext()) {
1313         		leftVariables.add(it.next());
1314         	}
1315         	variables.clear();       	
1316         	((Binary) expr).getRightOperand().accept(exprVal);
1317         	it = variables.iterator();
1318         	while (it.hasNext()) {
1319         		rightVariables.add(it.next());
1320         	}       	
1321         	variables.clear();
1322         	Iterator leftIt = leftVariables.iterator();
1323         	while (leftIt.hasNext()) {
1324         		Variable v = (Variable) leftIt.next();
1325         		if (rightVariables.contains(v)) {
1326         			root = v;
1327         		}
1328         	} 
1329         	if (root == null && !noRoot) {
1330         		addError(expr, ValidationError.AX_GRAPH_ERR + ":\nLeft and " +
1331         				"right part of expression do not have a common root " +
1332                         "variable:\n" + leSerializer.serialize(expr));
1333                 return false;
1334         	}
1335         	return true;
1336         }
1337         
1338         /*
1339          * Checks if the variables and molecules of a given logical expression
1340          * build a valid connected and acyclic graph.
1341          */
1342         protected boolean isValidGraph() {  
1343             listMap.clear();
1344             connected.clear();
1345 
1346             // fill the sets with the variables and the molecules
1347             expr.accept(exprVal);
1348             if ((!variables.isEmpty()) && checkGraph) {
1349                 buildLists();
1350             
1351                 Iterator it = variables.iterator();
1352                 Variable v1 = (Variable) it.next();
1353                 Variable v = null;
1354                 boolean valid = false;
1355                 
1356                 // check if the given graph is connected
1357                 while(it.hasNext()) {
1358                     v = (Variable) it.next();  
1359                     connected.clear();
1360                     valid = checkGraphConnected(v1, v);
1361                     if (!valid) {
1362                         addError(expr, ValidationError.AX_GRAPH_ERR + ":\nGraph is " +
1363                                 "not connected:\n" + leSerializer.serialize(expr));
1364                         return false;
1365                     }
1366                 }
1367                 
1368                 // check if the given graph is acyclic  
1369                 List <Variable> checkList = new Vector <Variable> ();
1370                 checkList.add(v1);
1371                 valid = checkGraphAcyclic(v1, v1, checkList);
1372                 if (valid) {
1373                     return true;
1374                 }
1375                 else {
1376                     addError(expr, ValidationError.AX_GRAPH_ERR + ":\nGraph contains " +
1377                             "cycle:\n" + leSerializer.serialize(expr));
1378                     return false;
1379                 }
1380             }
1381             return true;
1382         }
1383         
1384         /*
1385          * Build a Map with a specific variable as key and with a list as value, 
1386          * that contains all variables to which the key variable is connected.
1387          */
1388         private void buildLists() {
1389             Variable v1 = null;
1390             Variable v = null;
1391             
1392             Iterator <Term> it = variables.iterator();
1393             while (it.hasNext()) {
1394                 List <Term> list = new Vector <Term> ();
1395                 v1 = (Variable) it.next();
1396                 Iterator <List <Term>> itMol = molecules.iterator();
1397                 while (itMol.hasNext()) {
1398                     List <Term> l = itMol.next();
1399                     if (l.get(0).equals(v1)) {
1400                         v = (Variable) l.get(1);
1401                         list.add(v);
1402                     } 
1403                     else if (l.get(1).equals(v1)) {
1404                         v = (Variable) l.get(0);
1405                         list.add(v);
1406                     }  
1407                 }
1408                 listMap.put(v1, list);
1409             }
1410         }
1411         
1412         /*
1413          * Checks if variable v1 is connected to variable v2.
1414          */
1415         private boolean checkGraphConnected(Variable v1, Variable v2) {
1416             boolean found = false;
1417             boolean used = false;
1418             
1419             List <Term> l = listMap.get(v1);
1420             
1421             if (l.contains(v2)) {
1422                 return true;
1423             }
1424             else {
1425                 connected.add(v1);
1426                 
1427                 Iterator it = l.iterator();
1428                 while (it.hasNext()) {
1429                     Variable v = (Variable) it.next(); 
1430                     for (int i=0; i<connected.size(); i++) {
1431                         if (v.equals(connected.get(i))) {
1432                             used = true;
1433                         }
1434                     }
1435                     if (!used) {
1436                         found = checkGraphConnected(v, v2);
1437                     }
1438                     if (found) {
1439                         return true;
1440                     }
1441                     used = false;
1442                 }
1443                 return false;
1444             }
1445         }
1446            
1447         /*
1448          * Checks if a given graph contains a cycle. 
1449          */
1450         private boolean checkGraphAcyclic(Variable from, Variable v, List checkList) {
1451             if ((numberOfMolecules + 1) == variables.size()) {
1452                 return true;
1453             }
1454             else {
1455                 return false;
1456             }
1457         }
1458     }
1459 }