<!--
Indus, a program analysis and transformation toolkit for Java.
Copyright (c) ${date} Venkatesh Prasad Ranganath

All rights reserved.  This program and the accompanying materials are made 
available under the terms of the Eclipse Public License v1.0 which accompanies 
the distribution containing this program, and is available at 
http://www.opensource.org/licenses/eclipse-1.0.php.

For questions about the license, copyright, and software, contact 
	Venkatesh Prasad Ranganath at venkateshprasad.ranganath@gmail.com
                                
This software was developed by Venkatesh Prasad Ranganath in SAnToS Laboratory 
at Kansas State University.
-->

<xsd:schema 
  attributeFormDefault="qualified" 
  blockDefault="restriction" 
  elementFormDefault="qualified"
  finalDefault="restriction" 
  id="slicerConfig" 
  targetNamespace="http://indus.projects.cis.ksu.edu/slicer" 
  version="1.0"
  xml:lang="en" 
  xmlns:indus="http://indus.projects.cis.ksu.edu/indus"
  xmlns:slicer="http://indus.projects.cis.ksu.edu/slicer" 
  xmlns:xsd="http://www.w3.org/2001/XMLSchema">
  
  <xsd:import id="indusConfig" namespace="http://indus.projects.cis.ksu.edu/indus" schemaLocation="indusConfig.xsd"/>
    
  <xsd:complexType id="slicerConfiguration" name="slicerConfiguration">
    <xsd:annotation>
      <xsd:appinfo> Slicer configuration </xsd:appinfo>
      <xsd:documentation> This is a configuration of the Slicer. </xsd:documentation>
    </xsd:annotation>
    <xsd:complexContent>
      <xsd:extension base="indus:configuration">
        <xsd:sequence>
          <xsd:element name="criteria" type="slicer:criteria"/>
          <xsd:element name="control" type="slicer:control"/>
          <xsd:element name="interference" type="slicer:interference"/>
          <xsd:element name="divergence" type="slicer:divergence"/>
          <xsd:element name="ready" type="slicer:ready"/>
          <xsd:element name="synchronization" type="slicer:synchronization"/>
          <xsd:attribute name="callingcontext" type="slicer:callingcontext" />
        </xsd:sequence>
        <xsd:attribute name="executableSlice" type="xsd:boolean" use="required"/>
        <xsd:attribute name="slicetype" type="slicer:slicingType" use="required"/>
      </xsd:extension>
    </xsd:complexContent>
  </xsd:complexType>
  
  <xsd:complexType id="criteria" name="criteria">
    <xsd:annotation>
      <xsd:documentation> This captures info about mechanical criteria generation facilities. </xsd:documentation>
    </xsd:annotation>
    <xsd:sequence>
      <xsd:element name="deadlock" type="slicer:deadlock"/>
      <xsd:element name="assertion" type="slicer:assertion"/>
    </xsd:sequence>
  </xsd:complexType>
  
  <xsd:simpleType id="slicingType" name="slicingType">
    <xsd:annotation>
      <xsd:documentation> This captures the type of the slice based on the direction of the slice. </xsd:documentation>
    </xsd:annotation>
    <xsd:restriction base="xsd:token">
      <xsd:enumeration value="BACKWARD_SLICE"/>
      <xsd:enumeration value="FORWARD_SLICE"/>
      <xsd:enumeration value="COMPLETE_SLICE"/>
    </xsd:restriction>
  </xsd:simpleType>
  
  <xsd:simpleType id="deadlockCriteriaSelectionStrategy" name="deadlockCriteriaSelectionStrategy">
    <xsd:annotation>
      <xsd:documentation> This captures the strategy used to generate deadlock criteria. </xsd:documentation>
    </xsd:annotation>
    <xsd:restriction base="xsd:token">
      <xsd:enumeration value="CONTEXT_SENSITIVE_ESCAPING_SYNC_CONSTRUCTS"/>
      <xsd:enumeration value="ESCAPING_SYNC_CONSTRUCTS"/>
      <xsd:enumeration value="ALL_SYNC_CONSTRUCTS"/>
    </xsd:restriction>
  </xsd:simpleType>
  
  <xsd:attribute name="inApplicationClassesOnly" id="inApplicationClassesOnly" default="false" type="xsd:boolean"/>
  
  <xsd:complexType id="deadlock" name="deadlock">
	<xsd:attribute name="sliceForDeadlock" type="xsd:boolean" use="required"/>
    <xsd:attribute default="ESCAPING_SYNC_CONSTRUCTS" name="deadlockCriteriaSelectionStrategy"
		type="slicer:deadlockCriteriaSelectionStrategy"/>
	<xsd:attribute ref="slicer:inApplicationClassesOnly" use="required"/>
  </xsd:complexType>
  
  <xsd:complexType id="assertion" name="assertion">  	
	<xsd:attribute name="sliceToPreserveAssertions" type="xsd:boolean" use="required"/>
	<xsd:attribute ref="slicer:inApplicationClassesOnly" use="required"/>
  </xsd:complexType>	    
  
  <xsd:simpleType id="natureOfInterThreadAnalysis" name="natureOfInterThreadAnalysis">
    <xsd:annotation>
      <xsd:documentation> This captures the information to be used in dependences such as interference and ready
        dependence. </xsd:documentation>
    </xsd:annotation>
    <xsd:restriction base="xsd:token">
      <xsd:enumeration value="SYMBOL_AND_EQUIVCLS_BASED_INFO"/>
      <xsd:enumeration value="EQUIVALENCE_CLASS_BASED_INFO"/>
      <xsd:enumeration value="TYPE_BASED_INFO"/>
    </xsd:restriction>
  </xsd:simpleType>
  
  <xsd:simpleType id="procedureBoundaryProperty" name="procedureBoundaryProperty">
    <xsd:annotation>
      <xsd:documentation> This represents the property pertaining to procedural boundary. </xsd:documentation>
    </xsd:annotation>
    <xsd:restriction base="xsd:token">
      <xsd:enumeration value="INTRA_PROCEDURAL_ONLY"/>
      <xsd:enumeration value="INTER_PROCEDURAL_ONLY"/>
      <xsd:enumeration value="INTRA_AND_INTER_PROCEDURAL"/>
    </xsd:restriction>
  </xsd:simpleType>
  
  <xsd:attribute default="SYMBOL_AND_EQUIVCLS_BASED_INFO" name="natureOfInterThreadAnalysis"
    type="slicer:natureOfInterThreadAnalysis"/>
    
  <xsd:attribute name="active" type="xsd:boolean"/>
  
  <xsd:complexType id="control" name="control">
    <xsd:annotation>
      <xsd:documentation> This captures control dependence information. </xsd:documentation>
   	</xsd:annotation>
   	<xsd:attribute name="nonTerminationSensitive" type="xsd:boolean" use="required"/>
   	<xsd:attribute name="explicitExceptionalExitSensitive" type="xsd:boolean" use="required"/>
   	<xsd:attribute name="commonUncheckedExceptions" type="xsd:boolean" use="required"/>
  </xsd:complexType>
  
  <xsd:complexType id="divergence" name="divergence">
    <xsd:annotation>
      <xsd:documentation> This captures divergence dependence information. </xsd:documentation>
    </xsd:annotation>
    <xsd:attribute default="INTRA_PROCEDURAL_ONLY" name="natureOfDivergenceAnalysis"
      type="slicer:procedureBoundaryProperty"/>
    <xsd:attribute ref="slicer:active" use="required"/>
  </xsd:complexType>
  
  <xsd:complexType id="interference" name="interference">
    <xsd:annotation>
      <xsd:documentation> This captures interference dependence information. </xsd:documentation>
    </xsd:annotation>
    <xsd:attribute ref="slicer:active" use="required"/>
    <xsd:attribute ref="slicer:natureOfInterThreadAnalysis" use="required"/>
    <xsd:attribute name="useOFA" type="xsd:boolean" use="required"/>
  </xsd:complexType>
  
  <xsd:complexType id="ready" name="ready">
    <xsd:annotation>
		<xsd:documentation> This captures ready dependence information. The callSiteSensitive enables the call-sites
		that lead to blocking wait methods to be considered as blocking as well.</xsd:documentation>
    </xsd:annotation>
    <xsd:attribute id="rule1" name="rule1" type="xsd:boolean" use="required"/>
    <xsd:attribute id="rule2" name="rule2" type="xsd:boolean" use="required"/>
    <xsd:attribute id="rule3" name="rule3" type="xsd:boolean" use="required"/>
    <xsd:attribute id="rule4" name="rule4" type="xsd:boolean" use="required"/>
    <xsd:attribute ref="slicer:active" use="required"/>
    <xsd:attribute ref="slicer:natureOfInterThreadAnalysis" use="required"/>
    <xsd:attribute name="callSiteSensitive" type="xsd:boolean" use="required"/>
    <xsd:attribute name="useOFA" type="xsd:boolean" use="required"/>
    <xsd:attribute id="useSafeLockAnalysis" name="useSafeLockAnalysis" type="xsd:boolean" use="required"/>
  </xsd:complexType>
  
  <xsd:complexType id="synchronization" name="synchronization">  	
	<xsd:attribute ref="slicer:active" use="required"/>
  </xsd:complexType>	    
  
  <xsd:complexType id="callingcontext" name="callingcontext">
  	<xsd:annotation>
	  	<xsd:documentation>This captures info pertaining to property-aware slicing.</xsd:documentation>
  	</xsd:annotation>
  	<xsd:sequence>
  		<xsd:attribute name="contextLengthLimit" type="xsd:positiveInteger" default="10"/>
  		<xsd:attribute ref="slicer:active" use="required"/>
  	</xsd:sequence>
  </xsd:complexType>
  
</xsd:schema>
