module xsdexx/ctt
// Simple characterization of context-determined type tables in XSD 1.1

/*
* Copyright (c) 2009 Black Mesa Technologies LLC
* All rights reserved.

* Redistribution and use in source and binary forms, with or
* without modification, are permitted provided that the following
* conditions are met:

*     * Redistributions of source code must retain the above
*       copyright notice, this list of conditions and the following
*       disclaimer.

*     * Redistributions in binary form must reproduce the above
*       copyright notice, this list of conditions and the following
*       disclaimer in the documentation and/or other materials
*       provided with the distribution.

*     * Neither the name of Black Mesa Technologies LLC nor the
*       names of its contributors may be used to endorse or promote
*       products derived from this software without specific prior
*       written permission.

* THIS SOFTWARE IS PROVIDED BY BLACK MESA TECHNOLOGIES LLC ''AS
* IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
* FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT
* SHALL BLACK MESA TECHNOLOGIES LLC BE LIABLE FOR ANY DIRECT,
* INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
* BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
* THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
* SUCH DAMAGE.  

*/

// Revisions:
// 2009-02-23 : CMSMcQ : made file

// First, some signatures describing some kinds of objects we
// don't want to model in detail.

// qn : expanded name (a QName value)
sig qn {} 

// tt : a type table.  May extend one or more other type tables.
// But we don't actually need to model type table extension here.
sig tt {
  // extension_of : set tt
} 
sig constructed_tt extends tt {
  default_type : TypeDef
}{
  // establish that each constructed type table is unique
  all T : constructed_tt | 
    default_type = T.@default_type => T = this
}
/* }{
  // constructed type tables don't extend anything
  #extension_of = 0
} */

// kw:  just a convenience signature to allow us to think of
// some things as keyword values
abstract sig kw {} 
lone sig kwGlobal extends kw {}
lone sig kwStrict extends kw {}
lone sig kwLax extends kw {}
lone sig kwSkip extends kw {}

// Second, element declarations and wildcards.

// Element declarations have a name, may have a type table,
// and have a scope
sig ElemDecl {
  name : qn,
  declared_type : TypeDef,
  ttable : lone tt,
  scope : (kwGlobal + TypeDef)
}{
  // any element declaration scoped to a type must be 
  // among that type's children
  all t : TypeDef | scope = t => this in t.elemChildren
}

// Wildcards match QNames and have a kind:  they are strict, or
// lax, or skip wildcards.  We define them as separate subtypes
// primarily so that it is more convenient to style them differently
// in visualizations of instances.
abstract sig WildCard {
  matches : set qn,
  kind : (kwStrict + kwLax + kwSkip)
}
sig StrictWC extends WildCard {}{
  kind = kwStrict
}
sig LaxWC extends WildCard {}{
  kind = kwLax
}
sig SkipWC extends WildCard {}{
  kind = kwSkip
}

// Third, type definitions.  

// Type definitions have element children and wildcard children.
// And crucially for our purposes, they also define a mapping
// from QNames to their context-determined type tables (ctt).  
// We don't distinguish top-level from local types; the
// distinction does not appear important for this issue.

sig TypeDef {
  elemChildren : set ElemDecl,
  wcChildren : set WildCard,
  ctt : qn -> tt
}{

  // Here we constrain the TypeDef signature so that each ctt
  // includes everything the spec says to include, and nothing 
  // else

  /* What the spec says, in 3.4.4.1, is:

     Similarly: [Definition:] Every Complex Type Definition
     determines a partial functional mapping from element
     information items (and their expanded names) to Type
     Tables. The Type Table identified by this mapping is the
     context-determined type table for elements which match a
     Particle contained by the content model of the Complex Type
     Definition. For a given Complex Type Definition T and a
     given element information item E, the context-determined
     type table of E in T is as follows:

     1 Let D be an Element Declaration matched by E, given by
       the first case among the following which applies:

       1.1 If E has the same expanded name as some element
           declaration(s) contained by T's content model, whether
           directly, indirectly, or implicitly, then let D be any
           one of those Element Declarations.

       1.2 If E matches some wildcard particle contained by
           T's content model, whether directly or indirectly, and
           E matches some top-level Element Declaration, then let
           D be that top-level Element Declaration."  [and clause
           2.1 again]

     2 If E matches some Element Declaration as described above
       in clause 1, then the context-determined type table of E
       in T is given by the appropriate case among the following:

       2.1 If D has a Type Table, then the context-determined
           type table of E in T is the Type Table of D

       2.2 If D has no Type Table, then the
           context-determined type table of E in T is the Type
           Table whose {alternatives} is the empty sequence and
           whose {default type definition} is a Type Alternative
           whose {test} is absent and whose {type definition} is
           the declared {type definition} of D.

*/
  all Q : qn | all T : tt |
    (Q -> T in ctt) iff

    // Clause 1.1 + 2.1
    (some ED : elemChildren | 
        Q = ED.name and T = ED.ttable ) 

    // Clauses 1.1 + 2.2
    or (some ED : elemChildren | 
        Q = ED.name 
        and no ED.ttable 
        and T in constructed_tt
        and T.default_type = ED.declared_type
    )

    // Clauses 1.2 and 2.1
    or ( (no ED : elemChildren | Q = ED.name)
       and 
       (some W : wcChildren | some G : ElemDecl | 
         Q in W.matches
         and G.name = Q
         and G.scope = kwGlobal
         and G.ttable = T
      )
    ) 

    // Clauses 1.2 + 2.2 
    or ((no ED : elemChildren | Q = ED.name)
       and 
       (some W : wcChildren | some G : ElemDecl |
         Q in W.matches
         and G.name = Q
         and G.scope = kwGlobal
         and no G.ttable
         and T in constructed_tt 
         and T.default_type = G.declared_type
      )
    )

}

