Create a new CVC3TypeDeclarationGenerator. (94f6f45a) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/cvc3generator/CVC3TypeDeclarationGenerator.java

0 → 100644

+68 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2013 Matthew Dawson <jiangy76@mcmaster.ca>
		* Copyright (C) 2014 Yanjun Jiang <jiangy76@mcmaster.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.EnumerationVariableType;
		import ca.mcscert.jtet.expression.TypeDeclarationGenerator;
		import ca.mcscert.jtet.expression.VariableType;

		import java.util.Set;

		/**
		* @author Matthew Dawson
		* @author Yanjun Jiang
		*/
		final public class CVC3TypeDeclarationGenerator implements TypeDeclarationGenerator {
		@Override
		public String GenerateTypeDeclaration(Set<VariableType> types) {
		StringBuilder ret = new StringBuilder();
		// Generate all the enumeration types.
		for(VariableType type : types) {
		if (type instanceof EnumerationVariableType) {
		EnumerationVariableType enumType = (EnumerationVariableType) type;
		ret.append("DATATYPE\n ")
		.append((enumType).name())
		.append(" = ");

		boolean firstValue = false;
		for(String enumValue : enumType.enumerationValues()) {
		if (firstValue == true) {
		ret.append(" \| ");
		}
		firstValue = true;
		ret.append(enumValue);
		}
		ret.append("\nEND;\n");
		}
		}

		return ret.toString();
		}
		}

src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java

+3 −27

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
		* Copyright (C) 2014 Yanjun Jiang <jiangy76@mcmaster.ca>
		*
		* Redistribution and use in source and binary forms, with or without
		* modification, are permitted provided that the following conditions are
		@@ -29,14 +30,12 @@
		package ca.mcscert.jtet.cvc3generator;

		import ca.mcscert.jtet.expression.*;

		import java.util.HashSet;
		import java.util.Map;
		import java.util.Set;

		/**
		*
		* @author matthew
		* @author Yanjun Jiang
		*/
		final public class CVC3VariablesDeclarationGenerator implements VariablesDeclarationGenerator {
		public final static CVC3VariablesDeclarationGenerator Generator = new CVC3VariablesDeclarationGenerator();
		@@ -44,32 +43,9 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara
		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		Set<EnumerationVariableType> emittedEnumerations = new HashSet<EnumerationVariableType>();

		StringBuilder ret = new StringBuilder();
		// First generate all the enumeration types.
		for(Variable var : vars.values()) {
		if (var.type() instanceof EnumerationVariableType && !emittedEnumerations.contains(var.type())) {
		EnumerationVariableType enumType = (EnumerationVariableType) var.type();
		ret.append("DATATYPE\n ")
		.append((enumType).name())
		.append(" = ");

		boolean firstValue = false;
		for(String enumValue : enumType.enumerationValues()) {
		if (firstValue == true) {
		ret.append(" \| ");
		}
		firstValue = true;
		ret.append(enumValue);
		}
		ret.append("\nEND;\n");

		emittedEnumerations.add(enumType);
		}
		}

		// Then generate all the variables.
		// First generate all the variables.
		for(Variable var : vars.values()) {
		ret.append(var.outputName())
		.append(":")

src/test/java/ca/mcscert/jtet/expression/GenericTypeDeclarationGeneratorTest.java

+4 −0

Original line number	Diff line number	Diff line
		@@ -28,6 +28,7 @@
		*/
		package ca.mcscert.jtet.expression;

		import ca.mcscert.jtet.cvc3generator.CVC3TypeDeclarationGenerator;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.Parameterized;
		@@ -47,6 +48,9 @@ public class GenericTypeDeclarationGeneratorTest {
		@Parameters
		public static Collection<Object[]> data() {
		return Arrays.asList(new Object[][]{
		{new CVC3TypeDeclarationGenerator(),
		"DATATYPE\n Enum1 = e1 \| e2 \| e3\nEND;\n",
		}
		});
		}
		@Parameter(value = 0)

src/test/java/ca/mcscert/jtet/expression/GenericVariablesDeclarationGeneratorTest.java

+3 −3

Original line number	Diff line number	Diff line
		@@ -90,9 +90,9 @@ public class GenericVariablesDeclarationGeneratorTest {
		"x:BOOLEAN;\n",
		"x:BITVECTOR(8);\n",
		"x:BITVECTOR(8);\n",
		"DATATYPE\n MyEnum = e1 \| e2 \| e3\nEND;\nx:MyEnum;\n",
		"DATATYPE\n MyEnum = e1 \| e2 \| e3\nEND;\nnew_x_name:MyEnum;\n",
		"DATATYPE\n MyEnum = e1 \| e2 \| e3\nEND;\nx:MyEnum;\ny:MyEnum;\n"
		"x:MyEnum;\n",
		"new_x_name:MyEnum;\n",
		"x:MyEnum;\ny:MyEnum;\n"
		},
		{new EventBGenerator(),
		"<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"x\" org.eventb.core.identifier=\"x\"/>\n" +