1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16 package org.deri.wsmo4j.validator;
17
18 import java.util.*;
19
20 import org.deri.wsmo4j.io.serializer.wsml.LogExprSerializerWSML;
21 import org.omwg.logicalexpression.*;
22 import org.omwg.logicalexpression.terms.Term;
23 import org.omwg.ontology.*;
24 import org.wsmo.common.*;
25 import org.wsmo.factory.*;
26 import org.wsmo.validator.ValidationError;
27
28
29
30
31
32
33 public class WsmlFlightExpressionValidator implements Visitor {
34
35 private LogExprSerializerWSML leSerializer = null;
36
37 private LogicalExpressionFactory leFactory = null;
38
39 private WsmlFullValidator validator = null;
40
41 private Axiom axiom = null;
42
43 private List <ValidationError> errors = null;
44
45 private boolean body = false;
46
47 private boolean found = false;
48
49 private boolean builtIn = false;
50
51 private boolean foundBuiltIn = false;
52
53 private boolean foundNaf = false;
54
55 private boolean unSafe = false;
56
57 private boolean foundPos = false;
58
59 private String errorMessage = "";
60
61
62
63
64
65
66
67
68 protected WsmlFlightExpressionValidator(Axiom axiom, LogicalExpressionFactory leFactory, List <ValidationError> errors, WsmlFullValidator val) {
69 this.axiom = axiom;
70 this.errors = errors;
71 this.validator = val;
72 leSerializer = validator.leSerializer;
73 this.leFactory = leFactory;
74 }
75
76 public void setup() {
77 body = false;
78 found = false;
79 foundBuiltIn = false;
80 builtIn = false;
81 foundNaf = false;
82 foundPos = false;
83 }
84
85
86
87
88
89
90 public void visitAtom(Atom expr) {
91 if (!body) {
92 containsVariables(expr);
93 }
94 }
95
96
97
98
99
100
101 public void visitAttributeContraintMolecule(AttributeConstraintMolecule expr) {
102 if (!body) {
103 containsVariables(expr);
104 }
105 }
106
107
108
109
110
111
112 public void visitAttributeInferenceMolecule(AttributeInferenceMolecule expr) {
113 if (!body) {
114 containsVariables(expr);
115 }
116 }
117
118
119
120
121
122
123 public void visitAttributeValueMolecule(AttributeValueMolecule expr) {
124 if (!body) {
125 containsVariables(expr);
126 }
127 }
128
129
130
131
132
133
134 public void visitCompoundMolecule(CompoundMolecule expr) {
135 if (!body) {
136 containsVariables(expr);
137 }
138 }
139
140
141
142
143
144
145 public void visitMemberShipMolecule(MembershipMolecule expr) {
146 if (!body) {
147 containsVariables(expr);
148 }
149 }
150
151
152
153
154
155
156 public void visitSubConceptMolecule(SubConceptMolecule expr) {
157 if (!body) {
158 containsVariables(expr);
159 }
160 }
161
162
163
164
165
166
167
168 public void visitNegation(Negation expr) {
169
170 }
171
172
173
174
175
176
177 public void visitNegationAsFailure(NegationAsFailure expr) {
178 if (body) {
179 expr.getOperand().accept(this);
180 }
181 }
182
183
184
185
186
187
188 public void visitConstraint(Constraint expr) {
189
190 }
191
192
193
194
195
196
197 public void visitConjunction(Conjunction expr) {
198 if (body) {
199 expr.getLeftOperand().accept(this);
200 expr.getRightOperand().accept(this);
201 }
202 }
203
204
205
206
207
208
209 public void visitDisjunction(Disjunction expr) {
210 if (body) {
211 expr.getLeftOperand().accept(this);
212 expr.getRightOperand().accept(this);
213 }
214 }
215
216
217
218
219
220
221 public void visitInverseImplication(InverseImplication expr) {
222 if (body) {
223 addError(expr, ValidationError.AX_BODY_ERR + ": Must not " +
224 "contain an InverseImplication:\n" + leSerializer.serialize(expr));
225 body = false;
226 }
227 }
228
229
230
231
232
233
234 public void visitImplication(Implication expr) {
235 if (body) {
236 addError(expr, ValidationError.AX_BODY_ERR + ": Must not " +
237 "contain an Implication:\n" + leSerializer.serialize(expr));
238 body = false;
239 }
240 }
241
242
243
244
245
246
247 public void visitEquivalence(Equivalence expr) {
248 if (body) {
249 addError(expr, ValidationError.AX_BODY_ERR + ": Must not " +
250 "contain an Equivalence:\n" + leSerializer.serialize(expr));
251 body = false;
252 }
253 }
254
255
256
257
258
259
260 public void visitLogicProgrammingRule(LogicProgrammingRule expr) {
261 body = true;
262 expr.getRightOperand().accept(this);
263 holdsSafetyCondition(expr);
264 }
265
266
267
268
269
270
271 public void visitUniversalQuantification(UniversalQuantification expr) {
272 if (body) {
273 addError(expr, ValidationError.AX_BODY_ERR + ": Must not " +
274 "contain a UniversalQuantification:\n" + leSerializer.serialize(expr));
275 body = false;
276 }
277 }
278
279
280
281
282
283
284 public void visitExistentialQuantification(ExistentialQuantification expr) {
285 if (body) {
286 addError(expr, ValidationError.AX_BODY_ERR + ": Must not " +
287 "contain an ExistentialQuantification:\n" + leSerializer.serialize(expr));
288 body = false;
289 }
290 }
291
292 private boolean containsVariables(LogicalExpression expr) {
293 boolean flag = false;
294 if (expr instanceof CompoundMolecule) {
295 if (!((CompoundMolecule) expr).listAttributeConstraintMolecules().isEmpty()) {
296 Iterator it = ((CompoundMolecule) expr).listAttributeConstraintMolecules().iterator();
297 while (it.hasNext()) {
298 containsVariables((AttributeConstraintMolecule) it.next());
299 }
300 }
301 else if (!((CompoundMolecule) expr).listAttributeInferenceMolecules().isEmpty()) {
302 Iterator it = ((CompoundMolecule) expr).listAttributeInferenceMolecules().iterator();
303 while (it.hasNext()) {
304 containsVariables((AttributeInferenceMolecule) it.next());
305 }
306 }
307 else if (!((CompoundMolecule) expr).listAttributeValueMolecules().isEmpty()) {
308 Iterator it = ((CompoundMolecule) expr).listAttributeValueMolecules().iterator();
309 while (it.hasNext()) {
310 containsVariables((AttributeValueMolecule) it.next());
311 }
312 }
313 else if (!((CompoundMolecule) expr).listMemberShipMolecules().isEmpty()) {
314 Iterator it = ((CompoundMolecule) expr).listMemberShipMolecules().iterator();
315 while (it.hasNext()) {
316 containsVariables((MembershipMolecule) it.next());
317 }
318 }
319 else if (!((CompoundMolecule) expr).listSubConceptMolecules().isEmpty()) {
320 Iterator it = ((CompoundMolecule) expr).listSubConceptMolecules().iterator();
321 while (it.hasNext()) {
322 containsVariables((SubConceptMolecule) it.next());
323 }
324 }
325 }
326 else if (expr instanceof Molecule) {
327 if (((Molecule) expr).getLeftParameter() instanceof Variable) {
328 flag = true;
329 }
330 if (((Molecule) expr).getRightParameter() instanceof Variable) {
331 flag = true;
332 }
333 }
334 else if (expr instanceof Atom) {
335 Iterator it = ((Atom) expr).listParameters().iterator();
336 while (it.hasNext()) {
337 if (it.next() instanceof Variable) {
338 flag = true;
339 }
340 }
341 }
342 if (flag) {
343 addError(expr, ValidationError.AX_HEAD_ERR + ":\n Any variable-free " +
344 "admissible head formula is an admissible formula:\n" +
345 leSerializer.serialize(expr));
346 return false;
347 }
348 return true;
349 }
350
351 private void holdsSafetyCondition(LogicProgrammingRule l) {
352 LogicalExpression leL = l.getLeftOperand();
353 LogicalExpression leR = l.getRightOperand();
354 if (leL instanceof Conjunction) {
355 transformHeadConjunction(l);
356 }
357 else if (leL instanceof Equivalence) {
358 transformHeadEquivalence(l);
359 }
360 else if (leL instanceof Implication) {
361 transformHeadImplication(l);
362 }
363 else if (leL instanceof InverseImplication) {
364 transformHeadInverseImplication(l);
365 }
366 else if (leR instanceof Disjunction) {
367 transformBody(l);
368 }
369 else {
370 isSafe(l);
371 }
372 }
373
374 private void transformHeadInverseImplication(LogicProgrammingRule l) {
375 LogicProgrammingRule lpr;
376 Conjunction c;
377 c = leFactory.createConjunction(((Binary) l.getLeftOperand()).getRightOperand(),
378 l.getRightOperand());
379 lpr = leFactory.createLogicProgrammingRule(((Binary) l.getLeftOperand()).getLeftOperand(),
380 c);
381 holdsSafetyCondition(lpr);
382 }
383
384 private void transformHeadImplication(LogicProgrammingRule l) {
385 LogicProgrammingRule lpr;
386 Conjunction c;
387 c = leFactory.createConjunction(((Binary) l.getLeftOperand()).getLeftOperand(),
388 l.getRightOperand());
389 lpr = leFactory.createLogicProgrammingRule(((Binary) l.getLeftOperand()).getRightOperand(),
390 c);
391 holdsSafetyCondition(lpr);
392 }
393
394 private void transformHeadEquivalence(LogicProgrammingRule l) {
395 LogicProgrammingRule lpr1;
396 LogicProgrammingRule lpr2;
397 Implication i;
398 InverseImplication ini;
399 i = leFactory.createImplication(((Binary) l.getLeftOperand()).getLeftOperand(),
400 ((Binary) l.getLeftOperand()).getRightOperand());
401 ini = leFactory.createInverseImplication(((Binary) l.getLeftOperand()).getLeftOperand(),
402 ((Binary) l.getLeftOperand()).getRightOperand());
403 lpr1 = leFactory.createLogicProgrammingRule(i, l.getRightOperand());
404 lpr2 = leFactory.createLogicProgrammingRule(ini, l.getRightOperand());
405 holdsSafetyCondition(lpr1);
406 holdsSafetyCondition(lpr2);
407 }
408
409 private void transformHeadConjunction(LogicProgrammingRule l) {
410 LogicProgrammingRule lpr1;
411 LogicProgrammingRule lpr2;
412 lpr1 = leFactory.createLogicProgrammingRule(((Binary) l.getLeftOperand()).getLeftOperand(),
413 l.getRightOperand());
414 lpr2 = leFactory.createLogicProgrammingRule(
415 ((Binary) l.getLeftOperand()).getRightOperand(), l.getRightOperand());
416 holdsSafetyCondition(lpr1);
417 holdsSafetyCondition(lpr2);
418 }
419
420 private void transformBody(LogicProgrammingRule l) {
421 LogicProgrammingRule lpr1;
422 LogicProgrammingRule lpr2;
423 lpr1 = leFactory.createLogicProgrammingRule(l.getLeftOperand(), ((Disjunction) l
424 .getRightOperand()).getLeftOperand());
425 lpr2 = leFactory.createLogicProgrammingRule(l.getLeftOperand(), ((Disjunction) l
426 .getRightOperand()).getRightOperand());
427 holdsSafetyCondition(lpr1);
428 holdsSafetyCondition(lpr2);
429 }
430
431 private void isSafe(LogicProgrammingRule l) {
432 found = false;
433 foundPos = false;
434 LogicalExpression ll = l.getLeftOperand();
435 LogicalExpression lr = l.getRightOperand();
436 HashSet <Term> leftSet = new HashSet <Term> ();
437 leftSet = getSetOfHeadVariables(ll, leftSet);
438 if (!leftSet.isEmpty()) {
439 Iterator it = leftSet.iterator();
440 while (it.hasNext()) {
441 Variable v = (Variable) it.next();
442 checkBodyVariables(lr, v, false);
443 if (unSafe) {
444 addError(l, ValidationError.AX_SAFETY_COND + ": " +
445 "\nError: " + errorMessage + ":\n" +
446 leSerializer.serialize(l));
447 }
448 }
449 }
450 }
451
452 private HashSet <Term> getSetOfHeadVariables(LogicalExpression le, HashSet <Term> set) {
453 if (le instanceof Atom) {
454 for (int i = 0; i < ((Atom) le).getArity(); i++) {
455 if (((Atom) le).getParameter(i) instanceof Variable) {
456 set.add(((Atom) le).getParameter(i));
457 }
458 }
459 }
460 else if (le instanceof CompoundMolecule) {
461 Iterator i = ((CompoundMolecule) le).listOperands().iterator();
462 while (i.hasNext()) {
463 getSetOfHeadVariables((Molecule) i.next(), set);
464 }
465 }
466 else if (le instanceof Molecule) {
467 if (((Molecule) le).getLeftParameter() instanceof Variable) {
468 set.add(((Molecule) le).getLeftParameter());
469 }
470 if (((Molecule) le).getRightParameter() instanceof Variable) {
471 set.add(((Molecule) le).getRightParameter());
472 }
473 if (le instanceof AttributeMolecule) {
474 if (((AttributeMolecule) le).getAttribute() instanceof Variable) {
475 set.add(((AttributeMolecule) le).getAttribute());
476 }
477 }
478 }
479 return set;
480 }
481
482 private void checkBodyVariables(LogicalExpression le, Variable v, boolean naf) {
483 unSafe = false;
484 if (le instanceof Conjunction) {
485 LogicalExpression ll = ((Conjunction) le).getLeftOperand();
486 LogicalExpression lr = ((Conjunction) le).getRightOperand();
487 checkBodyVariables(ll, v, false);
488 checkBodyVariables(lr, v, false);
489 }
490 else if (le instanceof NegationAsFailure) {
491 LogicalExpression l = ((NegationAsFailure) le).getOperand();
492 if (!foundNaf) {
493 foundNaf = true;
494 checkBodyVariables(l, v, true);
495 }
496 else {
497 foundNaf = false;
498 checkBodyVariables(l, v, false);
499 }
500
501 }
502 else {
503 if (le instanceof Atom) {
504 if (le instanceof BuiltInAtom) {
505 builtIn = true;
506 }
507 for (int i = 0; i < ((Atom) le).getArity(); i++) {
508 if (((Atom) le).getParameter(i) instanceof Variable) {
509 if (((Atom) le).getParameter(i).equals(v)) {
510 found = true;
511 if (naf) {
512 foundNaf = true;
513 }
514 else {
515 foundPos = true;
516 }
517 if (builtIn) {
518 foundBuiltIn = true;
519 }
520 }
521 }
522 }
523 }
524 else if (le instanceof CompoundMolecule) {
525 Iterator i = ((CompoundMolecule) le).listOperands().iterator();
526 while (i.hasNext()) {
527 if (findVariable((Molecule) i.next(), v)) {
528 found = true;
529 if (naf) {
530 foundNaf = true;
531 }
532 if (builtIn) {
533 foundBuiltIn = true;
534 }
535 }
536 }
537 }
538 else if (le instanceof Molecule) {
539 if (findVariable((Molecule) le, v)) {
540 found = true;
541 if (naf) {
542 foundNaf = true;
543 }
544 else {
545 foundPos = true;
546 }
547 if (builtIn) {
548 foundBuiltIn = true;
549 }
550 }
551 }
552 if (foundNaf && !foundPos) {
553 unSafe = true;
554 errorMessage = "Variable " + v.toString() + " occurs in a negative body literal";
555 }
556 if (foundBuiltIn) {
557 unSafe = true;
558 errorMessage = "Variable " + v.toString() + " occurs in a body literal that "
559 + "corresponds to a built-in predicate";
560 }
561 if (!found) {
562 unSafe = true;
563 errorMessage = "Variable " + v.toString() + " does not occur in the body literal";
564 }
565 }
566 }
567
568 private boolean findVariable(Molecule m, Variable v) {
569 if (m.getLeftParameter().equals(v) || m.getRightParameter().equals(v)) {
570 return true;
571 }
572 if (!(m instanceof AttributeMolecule)) {
573 return false;
574 }
575 return ((AttributeMolecule) m).getAttribute().equals(v);
576 }
577
578 private void addError(LogicalExpression logexp, String msg) {
579 LogicalExpressionErrorImpl le = new LogicalExpressionErrorImpl(
580 axiom, logexp, msg, WSML.WSML_FLIGHT);
581 if (!errors.contains(le)) {
582 errors.add(le);
583 }
584 }
585 }