First Order Logic (FOL) to Schematron
(Beta)
Derives ISO Schematron rules from FOL constraints.
NOTE: this target has been implemented within the OGC Testbed 11. The use case there was to derive ISO Schematron rules from AIXM business rules. The full process is described on the page Deriving Schematron from AIXM Business Rules, which includes a sample configuration as well.
Conversion to ISO Schematron
For a valid FOL expression x, let τ(x) denote the equivalent XPath expression. The expression x may contain free variables (explicit or implicit), which need to be treated and bound to their definition context when computing τ(x).
The following table describes how all particular constructs of the First Order Logic language translate to XPath/Schematron.
NOTE: the derived ISO Schematron file uses ‘xslt2’ as queryBinding, which is based on an XSLT 2.0 implementation that supports XPath 2.0.
| First Order Logic construct (and category, if applicable) | Textual representation (in log output) |
In words | Schematron translation |
| Universal quantification | forall(t:x|p(t)) | All members of some set x of objects or values shall fulfill predicate p. | every τ(t) in τ(x) satisfies τ(p(τ(t)))where t translates to a unique $ prefixed variable name, and τ(x) translates to current() if the quantification is at the outmost level. |
| Existential quantification: „at least l and at most h” | exists{l,h}(t:x|p(t)) | The number of members of some set x of objects or values, which fulfill predicate p shall be between l and h. | for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return ($var>=τ(l) and $var<=τ(h)) |
| Existential quantification: „exactly n” | exists{n}(t:x|p(t)) | The number of members of some set x of objects or values, which fulfill predicate p shall be exactly n. | for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return ($var=n) |
| Existential quantification: “at most n” | exists{0..n}(t:x|p(t)) | The number of members of some set x of objects or values, which fulfill predicate p shall be at most n. | for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return $var<=n) |
| Existential quantification: “at least n” | exists{n..*}(t:x|p(t)) | The number of members of some set x of objects or values, which fulfill predicate p shall be at least n. | for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return ($var>=n) |
| Variable access | t defined in a quantification, such as forall(t:x|p(t)) | the variable name, either explicitly or implicitly provided | The variable name, preceded by ‘$’ – for example $x1, $c1.Note: this is the translation for τ(t), which is mentioned in the Schematron translations of quantifications. |
| Property call | x.pname | Set of object instances or values reached from the instance or set represented by x by applying property name, pname. | If pname is encoded as an XML attribute:τ(x)/@pnameOtherwise, if pname is simple-valued or if pname is object-valued and the last segment in the schema call:
τ(x)/pname Otherwise, if pname is object-valued and encoded inline: τ(x)/pname/* Otherwise, if pname is realized by reference using xlink:href pointing to object instances in the same document: //*[concat(α,@gml:id,β)= τ(x)/pname/@xlink:href] α and β are a prefix and a postfix to adjust xlink:href values and gml:ids. Typically bare name references are used – hence α=# and β=empty. Otherwise (if encoded inline or by reference): (τ(x)/pname/*)|//*[concat(α,@gml:id,β)= τ(x)/pname/@xlink:href] |
| Logical infix | and(x1,…,xn)or(x1,…,xn) | Logical combination as indicated | τ(x1) and … and τ(xn)τ(x1) or … or τ(xn) |
| Negation | not(x) | Logical negation of x | not(τ(x)) |
| Null check | isNull(x) | Determine if the value of x is null. | If the last segment of the patch expression in τ(x) is encoded as an XML attribute:not(string-length(normalize-space τ(x))))Otherwise:
τ(x)[@xsi:nil=’true’] |
| Equality | isEqualTo(e1,e2) | Equality of expressions e1, e2 | τ(e1)= τ(e2)Note: This assumes that equality on sets is fulfilled if at least one pair is equal. Otherwise some more refined code generation will be necessary. |
| Type check | isTypeOf(x,(ClassLiteral)z) | X is checked for complying with the type y identified by class literal z. | τ(x)[name()=’T1‘ or … or name()=’Ti’], whereTk is the qualified name of one of the concrete derivations of y, including y, if it is not abstract (names of abstract types are ignored). |
| String literal | ‘xxxxx’ | same | |
| Numeric literal | 123 or 3.1415 | same | |
| String literal list | (‘abc’,’def’,…) | List of ‘names’ | same |
| Class literal | class name (e.g. AirportHeliport) | name of the class | name of the class identified by the class literal |
Configuration
Class
The class for the Target implementation is de.interactive_instruments.ShapeChange.Target.FOL2Schematron.FOL2Schematron.
Parameters
The <targetParameters> recognized for this target include the following:
| Parameter Name | Required / Optional | Type | Default Value | Explanation |
| outputDirectory | Optional | String | <the current run directory> | The path to the folder in which the Schematron rules file will be created. |
| defaultEncodingRule | Optional | String | none | The identifier of the default encoding rule governing the conversion into Schematron. |
| schematronXlinkHrefPrefix | Optional | String | “#” | Prefix for xlink:href references. |
| schematronXlinkHrefPostfix | Optional | String | “” (the empty string) | Postfix for xlink:href references. |
Encoding Rules
An <EncodingRule> element defines an encoding rule.
Example:
<EncodingRule extends="iso19136_2007" name="aixm"> <rule name="rule-all-cls-aixmDatatype" /> <rule name="rule-all-prop-uomAsAttribute" /> </EncodingRule>
The name attribute of the <EncodingRule> element defines the identifier of the encoding rule to be used.
The optional extends attribute of the <EncodingRule> element includes all conversion rules from the referenced encoding rule in this encoding rule, too.
Each <rule> references either a conversion rule or – possibly in the future – a requirement or recommendation to be tested during the validation before the conversion process.
The following conversion rules are supported by this target. They amend or extend the default encoding behavior:
| Rule Name | Description |
| rule-all-cls-aixmDatatype | A <<datatype>> within an AIXM schema does not have its own object element. Within the XML Schema it only has a complex type with simple content definition containing a textual value (and possibly attribute(s)), but no element. |
| rule-all-prop-uomAsAttribute | When this rule is active, then the XML Schema encoding of a property with name “uom” is an XML attribute. The AIXM schema defines datatypes with such properties and encoding. |
Configuration Example
<TargetXmlSchema class="de.interactive_instruments.ShapeChange.Target.FOL2Schematron.FOL2Schematron" inputs="step3" mode="enabled"> <targetParameter name="outputDirectory" value="results/sch"/> <targetParameter name="defaultEncodingRule" value="aixm"/> <rules> <EncodingRule extends="iso19136_2007" name="aixm"> <rule name="rule-all-cls-aixmDatatype"/> <rule name="rule-all-prop-uomAsAttribute"/> </EncodingRule> </rules> <xi:include href="src/main/resources/config/StandardRules.xml"/> <xi:include href="src/main/resources/config/StandardNamespaces.xml"/> <xi:include href="src/main/resources/config/StandardMapEntries.xml"/> </TargetXmlSchema>