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  import java.util.HashMap;
19  import java.util.HashSet;
20  import java.util.Iterator;
21  import java.util.List;
22  import java.util.Map;
23  import java.util.Set;
24  import java.util.Vector;
25  
26  import org.deri.wsmo4j.io.serializer.wsml.LogExprSerializerWSML;
27  import org.deri.wsmo4j.logicalexpression.ConstantTransformer;
28  import org.omwg.logicalexpression.Atom;
29  import org.omwg.logicalexpression.AtomicExpression;
30  import org.omwg.logicalexpression.AttributeConstraintMolecule;
31  import org.omwg.logicalexpression.AttributeInferenceMolecule;
32  import org.omwg.logicalexpression.AttributeValueMolecule;
33  import org.omwg.logicalexpression.Binary;
34  import org.omwg.logicalexpression.CompoundMolecule;
35  import org.omwg.logicalexpression.Conjunction;
36  import org.omwg.logicalexpression.Constraint;
37  import org.omwg.logicalexpression.Disjunction;
38  import org.omwg.logicalexpression.Equivalence;
39  import org.omwg.logicalexpression.ExistentialQuantification;
40  import org.omwg.logicalexpression.Implication;
41  import org.omwg.logicalexpression.InverseImplication;
42  import org.omwg.logicalexpression.LogicProgrammingRule;
43  import org.omwg.logicalexpression.LogicalExpression;
44  import org.omwg.logicalexpression.MembershipMolecule;
45  import org.omwg.logicalexpression.Molecule;
46  import org.omwg.logicalexpression.Negation;
47  import org.omwg.logicalexpression.NegationAsFailure;
48  import org.omwg.logicalexpression.SubConceptMolecule;
49  import org.omwg.logicalexpression.UniversalQuantification;
50  import org.omwg.logicalexpression.Visitor;
51  import org.omwg.logicalexpression.terms.Term;
52  import org.omwg.ontology.Axiom;
53  import org.omwg.ontology.Variable;
54  import org.wsmo.common.WSML;
55  import org.wsmo.factory.LogicalExpressionFactory;
56  import org.wsmo.validator.ValidationError;
57  
58  
59  /**
60   * Checks logical expressions for wsml-core validity.
61   *
62   * <pre>
63   *  Created on Aug 19, 2005
64   *  Committed by $Author: morcen $
65   *  $Source$,
66   * </pre>
67   *
68   * @author nathalie.steinmetz@deri.org
69   * @version $Revision: 1946 $ $Date: 2007-04-02 15:13:28 +0300 (Mon, 02 Apr 2007) $
70   */
71  public class WsmlCoreExpressionValidator 
72          implements Visitor{
73  
74      private Set <Term> equivVariables = null;
75      
76      private Set <Term> lhsVariables = null;
77      
78      private Set <Term> rhsVariables = null;
79      
80      private int numberOfMolecules = 0;
81      
82      private Set <List <Term>> molecules = null;
83      
84      private WsmlCoreValidator validator = null;
85      
86      private LogExprSerializerWSML leSerializer = null;
87      
88      private LogicalExpressionFactory leFactory = null;
89      
90      private Axiom axiom = null;
91      
92      private List <ValidationError> errors = null;
93      
94      private String error;
95      
96      private boolean formula;
97      
98      private boolean rhs;
99      
100     private boolean lhs;
101     
102     private boolean errorFlag;
103     
104     
105     /**
106      * @param axiom whose logical expression is checked
107      * @param errors list that will be filled with error messages of found variant violations
108      */
109     protected WsmlCoreExpressionValidator(Axiom axiom, LogicalExpressionFactory leFactory, List <ValidationError> errors, WsmlCoreValidator val) {
110         this.axiom = axiom;
111         this.errors = errors;
112         this.validator = val;
113         leSerializer = validator.leSerializer;
114         this.leFactory = leFactory;
115     }
116 
117     protected void setup() {
118         lhsVariables = new HashSet <Term> ();
119         numberOfMolecules = 0;
120         molecules = new HashSet <List <Term>> ();
121         equivVariables = new HashSet <Term> ();
122         lhsVariables = new HashSet <Term> ();
123         rhsVariables = new HashSet <Term> ();
124         formula = false;
125         rhs = false;
126         lhs = false;
127         errorFlag = true;
128     }
129     
130     /**
131      * Checks if an atom is valid to wsml-core.
132      * 
133      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitAtom(org.omwg.logicalexpression.Atom)
134      */
135     public void visitAtom(Atom expr) {
136         Molecule molecule = atomToMolecule(expr);
137         if (molecule != null) {
138             molecule.accept(this);
139         }
140     }
141 
142     /**
143      * Checks if an AttributeConstraintMolecule is valid to wsml-core.
144      * 
145      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitAttributeContraintMolecule(org.omwg.logicalexpression.AttributeConstraintMolecule)
146      */
147     public void visitAttributeContraintMolecule(AttributeConstraintMolecule expr) {
148         String error = ":\n Cannot contain an AttributeConstraintMolecule:\n" 
149             + leSerializer.serialize(expr);
150         // An AttributeConstraintMolecule is no valid right-hand side formula
151         if (rhs) {      
152             if (errorFlag) {
153                 addError(expr, ValidationError.AX_RHS_ERR + error); 
154             }
155         }
156         else if (lhs) {
157             if (errorFlag) {
158                 addError(expr, ValidationError.AX_LHS_ERR + error);
159             }
160         }
161         else {
162             // the identifier must be a Concept
163             if (check(expr.getLeftParameter(), false, true, true, true, true)) {
164                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
165                         + "\nThe range identifier must be a Concept, " +
166                         "not a " + error + "\n" + leSerializer.serialize(expr));
167             }
168             // the arguments must be datatypes
169             if (check(expr.getRightParameter(), true, true, true, false, true)) {
170                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
171                         + "\nThe arguments must be " +
172                         "Datatypes, not " + error + "\n"  + leSerializer.serialize(expr));
173             }
174             // the attribute's name must be a Relation with concrete range
175             if ((check(expr.getAttribute(), true, true, false, true, true))
176                     || (!checkConcreteRelations(expr.getAttribute()))){
177                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":" 
178                         + "\nThe name must be a Relation with concrete range, " +
179                         "not a " + error + "\n" + leSerializer.serialize(expr));
180             } 
181         }
182     }
183 
184     /**
185      * Checks if an AttributeInferenceMolecule is valid to wsml-core.
186      * 
187      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitAttributeInferenceMolecule(org.omwg.logicalexpression.AttributeInferenceMolecule)
188      */
189     public void visitAttributeInferenceMolecule(AttributeInferenceMolecule expr) {
190         String error = ":\n Cannot contain an AttributeInferenceMolecule:\n" 
191             + leSerializer.serialize(expr);
192         // An AttributeInferenceMolecule is no valid right-hand side formula
193         if (rhs) {      
194             if (errorFlag) {
195                 addError(expr, ValidationError.AX_RHS_ERR + error);
196             }
197         }
198         else if (lhs) {
199             if (errorFlag) {
200                 addError(expr, ValidationError.AX_LHS_ERR + error);
201             }
202         }
203         else {
204             // the identifier must be a Concept
205             if (check(expr.getLeftParameter(), false, true, true, true, true)) {
206                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
207                         + "\nThe range identifier must be a Concept, " +
208                         "not a " + error + "\n" + leSerializer.serialize(expr));
209             }
210             // the arguments of an infering attribute must be datatypes or concepts
211             if (check(expr.getRightParameter(), false, true, true, false, true)) {
212                 addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe arguments " +
213                         "must be Datatypes or Concepts, " +
214                         "not " + error + "\n" + leSerializer.serialize(expr));
215             }    
216             else { 
217                 // if the argument is a datatype, the attribute's name must be a relation with concrete range
218                 if (checkDatatypes(expr.getRightParameter())) {
219                     if (!checkConcreteRelations(expr.getAttribute())) {
220                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
221                                 "must be a relation with concrete range " +
222                                 "(because the argument is a datatype)\n" + leSerializer.serialize(expr));   
223                     }
224                 }
225                 // if the argument is a concept, the attribute's name must be a relation with abstract range
226                 else if (checkConcepts(expr.getRightParameter())) {
227                     if (!checkAbstractRelations(expr.getAttribute())) {
228                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
229                                 "must be a relation with abstract range " +
230                                 "(because the argument is a concept)\n" + leSerializer.serialize(expr));   
231                     }
232                 }
233             }
234         }
235     }
236 
237     /**
238      * Checks if an AttributeValueMolecule is valid to wsml-core.
239      * 
240      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitAttributeValueMolecule(org.omwg.logicalexpression.AttributeValueMolecule)
241      */
242     public void visitAttributeValueMolecule(AttributeValueMolecule expr) {
243         // An AttributeValueMolecule is no valid right-hand side formula
244         if (rhs) {      
245             if (errorFlag) {
246                 addError(expr, ValidationError.AX_RHS_ERR + ":\n Cannot " +
247                         "contain an AttributeValueMolecule:\n" 
248                         + leSerializer.serialize(expr));
249             }
250         }
251         // check if an AttributeValueMolecule is a valid b-molecule
252         if (lhs || formula) {
253             // the identifier of the molecule must be a variable
254             if (!(expr.getLeftParameter() instanceof Variable)) {
255                 if (errorFlag) {
256                     addError(expr, ValidationError.AX_FORMULA_ERR + ": A valid b-molecule " +
257                             "must contain a variable as identifier\n" + leSerializer.serialize(expr));
258                 }
259                 return;
260             }
261             else if (!lhsVariables.contains(expr.getLeftParameter())) {
262                 lhsVariables.add(expr.getLeftParameter());
263             }
264             
265             // the name of the attribute must be a relation
266             if (!checkAbstractRelations(expr.getAttribute())) {
267                 if (errorFlag) {
268                     addError(expr, ValidationError.AX_FORMULA_ERR + ": A valid b-molecule's " +
269                             "attribute name must be a relation with abstract range\n" 
270                             + leSerializer.serialize(expr));
271                 }
272                 return;
273             }
274           
275             // the arguments of the attribute must be variables
276             if (!(expr.getRightParameter() instanceof Variable)) {
277                 if (errorFlag) {
278                     addError(expr, ValidationError.AX_FORMULA_ERR + ": A valid b-molecule's " +
279                             "attribute's arguments must be variables\n" + leSerializer.serialize(expr));
280                 }
281                 return;
282             }
283             else if (!lhsVariables.contains(expr.getRightParameter())) {
284                 lhsVariables.add(expr.getRightParameter());
285             }
286                   
287             List <Term> l = new Vector <Term> ();
288             l.add(expr.getLeftParameter());
289             if (!expr.getLeftParameter().equals(expr.getRightParameter())) {
290                 l.add(expr.getRightParameter());
291             }
292             numberOfMolecules = numberOfMolecules + 1;
293             molecules.add(l);
294         }
295         else {
296             // the identifier must be an Instance
297             if (check(expr.getLeftParameter(), true, false, true, true, true)) {
298                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":" 
299                         + "\nThe range identifier must be an Instance, " +
300                         "not a " + error + "\n" + leSerializer.serialize(expr));
301             }
302             // the arguments of a value definition attribute must be DataValues or Instances
303             if (check(expr.getRightParameter(), true, false, true, false, true)) {
304                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":\nThe arguments " +
305                         "must be DataValues or Instances, " +
306                         "not " + error + "\n" + leSerializer.serialize(expr));
307             }
308             else {
309                 // if the argument is a DataValue, the attribute's name must be a relation with concrete range
310                 if (checkDatatypes(expr.getRightParameter())) {
311                     if (!checkConcreteRelations(expr.getAttribute())) {
312                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
313                                 "must be a relation with concrete range " +
314                                 "(because the argument is a DataValue)\n" + leSerializer.serialize(expr));   
315                     }
316                 }
317                 // if the argument is an instance, the attribute's name must be a relation with abstract range
318                 else if (checkInstances(expr.getRightParameter())) {
319                     if (!checkAbstractRelations(expr.getAttribute())) {
320                         addError(expr, ValidationError.AX_ATOMIC_ERR + ": \nThe name " +
321                                 "must be a relation with abstract range " +
322                                 "(because the argument is an instance)\n" + leSerializer.serialize(expr));   
323                     }
324                 }
325             }
326         }
327     }
328 
329     /**
330      * Checks if a CompoundMolecule is valid to wsml-core.
331      *
332      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitCompoundMolecule(org.omwg.logicalexpression.CompoundMolecule)
333      */
334     public void visitCompoundMolecule(CompoundMolecule expr) {
335         Iterator i = expr.listOperands().iterator();
336         while(i.hasNext()){
337             ((Molecule)i.next()).accept(this);
338         }
339     }
340 
341     /**
342      * Checks if a MembershipMolecule is valid to wsml-core.
343      *
344      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitMemberShipMolecule(org.omwg.logicalexpression.MembershipMolecule)
345      */
346     public void visitMemberShipMolecule(MembershipMolecule expr) {
347         // Checks if a MembershipMolecule is a valid a-molecule
348         if (rhs) {
349             // the identifier of the molecule must be a variable
350             if (!(expr.getLeftParameter() instanceof Variable)) {
351                 if (errorFlag) {
352                     addError(expr, ValidationError.AX_FORMULA_ERR + ":\n A valid a-molecule " +
353                             "must contain a variable as identifier\n" + leSerializer.serialize(expr));
354                 }
355             }
356             else {
357                 if (!equivVariables.contains(expr.getLeftParameter())) {
358                     equivVariables.add(expr.getLeftParameter());
359                 }
360                 if (!rhsVariables.contains(expr.getLeftParameter())) {
361                     rhsVariables.add(expr.getLeftParameter());
362                 }
363             }
364             // the argument of the molecule must be a Concept
365             if (check(expr.getRightParameter(), false, true, true, true, true)) {
366                 if (errorFlag) {
367                     addError(expr, ValidationError.AX_FORMULA_ERR + ":" 
368                             + "\nError: The arguments of an a-molecule must be Concepts\n"
369                             + leSerializer.serialize(expr));
370                 }
371             }
372         }
373         else if (lhs) {
374             if (errorFlag) {
375                 addError(expr, ValidationError.AX_LHS_ERR + ":\n Cannot " +
376                         "contain a MembershipMolecule:\n" 
377                         + leSerializer.serialize(expr));
378             }
379         }
380         else {
381             // the identifier must be an Instance
382             if (check(expr.getLeftParameter(), true, false, true, true, true)) {
383                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":" 
384                         + "\nThe identifier must be an Instance, " +
385                         "not a " + error + "\n" + leSerializer.serialize(expr));
386             }
387             // the arguments must be Concepts
388             if (check(expr.getRightParameter(), false, true, true, true, true)) {
389                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
390                         + "\nThe arguments must be Concepts, " +
391                         "not " + error + "\n" + leSerializer.serialize(expr));
392             }
393         }
394     }
395 
396     /**
397      * Checks if a SubConceptMolecule is valid to wsml-core.
398      *
399      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitSubConceptMolecule(org.omwg.logicalexpression.SubConceptMolecule)
400      */
401     public void visitSubConceptMolecule(SubConceptMolecule expr) {
402         String error = ":\n Cannot contain a SubConceptMolecule:\n" 
403             + leSerializer.serialize(expr);
404         // A SubConceptMolecule is no valid right-hand side formula
405         if (rhs) {      
406             if (errorFlag) {
407                 addError(expr, ValidationError.AX_RHS_ERR + error);
408             }
409         }
410         else if (lhs) {
411             if (errorFlag) {
412                 addError(expr, ValidationError.AX_LHS_ERR + error);
413             }
414         }
415         else {
416             error = "";
417             // the identifier must be a Concept
418             if (check(expr.getLeftParameter(), false, true, true, true, true)) {
419                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
420                         + "\nThe identifier must be a Concept, " +
421                         "not a " + error + "\n" + leSerializer.serialize(expr));
422             }
423             // the arguments must be Concepts
424             if (check(expr.getRightParameter(), false, true, true, true, true)) {
425                 addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
426                         + "\nThe arguments must be Concepts, " +
427                         "not " + error + "\n" + leSerializer.serialize(expr));
428             }
429         }
430     }
431   
432     /**
433      * Checks if a Negation is valid to wsml-core.
434      * 
435      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitNegation(org.omwg.logicalexpression.Negation)
436      */
437     public void visitNegation(Negation expr) {
438         String error = ":\n Cannot contain a Negation:\n" 
439             + leSerializer.serialize(expr);
440         // A negation is no valid right-hand side formula
441         if (rhs) {
442             if (errorFlag) {
443                 addError(expr, ValidationError.AX_RHS_ERR + error);
444             }
445         }
446         else if (lhs) {
447             if (errorFlag) {
448                 addError(expr, ValidationError.AX_LHS_ERR + error);
449             }
450         }
451         else {
452             addError(expr, ValidationError.AX_FORMULA_ERR + ": A Negation is" +
453                     " not a valid formula\n"  + leSerializer.serialize(expr));
454         }
455     }
456 
457     /**
458      * Checks if a NegationAsFailure is valid to wsml-core.
459      * 
460      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitNegationAsFailure(org.omwg.logicalexpression.NegationAsFailure)
461      */
462     public void visitNegationAsFailure(NegationAsFailure expr) {
463         String error = ":\n Cannot contain a NegationAsFailure:\n" 
464             + leSerializer.serialize(expr);
465         // A NegationAsFailure is no valid right-hand side formula
466         if (rhs) {
467             if (errorFlag) {
468                 addError(expr, ValidationError.AX_RHS_ERR + error);
469             }
470         }
471         else if (lhs) {
472             if (errorFlag) {
473                 addError(expr, ValidationError.AX_LHS_ERR + error);
474             }
475         }
476         else {
477             addError(expr, ValidationError.AX_FORMULA_ERR + ": A NegationAsFailure " +
478                     "is not a valid formula\n"  + leSerializer.serialize(expr));
479         }
480     }
481 
482     /**
483      * Checks if a Constraint is valid to wsml-core.
484      * 
485      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitConstraint(org.omwg.logicalexpression.Constraint)
486      */
487     public void visitConstraint(Constraint expr) {
488         String error = ":\n Cannot contain a Constraint:\n" 
489             + leSerializer.serialize(expr);
490         // A Constraint is no valid right-hand side formula
491         if (rhs) {
492             if (errorFlag) {
493                 addError(expr, ValidationError.AX_RHS_ERR + error);
494             }
495         }
496         else if (lhs) {
497             if (errorFlag) {
498                 addError(expr, ValidationError.AX_LHS_ERR + error);
499             }
500         }
501         else {
502             addError(expr, ValidationError.AX_FORMULA_ERR + ": A Constraint is not " +
503                     "a valid formula\n"  + leSerializer.serialize(expr));
504         }
505     }
506 
507     /**
508      * Checks if a Conjunction is valid to wsml-core.
509      * 
510      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitConjunction(org.omwg.logicalexpression.Conjunction)
511      */
512     public void visitConjunction(Conjunction expr) {
513         // Checks if a Conjunction is a valid right-hand side formula
514         if (rhs || lhs) {
515             expr.getLeftOperand().accept(this);
516             expr.getRightOperand().accept(this);
517         }
518         else {
519             if((expr.getLeftOperand() instanceof Conjunction) 
520                     || (expr.getLeftOperand() instanceof AtomicExpression)){
521                 expr.getLeftOperand().accept(this); 
522             }
523             else {
524                 addError(expr, ValidationError.AX_FORMULA_ERR + ": Invalid " +
525                         "Conjunction, all operands must be valid atomic " +
526                         "formulae\n" + leSerializer.serialize(expr));
527             }
528             if ((expr.getRightOperand() instanceof Conjunction)
529                     || (expr.getRightOperand() instanceof AtomicExpression)){
530                 expr.getRightOperand().accept(this);
531             }
532             else {
533                 addError(expr, ValidationError.AX_FORMULA_ERR + ": Invalid " +
534                         "Conjunction, all operands must be valid atomic " +
535                         "formulae\n" + leSerializer.serialize(expr));
536             }
537         }
538     }
539 
540     /**
541      * Checks if a Disjunction is valid to wsml-core.
542      * 
543      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitDisjunction(org.omwg.logicalexpression.Disjunction)
544      */
545     public void visitDisjunction(Disjunction expr) {
546         // A Disjunction is no valid right-hand side formula
547         if (rhs) {
548             if (errorFlag) {
549                 addError(expr, ValidationError.AX_RHS_ERR + ":\n Cannot " +
550                         "contain a Disjunction:\n" + leSerializer.serialize(expr));
551             }
552         }
553         // Checks if a specified Disjunction is a valid left-hand side formula
554         else if (lhs) {
555             expr.getLeftOperand().accept(this);
556             expr.getRightOperand().accept(this);
557         }
558         else {
559             addError(expr, ValidationError.AX_FORMULA_ERR + ": A Disjunction is not " +
560                     "a valid formula\n"  + leSerializer.serialize(expr));
561         }
562     }
563 
564     /**
565      * Checks if an InverseImplication is valid to wsml-core.
566      * 
567      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitInverseImplication(org.omwg.logicalexpression.InverseImplication)
568      */
569     public void visitInverseImplication(InverseImplication expr) {
570         String error = ":\n Cannot contain an InverseImplication:\n" 
571             + leSerializer.serialize(expr);
572         // An InverseImplication is no valid right-hand side formula
573         if (rhs) {
574             if (errorFlag) {
575                 addError(expr, ValidationError.AX_RHS_ERR + error);
576             }
577         }
578         else if (lhs) {
579             if (errorFlag) {
580                 addError(expr, ValidationError.AX_LHS_ERR + error);
581             }
582         }
583         else {
584             rhsVariables.clear();
585             lhsVariables.clear();
586             molecules.clear();
587             LogicalExpression left = expr.getLeftOperand();    
588             LogicalExpression right = expr.getRightOperand();
589 
590             // check on transitive attribute structure
591             if (((left instanceof Atom) 
592                    || (left instanceof AttributeValueMolecule)) && 
593                    (right instanceof Conjunction)) {
594                LogicalExpression leftConjunction = ((Conjunction) right).getLeftOperand();
595                LogicalExpression rightConjunction = ((Conjunction) right).getRightOperand();
596                if (((leftConjunction instanceof Atom) 
597                        || (leftConjunction instanceof AttributeValueMolecule)) 
598                        && ((rightConjunction instanceof Atom) 
599                        || (rightConjunction instanceof AttributeValueMolecule))) {
600                    isValidTransitiveInvImpl(expr);
601                }
602            }
603            // check on symmetric, sub-attribute and inverse attribute structure
604            else if (((left instanceof Atom) || (left instanceof AttributeValueMolecule)) && 
605                    ((right instanceof Atom) || (right instanceof AttributeValueMolecule))) {
606                isValidInverseImplication(expr);
607            }
608            else {
609                // check on right-hand side impliedBy left-hand side structure
610                errorFlag = false;
611                rhs = true;  
612                left.accept(this);
613                rhs = false;
614                lhs = true;
615                right.accept(this);
616                lhs = false;
617                
618                Iterator it = rhsVariables.iterator();
619                while (it.hasNext()) {
620                    if (!lhsVariables.contains(it.next())) {
621                        addError(expr, ValidationError.AX_IMPL_BY_ERR + ": All " +
622                                "variables in 'a' from 'a impliedBy b' " +
623                                "must also be contained in 'b'\n" + leSerializer.serialize(expr));
624                    }
625                }
626                if (lhsVariables.size() > 0) {
627                    Graph graph = new Graph();
628                    graph.isValidGraph(expr);
629                }
630            }
631         }
632     }
633 
634     /**
635      * Checks if an Implication is valid to wsml-core.
636      * 
637      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitImplication(org.omwg.logicalexpression.Implication)
638      */
639     public void visitImplication(Implication expr) {
640         String error = ":\n Cannot contain an Implication:\n" 
641             + leSerializer.serialize(expr);
642         // An Implication is no valid right-hand side formula
643         if (rhs) {
644             if (errorFlag) {
645                 addError(expr, ValidationError.AX_RHS_ERR + error);
646             }
647         }
648         else if (lhs) {
649             if (errorFlag) {
650                 addError(expr, ValidationError.AX_LHS_ERR + error);
651             }
652         }
653         else {
654             LogicalExpression left = expr.getLeftOperand();
655             LogicalExpression right = expr.getRightOperand();
656             InverseImplication invImp = leFactory.createInverseImplication(right, left);
657             invImp.accept(this);
658         }
659     }
660 
661     /**
662      * Checks if an Equivalence is valid to wsml-core.
663      * 
664      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitEquivalence(org.omwg.logicalexpression.Equivalence)
665      */
666     public void visitEquivalence(Equivalence expr) {
667         String error = ":\n Cannot contain an Equivalence:\n" 
668             + leSerializer.serialize(expr);
669         // An Equivalence is no valid right-hand side formula
670         if (rhs) {
671             if (errorFlag) {
672                 addError(expr, ValidationError.AX_RHS_ERR + error);
673             }
674         }
675         else if (lhs) {
676             if (errorFlag) {
677                 addError(expr, ValidationError.AX_LHS_ERR + error);
678             }
679         }
680         else {
681             equivVariables.clear();
682             rhs = true;
683             expr.getLeftOperand().accept(this);
684             expr.getRightOperand().accept(this);
685 
686             if (equivVariables.size() > 1) {
687                 addError(expr, ValidationError.AX_EQUIV_ERR + ": The Equivalence formula " +
688                         "can only contain one variable\n" + leSerializer.serialize(expr));
689                 equivVariables.clear();
690             }
691             equivVariables.clear();
692         }
693     }
694 
695     /**
696      * Checks if a LogicProgrammingRule is valid to wsml-core.
697      * 
698      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitLogicProgrammingRule(org.omwg.logicalexpression.LogicProgrammingRule)
699      */
700     public void visitLogicProgrammingRule(LogicProgrammingRule expr) {
701         String error = ":\n Cannot contain a LogicProgrammingRule:\n" 
702             + leSerializer.serialize(expr);
703         // A LogicProgrammingRule is no valid right-hand side formula
704         if (rhs) {
705             if (errorFlag) {
706                 addError(expr, ValidationError.AX_RHS_ERR + error);
707             }
708         }
709         else if (lhs) {
710             if (errorFlag) {
711                 addError(expr, ValidationError.AX_LHS_ERR + error);
712             }
713         }
714         else {
715             addError(expr, ValidationError.AX_FORMULA_ERR + ": A LogicProgrammingRule" +
716                     " is not a valid formula\n"  + leSerializer.serialize(expr));
717         }
718     }
719 
720     /**
721      * Checks if a UniversalQuantification is valid to wsml-core.
722      * 
723      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitUniversalQuantification(org.omwg.logicalexpression.UniversalQuantification)
724      */
725     public void visitUniversalQuantification(UniversalQuantification expr) {
726         String error = ":\n Cannot contain an UniversalQuantification:\n" 
727             + leSerializer.serialize(expr);
728         // An UniversalQuantification is no valid right-hand side formula
729         if (rhs) {
730             if (errorFlag) {
731                 addError(expr, ValidationError.AX_RHS_ERR + error);
732             }
733         }
734         else if (lhs) {
735             if (errorFlag) {
736                 addError(expr, ValidationError.AX_LHS_ERR + error);
737             }
738         }
739         else {
740             addError(expr, ValidationError.AX_FORMULA_ERR + ": A UniversalQuantification" +
741                     " is not a valid formula\n"  + leSerializer.serialize(expr));
742         }
743     }
744 
745     /**
746      * Checks if an ExistentialQuantification is valid to wsml-core.
747      * 
748      * @see org.deri.wsmo4j.validator.WsmlFlightExpressionValidator#visitExistentialQuantification(org.omwg.logicalexpression.ExistentialQuantification)
749      */
750     public void visitExistentialQuantification(ExistentialQuantification expr) {
751         String error = ":\n Cannot contain an ExistentialQuantification:\n" 
752             + leSerializer.serialize(expr);
753         // An ExistentialQuantification is no valid right-hand side formula
754         if (rhs) {
755             if (errorFlag) {
756                 addError(expr, ValidationError.AX_RHS_ERR + error);
757             }
758         }
759         else if (lhs) {
760             if (errorFlag) {
761                 addError(expr, ValidationError.AX_LHS_ERR + error);
762             }
763         }
764         else {
765             addError(expr, ValidationError.AX_FORMULA_ERR + ":\n A ExistentialQuantification" +
766                     " is not a valid formula\n"  + leSerializer.serialize(expr));
767         }
768     }
769     
770     /*
771      * Gets an atom and transforms it into a value definition molecule
772      */
773     private Molecule atomToMolecule(Atom expr) {
774         Molecule molecule = null;
775         // the atom must be a binary atom
776         if (expr.getArity() != 2) {
777             addError(expr, ValidationError.AX_ATOMIC_ERR + ":\nThe atom must " +
778                     "be a binary atom\n" + leSerializer.serialize(expr));
779             return molecule;
780         }
781         else {
782             molecule = leFactory.createAttributeValue(
783                     expr.getParameter(0), expr.getIdentifier(), expr.getParameter(1));
784             
785             return molecule;
786         }
787     }
788        
789     /*
790      * Checks if a specified InverseImplication, containing a molecule and a 
791      * conjunction as operands, is a valid transitive construction
792      */
793     private void isValidTransitiveInvImpl(InverseImplication expr) {
794         AttributeValueMolecule left = null;
795         AttributeValueMolecule conLeft = null;
796         AttributeValueMolecule conRight = null;
797         LogicalExpression l = expr.getLeftOperand();
798         LogicalExpression cLeft = ((Conjunction) expr.getRightOperand()).getLeftOperand();
799         LogicalExpression cRight = ((Conjunction) expr.getRightOperand()).getRightOperand();
800         if (l instanceof Atom) {
801             left = (AttributeValueMolecule) atomToMolecule((Atom) l);
802         }
803         else {
804             left = (AttributeValueMolecule) l;
805         }
806         if (cLeft instanceof Atom) {
807             conLeft = (AttributeValueMolecule) atomToMolecule((Atom) cLeft);
808         }
809         else {
810             conLeft = (AttributeValueMolecule) cLeft;
811         }
812         if (cRight instanceof Atom) {
813             conRight = (AttributeValueMolecule) atomToMolecule((Atom) cRight);
814         }
815         else{
816             conRight = (AttributeValueMolecule) cRight;
817         }
818         if (left == null || conLeft == null || conRight == null) {
819             addError(expr, ValidationError.AX_IMPL_BY_ERR + ": Invalid atom\n" +
820                     leSerializer.serialize(expr));
821             return;
822         }
823 
824         rhs = false;
825         lhs = false;
826         formula = true;
827         left.accept(this);
828         conLeft.accept(this);
829         conRight.accept(this);
830         
831         if (left.getLeftParameter() instanceof Variable 
832                 && conLeft.getLeftParameter() instanceof Variable
833                 && conRight.getLeftParameter() instanceof Variable
834                 && left.getRightParameter() instanceof Variable
835                 && conLeft.getRightParameter() instanceof Variable
836                 && conRight.getRightParameter() instanceof Variable
837                 && left.getAttribute() instanceof Term
838                 && conLeft.getAttribute() instanceof Term
839                 && conRight.getAttribute() instanceof Term) {
840             Variable leftTerm = (Variable) left.getLeftParameter();
841             Variable conLeftTerm = (Variable) conLeft.getLeftParameter();
842             Variable conRightTerm = (Variable) conRight.getLeftParameter();
843             Term leftRel = left.getAttribute();
844             Term conLeftRel = conLeft.getAttribute();
845             Term conRightRel = conRight.getAttribute();     
846             Variable leftArg = (Variable) left.getRightParameter();
847             Variable conLeftArg = (Variable) conLeft.getRightParameter();
848             Variable conRightArg = (Variable) conRight.getRightParameter();
849             
850             // check on globally transitive attribute/relation
851             if (leftTerm.equals(conLeftTerm) && leftTerm.equals(conRightTerm)) {
852                 addError(expr, ValidationError.AX_IMPL_BY_ERR + ": The molecule's " +
853                         "term must be contained in exactly one of the conjunction's " +
854                         "molecule's terms\n" + leSerializer.serialize(expr));
855             }
856             else if (!(leftRel.equals(conLeftRel)) || !(leftRel.equals(conRightRel))) {
857                 addError(expr, ValidationError.AX_IMPL_BY_ERR + ": The molecule's " +
858                         "attribute's names must be equal\n" + leSerializer.serialize(expr));
859             }
860             else if (leftTerm.equals(conLeftTerm)) {
861                 if (!(leftArg.equals(conRightArg)) || !(conLeftArg.equals(conRightTerm))) {
862                     addError(expr, ValidationError.AX_IMPL_BY_ERR + ": No valid" +
863                             " transitive construction\n" + leSerializer.serialize(expr));
864                 }
865             }
866             else if (leftTerm.equals(conRightTerm)) {
867                 if (!(leftArg.equals(conLeftArg)) || !(conRightArg.equals(conLeftTerm))) {
868                     addError(expr, ValidationError.AX_IMPL_BY_ERR + ": No valid" +
869                             " transitive construction\n" + leSerializer.serialize(expr));
870                 }
871             }
872         }
873     }
874     
875     /*
876      * Checks if an Inverse Implication, containing two molecules as Operands, 
877      * is a valid construction. Valid constructions are symmetric, sub-attribute 
878      * and inverse attribute structures
879      */
880     private void isValidInverseImplication(InverseImplication expr) {
881         AttributeValueMolecule left = null;
882         AttributeValueMolecule right = null;
883         LogicalExpression l = expr.getLeftOperand();
884         LogicalExpression r = expr.getRightOperand();
885         if (l instanceof Atom) {
886             left = (AttributeValueMolecule) atomToMolecule((Atom) l);
887         }
888         else {
889             left = (AttributeValueMolecule) l;
890         }
891         if (r instanceof Atom) {
892             right = (AttributeValueMolecule) atomToMolecule((Atom) r);
893         }
894         else {
895             right = (AttributeValueMolecule) r;
896         }
897         if (left == null || right == null) {
898             addError(expr, ValidationError.AX_IMPL_BY_ERR + ": Invalid atom" +
899                     leSerializer.serialize(expr));
900             return;
901         }
902         errorFlag = true;
903         rhs = false;
904         lhs = false;
905         formula = true;
906         left.accept(this);
907         right.accept(this);
908         
909         if (left.getLeftParameter() instanceof Variable 
910                 && right.getLeftParameter() instanceof Variable
911                 && left.getRightParameter() instanceof Variable
912                 && right.getRightParameter() instanceof Variable
913                 && left.getAttribute() instanceof Term
914                 && right.getAttribute() instanceof Term) {
915          
916             Variable leftTerm = (Variable) left.getLeftParameter();
917             Variable rightTerm = (Variable) right.getLeftParameter();
918             Term leftRel = left.getAttribute();
919             Term rightRel = right.getAttribute();       
920             Variable leftArg = (Variable) left.getRightParameter();
921             Variable rightArg = (Variable) right.getRightParameter();
922                 
923             // check on globally symmetric and inverse attribute/relation
924             if (!(leftTerm.equals(rightArg)) || !(leftArg.equals(rightTerm))) {
925                 
926                 // check on globally sub-attribute/relation
927                 if (!(leftTerm.equals(rightTerm)) || !(leftArg.equals(rightArg)) || leftRel.equals(rightRel)) {
928                     addError(expr, ValidationError.AX_IMPL_BY_ERR + ": No valid" +
929                             " symmetric, sub-attribute or inverse construction\n" + 
930                             leSerializer.serialize(expr));
931                 } 
932             }
933         }
934     }
935     
936     /*
937      * Check if a specified Molecule's parameter or a term is used in the actual 
938      * axiom as Instance, Relation or Datatype, or whether it is a Variable
939      */
940     private boolean check(Object o, boolean concept, boolean instance, 
941             boolean relation, boolean datatype, boolean variable) {
942         if (o instanceof Molecule) {
943             if (concept && checkConcepts(((Molecule) o).getLeftParameter())) {
944                 error = "Concept";
945                 return true;
946             }
947             if (instance && checkInstances(((Molecule) o).getLeftParameter())) {
948                 error = "Instance";
949                 return true;
950             }
951             else if (relation && checkRelations(((Molecule) o).getLeftParameter())) {
952                 error = "Relation";
953                 return true;
954             }
955             else if (datatype && checkDatatypes(((Molecule) o).getLeftParameter())) {
956                 error = "Datatype";
957                 return true;
958             }
959             else if (variable && (((Molecule) o).getLeftParameter() instanceof Variable)) {
960                 error = "Variable";
961                 return true;
962             }
963         }
964         else if (o instanceof Term) {
965             if (concept && checkConcepts(o)) {
966                 error = "Concept";
967             }
968             if (instance && checkInstances(o)) {
969                 error = "Instance";
970                 return true;
971             }
972             else if (relation && checkRelations(o)) {
973                 error = "Relation";
974                 return true;
975             }
976             else if (datatype && checkDatatypes(o)) {
977                 error = "Datatype";
978                 return true;
979             }
980             else if (variable && (o instanceof Variable)) {
981                 error = "Variable";
982                 return true;
983             }
984         }
985         return false;
986     }
987     
988     /*
989      * Checks if a specified Term is contained in the concepts vector
990      */
991     private boolean checkConcepts(Object o) {
992         return validator.getIdConcepts().contains(o);
993     }
994     
995     /*
996      * Checks if a specified Term is contained in the instances vector
997      */
998     private boolean checkInstances(Object o) {
999         return validator.getIdInstances().contains(o);
1000     }
1001     
1002     /*
1003      * Checks if a specified Term is contained in the relations vector
1004      */
1005     private boolean checkRelations(Object o) {
1006         return validator.getIdRelations().contains(o);
1007     }
1008     
1009     /*
1010      * Checks if a specified Term is contained in the abstract relations vector
1011      */
1012     private boolean checkAbstractRelations(Object o) {
1013         return validator.getIdAbstractRelations().contains(o);
1014     }
1015     
1016     /*
1017      * Checks if a specified Term is contained in the concrete relations vector
1018      */
1019     private boolean checkConcreteRelations(Object o) {
1020         return validator.getIdConcreteRelations().contains(o);
1021     }
1022     
1023     /*
1024      * Checks if a specified Term is contained in the datatypes vector
1025      */
1026     private boolean checkDatatypes(Object o) {
1027         return ConstantTransformer.getInstance().isDataType(o.toString());
1028     }
1029 
1030     public int getNumberOfMolecules() {
1031         return numberOfMolecules;
1032     }
1033 
1034     public Set getLHSVariables() {
1035         return lhsVariables;
1036     }
1037     
1038     /*
1039      * Adds a new ValidationError to the error list
1040      */
1041     private void addError(LogicalExpression logexp, String msg) {
1042         LogicalExpressionErrorImpl le = new LogicalExpressionErrorImpl(
1043                 axiom, logexp, msg, WSML.WSML_CORE);
1044         if (!errors.contains(le)) {
1045             errors.add(le);
1046         }
1047     }
1048     
1049 protected class Graph {
1050         
1051         private Map <Variable, List <Variable>> listMap = new HashMap <Variable, List <Variable>> ();
1052         private List <Variable> connected = new Vector <Variable> ();
1053         
1054         /*
1055          * Checks if the variables and molecules of a given inverse implication
1056          * build a valid connected and acyclic graph.
1057          */
1058         protected boolean isValidGraph(Binary expr) {      
1059             listMap.clear();
1060             connected.clear();
1061             
1062             buildLists();
1063         
1064             Iterator it = lhsVariables.iterator();
1065             Variable v1 = (Variable) it.next();
1066             Variable v = null;
1067             boolean valid = false;
1068             
1069             // check if the given graph is connected
1070             while(it.hasNext()) {
1071                 v = (Variable) it.next();       
1072                 valid = checkGraphConnected(v1, v);
1073                 if (!valid) {
1074                     addError(expr, ValidationError.AX_GRAPH_ERR + ":\nGraph is " +
1075                             "not connected:\n" + leSerializer.serialize(expr));
1076                     return false;
1077                 }
1078             }
1079             
1080             // check if the given graph is acyclic  
1081             List <Variable> checkList = new Vector <Variable> ();
1082             checkList.add(v1);
1083             valid = checkGraphAcyclic(v1, v1, checkList);
1084             if (valid) {
1085                 return true;
1086             }
1087             else {
1088                 addError(expr, ValidationError.AX_GRAPH_ERR + ":\nGraph contains " +
1089                         "cycle:\n" + leSerializer.serialize(expr));
1090                 return false;
1091             }
1092         }
1093         
1094         /*
1095          * Build a Map with a specific variable as key and with a list as value, 
1096          * that contains all variables to which the key variable is connected.
1097          */
1098         private void buildLists() {
1099             Variable v1 = null;
1100             Variable v = null;
1101             
1102             Iterator it = lhsVariables.iterator();
1103             while (it.hasNext()) {
1104                 List <Variable> list = new Vector <Variable> ();
1105                 v1 = (Variable) it.next();
1106                 Iterator itMol = molecules.iterator();
1107                 while (itMol.hasNext()) {
1108                     List l = (List) itMol.next();
1109                     if (l.get(0).equals(v1)) {
1110                         v = (Variable) l.get(1);
1111                         list.add(v);
1112                     } 
1113                     else if (l.get(1).equals(v1)) {
1114                         v = (Variable) l.get(0);
1115                         list.add(v);
1116                     }  
1117                 }
1118                 listMap.put(v1, list);
1119             }
1120         }
1121         
1122         /*
1123          * Checks if variable v1 is connected to variable v2.
1124          */
1125         private boolean checkGraphConnected(Variable v1, Variable v2) {
1126             boolean found = false;
1127             boolean used = false;
1128             
1129             List <Variable> l = listMap.get(v1);
1130             
1131             if (l.contains(v2)) {
1132                 return true;
1133             }
1134             else {
1135                 connected.add(v1);
1136                 Iterator it = l.iterator();
1137                 while (it.hasNext()) {
1138                     Variable v = (Variable) it.next(); 
1139                     for (int i=0; i<connected.size(); i++) {
1140                         if (v.equals(connected.get(i))) {
1141                             used = true;
1142                         }
1143                     }
1144                     if (!used) {
1145                         found = checkGraphConnected(v, v2);
1146                     }
1147                     if (found) {
1148                         return true;
1149                     }
1150                     used = false;
1151                 }
1152                 return false;
1153             }
1154         }
1155            
1156         /*
1157          * Checks if a given graph contains a cycle. 
1158          */
1159         private boolean checkGraphAcyclic(Variable from, Variable v, List checkList) {
1160             if ((numberOfMolecules + 1) == lhsVariables.size()) {
1161                 return true;
1162             }
1163             else {
1164                 return false;
1165             }
1166         }
1167     }
1168     
1169 }