| Given Input Type | XQuery Expression | Expected Output Type |
<!ELEMENT r (b*,c?,d)> <!ELEMENT b EMPTY> <!ELEMENT c EMPTY> <!ELEMENT d EMPTY> |
<r>{for $y in child::* return <a>{$y}</a>}</r>
|
<!ELEMENT r (a*)> <!ELEMENT a (b|c|d)> <!ELEMENT b EMPTY> <!ELEMENT c EMPTY> <!ELEMENT d EMPTY> |
Explanation
Same example as the previous one except that the output type is modified so that "c" is allowed inside an "a" element.
Full Trace
The full trace generated by the implementation for the example above:
Static type-checking 'sample.xq' with input type 'input.dtd' starting at 'r' and output type 'output.dtd' starting at 'r'...
Read in sample.xq:
<r>{for $y in child::* return <a>{$y}</a>}</r>
Considered Input XQuery expression:
element r {for $y in child::* return element a {$y } }
Parsing tree grammar 'output.dtd'...
CFT: 10 type variables, 10 production rules, 5 element names.
Resulting CFT is:
$Empty -> EMPTYSET
$Epsilon -> ()
$Any -> ()
$PCData -> ()
$d -> d(())
$b -> b(())
$c -> c(())
$a -> a((($b | $c) | $d))
$1 -> ($a | ($a, $1))
$r -> r(($1 | ()))
Start symbol is $r
10 type variables, 10 production rules, 5 element names.
BTT: 8 type variables, 7 production rules, 6 element names.
Resulting BTT is:
$Epsilon -> EPSILON
$Any -> *($Any, $Any) | EPSILON
$Empty -> EMPTYSET
$2 -> d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
$3 -> a($2, $Epsilon) | a($2, $3)
$1 -> EPSILON | a($2, $Epsilon) | a($2, $3)
$r -> r($1, $Epsilon)
Start Symbol is $r
7 type variables, 7 production rules, 6 element names.
Inferring Input Type...
elem_elem element r {for $y in child::* return element a {$y } } , r($1, $Epsilon)
expr_union for $y in child::* return element a {$y } , EPSILON | a($2, $Epsilon) | a($2, $3)
for_empty for $y in child::* return element a {$y } , EPSILON
child_empty: input root child::* , EPSILON
child_empty returns (~<-1>T & ~<-2>T & ~<1>T)
in_child for child::*
in_child for child::* returns (mu X1.(<-2>X1 | <-1>(~<-1>T & ~<-2>T)))
elem_empty returns: false
for_empty: t1 is (~<-1>T & ~<-2>T & ~<1>T)
for_empty: t is (mu X1.(<-2>X1 | <-1>(~<-1>T & ~<-2>T)))
for_empty: t2 is F
for_empty: t2subst F
for_empty returns (~<-1>T & ~<-2>T & ~<1>T)
expr_union for $y in child::* return element a {$y } , a($2, $Epsilon) | a($2, $3)
for_elem for $y in child::* return element a {$y } , a($2, $Epsilon)
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
for_elem for $y in child::* return element a {$y } , a($2, $3)
elem_elem element a {$y } , a($2, $3)
elem_elem returns false
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
expr_union element a {$y } , a($2, $Epsilon) | a($2, $3)
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem element a {$y } , a($2, $3)
elem_elem returns false
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
expr_union element a {$y } , a($2, $Epsilon) | a($2, $Epsilon)
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
expr_union element a {$y } , a($2, $Epsilon) | a($2, $3)
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem element a {$y } , a($2, $3)
elem_elem returns false
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
expr_union element a {$y } , a($2, $Epsilon) | a($2, $Epsilon)
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem element a {$y } , a($2, $Epsilon)
expr_union $y , d($Epsilon, $Epsilon) | b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , d($Epsilon, $Epsilon)
var_elem returns: (X2 & d & ~<1>T)
expr_union $y , b($Epsilon, $Epsilon) | c($Epsilon, $Epsilon)
var_elem $y , b($Epsilon, $Epsilon)
var_elem returns: (X2 & b & ~<1>T)
var_elem $y , c($Epsilon, $Epsilon)
var_elem returns: (X2 & c & ~<1>T)
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
elem_elem returns: ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
expr_union returns:((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))
Recursive pattern detected, variable inserted: X3
Recursive pattern created: (mu X3.((~<2>T & ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))) | (<2>X3 & ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T)))))
Recursive pattern created: (mu X3.((~<2>T & ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T))) | (<2>X3 & ((X2 & b & ~<1>T) | (X2 & c & ~<1>T) | (X2 & d & ~<1>T)))))
expr_union returns:((~<-1>T & ~<-2>T & <1>(~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T)))) | (<1>(<2>(mu X4.((~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) | (<2>X4 & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))))) & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) & ~<-1>T & ~<-2>T))
expr_union returns:((~<-1>T & ~<-2>T & <1>(~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T)))) | (<1>(<2>(mu X4.((~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) | (<2>X4 & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))))) & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) & ~<-1>T & ~<-2>T) | (~<-1>T & ~<-2>T & ~<1>T))
elem_elem returns: ((~<-1>T & ~<-2>T & <1>(~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T)))) | (<1>(<2>(mu X4.((~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) | (<2>X4 & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))))) & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) & ~<-1>T & ~<-2>T) | (~<-1>T & ~<-2>T & ~<1>T))
Inferred input type represented as a formula:
((~<-1>T & ~<-2>T & <1>(~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T)))) | (<1>(<2>(mu X4.((~<2>T & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) | (<2>X4 & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))))) & ((b & ~<1>T) | (c & ~<1>T) | (d & ~<1>T))) & ~<-1>T & ~<-2>T) | (~<-1>T & ~<-2>T & ~<1>T))
Parsing and compiling input type 'input.dtd' starting at 'r'...
Parsing tree grammar 'input.dtd'...
CFT: 9 type variables, 9 production rules, 4 element names.
Resulting CFT is:
$Empty -> EMPTYSET
$Epsilon -> ()
$Any -> ()
$PCData -> ()
$d -> d(())
$b -> b(())
$c -> c(())
$1 -> ($b | ($b, $1))
$r -> r(((($1 | ()), ($c | ())), $d))
Start symbol is $r
9 type variables, 9 production rules, 4 element names.
BTT: 9 type variables, 8 production rules, 5 element names.
Resulting BTT is:
$Epsilon -> EPSILON
$Any -> *($Any, $Any) | EPSILON
$Empty -> EMPTYSET
$3 -> d($Epsilon, $Epsilon)
$2 -> c($Epsilon, $3) | d($Epsilon, $Epsilon)
$4 -> b($Epsilon, $2) | b($Epsilon, $4)
$1 -> b($Epsilon, $2) | b($Epsilon, $4) | c($Epsilon, $3) | d($Epsilon, $Epsilon)
$r -> r($1, $Epsilon)
Start Symbol is $r
8 type variables, 8 production rules, 5 element names.
Converted tree grammar into BTT [3 ms].
Translated BTT into Tree Logic [7 ms].
input:
(let
X5=(~<2>T & r & <1>X6),
X6=((~<2>T & d & ~<1>T) | (b & ~<1>T & <2>X8) | (b & <2>X7 & ~<1>T) | (<2>X9 & c & ~<1>T)),
X7=((~<2>T & d & ~<1>T) | (<2>X9 & c & ~<1>T)),
X8=((b & ~<1>T & <2>X8) | (b & <2>X7 & ~<1>T)),
X9=(~<2>T & d & ~<1>T)
in
X5)
neg_inferred: (<-1>T | <-2>T | (mu X11.((~<2>T | <2>X11) & (<1>(<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T))) | <-1>T | <-2>T | ~<1>T) & (<1>(~<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T)) | <2>(mu X12.((<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T))) & (~<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T)) | <2>X12)))) | <-1>T | <-2>T | ~<1>T) & (<-1>T | <-2>T | <1>T) & (<1>X11 | ~<1>T))))
Global formula contains the following total numbers of occurrences (including duplicates):
22 atomic propositions, 58 modalities, 13 variables, 3 fixpoint binder, 34 negations, 17 conjunctions, 25 disjunctions.
Satisfiability Tested Formula:
(mu X13.(<2>X13 | <1>X13 | (~<-1>T &
(let
X5=(~<2>T & r & <1>X6),
X6=((~<2>T & d & ~<1>T) | (b & ~<1>T & <2>X8) | (b & <2>X7 & ~<1>T) | (<2>X9 & c & ~<1>T)),
X7=((~<2>T & d & ~<1>T) | (<2>X9 & c & ~<1>T)),
X8=((b & ~<1>T & <2>X8) | (b & <2>X7 & ~<1>T)),
X9=(~<2>T & d & ~<1>T)
in
X5) & ~<2>T & (<-1>T | <-2>T | (mu X11.((~<2>T | <2>X11) & (<1>(<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T))) | <-1>T | <-2>T | ~<1>T) & (<1>(~<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T)) | <2>(mu X12.((<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T))) & (~<2>T | ((~d | <1>T) & (~b | <1>T) & (~c | <1>T)) | <2>X12)))) | <-1>T | <-2>T | ~<1>T) & (<-1>T | <-2>T | <1>T) & (<1>X11 | ~<1>T)))) & ~<-2>T)))
Warning: no suitable native BDD library found.
Falling back to the Java one.
Computing Relevant Closure...
Computed Relevant Closure [8 ms].
Computed Lean [1 ms].
Lean size is 21. It contains 15 eventualities and 6 symbols.
Fixpoint Computation Initialized [17 ms].
Computing Fixpoint....[17 ms].
Formula is unsatisfiable [47 ms].
Static type checking succeeded! No error detected.