Skip to content
/*
* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParser;
import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameter;
import org.junit.runners.Parameterized.Parameters;
import java.util.Arrays;
import java.util.Collection;
import java.util.Map;
import static org.junit.Assert.*;
/**
* @author Matthew Dawson <matthew@mjdsystems.ca>
*/
@RunWith(Parameterized.class)
public class GenericGeneratorTest {
@Parameters
public static Collection<Object[]> data() {
return Arrays.asList(new Object[][]{
{new SMTLIBGenerator(),
"(=> (or (= (* x 5.0) (/ 1.0 (- 4.0))) (or (and (> x (+ 8.0 3.0)) (< 9.0 (- x 2.0))) (or (>= x 12.0) (or (not (<= 34.0 (- x))) (> 5.0 4.0))))) (distinct x 5.0))",
null,
null},
{new CVC3Generator(),
"((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",
"(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVSGE(x,0bin00110000) OR ((NOT BVSLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))",
"(((BVMULT(8,x,0bin00010100) = BVUDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))"
}
});
}
static private String query = "(x * 5) = (1 / -4) OR ((x > (8 + 3)) AND (9 < x - 2)) OR x >= 12 OR NOT (34 <= -x) OR (5 > 4) => (x /= 5)";
static private VariableType outputType = new BooleanVariableType();
@Parameter(value = 0)
public CheckerGenerator generator;
@Parameter(value = 1)
public String RealExpectedOutput;
@Parameter(value = 2)
public String SignedFixedPointExpectedOutput;
@Parameter(value = 3)
public String UnsignedFixedPointExpectedOutput;
@Test
public void RealTest() {
if (RealExpectedOutput != null) {
VariableCollection vars = variableParser.parseVariables("x");
Expression expr = PVSSimpleParser.parsePVSCode(vars, query);
assertEquals(RealExpectedOutput, expr.getCheckerOutput(generator, outputType));
}
}
@Test
public void SignedFixedPointTest() {
if (SignedFixedPointExpectedOutput != null) {
VariableCollection vars = variableParser.parseVariables("x:fixedt(1, 8, 2)");
Expression expr = PVSSimpleParser.parsePVSCode(vars, query);
assertEquals(SignedFixedPointExpectedOutput, expr.getCheckerOutput(generator, outputType));
}
}
@Test
public void UnsignedFixedPointTest() {
if (UnsignedFixedPointExpectedOutput != null) {
VariableCollection vars = variableParser.parseVariables("x:fixedt(0, 8, 2)");
Expression expr = PVSSimpleParser.parsePVSCode(vars, query);
assertEquals(UnsignedFixedPointExpectedOutput, expr.getCheckerOutput(generator, outputType));
}
}
VariableParser variableParser = new VariableParser();
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
import static org.junit.Assert.*;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
/**
*
* @author matthew
*/
@RunWith(JUnit4.class)
public class MatlabExpressionBinaryOperationTest {
/**
* Test of type method, of class ExpressionBinaryOperation.
*/
@Test
public void testWithSimpleRealVariablesAddedTogether() {
Variable l = new Variable("a", new RealVariableType()), r = new Variable("b", new RealVariableType());
ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r);
String CVC3Output = "(a + b)";
VariableType expressionType = new RealVariableType();
assertEquals(CVC3Output, instance.getCheckerOutput(generator, expressionType));
assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType));
}
/**
* Test of type method, of class ExpressionBinaryOperation.
*/
@Test
public void testWithSimpleFixedPointVariablesAddedTogether() {
Variable l = new Variable("a", new FixedPointVariableType(true, 17, 4)), r = new Variable("b", new FixedPointVariableType(true, 17, 4));
ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r);
String CVC3Output = "BVPLUS(17,a,b)";
VariableType expressionType = new FixedPointVariableType(true, 17, 4);
assertEquals(CVC3Output, instance.getCheckerOutput(generator, expressionType));
assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType));
}
/**
* Test of setLHS/RHS, verify they set variables correctly.
*/
@Test
public void testSettingsLHSAndRHS() {
Variable l = new Variable("a", new RealVariableType()), r = new Variable("b", new RealVariableType());
ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r);
//Reverse a+b to b+a.
instance.setLHS(r);
instance.setRHS(l);
String CVC3Output = "(b + a)";
VariableType expressionType = new RealVariableType();
assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType));
assertEquals(CVC3Output, instance.getCheckerOutput(new CVC3Generator(), expressionType));
}
/**
* Test when RHS/LHS have different castable types.
*/
@Test
public void testCastableTypes() {
Literal lit = new Literal("5");
Variable var = new Variable("A", new RealVariableType());
VariableType exprType;
// Test when adding a Real var to a lit, type always becomes Real.
exprType = new RealVariableType();
assertEquals(exprType, new ExpressionBinaryOperation(lit, BinaryOperation.Addition, var).actualOutputTypeForRequestedOutput(exprType));
assertEquals(exprType, new ExpressionBinaryOperation(var, BinaryOperation.Addition, lit).actualOutputTypeForRequestedOutput(exprType));
// Test when comparing a Real var to a lit, type always becomes boolean.
exprType = new BooleanVariableType();
assertEquals(exprType, new ExpressionBinaryOperation(lit, BinaryOperation.Equals, var).actualOutputTypeForRequestedOutput(exprType));
assertEquals(exprType, new ExpressionBinaryOperation(var, BinaryOperation.Equals, lit).actualOutputTypeForRequestedOutput(exprType));
}
/**
* Test operations changing types (== doing REAL+REAL -> BOOLEAN)
*/
@Test
public void testCastingOperations() {
Literal l = new Literal("5"), r = new Literal("6");
ExpressionBinaryOperation exp = new ExpressionBinaryOperation(l, BinaryOperation.Equals, r);
// Test when adding a Real var to a lit, type always becomes Real.
VariableType expressionType = new BooleanVariableType();
assertEquals(expressionType, exp.actualOutputTypeForRequestedOutput(expressionType));
assertEquals("(5 = 6)", exp.getCheckerOutput(generator, expressionType));
}
/**
* Test operations fails when a requested type is invalid!
*/
@Test(expected=IllegalArgumentException.class)
public void testInvalidOutputType() {
Literal l = new Literal("5"), r = new Literal("6");
ExpressionBinaryOperation exp = new ExpressionBinaryOperation(l, BinaryOperation.Equals, r);
exp.getCheckerOutput(generator, new RealVariableType()); //Returns a boolean, so will fail.
}
/**
* Test doing multiple boolean operations AND'd together.
*/
@Test
public void testBooleanAndFromComparision() {
Expression l = new Variable("a", new RealVariableType()), r = new Literal("6"),
l2 = new Variable("b", new RealVariableType()), r2 = new Literal("8");
ExpressionBinaryOperation exp = new ExpressionBinaryOperation(new ExpressionBinaryOperation(l, BinaryOperation.Equals, r),
BinaryOperation.BooleanAnd,
new ExpressionBinaryOperation(l2, BinaryOperation.Equals, r2));
// Test when adding a Real var to a lit, type always becomes Real.
VariableType expressionType = new BooleanVariableType();
assertEquals(expressionType, exp.actualOutputTypeForRequestedOutput(expressionType));
assertEquals("((a = 6) AND (b = 8))", exp.getCheckerOutput(generator, expressionType));
}
CheckerGenerator generator = new CVC3Generator();
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression;
import static org.hamcrest.CoreMatchers.is;
import static org.junit.Assert.*;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
import java.util.HashMap;
import java.util.Map;
/**
*
* @author matthew
*/
@RunWith(JUnit4.class)
public class VariableTest {
@Test
public void exerciseVariable() {
String name = "Var";
VariableType type = new RealVariableType();
Variable var = new Variable(name, type);
assertSame(name, var.name());
assertSame(type, var.type());
assertEquals(name, var.getCheckerOutput(null, new RealVariableType()));
Map<String, Variable> varList = new HashMap<String, Variable>();
varList.put(name, var);
VariableCollection variableCollection = new VariableCollection(varList);
CheckerGenerator generator = new CVC3Generator();
assertEquals(name+":REAL;\n", generator.GenerateVariablesDeclaration(variableCollection));
generator = new SMTLIBGenerator();
assertEquals("(declare-fun " +name+ " () Real)\n", generator.GenerateVariablesDeclaration(variableCollection));
}
@Test
public void testSubtypePredicate() {
// Construct a basic variable. Assume it is correct due to the above test.
Variable var = new Variable("var", new RealVariableType());
// Next create a subtype predicate. For now, make it work over positive reals (excluding 0)
Expression predicate = new ExpressionBinaryOperation(var, BinaryOperation.GreaterThen, new Literal("0"));
var.type().setSubtypePredicate(predicate);
// Verify the predicate took.
assertThat(var.type().subtypePredicate(), is(predicate));
// Make a variable list for the generators.
Map<String, Variable> varList = new HashMap<String, Variable>();
varList.put("var", var);
VariableCollection variableCollection = new VariableCollection(varList);
CheckerGenerator generator = new CVC3Generator();
String varDecl = generator.GenerateVariablesDeclaration(variableCollection);
assertThat(varDecl, is("var:REAL;\nASSERT (var > 0);\n"));
generator = new SMTLIBGenerator();
varDecl = generator.GenerateVariablesDeclaration(variableCollection);
assertThat(varDecl, is("(declare-fun var () Real)\n(assert (> var 0.0))\n"));
}
// Verify handling of invalid type to getCheckerOutput
@Test(expected=IllegalArgumentException.class)
public void testInvalidOutputType() {
String name = "Var";
VariableType type = new BooleanVariableType();
Variable var = new Variable(name, type);
var.getCheckerOutput(null, new RealVariableType()); //Returns a boolean, so will fail.
}
}
package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
import junit.framework.Test;
import junit.framework.TestCase;
import junit.framework.TestSuite;
/**
* Unit test for simple App.
*/
public class AppTest
extends TestCase
{
/**
* Create the test case
*
* @param testName name of the test case
*/
public AppTest( String testName )
{
super( testName );
}
/**
* @return the suite of tests being tested
*/
public static Test suite()
{
return new TestSuite( AppTest.class );
}
/**
* Rigourous Test :-)
*/
public void testApp()
{
assertTrue( true );
}
/**
* Rigourous Test :-)
*/
public void testAppFail()
{
assertFalse( false );
}
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
import org.junit.Test;
import static org.junit.Assert.*;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
/**
*
* @author matthew
*/
@RunWith(JUnit4.class)
public class BooleanVariableTypeTest {
/**
* Test of getCVC3Definition method, of class RealVariableType.
*/
@Test
public void testGetCVC3Definition() {
CVC3Generator generator = new CVC3Generator();
String variableName = "test_variable";
BooleanVariableType instance = new BooleanVariableType();
String expResult = "BOOLEAN";
String result = generator.GenerateVariableType(instance);
assertEquals(expResult, result);
}
/**
* Test of SMT-LIB generation of boolean type.
*/
@Test
public void testGetSMTLIBDefinition() {
SMTLIBGenerator generator = new SMTLIBGenerator();
String variableName = "test_variable";
BooleanVariableType instance = new BooleanVariableType();
String expResult = "Bool";
String result = generator.GenerateVariableType(instance);
assertEquals(expResult, result);
}
/**
* Test of equals method, of class RealVariableType.
*/
@Test
public void testEquals() {
BooleanVariableType test = new BooleanVariableType();
assertTrue(test.equals(new BooleanVariableType()));
assertTrue(test.equals(test));
assertFalse(test.equals(new Object()));
}
/**
* Test of hashCode method, of class RealVariableType.
*/
@Test
public void testHashCode() {
BooleanVariableType instance = new BooleanVariableType();
assertEquals(0, instance.hashCode());
}
/**
* Test of canCastToType method, of class RealVariableType. Reals (for now)
* don't cast.
*/
@Test
public void testCanCastToType() {
BooleanVariableType instance = new BooleanVariableType();
assertFalse(instance.canCastToType(new RealVariableType()));
assertFalse(instance.canCastToType(new BooleanVariableType()));
}
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;
import org.junit.Test;
import static org.junit.Assert.*;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
/**
*
* @author matthew
*/
@RunWith(JUnit4.class)
public class MatlabLiteralTest {
/**
* Test of canHandleOutputType method, of class Literal.
*/
@Test
public void testType() {
Literal instance = new Literal(null);
VariableType exprType = new RealVariableType();
assertEquals(exprType, instance.actualOutputTypeForRequestedOutput(exprType));
}
/**
* Test of getCVC3Output method, of class Literal. Test only natural numbers;
*/
@Test
public void testGetCVC3Output() {
Literal instance = new Literal("5");
assertEquals("5", instance.getCheckerOutput(generator, new RealVariableType()));
assertEquals("0bin00101", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 0)));
assertEquals("0bin01010", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
}
/**
* Test of getCVC3Output method, of class Literal. Test fun fixed point number;
*/
@Test
public void testCVC3OutputOnInterestingFixedPoint() {
Literal instance = new Literal("0");
assertEquals("0bin00000", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
instance = new Literal("5.5");
assertEquals("0bin01011", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
instance = new Literal("-5.5");
assertEquals("0bin10101", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1)));
instance = new Literal("-5");
assertEquals("0bin11011", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 0)));
}
CheckerGenerator generator = new CVC3Generator();
}
/*
* To change this template, choose Tools | Templates
* and open the template in the editor.
*/
package ca.mcmaster.cas.tabularexpressiontoolbox.expression.test;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;
import org.junit.Test;
import static org.junit.Assert.*;
import org.junit.runner.RunWith;
import org.junit.runners.JUnit4;
/**
*
* @author matthew
*/
@RunWith(JUnit4.class)
public class RealVariableTypeTest {
/**
* Test of getCVC3Definition method, of class RealVariableType.
*/
@Test
public void testGetCVC3Definition() {
CVC3Generator generator = new CVC3Generator();
String variableName = "test_variable";
RealVariableType instance = new RealVariableType();
String expResult = "REAL";
String result = generator.GenerateVariableType(instance);
assertEquals(expResult, result);
}
/**
* Test SMTLIB generates the correct type.
*/
@Test
public void testGetSMTLIBDefinition() {
SMTLIBGenerator generator = new SMTLIBGenerator();
String variableName = "test_variable";
RealVariableType instance = new RealVariableType();
String expResult = "Real";
String result = generator.GenerateVariableType(instance);
assertEquals(expResult, result);
}
/**
* Test of equals method, of class RealVariableType.
*/
@Test
public void testEquals() {
RealVariableType test = new RealVariableType();
assertTrue(test.equals(new RealVariableType()));
assertTrue(test.equals(test));
assertFalse(test.equals(new Object()));
}
/**
* Test of hashCode method, of class RealVariableType.
*/
@Test
public void testHashCode() {
RealVariableType instance = new RealVariableType();
assertEquals(0, instance.hashCode());
}
/**
* Test of canCastToType method, of class RealVariableType. Reals (for now)
* don't cast.
*/
@Test
public void testCanCastToType() {
RealVariableType instance = new RealVariableType();
assertFalse(instance.canCastToType(new RealVariableType()));
assertFalse(instance.canCastToType(new BooleanVariableType()));
}
}
classdef (Sealed) TET < handle
%TET provides the global settings for the Tabular Expression Toolbox
% TET provides the system through which all global settings are
% accssed and changed. It also provides a convient place for some
% globals used in the TET.
properties (Access = private)
variableParser = ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser
end
methods
function variableParser = getVariableParser(obj)
variableParser = obj.variableParser;
end
end
methods (Access = private)
function obj = TET
end
end
methods (Static)
function singleObj = getInstance
persistent localObj
if isempty(localObj) || ~isvalid(localObj)
localObj = TET;
end
singleObj = localObj;
end
end
end
This diff is collapsed.