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 |
0
| protected WsmlDLExpressionValidator(Axiom axiom, LogicalExpressionFactory leFactory, List <ValidationError> errors, WsmlDLValidator validator) {
|
87 |
0
| this.validator = validator;
|
88 |
0
| leSerializer = validator.leSerializer;
|
89 |
0
| this.leFactory = leFactory;
|
90 |
0
| this.axiom = axiom;
|
91 |
0
| this.errors = errors;
|
92 |
0
| formula = false;
|
93 |
0
| validDescription = false;
|
94 |
0
| quantifier = false;
|
95 |
0
| universalRight = false;
|
96 |
0
| existential = false;
|
97 |
0
| bMol = false;
|
98 |
0
| graph = false;
|
99 |
0
| checkGraph = false;
|
100 |
0
| checkForRoot = false;
|
101 |
0
| noRoot = false;
|
102 |
0
| error = null;
|
103 |
0
| variables = new HashSet <Term>();
|
104 |
0
| molecules = new HashSet <List <Term>>();
|
105 |
0
| root = null;
|
106 |
0
| numberOfMolecules = 0;
|
107 |
| } |
108 |
| |
109 |
0
| protected void setup() {
|
110 |
0
| formula = false;
|
111 |
0
| quantifier = false;
|
112 |
0
| universalRight = false;
|
113 |
0
| existential = false;
|
114 |
0
| bMol = false;
|
115 |
0
| variables = new HashSet <Term>();
|
116 |
0
| root = null;
|
117 |
0
| noRoot = false;
|
118 |
| |
119 |
0
| setGraph(false);
|
120 |
| } |
121 |
| |
122 |
| |
123 |
| |
124 |
| |
125 |
| |
126 |
| |
127 |
0
| public void visitAtom(Atom expr) {
|
128 |
| |
129 |
0
| if (universalRight) {
|
130 |
0
| quantifier = true;
|
131 |
0
| 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 |
0
| if (!expr.getIdentifier().toString().equals(Constants.STRONG_EQUAL)) {
|
136 |
0
| addError(expr, error);
|
137 |
0
| validDescription = false;
|
138 |
| } |
139 |
0
| universalRight = false;
|
140 |
| } |
141 |
0
| else if (existential) {
|
142 |
0
| quantifier = true;
|
143 |
0
| 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 |
0
| if (!expr.getIdentifier().toString().equals(Constants.STRONG_EQUAL)) {
|
148 |
0
| addError(expr, error);
|
149 |
0
| validDescription = false;
|
150 |
| } |
151 |
0
| existential = false;
|
152 |
| } |
153 |
0
| if ((expr.getIdentifier().toString().equals(Constants.WSML_NAMESPACE +
|
154 |
| Constants.TRUE)) || |
155 |
| (expr.getIdentifier().toString().equals(Constants.WSML_NAMESPACE + |
156 |
| Constants.FALSE))) { |
157 |
0
| noRoot = true;
|
158 |
| } |
159 |
0
| else if (expr instanceof BuiltInAtom && !quantifier) {
|
160 |
0
| String error = ValidationError.AX_ATOMIC_ERR + ":\n" +
|
161 |
| "Built-in atoms are not allowed:\n" + |
162 |
| leSerializer.serialize(expr); |
163 |
0
| addError(expr, error);
|
164 |
| } |
165 |
0
| 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 |
0
| Molecule molecule = atomToMolecule(expr);
|
170 |
0
| if (molecule != null) {
|
171 |
0
| molecule.accept(this);
|
172 |
| } |
173 |
| } |
174 |
| } |
175 |
| |
176 |
| |
177 |
| |
178 |
| |
179 |
0
| public void visitAttributeContraintMolecule(AttributeConstraintMolecule expr) {
|
180 |
| |
181 |
0
| error = "";
|
182 |
| |
183 |
0
| if (formula) {
|
184 |
0
| isValidBMolecule(expr);
|
185 |
| } |
186 |
| else { |
187 |
| |
188 |
0
| if (check(expr.getLeftParameter(), false, true, true, true, true)) {
|
189 |
0
| 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 |
0
| if (check(expr.getRightParameter(), true, true, true, false, true)) {
|
195 |
0
| addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
|
196 |
| + "\nThe arguments must be " + |
197 |
| "Datatypes, not " + error + "\n" + leSerializer.serialize(expr)); |
198 |
| } |
199 |
| |
200 |
0
| if ((check(expr.getAttribute(), true, true, false, true, true))
|
201 |
| || (!checkConcreteRelations(expr.getAttribute()))){ |
202 |
0
| 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 |
0
| public void visitAttributeInferenceMolecule(AttributeInferenceMolecule expr) {
|
213 |
| |
214 |
0
| error = "";
|
215 |
| |
216 |
0
| if (formula) {
|
217 |
0
| isValidBMolecule(expr);
|
218 |
| } |
219 |
| else { |
220 |
| |
221 |
0
| if (check(expr.getLeftParameter(), false, true, true, true, true)) {
|
222 |
0
| 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 |
0
| if (check(expr.getRightParameter(), false, true, true, false, true)) {
|
228 |
0
| 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 |
0
| if (checkDatatypes(expr.getRightParameter())) {
|
235 |
0
| if (!checkConcreteRelations(expr.getAttribute())) {
|
236 |
0
| 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 |
0
| else if (checkConcepts(expr.getRightParameter())) {
|
243 |
0
| if (!checkAbstractRelations(expr.getAttribute())) {
|
244 |
0
| 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 |
0
| public void visitAttributeValueMolecule(AttributeValueMolecule expr) {
|
257 |
| |
258 |
0
| error = "";
|
259 |
| |
260 |
0
| if (formula) {
|
261 |
0
| isValidBMolecule(expr);
|
262 |
| } |
263 |
| else { |
264 |
| |
265 |
0
| if (check(expr.getLeftParameter(), true, false, true, true, true)) {
|
266 |
0
| 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 |
0
| if (check(expr.getRightParameter(), true, false, true, false, true)) {
|
272 |
0
| 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 |
0
| if (checkDatatypes(expr.getRightParameter())) {
|
279 |
0
| if (!checkConcreteRelations(expr.getAttribute())) {
|
280 |
0
| 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 |
0
| else if (checkInstances(expr.getRightParameter())) {
|
287 |
0
| if (!checkAbstractRelations(expr.getAttribute())) {
|
288 |
0
| 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 |
0
| public void visitCompoundMolecule(CompoundMolecule expr) {
|
301 |
| |
302 |
0
| Iterator i = expr.listOperands().iterator();
|
303 |
0
| while(i.hasNext()){
|
304 |
0
| ((Molecule)i.next()).accept(this);
|
305 |
| } |
306 |
| } |
307 |
| |
308 |
| |
309 |
| |
310 |
| |
311 |
0
| public void visitMemberShipMolecule(MembershipMolecule expr) {
|
312 |
| |
313 |
0
| error = "";
|
314 |
| |
315 |
0
| if (formula) {
|
316 |
0
| if (universalRight) {
|
317 |
0
| 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 |
0
| validDescription = false;
|
322 |
0
| universalRight = false;
|
323 |
| } |
324 |
| else { |
325 |
| |
326 |
0
| if (!(expr.getLeftParameter() instanceof Variable)) {
|
327 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":"
|
328 |
| + "\nThe identifier of an a-molecule must be a Variable\n" |
329 |
| + leSerializer.serialize(expr)); |
330 |
0
| validDescription = false;
|
331 |
| } |
332 |
| |
333 |
0
| if (check(expr.getRightParameter(), true, false, false, false, false)) {
|
334 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":"
|
335 |
| + "\nThe argument of an a-molecule must be a Concept\n" |
336 |
| + leSerializer.serialize(expr)); |
337 |
0
| validDescription = false;
|
338 |
| } |
339 |
0
| if (graph && (!variables.contains(expr.getLeftParameter()))) {
|
340 |
| |
341 |
0
| variables.add(expr.getLeftParameter());
|
342 |
| } |
343 |
| } |
344 |
| } |
345 |
| else { |
346 |
| |
347 |
0
| if (check(expr.getLeftParameter(), true, false, true, true, true)) {
|
348 |
0
| addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
|
349 |
| + "\nThe identifier must be an Instance, " + |
350 |
| "not a " + error + "\n" + leSerializer.serialize(expr)); |
351 |
| } |
352 |
| |
353 |
0
| if (check(expr.getRightParameter(), false, true, true, true, true)) {
|
354 |
0
| 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 |
0
| public void visitSubConceptMolecule(SubConceptMolecule expr) {
|
365 |
| |
366 |
0
| if (universalRight) {
|
367 |
0
| 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 |
0
| validDescription = false;
|
372 |
0
| universalRight = false;
|
373 |
| } |
374 |
0
| else if (existential) {
|
375 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
376 |
| "The ExistentialQuantifier may not contain a " + |
377 |
| "SubConceptMolecule:\n" + leSerializer.serialize(expr)); |
378 |
0
| validDescription = false;
|
379 |
0
| existential = false;
|
380 |
| } |
381 |
| else { |
382 |
0
| error = "";
|
383 |
| |
384 |
0
| if (check(expr.getLeftParameter(), false, true, true, true, true)) {
|
385 |
0
| addError(expr, ValidationError.AX_ATOMIC_ERR + ":"
|
386 |
| + "\nThe identifier must be a Concept, " + |
387 |
| "not a " + error + "\n" + leSerializer.serialize(expr)); |
388 |
| } |
389 |
| |
390 |
0
| if (check(expr.getRightParameter(), false, true, true, true, true)) {
|
391 |
0
| 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 |
0
| public void visitNegation(Negation expr) {
|
404 |
| |
405 |
| |
406 |
0
| if (formula) {
|
407 |
0
| if (universalRight || existential) {
|
408 |
0
| if (!(expr.getOperand() instanceof BuiltInAtom)) {
|
409 |
0
| 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 |
0
| validDescription = false;
|
413 |
0
| existential = false;
|
414 |
0
| universalRight = false;
|
415 |
0
| return;
|
416 |
| } |
417 |
| } |
418 |
0
| expr.getOperand().accept(this);
|
419 |
| } |
420 |
| else { |
421 |
0
| 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 |
0
| public void visitNegationAsFailure(NegationAsFailure expr) {
|
432 |
| |
433 |
0
| if (universalRight) {
|
434 |
0
| 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 |
0
| validDescription = false;
|
439 |
0
| universalRight = false;
|
440 |
| } |
441 |
0
| else if (existential) {
|
442 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
443 |
| "The ExistentialQuantifier may not contain a " + |
444 |
| "NegationAsFailure:\n" + leSerializer.serialize(expr)); |
445 |
0
| validDescription = false;
|
446 |
0
| existential = false;
|
447 |
| } |
448 |
0
| else if (existential) {
|
449 |
0
| expr.accept(this);
|
450 |
| } |
451 |
| else { |
452 |
0
| 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 |
0
| public void visitConstraint(Constraint expr) {
|
463 |
| |
464 |
0
| if (universalRight) {
|
465 |
0
| 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 |
0
| validDescription = false;
|
470 |
0
| universalRight = false;
|
471 |
| } |
472 |
0
| else if (existential) {
|
473 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
474 |
| "The ExistentialQuantifier may not contain a " + |
475 |
| "Constraint:\n" + leSerializer.serialize(expr)); |
476 |
0
| validDescription = false;
|
477 |
0
| existential = false;
|
478 |
| } |
479 |
| else { |
480 |
0
| 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 |
0
| public void visitConjunction(Conjunction expr) {
|
491 |
| |
492 |
| |
493 |
| |
494 |
| |
495 |
| |
496 |
0
| if (formula) {
|
497 |
0
| if (universalRight) {
|
498 |
0
| 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 |
0
| validDescription = false;
|
503 |
0
| universalRight = false;
|
504 |
| } |
505 |
| else { |
506 |
0
| 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 |
0
| 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 |
0
| validDescription = false;
|
518 |
0
| existential = false;
|
519 |
0
| return;
|
520 |
| } |
521 |
| else { |
522 |
0
| expr.getLeftOperand().accept(this);
|
523 |
0
| expr.getRightOperand().accept(this);
|
524 |
| } |
525 |
| } |
526 |
| } |
527 |
| else { |
528 |
0
| 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 |
0
| public void visitDisjunction(Disjunction expr) {
|
539 |
| |
540 |
| |
541 |
0
| if (formula) {
|
542 |
0
| if (universalRight) {
|
543 |
0
| if (((!(expr.getLeftOperand() instanceof Negation))
|
544 |
| && (!(expr.getLeftOperand() instanceof Disjunction))) |
545 |
| || ((!(expr.getRightOperand() instanceof Negation)) |
546 |
| && (!(expr.getRightOperand() instanceof Disjunction)))){ |
547 |
0
| 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 |
0
| validDescription = false;
|
551 |
0
| universalRight = false;
|
552 |
0
| return;
|
553 |
| } |
554 |
| } |
555 |
0
| expr.getLeftOperand().accept(this);
|
556 |
0
| expr.getRightOperand().accept(this);
|
557 |
| } |
558 |
| else { |
559 |
0
| 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 |
0
| public void visitInverseImplication(InverseImplication expr) {
|
570 |
| |
571 |
0
| if (universalRight) {
|
572 |
0
| 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 |
0
| validDescription = false;
|
577 |
0
| universalRight = false;
|
578 |
| } |
579 |
0
| else if (existential) {
|
580 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
581 |
| "The ExistentialQuantifier may not contain a " + |
582 |
| "InverseImplication:\n" + leSerializer.serialize(expr)); |
583 |
0
| validDescription = false;
|
584 |
0
| existential = false;
|
585 |
| } |
586 |
| else { |
587 |
0
| if (formula == true) {
|
588 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
589 |
| "Nested Implications are not allowed:\n" + |
590 |
| leSerializer.serialize(expr)); |
591 |
0
| validDescription = false;
|
592 |
| } |
593 |
| else { |
594 |
0
| formula = true;
|
595 |
0
| validDescription = true;
|
596 |
| |
597 |
0
| expr.getLeftOperand().accept(this);
|
598 |
0
| expr.getRightOperand().accept(this);
|
599 |
| } |
600 |
| |
601 |
0
| LogicalExpression left = expr.getLeftOperand();
|
602 |
0
| LogicalExpression right = expr.getRightOperand();
|
603 |
0
| left.accept(this);
|
604 |
0
| right.accept(this);
|
605 |
0
| if (!validDescription) {
|
606 |
0
| addError(expr, ValidationError.AX_IMPL_BY_ERR + ":\n"
|
607 |
| + leSerializer.serialize(expr)); |
608 |
0
| return;
|
609 |
| } |
610 |
| |
611 |
| |
612 |
0
| if (((left instanceof Atom) || (left instanceof AttributeValueMolecule)) &&
|
613 |
| (right instanceof Conjunction)) { |
614 |
0
| LogicalExpression leftConjunction = ((Conjunction) right).getLeftOperand();
|
615 |
0
| LogicalExpression rightConjunction = ((Conjunction) right).getRightOperand();
|
616 |
0
| if (((leftConjunction instanceof Atom)
|
617 |
| || (leftConjunction instanceof AttributeValueMolecule)) |
618 |
| && ((rightConjunction instanceof Atom) |
619 |
| || (rightConjunction instanceof AttributeValueMolecule))) { |
620 |
0
| if (isValidTransitiveInvImpl(expr)) {
|
621 |
0
| validDescription = false;
|
622 |
| } |
623 |
0
| return;
|
624 |
| } |
625 |
| } |
626 |
| |
627 |
| |
628 |
0
| if (((left instanceof Atom) || (left instanceof AttributeValueMolecule)) &&
|
629 |
| ((right instanceof Atom) || (right instanceof AttributeValueMolecule))) { |
630 |
0
| if (isValidInverseImplication(expr)) {
|
631 |
0
| validDescription = false;
|
632 |
| } |
633 |
0
| return;
|
634 |
| } |
635 |
| |
636 |
0
| if (validDescription) {
|
637 |
| |
638 |
| |
639 |
0
| checkForRoot = true;
|
640 |
0
| new Graph(expr, this);
|
641 |
0
| checkForRoot = false;
|
642 |
| |
643 |
0
| new Graph(expr.getLeftOperand(), this);
|
644 |
0
| new Graph(expr.getRightOperand(), this);
|
645 |
| |
646 |
| } |
647 |
| } |
648 |
| } |
649 |
| |
650 |
| |
651 |
| |
652 |
| |
653 |
| |
654 |
| |
655 |
0
| public void visitImplication(Implication expr) {
|
656 |
| |
657 |
0
| if (universalRight) {
|
658 |
0
| 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 |
0
| validDescription = false;
|
663 |
0
| universalRight = false;
|
664 |
| } |
665 |
0
| else if (existential) {
|
666 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
667 |
| "The ExistentialQuantifier may not contain a " + |
668 |
| "Implication:\n" + leSerializer.serialize(expr)); |
669 |
0
| validDescription = false;
|
670 |
0
| existential = false;
|
671 |
| } |
672 |
| else { |
673 |
0
| if (formula == true) {
|
674 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
675 |
| "Nested Implications are not allowed:\n" + |
676 |
| leSerializer.serialize(expr)); |
677 |
0
| validDescription = false;
|
678 |
| } |
679 |
| else { |
680 |
0
| formula = true;
|
681 |
0
| validDescription = true;
|
682 |
| |
683 |
0
| expr.getLeftOperand().accept(this);
|
684 |
0
| expr.getRightOperand().accept(this);
|
685 |
| } |
686 |
| |
687 |
0
| if (!validDescription) {
|
688 |
0
| addError(expr, ValidationError.AX_IMP_ERR + ":\n" +
|
689 |
| leSerializer.serialize(expr)); |
690 |
| } |
691 |
| else { |
692 |
| |
693 |
| |
694 |
0
| checkForRoot = true;
|
695 |
0
| new Graph(expr, this);
|
696 |
0
| checkForRoot = false;
|
697 |
| |
698 |
0
| new Graph(expr.getLeftOperand(), this);
|
699 |
0
| new Graph(expr.getRightOperand(), this);
|
700 |
| } |
701 |
| } |
702 |
| } |
703 |
| |
704 |
| |
705 |
| |
706 |
| |
707 |
| |
708 |
| |
709 |
0
| public void visitEquivalence(Equivalence expr) {
|
710 |
| |
711 |
0
| if (universalRight) {
|
712 |
0
| 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 |
0
| validDescription = false;
|
717 |
0
| universalRight = false;
|
718 |
| } |
719 |
0
| else if (existential) {
|
720 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
721 |
| "The ExistentialQuantifier may not contain a " + |
722 |
| "Equivalence:\n" + leSerializer.serialize(expr)); |
723 |
0
| validDescription = false;
|
724 |
0
| existential = false;
|
725 |
| } |
726 |
| else { |
727 |
0
| if (formula == true) {
|
728 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
729 |
| "Nested Implications are not allowed:\n" + |
730 |
| leSerializer.serialize(expr)); |
731 |
0
| validDescription = false;
|
732 |
0
| existential = false;
|
733 |
| } |
734 |
| else { |
735 |
0
| formula = true;
|
736 |
0
| validDescription = true;
|
737 |
0
| expr.getLeftOperand().accept(this);
|
738 |
0
| expr.getRightOperand().accept(this);
|
739 |
| } |
740 |
| |
741 |
0
| if (!validDescription) {
|
742 |
0
| addError(expr, ValidationError.AX_EQUIV_ERR + ":\n" +
|
743 |
| "Invalid Equivalence Formula:\n" + |
744 |
| leSerializer.serialize(expr)); |
745 |
| } |
746 |
| else { |
747 |
| |
748 |
| |
749 |
0
| checkForRoot = true;
|
750 |
0
| new Graph(expr, this);
|
751 |
0
| checkForRoot = false;
|
752 |
| |
753 |
0
| new Graph(expr.getLeftOperand(), this);
|
754 |
0
| new Graph(expr.getRightOperand(), this);
|
755 |
| } |
756 |
| } |
757 |
| } |
758 |
| |
759 |
| |
760 |
| |
761 |
| |
762 |
| |
763 |
| |
764 |
0
| public void visitLogicProgrammingRule(LogicProgrammingRule expr) {
|
765 |
| |
766 |
0
| if (universalRight) {
|
767 |
0
| 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 |
0
| validDescription = false;
|
772 |
0
| universalRight = false;
|
773 |
| } |
774 |
0
| else if (existential) {
|
775 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
776 |
| "The ExistentialQuantifier may not contain a " + |
777 |
| "LogicProgrammingRule:\n" + leSerializer.serialize(expr)); |
778 |
0
| validDescription = false;
|
779 |
0
| existential = false;
|
780 |
| } |
781 |
| else { |
782 |
0
| 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 |
0
| public void visitUniversalQuantification(UniversalQuantification expr) {
|
793 |
| |
794 |
0
| if (universalRight) {
|
795 |
0
| 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 |
0
| validDescription = false;
|
800 |
0
| universalRight = false;
|
801 |
| } |
802 |
| else { |
803 |
| |
804 |
0
| if (formula) {
|
805 |
0
| Vector operands = (Vector) expr.listOperands();
|
806 |
0
| if ((operands.size() == 1) && (operands.get(0) instanceof Implication)) {
|
807 |
0
| Implication imp = (Implication) operands.get(0);
|
808 |
0
| if (expr.listVariables().size() == 1) {
|
809 |
0
| isValidBMolecule(imp.getLeftOperand());
|
810 |
0
| imp.getRightOperand().accept(this);
|
811 |
| } |
812 |
| else { |
813 |
0
| if ((imp.getLeftOperand() instanceof Conjunction)
|
814 |
| || (imp.getLeftOperand() instanceof Negation) |
815 |
| || (imp.getLeftOperand() instanceof AttributeMolecule) |
816 |
| || (imp.getLeftOperand() instanceof MembershipMolecule)) { |
817 |
0
| imp.getLeftOperand().accept(this);
|
818 |
| } |
819 |
| else { |
820 |
0
| 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 |
0
| validDescription = false;
|
825 |
0
| return;
|
826 |
| } |
827 |
0
| if ((imp.getRightOperand() instanceof Disjunction)
|
828 |
| || (imp.getRightOperand() instanceof Negation) |
829 |
| || (imp.getRightOperand() instanceof BuiltInAtom)) { |
830 |
0
| universalRight = true;
|
831 |
0
| imp.getRightOperand().accept(this);
|
832 |
| } |
833 |
| else { |
834 |
0
| 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 |
0
| validDescription = false;
|
839 |
0
| return;
|
840 |
| } |
841 |
| } |
842 |
| } |
843 |
| else { |
844 |
0
| addError (expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
845 |
| "UniversalQuantification is only allowed with an " + |
846 |
| "implication as operand:\n" + leSerializer.serialize(expr)); |
847 |
0
| validDescription = false;
|
848 |
| } |
849 |
0
| if (graph) {
|
850 |
0
| checkGraph = true;
|
851 |
0
| Set <Variable> vs = expr.listVariables();
|
852 |
0
| Iterator it = vs.iterator();
|
853 |
0
| while (it.hasNext()) {
|
854 |
0
| Variable v = (Variable) it.next();
|
855 |
0
| if (!variables.contains(v)) {
|
856 |
0
| variables.add(v);
|
857 |
| } |
858 |
| } |
859 |
| } |
860 |
| } |
861 |
| else { |
862 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
863 |
| "UniversalQuantification is not allowed:\n" + leSerializer.serialize(expr)); |
864 |
0
| validDescription = false;
|
865 |
| } |
866 |
| } |
867 |
| } |
868 |
| |
869 |
| |
870 |
| |
871 |
| |
872 |
| |
873 |
| |
874 |
0
| public void visitExistentialQuantification(ExistentialQuantification expr) {
|
875 |
| |
876 |
0
| if (universalRight) {
|
877 |
0
| 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 |
0
| validDescription = false;
|
882 |
0
| universalRight = false;
|
883 |
| } |
884 |
| else { |
885 |
| |
886 |
0
| if (formula) {
|
887 |
0
| Vector operands = (Vector) expr.listOperands();
|
888 |
0
| int size = operands.size();
|
889 |
0
| for (int i=0; i<size; i++) {
|
890 |
0
| if (!(operands.get(i) instanceof Conjunction) &&
|
891 |
| !(operands.get(i) instanceof AttributeValueMoleculeImpl)) { |
892 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
893 |
| "ExistentialQuantifier is only allowed with " + |
894 |
| "conjunctions as operands:\n" + leSerializer.serialize(expr)); |
895 |
0
| validDescription = false;
|
896 |
0
| return;
|
897 |
| } |
898 |
| } |
899 |
0
| if (expr.listVariables().size() == 1) {
|
900 |
| |
901 |
0
| bMol = false;
|
902 |
0
| if (operands.get(0) instanceof Conjunction) {
|
903 |
0
| ((Conjunction) operands.get(0)).getLeftOperand().accept(this);
|
904 |
| } |
905 |
| else { |
906 |
0
| ((LogicalExpression) operands.get(0)).accept(this);
|
907 |
| } |
908 |
0
| if (!graph && !bMol) {
|
909 |
0
| 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 |
0
| if (operands.get(0) instanceof Conjunction) {
|
915 |
0
| ((Conjunction) operands.get(0)).getRightOperand().accept(this);
|
916 |
| } |
917 |
| } |
918 |
| else { |
919 |
0
| existential = true;
|
920 |
0
| for (int i=0; i<size; i++) {
|
921 |
0
| ((Conjunction) operands.get(i)).getLeftOperand().accept(this);
|
922 |
0
| ((Conjunction) operands.get(i)).getRightOperand().accept(this);
|
923 |
| } |
924 |
| } |
925 |
0
| if (graph) {
|
926 |
0
| checkGraph = true;
|
927 |
0
| Set <Variable> vs = expr.listVariables();
|
928 |
0
| Iterator it = vs.iterator();
|
929 |
0
| while (it.hasNext()) {
|
930 |
0
| Variable v = (Variable) it.next();
|
931 |
0
| if (!variables.contains(v)) {
|
932 |
0
| variables.add(v);
|
933 |
| } |
934 |
| } |
935 |
| } |
936 |
| } |
937 |
| else { |
938 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":\n" +
|
939 |
| "ExistentialQuantifier is not allowed:\n" + leSerializer.serialize(expr)); |
940 |
0
| validDescription = false;
|
941 |
| } |
942 |
| } |
943 |
| } |
944 |
| |
945 |
| |
946 |
| |
947 |
| |
948 |
0
| private Molecule atomToMolecule(Atom expr) {
|
949 |
0
| Molecule molecule = null;
|
950 |
| |
951 |
0
| if (expr.getArity() != 2) {
|
952 |
0
| addError(expr, ValidationError.AX_ATOMIC_ERR + ":\nThe atom must " +
|
953 |
| "be a binary atom\n" + leSerializer.serialize(expr)); |
954 |
0
| return molecule;
|
955 |
| } |
956 |
| else { |
957 |
0
| molecule = leFactory.createAttributeValue(
|
958 |
| expr.getParameter(0), expr.getIdentifier(), expr.getParameter(1)); |
959 |
0
| return molecule;
|
960 |
| } |
961 |
| } |
962 |
| |
963 |
| |
964 |
| |
965 |
| |
966 |
0
| private void isValidBMolecule(LogicalExpression le) {
|
967 |
0
| if (universalRight) {
|
968 |
0
| 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 |
0
| validDescription = false;
|
973 |
0
| universalRight = false;
|
974 |
| } |
975 |
| else { |
976 |
0
| AttributeValueMolecule expr = null;
|
977 |
0
| if (le instanceof Atom) {
|
978 |
0
| le = atomToMolecule((Atom) le);
|
979 |
0
| if (le == null) {
|
980 |
0
| validDescription = false;
|
981 |
| } |
982 |
| } |
983 |
0
| if (le instanceof AttributeValueMolecule) {
|
984 |
0
| expr = (AttributeValueMolecule) le;
|
985 |
| |
986 |
| |
987 |
0
| if (!(expr.getLeftParameter() instanceof Variable)) {
|
988 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ":"
|
989 |
| + "\nThe argument must be a Variable\n" |
990 |
| + leSerializer.serialize(expr)); |
991 |
0
| validDescription = false;
|
992 |
| } |
993 |
| |
994 |
0
| if (check(expr.getAttribute(), true, true, false, true, true)) {
|
995 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ": The " +
|
996 |
| "attribute name must be a relation\n" + leSerializer.serialize(expr)); |
997 |
0
| validDescription = false;
|
998 |
| } |
999 |
| |
1000 |
0
| if (!(expr.getRightParameter() instanceof Variable)) {
|
1001 |
0
| addError(expr, ValidationError.AX_FORMULA_ERR + ": The " +
|
1002 |
| "attribute's arguments must be variables\n" + leSerializer.serialize(expr)); |
1003 |
0
| validDescription = false;
|
1004 |
| } |
1005 |
| |
1006 |
0
| if (graph) {
|
1007 |
0
| checkGraph = true;
|
1008 |
0
| if (!variables.contains(expr.getLeftParameter())) {
|
1009 |
0
| variables.add(expr.getLeftParameter());
|
1010 |
| } |
1011 |
0
| if (!variables.contains(expr.getRightParameter())) {
|
1012 |
0
| variables.add(expr.getRightParameter());
|
1013 |
| } |
1014 |
0
| List <Term> list = new Vector <Term> ();
|
1015 |
0
| list.add(expr.getLeftParameter());
|
1016 |
0
| if (!expr.getLeftParameter().equals(expr.getRightParameter())) {
|
1017 |
0
| list.add(expr.getRightParameter());
|
1018 |
| } |
1019 |
0
| Iterator it = molecules.iterator();
|
1020 |
0
| while (it.hasNext()) {
|
1021 |
0
| List l = (List) it.next();
|
1022 |
0
| if ((l.get(0).equals(expr.getLeftParameter())) &&
|
1023 |
| (l.get(1).equals(expr.getRightParameter()))) { |
1024 |
0
| return;
|
1025 |
| } |
1026 |
| } |
1027 |
0
| numberOfMolecules = numberOfMolecules + 1;
|
1028 |
0
| molecules.add(list);
|
1029 |
| } |
1030 |
0
| bMol = true;
|
1031 |
| } |
1032 |
| else { |
1033 |
0
| addError(le, ValidationError.AX_FORMULA_ERR + ": This b-molecule" +
|
1034 |
| " must be an atom or an AttributeValueMolecule" + |
1035 |
| leSerializer.serialize(le)); |
1036 |
0
| validDescription = false;
|
1037 |
| } |
1038 |
| } |
1039 |
| } |
1040 |
| |
1041 |
| |
1042 |
| |
1043 |
| |
1044 |
| |
1045 |
0
| private boolean isValidTransitiveInvImpl(InverseImplication expr) {
|
1046 |
0
| AttributeValueMolecule left, conjunctionLeft, conjunctionRight;
|
1047 |
| |
1048 |
| |
1049 |
0
| if (expr.getLeftOperand() instanceof Atom) {
|
1050 |
0
| left = (AttributeValueMolecule) atomToMolecule((Atom) expr.getLeftOperand());
|
1051 |
| } |
1052 |
| else { |
1053 |
0
| left = (AttributeValueMolecule) expr.getLeftOperand();
|
1054 |
| } |
1055 |
0
| if (((Conjunction) expr.getRightOperand()).getLeftOperand() instanceof Atom) {
|
1056 |
0
| conjunctionLeft = (AttributeValueMolecule) atomToMolecule((Atom)
|
1057 |
| ((Conjunction) expr.getRightOperand()).getLeftOperand()); |
1058 |
| } |
1059 |
| else { |
1060 |
0
| conjunctionLeft = (AttributeValueMolecule) (
|
1061 |
| (Conjunction) expr.getRightOperand()).getLeftOperand(); |
1062 |
| } |
1063 |
0
| if (((Conjunction) expr.getRightOperand()).getRightOperand() instanceof Atom) {
|
1064 |
0
| conjunctionRight = (AttributeValueMolecule) atomToMolecule((Atom)
|
1065 |
| ((Conjunction) expr.getRightOperand()).getRightOperand()); |
1066 |
| } |
1067 |
| else { |
1068 |
0
| conjunctionRight = (AttributeValueMolecule) ((Conjunction) expr.getRightOperand()).getRightOperand();
|
1069 |
| } |
1070 |
| |
1071 |
0
| Variable leftVariable = (Variable) left.getLeftParameter();
|
1072 |
0
| Variable conjunctionLeftVariable = (Variable) conjunctionLeft.getLeftParameter();
|
1073 |
0
| Variable conjunctionRightVariable = (Variable) conjunctionRight.getLeftParameter();
|
1074 |
0
| Term leftRelation = left.getAttribute();
|
1075 |
0
| Term conjunctionLeftRelation = conjunctionLeft.getAttribute();
|
1076 |
0
| Term conjunctionRightRelation = conjunctionRight.getAttribute();
|
1077 |
0
| Variable leftArgument = (Variable) left.getRightParameter();
|
1078 |
0
| Variable conjunctionLeftArgument = (Variable) conjunctionLeft.getRightParameter();
|
1079 |
0
| Variable conjunctionRightArgument = (Variable) conjunctionRight.getRightParameter();
|
1080 |
| |
1081 |
| |
1082 |
0
| if (leftVariable.equals(conjunctionLeftVariable)
|
1083 |
| && leftVariable.equals(conjunctionRightVariable)) { |
1084 |
0
| return false;
|
1085 |
| } |
1086 |
0
| else if (!(leftRelation.equals(conjunctionLeftRelation))
|
1087 |
| || !(leftRelation.equals(conjunctionRightRelation))) { |
1088 |
0
| return false;
|
1089 |
| } |
1090 |
0
| else if (leftVariable.equals(conjunctionLeftVariable)) {
|
1091 |
0
| if (!(leftArgument.equals(conjunctionRightArgument))
|
1092 |
| || !(conjunctionLeftArgument.equals(conjunctionRightVariable))) { |
1093 |
0
| return false;
|
1094 |
| } |
1095 |
| } |
1096 |
0
| else if (leftVariable.equals(conjunctionRightVariable)) {
|
1097 |
0
| if (!(leftArgument.equals(conjunctionLeftArgument))
|
1098 |
| || !(conjunctionRightArgument.equals(conjunctionLeftVariable))) { |
1099 |
0
| return false;
|
1100 |
| } |
1101 |
| } |
1102 |
0
| return true;
|
1103 |
| } |
1104 |
| |
1105 |
| |
1106 |
| |
1107 |
| |
1108 |
| |
1109 |
| |
1110 |
0
| private boolean isValidInverseImplication(InverseImplication expr) {
|
1111 |
0
| AttributeValueMolecule left = null;
|
1112 |
0
| AttributeValueMolecule right = null;
|
1113 |
| |
1114 |
| |
1115 |
0
| if (expr.getLeftOperand() instanceof Atom) {
|
1116 |
0
| left = (AttributeValueMolecule) atomToMolecule((Atom) expr.getLeftOperand());
|
1117 |
| } |
1118 |
| else { |
1119 |
0
| left = (AttributeValueMolecule) expr.getLeftOperand();
|
1120 |
| } |
1121 |
0
| if (expr.getRightOperand() instanceof Atom) {
|
1122 |
0
| right = (AttributeValueMolecule) atomToMolecule((Atom) expr.getRightOperand());
|
1123 |
| } |
1124 |
| else { |
1125 |
0
| right = (AttributeValueMolecule) expr.getRightOperand();
|
1126 |
| } |
1127 |
0
| if (left == null || right == null) {
|
1128 |
0
| return false;
|
1129 |
| } |
1130 |
| else { |
1131 |
0
| Variable leftVariable = (Variable) left.getLeftParameter();
|
1132 |
0
| Variable rightVariable = (Variable) right.getLeftParameter();
|
1133 |
0
| Term leftRelation = left.getAttribute();
|
1134 |
0
| Term rightRelation = right.getAttribute();
|
1135 |
0
| Variable leftArgument = (Variable) left.getRightParameter();
|
1136 |
0
| Variable rightArgument = (Variable) right.getRightParameter();
|
1137 |
| |
1138 |
| |
1139 |
0
| if (!(leftVariable.equals(rightArgument)) || !(leftArgument.equals(rightVariable))) {
|
1140 |
| |
1141 |
| |
1142 |
0
| if (!(leftVariable.equals(rightVariable)) || !(leftArgument.equals(rightArgument))
|
1143 |
| || leftRelation.equals(rightRelation)) { |
1144 |
0
| return false;
|
1145 |
| } |
1146 |
| } |
1147 |
0
| return true;
|
1148 |
| } |
1149 |
| } |
1150 |
| |
1151 |
| |
1152 |
| |
1153 |
| |
1154 |
| |
1155 |
0
| private boolean check(Object o, boolean concept, boolean instance,
|
1156 |
| boolean relation, boolean datatype, boolean variable) { |
1157 |
0
| if (o instanceof Molecule) {
|
1158 |
0
| if (concept && checkConcepts(((Molecule) o).getLeftParameter())) {
|
1159 |
0
| error = "Concept";
|
1160 |
0
| return true;
|
1161 |
| } |
1162 |
0
| if (instance && checkInstances(((Molecule) o).getLeftParameter())) {
|
1163 |
0
| error = "Instance";
|
1164 |
0
| return true;
|
1165 |
| } |
1166 |
0
| else if (relation && checkRelations(((Molecule) o).getLeftParameter())) {
|
1167 |
0
| error = "Relation";
|
1168 |
0
| return true;
|
1169 |
| } |
1170 |
0
| else if (datatype && checkDatatypes(((Molecule) o).getLeftParameter())) {
|
1171 |
0
| error = "Datatype";
|
1172 |
0
| return true;
|
1173 |
| } |
1174 |
0
| else if (variable && (((Molecule) o).getLeftParameter() instanceof Variable)) {
|
1175 |
0
| error = "Variable";
|
1176 |
0
| return true;
|
1177 |
| } |
1178 |
| } |
1179 |
0
| else if (o instanceof Term) {
|
1180 |
0
| if (concept && checkConcepts(o)) {
|
1181 |
0
| error = "Concept";
|
1182 |
| } |
1183 |
0
| if (instance && checkInstances(o)) {
|
1184 |
0
| error = "Instance";
|
1185 |
0
| return true;
|
1186 |
| } |
1187 |
0
| else if (relation && checkRelations(o)) {
|
1188 |
0
| error = "Relation";
|
1189 |
0
| return true;
|
1190 |
| } |
1191 |
0
| else if (datatype && checkDatatypes(o)) {
|
1192 |
0
| error = "Datatype";
|
1193 |
0
| return true;
|
1194 |
| } |
1195 |
0
| else if (variable && (o instanceof Variable)) {
|
1196 |
0
| error = "Variable";
|
1197 |
0
| return true;
|
1198 |
| } |
1199 |
| } |
1200 |
0
| return false;
|
1201 |
| } |
1202 |
| |
1203 |
| |
1204 |
| |
1205 |
| |
1206 |
0
| private boolean checkConcepts(Object o) {
|
1207 |
0
| return validator.getIdConcepts().contains(o);
|
1208 |
| } |
1209 |
| |
1210 |
| |
1211 |
| |
1212 |
| |
1213 |
0
| private boolean checkInstances(Object o) {
|
1214 |
0
| return validator.getIdInstances().contains(o);
|
1215 |
| } |
1216 |
| |
1217 |
| |
1218 |
| |
1219 |
| |
1220 |
0
| private boolean checkRelations(Object o) {
|
1221 |
0
| return validator.getIdRelations().contains(o);
|
1222 |
| } |
1223 |
| |
1224 |
| |
1225 |
| |
1226 |
| |
1227 |
0
| private boolean checkAbstractRelations(Object o) {
|
1228 |
0
| return validator.getIdAbstractRelations().contains(o);
|
1229 |
| } |
1230 |
| |
1231 |
| |
1232 |
| |
1233 |
| |
1234 |
0
| private boolean checkConcreteRelations(Object o) {
|
1235 |
0
| return validator.getIdConcreteRelations().contains(o);
|
1236 |
| } |
1237 |
| |
1238 |
| |
1239 |
| |
1240 |
| |
1241 |
0
| private boolean checkDatatypes(Object o) {
|
1242 |
0
| return ConstantTransformer.getInstance().isDataType(o.toString());
|
1243 |
| } |
1244 |
| |
1245 |
0
| public Set getMolecules() {
|
1246 |
0
| return molecules;
|
1247 |
| } |
1248 |
| |
1249 |
0
| public int getNumberOfMolecules() {
|
1250 |
0
| return numberOfMolecules;
|
1251 |
| } |
1252 |
| |
1253 |
0
| public Set getVariables() {
|
1254 |
0
| return variables;
|
1255 |
| } |
1256 |
| |
1257 |
0
| public Variable getRoot() {
|
1258 |
0
| return root;
|
1259 |
| } |
1260 |
| |
1261 |
0
| protected void setGraph(boolean graph) {
|
1262 |
0
| this.graph = graph;
|
1263 |
0
| checkGraph = false;
|
1264 |
0
| variables = new HashSet <Term> ();
|
1265 |
0
| molecules = new HashSet <List <Term>> ();
|
1266 |
0
| numberOfMolecules = 0;
|
1267 |
| } |
1268 |
| |
1269 |
| |
1270 |
| |
1271 |
| |
1272 |
0
| private void addError(LogicalExpression logexp, String msg) {
|
1273 |
0
| LogicalExpressionErrorImpl le = new LogicalExpressionErrorImpl(
|
1274 |
| axiom, logexp, msg, WSML.WSML_DL); |
1275 |
0
| if (!errors.contains(le)) {
|
1276 |
0
| 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 |
0
| public Graph(LogicalExpression expr, WsmlDLExpressionValidator exprVal) {
|
1290 |
0
| this.expr = expr;
|
1291 |
0
| this.exprVal = exprVal;
|
1292 |
0
| if (checkForRoot) {
|
1293 |
0
| root = null;
|
1294 |
0
| leftVariables.clear();
|
1295 |
0
| rightVariables.clear();
|
1296 |
0
| exprVal.setGraph(true);
|
1297 |
0
| hasRootVariable();
|
1298 |
| } |
1299 |
0
| else if (!quantifier){
|
1300 |
0
| exprVal.setGraph(true);
|
1301 |
0
| isValidGraph();
|
1302 |
| } |
1303 |
| } |
1304 |
| |
1305 |
| |
1306 |
| |
1307 |
| |
1308 |
| |
1309 |
0
| public boolean hasRootVariable() {
|
1310 |
0
| ((Binary) expr).getLeftOperand().accept(exprVal);
|
1311 |
0
| Iterator <Term> it = variables.iterator();
|
1312 |
0
| while (it.hasNext()) {
|
1313 |
0
| leftVariables.add(it.next());
|
1314 |
| } |
1315 |
0
| variables.clear();
|
1316 |
0
| ((Binary) expr).getRightOperand().accept(exprVal);
|
1317 |
0
| it = variables.iterator();
|
1318 |
0
| while (it.hasNext()) {
|
1319 |
0
| rightVariables.add(it.next());
|
1320 |
| } |
1321 |
0
| variables.clear();
|
1322 |
0
| Iterator leftIt = leftVariables.iterator();
|
1323 |
0
| while (leftIt.hasNext()) {
|
1324 |
0
| Variable v = (Variable) leftIt.next();
|
1325 |
0
| if (rightVariables.contains(v)) {
|
1326 |
0
| root = v;
|
1327 |
| } |
1328 |
| } |
1329 |
0
| if (root == null && !noRoot) {
|
1330 |
0
| 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 |
0
| return false;
|
1334 |
| } |
1335 |
0
| return true;
|
1336 |
| } |
1337 |
| |
1338 |
| |
1339 |
| |
1340 |
| |
1341 |
| |
1342 |
0
| protected boolean isValidGraph() {
|
1343 |
0
| listMap.clear();
|
1344 |
0
| connected.clear();
|
1345 |
| |
1346 |
| |
1347 |
0
| expr.accept(exprVal);
|
1348 |
0
| if ((!variables.isEmpty()) && checkGraph) {
|
1349 |
0
| buildLists();
|
1350 |
| |
1351 |
0
| Iterator it = variables.iterator();
|
1352 |
0
| Variable v1 = (Variable) it.next();
|
1353 |
0
| Variable v = null;
|
1354 |
0
| boolean valid = false;
|
1355 |
| |
1356 |
| |
1357 |
0
| while(it.hasNext()) {
|
1358 |
0
| v = (Variable) it.next();
|
1359 |
0
| connected.clear();
|
1360 |
0
| valid = checkGraphConnected(v1, v);
|
1361 |
0
| if (!valid) {
|
1362 |
0
| addError(expr, ValidationError.AX_GRAPH_ERR + ":\nGraph is " +
|
1363 |
| "not connected:\n" + leSerializer.serialize(expr)); |
1364 |
0
| return false;
|
1365 |
| } |
1366 |
| } |
1367 |
| |
1368 |
| |
1369 |
0
| List <Variable> checkList = new Vector <Variable> ();
|
1370 |
0
| checkList.add(v1);
|
1371 |
0
| valid = checkGraphAcyclic(v1, v1, checkList);
|
1372 |
0
| if (valid) {
|
1373 |
0
| return true;
|
1374 |
| } |
1375 |
| else { |
1376 |
0
| addError(expr, ValidationError.AX_GRAPH_ERR + ":\nGraph contains " +
|
1377 |
| "cycle:\n" + leSerializer.serialize(expr)); |
1378 |
0
| return false;
|
1379 |
| } |
1380 |
| } |
1381 |
0
| return true;
|
1382 |
| } |
1383 |
| |
1384 |
| |
1385 |
| |
1386 |
| |
1387 |
| |
1388 |
0
| private void buildLists() {
|
1389 |
0
| Variable v1 = null;
|
1390 |
0
| Variable v = null;
|
1391 |
| |
1392 |
0
| Iterator <Term> it = variables.iterator();
|
1393 |
0
| while (it.hasNext()) {
|
1394 |
0
| List <Term> list = new Vector <Term> ();
|
1395 |
0
| v1 = (Variable) it.next();
|
1396 |
0
| Iterator <List <Term>> itMol = molecules.iterator();
|
1397 |
0
| while (itMol.hasNext()) {
|
1398 |
0
| List <Term> l = itMol.next();
|
1399 |
0
| if (l.get(0).equals(v1)) {
|
1400 |
0
| v = (Variable) l.get(1);
|
1401 |
0
| list.add(v);
|
1402 |
| } |
1403 |
0
| else if (l.get(1).equals(v1)) {
|
1404 |
0
| v = (Variable) l.get(0);
|
1405 |
0
| list.add(v);
|
1406 |
| } |
1407 |
| } |
1408 |
0
| listMap.put(v1, list);
|
1409 |
| } |
1410 |
| } |
1411 |
| |
1412 |
| |
1413 |
| |
1414 |
| |
1415 |
0
| private boolean checkGraphConnected(Variable v1, Variable v2) {
|
1416 |
0
| boolean found = false;
|
1417 |
0
| boolean used = false;
|
1418 |
| |
1419 |
0
| List <Term> l = listMap.get(v1);
|
1420 |
| |
1421 |
0
| if (l.contains(v2)) {
|
1422 |
0
| return true;
|
1423 |
| } |
1424 |
| else { |
1425 |
0
| connected.add(v1);
|
1426 |
| |
1427 |
0
| Iterator it = l.iterator();
|
1428 |
0
| while (it.hasNext()) {
|
1429 |
0
| Variable v = (Variable) it.next();
|
1430 |
0
| for (int i=0; i<connected.size(); i++) {
|
1431 |
0
| if (v.equals(connected.get(i))) {
|
1432 |
0
| used = true;
|
1433 |
| } |
1434 |
| } |
1435 |
0
| if (!used) {
|
1436 |
0
| found = checkGraphConnected(v, v2);
|
1437 |
| } |
1438 |
0
| if (found) {
|
1439 |
0
| return true;
|
1440 |
| } |
1441 |
0
| used = false;
|
1442 |
| } |
1443 |
0
| return false;
|
1444 |
| } |
1445 |
| } |
1446 |
| |
1447 |
| |
1448 |
| |
1449 |
| |
1450 |
0
| private boolean checkGraphAcyclic(Variable from, Variable v, List checkList) {
|
1451 |
0
| if ((numberOfMolecules + 1) == variables.size()) {
|
1452 |
0
| return true;
|
1453 |
| } |
1454 |
| else { |
1455 |
0
| return false;
|
1456 |
| } |
1457 |
| } |
1458 |
| } |
1459 |
| } |