// No two top-level element declarations have the same
// expanded name.  
fact top_level_ED_unique {
  all E1, E2 : ElemDecl |
    E1.scope = kwGlobal 
    and E2.scope = kwGlobal
    and E1.name = E2.name
    => E1 = E2
}

// XSD 1.1 Structures, sec. 3.8.6.3 imposes the constraint 
// Element Declarations Consistent.  We define it as a predicate
// rather than a fact, so that we can explore the effect of having
// it and not having it.

/* What the spec says is:

    Schema Component Constraint: Element Declarations Consistent

    If the {particles} property contains, either directly,
    indirectly (that is, within the {particles} property of a
    contained model group, recursively), or implicitly, two or
    more element declarations with the same expanded name, then
    all their type definitions must be the same top-level
    definition, that is, all of the following must be true:

      1 All their declared {type definition}s have a non-absent
        {name}.

      2 All their declared {type definition}s have the same
        {name}.

      3 All their declared {type definition}s have the same
        {target namespace}.

      4 All their {type table}s are either all absent or else
        all are present and have the same sequence of
        {alternatives} and the same {default type definition}.

    If all of the following are true:

      1 The {particles} property contains (either directly,
        indirectly, or implicitly) one or more element
        declarations with the same expanded name Q; call these
        element declarations EDS.

      2 At least one of the following is true

        2.1 The {particles} property contains one or more
            strict or lax wildcard particles which match Q.

        2.2 The Model Group is the {term} of the content
            model of some Complex Type Definition CTD and
            CTD.{content type} has an {open content} with a
            strict or lax Wildcard which matches Q.

      3 There exists a top-level element declaration G with the
        expanded name Q.

    then the {type table}s of EDS and the {type table} of G must
    either all be absent or else all be present and have the same
    sequence of {alternatives} and the same {default type
    definition}.
  */

// translated now into Alloy, this is:
pred EDC {

  all T : TypeDef | all E1, E2 : ElemDecl |
    (E1 in T.elemChildren and E2 in T.elemChildren)
    => 
    (E1.declared_type = E2.declared_type
    and E1.ttable = E2.ttable)

  all T : TypeDef | all EDS, EG : ElemDecl | all W : WildCard |
    ( EDS in T.elemChildren 
      and W in T.wcChildren
      and W.kind in (kwStrict + kwLax)
      and EDS.name in W.matches
      and EDS.name = EG.name
    ) => (
      EDS.ttable = EG.ttable
    )
}

run {} for 3

// Test the claim that the context-determined type table
// for a given QName, in a given type, is unique.
assert ctt_unique {
  all Q : qn | all T : TypeDef | lone Q.(T.ctt)
}
check ctt_unique for 3
// There are counter-examples, which shows that the definition
// of ctt is not by itself enough to make the context-determined
// type table unique.

// Now test the proposition in the Note:
/* 

    Note: The constraint Element Declarations Consistent
    (§3.8.6.3) ensures that even if E matches more than one such
    declaration D, there will be just one context-determined type
    table."

*/
assert EDC_entails_ctt_unique {
  EDC => (all Q : qn | all T : TypeDef | lone Q.(T.ctt))
}
check EDC_entails_ctt_unique for 7