Commit e2975dd3 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Remove jTET from this repository, since it exists elsewhere now. 

Remove the jTET from here, as it exists as a standalone library
now.
parent fbbbd641

.gitignore

+1 −5
Original line number Diff line number Diff line 
/jTET/target/

/jTET/gen/

.idea/

.pvscontext

/jTET/jtet.iml
 
/jTET/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar

jTET/README

0 → 100644
+4 −0
Original line number Diff line number Diff line 
This folder needs a copy of the jTET library, currently available at:

https://groke.mcmaster.ca/gitlab/tables/jtet/

Place the target/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar file in this

directory and the TET will automatically pick it up.

jTET/pom.xml

deleted100644 → 0
+0 −121
Original line number Diff line number Diff line 
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"

         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">

    <modelVersion>4.0.0</modelVersion>

    <prerequisites>

        <maven>3.0</maven>

    </prerequisites>



    <groupId>ca.mcscert.jtet</groupId>

    <artifactId>jtet</artifactId>

    <version>1.0-SNAPSHOT</version>

    <packaging>jar</packaging>



    <name>jTET</name>

    <url>http://maven.apache.org</url>



    <properties>

        <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

    </properties>



    <dependencies>

        <dependency>

            <groupId>junit</groupId>

            <artifactId>junit</artifactId>

            <version>4.11</version>

            <scope>test</scope>

        </dependency>

        <dependency>

            <groupId>org.antlr</groupId>

            <artifactId>antlr4-runtime</artifactId>

            <version>4.2.2</version>

        </dependency>

        <dependency>

            <groupId>org.apache.commons</groupId>

            <artifactId>commons-lang3</artifactId>

            <version>3.3.2</version>

        </dependency>

    </dependencies>

  

    <build>

        <plugins>

            <plugin>

                <groupId>org.antlr</groupId>

                <artifactId>antlr4-maven-plugin</artifactId>

                <version>4.2.2</version>

                <configuration>

                    <sourceDirectory>src/main/java</sourceDirectory>

                </configuration>

                <executions>

                    <execution>

                        <goals>

                            <goal>antlr4</goal>

                        </goals>

                    </execution>

                </executions>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-compiler-plugin</artifactId>

                <version>3.1</version>

                <configuration>

                    <showDeprecation>true</showDeprecation>

                    <source>1.6</source>

                    <target>1.6</target>

                </configuration>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-assembly-plugin</artifactId>

                <version>2.4</version>

                <configuration>

                    <descriptorRefs>

                        <descriptorRef>jar-with-dependencies</descriptorRef>

                    </descriptorRefs>

                </configuration>

                <executions>

                    <execution>

                        <phase>package</phase>

                        <goals>

                            <goal>single</goal>

                        </goals>

                    </execution>

                </executions>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-clean-plugin</artifactId>

                <version>2.5</version>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-deploy-plugin</artifactId>

                <version>2.8.1</version>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-install-plugin</artifactId>

                <version>2.5.1</version>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-jar-plugin</artifactId>

                <version>2.4</version>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-resources-plugin</artifactId>

                <version>2.6</version>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-site-plugin</artifactId>

                <version>3.3</version>

            </plugin>

            <plugin>

                <groupId>org.apache.maven.plugins</groupId>

                <artifactId>maven-surefire-plugin</artifactId>

                <version>2.17</version>

            </plugin>

        </plugins>

    </build>

</project>

jTET/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

deleted100644 → 0
+0 −174
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * 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 the McMaster Centre for Software Certification 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 THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 THE COPYRIGHT OWNER OR CONTRIBUTORS 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.

 */

package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.CVC3Generator;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerGenerator;

import java.util.ArrayList;

import java.util.ArrayDeque;

import java.util.Deque;

import java.util.List;



import org.apache.commons.lang3.StringUtils;



