1
2
3
4
5
6
7
8
9
10
11
12
13
14
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
35
36
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
84
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
124
125
126
127 public void visitAtom(Atom expr) {
128
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
178
179 public void visitAttributeContraintMolecule(AttributeConstraintMolecule expr) {
180
181 error = "";
182
183 if (formula) {
184 isValidBMolecule(expr);
185 }
186 else {
187
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
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
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
211
212 public void visitAttributeInferenceMolecule(AttributeInferenceMolecule expr) {
213
214 error = "";
215
216 if (formula) {
217 isValidBMolecule(expr);
218 }
219 else {
220
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
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
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
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
255
256 public void visitAttributeValueMolecule(AttributeValueMolecule expr) {
257
258 error = "";
259
260 if (formula) {
261 isValidBMolecule(expr);
262 }
263 else {
264
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
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
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
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
299
300 public void visitCompoundMolecule(CompoundMolecule expr) {
301
302 Iterator i = expr.listOperands().iterator();
303 while(i.hasNext()){
304 ((Molecule)i.next()).accept(this);
305 }
306 }
307
308
309
310
311 public void visitMemberShipMolecule(MembershipMolecule expr) {
312
313 error = "";
314
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
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
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
341 variables.add(expr.getLeftParameter());
342 }
343 }
344 }
345 else {
346
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
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
363
364 public void visitSubConceptMolecule(SubConceptMolecule expr) {
365
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
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
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
400
401
402
403 public void visitNegation(Negation expr) {
404
405
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
428
429
430
431 public void visitNegationAsFailure(NegationAsFailure expr) {
432
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
459
460
461
462 public void visitConstraint(Constraint expr) {
463
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
487
488
489
490 public void visitConjunction(Conjunction expr) {
491
492
493
494
495
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
535
536
537
538 public void visitDisjunction(Disjunction expr) {
539
540
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
566
567
568
569 public void visitInverseImplication(InverseImplication expr) {
570
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
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
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
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
652
653
654
655 public void visitImplication(Implication expr) {
656
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
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
706
707
708
709 public void visitEquivalence(Equivalence expr) {
710
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
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
761
762
763
764 public void visitLogicProgrammingRule(LogicProgrammingRule expr) {
765
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
789
790
791
792 public void visitUniversalQuantification(UniversalQuantification expr) {
793
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
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
871
872
873
874 public void visitExistentialQuantification(ExistentialQuantification expr) {
875
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
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
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
947
948 private Molecule atomToMolecule(Atom expr) {
949 Molecule molecule = null;
950
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
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
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
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
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
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
1043
1044
1045 private boolean isValidTransitiveInvImpl(InverseImplication expr) {
1046 AttributeValueMolecule left, conjunctionLeft, conjunctionRight;
1047
1048
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
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
1107
1108
1109
1110 private boolean isValidInverseImplication(InverseImplication expr) {
1111 AttributeValueMolecule left = null;
1112 AttributeValueMolecule right = null;
1113
1114
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
1139 if (!(leftVariable.equals(rightArgument)) || !(leftArgument.equals(rightVariable))) {
1140
1141
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
1153
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
1205
1206 private boolean checkConcepts(Object o) {
1207 return validator.getIdConcepts().contains(o);
1208 }
1209
1210
1211
1212
1213 private boolean checkInstances(Object o) {
1214 return validator.getIdInstances().contains(o);
1215 }
1216
1217
1218
1219
1220 private boolean checkRelations(Object o) {
1221 return validator.getIdRelations().contains(o);
1222 }
1223
1224
1225
1226
1227 private boolean checkAbstractRelations(Object o) {
1228 return validator.getIdAbstractRelations().contains(o);
1229 }
1230
1231
1232
1233
1234 private boolean checkConcreteRelations(Object o) {
1235 return validator.getIdConcreteRelations().contains(o);
1236 }
1237
1238
1239
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
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
1307
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
1340
1341
1342 protected boolean isValidGraph() {
1343 listMap.clear();
1344 connected.clear();
1345
1346
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
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
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
1386
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
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
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 }