1   /*
2   wsmo4j - a WSMO API and Reference Implementation
3   
4   Copyright (c) 2005, University of Innsbruck, Austria
5   
6   This library is free software; you can redistribute it and/or modify it under
7   the terms of the GNU Lesser General Public License as published by the Free
8   Software Foundation; either version 2.1 of the License, or (at your option)
9   any later version.
10  This library is distributed in the hope that it will be useful, but WITHOUT
11  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
12  FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
13  details.
14  You should have received a copy of the GNU Lesser General Public License along
15  with this library; if not, write to the Free Software Foundation, Inc.,
16  59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
17  */
18  package test.wsmo4j.validator;
19  
20  import org.deri.wsmo4j.validator.ValidationErrorImpl;
21  import org.deri.wsmo4j.validator.WsmlCoreValidator;
22  import org.deri.wsmo4j.validator.WsmlDLValidator;
23  import org.deri.wsmo4j.validator.WsmlFlightValidator;
24  import org.deri.wsmo4j.validator.WsmlRuleValidator;
25  import org.wsmo.validator.ValidationError;
26  
27  /**
28   * Different error types are tested via constructed invalid 
29   * axiom definitions.
30   * 
31   * <pre>
32   * Created on Dec 19, 2005
33   * Committed by $Author: morcen $
34   * $Source$,
35   * </pre>
36   * 
37   * @author nathalie.steinmetz@deri.org
38   * @version $Revision: 1946 $ $Date: 2007-04-02 15:13:28 +0300 (Mon, 02 Apr 2007) $
39   */
40  public class ValidatorLogExprTests extends ValidatorTestCase {
41  
42      /* Core LogicalExpression Tests */
43      
44      /**
45       * This test checks for the validity of a SubConceptOfMolecule.
46       * At subConceptOf, the identifier and the arguments need to be Concepts.
47       */
48      public void testCoreInvalidMoleculeSubConceptOf() throws Exception {
49          createAxiomDef("Man subConceptOf _integer.");
50          createAxiomDef("Man memberOf Human");
51          WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
52          v.isValid(ontology, errors, warnings);
53          ValidationError ve = errors.firstElement();
54  //        printWarning(warnings);
55  //        printError(errors);
56          assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_ATOMIC_ERR));
57          removeAxiomDef();
58      }
59      
60      /**
61       * This test checks for the validity of a MembershipMolecule
62       * At memberOf, the identifier must be an instance and the arguments 
63       * need to be Concepts.
64       */
65      public void testCoreInvalidMoleculeMemberOf() throws Exception {
66          createAxiomDef("Man memberOf Man.");
67          WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
68          v.isValid(ontology, errors, warnings);
69          ValidationError ve = errors.firstElement();
70  //        printWarning(warnings);
71  //        printError(errors);
72          assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_ATOMIC_ERR));
73          removeAxiomDef();
74      }
75      
76      
77      /**
78       * This test checks for the validity of an transitive InverseImplication.
79       */
80      public void testCoreInvalidTransitiveAttribute() throws Exception {
81          createAxiomDef("?x[ageOf hasValue ?y] impliedBy " +
82                  "?x[ageOfHuman hasValue ?z] and ?z[ageOfHuman hasValue ?y].");
83          WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
84          boolean b = v.isValid(ontology, errors, warnings);
85          ValidationError ve = errors.firstElement();
86  //        printWarning(warnings);
87  //        printError(errors);
88          assertFalse(b);
89          assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_IMPL_BY_ERR));
90          removeAxiomDef();
91      }
92      
93      /**
94       * This test checks for the validity of an InverseImplication.
95       */
96      public void testCoreValidInvImplAttribute() throws Exception {
97          createAxiomDef("?x[ageOfHuman hasValue ?y] impliedBy ?y[ageOfHuman hasValue ?x].");
98          WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
99          boolean b = v.isValid(ontology, errors, warnings);
100 //        printWarning(warnings);
101 //        printError(errors);
102         assertTrue(b);
103         removeAxiomDef();
104     }
105     
106     /**
107      * This test checks for the validity of an sub-attribute InverseImplication.
108      */
109     public void testCoreValidSubAttribute() throws Exception {
110         createAxiomDef("?x[ageOfAnimal hasValue ?y] impliedBy ?x[ageOfHuman hasValue ?y].");
111         WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
112         boolean b = v.isValid(ontology, errors, warnings);
113 //        printWarning(warnings);
114 //        printError(errors);
115         assertTrue(b);
116         removeAxiomDef();
117     }
118     
119     /**
120      * This test checks for the validity of an Equivalence
121      */
122     public void testCoreValidEquivalence() throws Exception { 
123         createAxiomDef("?x memberOf c equivalent ?x memberOf {d,e}.");
124 //        createAxiomDef("?x memberOf c equivalent ?x memberOf d and ?x memberOf e or ?x memberOf f.");
125         WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
126         boolean b = v.isValid(ontology, errors, warnings);
127 //        printWarning(warnings);
128 //        printError(errors);
129         assertTrue(b);
130         removeAxiomDef();
131     }
132     
133     /**
134      * This test checks for the validity of an InverseImplication (the variable 
135      * graph of the left-hand side formula must be connected and acyclic).
136      */
137     public void testCoreGraph() throws Exception {
138         createAxiomDef("?x memberOf Human impliedBy ?x[ageOfHuman hasValue ?y] and " +
139                 "?y[ageOfHuman hasValue ?z] and ?y[ageOfHuman hasValue ?w].");
140         WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
141         boolean b = v.isValid(ontology, errors, warnings);
142 //        printWarning(warnings);
143 //        printError(errors);
144         assertTrue(b);
145         removeAxiomDef();
146     }
147     
148     /**
149      * This test checks for the validity of an InverseImplication (the variable 
150      * graph of the left-hand side formula must be connected and acyclic).
151      */
152     public void testCoreGraphWithCycle() throws Exception {
153         createAxiomDef("?x memberOf Human impliedBy ?x[ageOfHuman hasValue ?y] and " +
154                 "?y[ageOfHuman hasValue ?z] and ?z[ageOfHuman hasValue ?x].");
155         WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
156         v.isValid(ontology, errors, warnings);
157         ValidationError ve = errors.firstElement();
158 //        printWarning(warnings);
159 //        printError(errors);
160         assertTrue(ve.getReason().startsWith(ValidationError.AX_GRAPH_ERR));
161         removeAxiomDef();
162     }
163     
164     /**
165      * This test checks for the validity of an InverseImplication (the variable 
166      * graph of the left-hand side formula must be connected and acyclic).
167      */
168     public void testCoreUnconnectedGraph() throws Exception {
169         createAxiomDef("?x memberOf Human impliedBy ?x[ageOfHuman hasValue ?y] and " +
170                 "?y[ageOfHuman hasValue ?z] and ?w[ageOfHuman hasValue ?v].");
171         WsmlCoreValidator v = new WsmlCoreValidator(leFactory);
172         v.isValid(ontology, errors, warnings);
173         ValidationError ve = errors.firstElement();
174 //        printWarning(warnings);
175 //        printError(errors);
176         assertTrue(ve.getReason().startsWith(ValidationError.AX_GRAPH_ERR));
177         removeAxiomDef();
178     }
179     
180     /* DL LogicalExpression Tests */
181     
182     /**
183      * This test checks an invalid DL LogicalExpression.
184      */
185     public void testDLInvalidDisjunction() throws Exception {
186         createAxiomDef("?x memberOf Man or ?x memberOf Person.");
187         WsmlDLValidator v = new WsmlDLValidator(leFactory);
188         boolean b = v.isValid(ontology, errors, warnings);
189 //        printWarning(warnings);
190 //        printError(errors);
191         assertFalse(b);
192         removeAxiomDef();
193     }
194     
195     /**
196      * This test checks an valid DL Implication.
197      */
198     public void testDLValidImplication() throws Exception {
199         createAxiomDef("(forall ?a (?b[hasChild hasValue ?a] implies ?a memberOf Child)) implies ?b memberOf Father.");
200         WsmlDLValidator v = new WsmlDLValidator(leFactory);
201         boolean b = v.isValid(ontology, errors, warnings);
202 //        printWarning(warnings);
203 //        printError(errors);
204         assertTrue(b);
205         removeAxiomDef();
206     }
207     
208     /**
209      * This test checks the validity of an DL Quantification.
210      */
211     public void testDLValidQuantifications() throws Exception {
212         createAxiomDef("?x memberOf Human implies exists ?y(?x[father hasValue ?y] and ?y memberOf Human)" +
213                 " and forall ?y(?x[father hasValue ?y] implies ?y memberOf Human).");
214         WsmlDLValidator v = new WsmlDLValidator(leFactory);
215         boolean b = v.isValid(ontology, errors, warnings);
216 //        printWarning(warnings);
217 //        printError(errors);
218         assertTrue(b);
219         removeAxiomDef();
220     }
221  
222     /**
223      * This test checks the validity of an DL Quantification.
224      */
225     public void testDLValidUniversalQuantification() throws Exception {
226         createAxiomDef("(forall {?a, ?b, ?c} (?a[age hasValue ?c] and ?b[age hasValue ?c] " +
227                 "and (?a[age hasValue ?c] and ?a memberOf Human) implies " +
228                 "neg(?a :=: ?b) or neg(?a :=: ?c) or neg(?b :=: ?c))) " +
229                 "implies ?b memberOf Human.");
230         WsmlDLValidator v = new WsmlDLValidator(leFactory);
231         boolean b = v.isValid(ontology, errors, warnings);
232 //        printWarning(warnings);
233 //        printError(errors);
234         assertTrue(b);
235         removeAxiomDef();
236     }
237     
238     /**
239      * This test checks the validity of an DL Quantification.
240      */
241     public void testDLValidExistentialQuantification() throws Exception {
242         createAxiomDef("(exists {?a, ?b} (?a[age hasValue ?c] and ?b[age hasValue ?c] " +
243                 "and (?a[age hasValue ?c] and ?a memberOf Human) and " +
244                 "neg(?a :=: ?b) and neg(?a = ?c) and neg(?b :=: ?c))) " +
245                 "implies ?b memberOf Human.");
246         WsmlDLValidator v = new WsmlDLValidator(leFactory);
247         boolean b = v.isValid(ontology, errors, warnings);
248 //        printWarning(warnings);
249 //        printError(errors);
250         assertTrue(b);
251         removeAxiomDef();
252     }
253     
254     /**
255      * This test checks the validity of an InverseImplication.
256      */
257     public void testDLValidInvImpl() throws Exception {
258         createAxiomDef("?x[ageOfHuman hasValue ?y] impliedBy " +
259         "?x[ageOfPerson hasValue ?y].");
260         WsmlDLValidator v = new WsmlDLValidator(leFactory);
261         boolean b = v.isValid(ontology, errors, warnings);
262 //        printWarning(warnings);
263 //        printError(errors);
264         assertTrue(b);
265         removeAxiomDef();
266     }
267     
268     /**
269      * This test checks for the validity of an transitive InverseImplication.
270      */
271     public void testDLValidTransitiveAttribute() throws Exception {
272         createAxiomDef("?x[ageOfHuman hasValue ?y] impliedBy " +
273                 "?x[ageOfHuman hasValue ?z] and ?z[ageOfHuman hasValue ?x].");
274         WsmlDLValidator v = new WsmlDLValidator(leFactory);
275         boolean b = v.isValid(ontology, errors, warnings);
276 //        printWarning(warnings);
277 //        printError(errors);
278         assertTrue(b);
279         removeAxiomDef();
280     }
281     
282     /**
283      * This test checks for the validity of an transitive InverseImplication.
284      */
285     public void testDLValidInverseImplication() throws Exception {
286         createAxiomDef("?x[p hasValue ?y] impliedBy " +
287                 "?x[p hasValue ?z] and ?z[q hasValue ?w].");
288         WsmlDLValidator v = new WsmlDLValidator(leFactory);
289         boolean b = v.isValid(ontology, errors, warnings);
290 //        printWarning(warnings);
291         printError(errors);
292         assertTrue(b);
293         removeAxiomDef();
294     }
295     
296     /**
297      * This test checks for the validity of an InverseImplication.
298      */
299     public void testDLValidInvImplAttribute() throws Exception {
300         createAxiomDef("?x[ageOfHuman hasValue ?y] impliedBy ?y[ageOfHuman hasValue ?x].");
301         WsmlDLValidator v = new WsmlDLValidator(leFactory);
302         boolean b = v.isValid(ontology, errors, warnings);
303 //        printWarning(warnings);
304 //        printError(errors);
305         assertTrue(b);
306         removeAxiomDef();
307     }
308     
309     /**
310      * This test checks for the validity of an InverseImplication.
311      */
312     public void testDLGraph() throws Exception {
313         createAxiomDef("?x memberOf Human impliedBy ?x[ageOfHuman hasValue ?y] and " +
314                 "?y[ageOfHuman hasValue ?z] and ?y[ageOfHuman hasValue ?w].");
315         WsmlDLValidator v = new WsmlDLValidator(leFactory);
316         boolean b = v.isValid(ontology, errors, warnings);
317 //        printWarning(warnings);
318 //        printError(errors);
319         assertTrue(b);
320         removeAxiomDef();
321     }
322     
323     /**
324      * This test checks for the validity of an InverseImplication (the variable 
325      * graph of each description must be connected and acyclic).
326      */
327     public void testDLGraphWithCycle() throws Exception {
328         createAxiomDef("?x memberOf Human impliedBy ?x[ageOfHuman hasValue ?y] and " +
329                 "?y[ageOfHuman hasValue ?z] and ?z[ageOfHuman hasValue ?x].");
330         WsmlDLValidator v = new WsmlDLValidator(leFactory);
331         v.isValid(ontology, errors, warnings);
332         ValidationError ve = errors.firstElement();
333 //        printWarning(warnings);
334 //        printError(errors);
335         assertTrue(ve.getReason().startsWith(ValidationError.AX_GRAPH_ERR));
336         removeAxiomDef();
337     }
338     
339     /**
340      * This test checks for the validity of an InverseImplication (the variable 
341      * graph of each description must be connected and acyclic).
342      */
343     public void testDLUnconnectedGraph() throws Exception {
344         createAxiomDef("?x memberOf Human impliedBy ?x[ageOfHuman hasValue ?y] and " +
345                 "?y[ageOfHuman hasValue ?z] and ?w[ageOfHuman hasValue ?v].");
346         WsmlDLValidator v = new WsmlDLValidator(leFactory);
347         v.isValid(ontology, errors, warnings);
348         ValidationError ve = errors.firstElement();
349 //        printWarning(warnings);
350 //        printError(errors);
351         assertTrue(ve.getReason().startsWith(ValidationError.AX_GRAPH_ERR));
352         removeAxiomDef();
353     }
354     
355     /* Flight LogicalExpression Tests */
356         
357     /**
358      * This test checks for the validity of a proposition.
359      */
360     public void testFlightProposition() throws Exception {
361         createAxiomDef("a.");
362         WsmlFlightValidator v = new WsmlFlightValidator(leFactory);
363         boolean b = v.isValid(ontology, errors, warnings);
364 //        printWarning(warnings);
365 //        printError(errors);
366         assertTrue(b);
367     }
368     
369     /**
370      * This test checks the flight safety condition.
371      */
372     public void testFlightSafetyCondition() throws Exception {
373         createAxiomDef("p(?y) :- a(?y) and b(?x).");
374         createAxiomDef("p(?x) impliedBy p(?z) :- p(?x).");
375         createAxiomDef("p(?x) implies p(?z) :- p(?z).");
376         createAxiomDef("p(?x) :- naf naf p(?x).");
377         createAxiomDef("p(?x) equivalent p(?y) :- p(?x) and p(?y)");
378         WsmlFlightValidator v = new WsmlFlightValidator(leFactory);
379         boolean b = v.isValid(ontology, errors, warnings);
380 //        printWarning(warnings);
381 //        printError(errors);  
382         assertTrue(b);
383     }
384     
385     /**
386      * This test checks the safety of built-in predicates.
387      */
388     public void testFlightSafetyOfBuiltInPredicate() throws Exception {
389         createAxiomDef("a[b hasValue ?x] :- ?x > 25 and b. ");
390         WsmlFlightValidator v = new WsmlFlightValidator(leFactory);
391         v.isValid(ontology, errors, warnings);
392         ValidationError ve = errors.firstElement();
393 //        printWarning(warnings);
394 //        printError(errors);   
395         assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_SAFETY_COND));
396     }
397     
398     /**
399      * This test checks the safety of an negative body literal.
400      */
401     public void testFlightSafetyOfNegativeBodyLiteral() throws Exception {
402         createAxiomDef("?x[isAlive hasValue _boolean(\"true\")] :- " +
403                 "naf ?x[hasObit hasValue ?obit] memberOf Human.");
404         WsmlFlightValidator v = new WsmlFlightValidator(leFactory);
405         v.isValid(ontology, errors, warnings);
406         ValidationError ve = errors.firstElement();
407 //        printWarning(warnings);
408 //        printError(errors);
409         assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_SAFETY_COND));
410     }
411     
412     /**
413      * This test checks the safety of function symbols.
414      */
415     public void testFlightFunctionSymbol() throws Exception {
416         createAxiomDef("a(b)[c(d) hasValue d(e)].");
417         WsmlFlightValidator v = new WsmlFlightValidator(leFactory);
418         v.isValid(ontology, errors, warnings);
419 //        printWarning(warnings);
420 //        printError(errors);
421         assertEquals(3,errors.size());
422     }
423     
424     /* Rule LogicalExpression Tests */
425     
426     /**
427      * This test checks the validity of an rule logic programming rule.
428      */
429     public void testRuleHeadEqual() throws Exception {
430         createAxiomDef("a = b");
431         WsmlRuleValidator v = new WsmlRuleValidator(leFactory);
432         v.isValid(ontology, errors, warnings);
433         ValidationError ve = errors.firstElement();
434 //        printWarning(warnings);
435 //        printError(errors);
436         assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_HEAD_ERR));
437     }
438     
439     /**
440      * This test checks the validity of an rule logic programming rule.
441      */
442     public void testRuleHeadNegation() throws Exception {
443         createAxiomDef("naf ?x[hasObit hasValue ?obit] memberOf Human");
444         WsmlRuleValidator v = new WsmlRuleValidator(leFactory);
445         v.isValid(ontology, errors, warnings);
446         ValidationError ve = errors.firstElement();
447 //        printWarning(warnings);
448 //        printError(errors);
449         assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_HEAD_ERR));
450     }
451     
452     /**
453      * This test checks the validity of an rule logic programming rule.
454      */
455     public void testRuleBodyStrongEqual() throws Exception {
456         createAxiomDef("?x[isAlive hasValue _boolean(\"true\")] :- " +
457                         "?x :=: a.");
458         WsmlRuleValidator v = new WsmlRuleValidator(leFactory);
459         v.isValid(ontology, errors, warnings);
460         ValidationError ve = errors.firstElement();
461 //        printWarning(warnings);
462 //        printError(errors);
463         assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_BODY_ERR));
464     }
465     
466     /**
467      * This test checks the validity of an rule logic programming rule.
468      */
469     public void testRuleBodyNegation() throws Exception {
470         createAxiomDef("?x[isAlive hasValue _boolean(\"true\")] :- " +
471         "neg ?x[hasObit hasValue ?obit] memberOf Human.");
472         WsmlRuleValidator v = new WsmlRuleValidator(leFactory);
473         v.isValid(ontology, errors, warnings);
474         ValidationError ve = errors.firstElement();
475 //        printWarning(warnings);
476 //        printError(errors);
477         assertTrue(ve.getReason().startsWith(ValidationErrorImpl.AX_BODY_ERR));
478     }
479     
480 }
481 
482 /*
483  *$Log$
484  *Revision 1.5  2007/04/02 12:13:23  morcen
485  *Generics support added to wsmo-api, wsmo4j and wsmo-test
486  *
487  *Revision 1.4  2006/10/06 09:04:06  nathaliest
488  *fixed bug in wsml-dl validation concerning inverse implications
489  *
490  *Revision 1.3  2006/10/05 13:09:28  nathaliest
491  *fixed metamodelling bug
492  *
493  *Revision 1.2  2006/01/05 14:57:48  nathaliest
494  *Validator uses leFactory taken in constructor from properties map
495  *
496  *Revision 1.1  2005/12/19 11:23:01  nathaliest
497  *restructured validator tests
498  *
499  */