/**

 *

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

final public class HierarchicalGridCVC3Generator implements HierarchcialGridCheckerGenerator {



    public HierarchicalGridCVC3Generator(VariableCollection variableDefinitions, int queryCountStart) {

        m_variableDefinitions = variableDefinitions;

        m_currentTCC = queryCountStart;

    }



    private String generateQueryPrefix() {

        if (!m_parentCellsCVC3Code.isEmpty()){

            String output = "(";

            output += StringUtils.join(m_parentCellsCVC3Code, " AND ");

            output += ") => ";

            return output;

        }

        return "";

    }



    private void outputCells() {

        // First is disjoint testing.

        m_output += "ECHO \"begin" + m_currentTCC + "\";\n";

        m_output += "PUSH;\n";



        String query = "QUERY ";

        query += generateQueryPrefix();

        query += "(" + StringUtils.join(m_currentDisjointQueries, " AND\n");

        query += ");";

        m_queries.add(query);

        m_output += query + "\n";



        m_output += "POP;\n";

        m_output += "ECHO \"end" + m_currentTCC + "\";\n";



        // Finished first TCC, increment counter.

        m_currentTCC++;



        // Next is complete.

        m_output += "ECHO \"begin" + m_currentTCC + "\";\n";

        m_output += "PUSH;\n";



        query = "QUERY ";

        query += generateQueryPrefix();

        query += "(" + StringUtils.join(m_currentCompleteQueries, " OR ");

        query += ");";

        m_queries.add(query);

        m_output += query + "\n";



        m_output += "POP;\n";

        m_output += "ECHO \"end" + m_currentTCC + "\";\n";



        // Finished other TCC, increment counter.

        m_currentTCC++;



        m_currentlyRunning = false;



        // And finally clear the running list of current queries.

        m_currentCompleteQueries.clear();

        m_currentDisjointQueries.clear();

    }



    @Override

    public void descendIntoGridFromCell(Cell cell) {

        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType));

        m_currentlyRunning = true;

    }



    @Override

    public void ascendFromGrid() {

        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.removeFirst();

    }



    @Override

    public void handleEdgeCell(Cell cell) {

        handleLeafCell(cell);

    }



    @Override

    public void handleLeafCell(Cell cell) {

        // First get the appropriate CVC3 code from matlab.

        String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType);



        // Next form the disjoint queries and add to the list.

        for(String otherCellCode : m_currentCompleteQueries) {

            String newDisjointQuery = "NOT ( " + otherCellCode  + " AND " + newCellCode + " )";

            m_currentDisjointQueries.add(newDisjointQuery);

        }



        // Lastly add the cell to the list for the complete query

        m_currentCompleteQueries.add(newCellCode);

    }



    @Override

    public String getFinalString() {

        if (m_currentlyRunning) {

            outputCells();

        }

        return m_output;

    }



    public List<String> getFinalQueries() {

        if (m_currentlyRunning) {

            outputCells();

        }

        return m_queries;

    }



    Deque<String> m_parentCellsCVC3Code = new ArrayDeque<String>();



    List<String> m_currentDisjointQueries = new ArrayList<String>();

    List<String> m_currentCompleteQueries = new ArrayList<String>();

    

    boolean m_currentlyRunning = true;

    int m_currentTCC = 1;



    String m_output = "";

    List<String> m_queries = new ArrayList<String>();



    // To fix properly.

    VariableCollection m_variableDefinitions;

    static BooleanVariableType m_booleanType = new BooleanVariableType();

    CVC3Generator m_CVC3Generator = new CVC3Generator();

}

jTET/src/main/java/ca/mcscert/jtet/expression/BinaryOperation.java

deleted100644 → 0
+0 −81
Original line number Diff line number Diff line 
/*

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcscert.jtet.expression;



import java.util.Arrays;

import java.util.Collection;



/**

 *

 * @author matthew

 */

public enum BinaryOperation {



    Addition,

    Minus,

    Multiplication,

    Division,

    Exponentiation,



    GreaterThen,

    GreaterThenEqual,

    LessThen,

    LessThenEqual,

    Equals,

    NotEquals,



    Implies,

    BooleanAnd,

    BooleanOr;



    Collection<VariableTypeMarker> getInputTypeForOutput(VariableTypeMarker outputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr || this == Implies || this == GreaterThen || this == GreaterThenEqual ||

                this == LessThen || this == LessThenEqual || this == Equals || this == NotEquals) {

            if (!outputType.equals(new BooleanVariableType())) {

                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");

            }

        }

        if (outputType instanceof  EnumerationVariableType) {

            if (this != Equals && this != NotEquals) {

                throw new IllegalArgumentException("Enumeration types can only be checked for equality!");

            }

        }



        // Comparisions produce boolean outputs!

        switch(this) {

            case GreaterThen:

            case GreaterThenEqual:

            case LessThen:

            case LessThenEqual:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});

            case Equals:

            case NotEquals:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker(), new EnumerationVariableType.Marker()});

        }

        return Arrays.asList(new VariableTypeMarker[]{outputType});

    }



    public VariableType getOutputForInput(VariableType inputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr || this == Implies) {

            if (!inputType.equals(new BooleanVariableType())) {

                throw new IllegalArgumentException("Boolean operators require a boolean input type!");

            }

        }



        // Comparisions produce boolean outputs!

        switch(this) {

            case GreaterThen:

            case GreaterThenEqual:

            case LessThen:

            case LessThenEqual:

            case Equals:

            case NotEquals:

                return new BooleanVariableType();

        }

        return inputType;

    }

}