Make VariableCollection handle both input and output variables. (7166a03a) · Commits · tables / jtet

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

+1 −1

Original line number	Diff line number	Diff line
		@@ -42,7 +42,7 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara

		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		Map<String, Variable> vars = variableCollection.getAllVariables();
		StringBuilder ret = new StringBuilder();

		// First generate all the variables.

src/main/java/ca/mcscert/jtet/eventbgenerator/EventBVariablesDeclarationGenerator.java

+3 −3

Original line number	Diff line number	Diff line
		@@ -62,7 +62,7 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla
		private String generateVariablesXml(VariableCollection variableCollection) {
		final String variableXmlPost = "\"/>\n";
		String ret = "";
		Map<String, Variable> vars = variableCollection.getVariables();
		Map<String, Variable> vars = variableCollection.getAllVariables();

		//generate all the variables one by one.
		for(Variable var : vars.values()) {
		@@ -86,7 +86,7 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla
		String ret = "";
		int invariantsNum = 1;
		final String invariantXmlPost = "\"/>\n";
		Map<String, Variable> vars = variableCollection.getVariables();
		Map<String, Variable> vars = variableCollection.getInputVariables();

		//generate all the Invariants one by one.
		for (Variable var : vars.values()) {
		@@ -130,7 +130,7 @@ final public class EventBVariablesDeclarationGenerator implements VariablesDecla

		private String generateInitEventActionsXml(VariableCollection variableCollection) {
		String ret = "";
		Map<String, Variable> vars = variableCollection.getVariables();
		Map<String, Variable> vars = variableCollection.getInputVariables();

		//generate all the Initialisation actions one by one.
		int actionNo = 0;

src/main/java/ca/mcscert/jtet/expression/PartialVariableCollection.java

0 → 100644

+54 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 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.expression;

		import java.util.Collections;
		import java.util.HashMap;
		import java.util.Map;
		import java.util.Set;

		/**
		* @author Matthew Dawson <matthew@mjdsystems.ca>
		*/
		final public class PartialVariableCollection {
		public PartialVariableCollection(Map<String, Variable> variables, Set<EnumerationVariableType> enumerationTypes) {
		m_variables = Collections.unmodifiableMap(variables);
		if (enumerationTypes == null) {
		enumerationTypes = Collections.emptySet();
		}
		m_enumerationTypes = Collections.unmodifiableSet(enumerationTypes);
		}

		public PartialVariableCollection(Map<String, Variable> variables) {
		this(variables, null);
		}

		public final Map<String,Variable> m_variables;
		public final Set<EnumerationVariableType> m_enumerationTypes;
		}

src/main/java/ca/mcscert/jtet/expression/VariableCollection.java

+58 −31

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
		* Copyright (C) 2014 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
		@@ -28,10 +28,7 @@
		*/
		package ca.mcscert.jtet.expression;

		import java.util.Collections;
		import java.util.HashMap;
		import java.util.Map;
		import java.util.Set;
		import java.util.*;

		/**
		* VariableCollection stores a set of variables for use by expression parsers.
		@@ -49,22 +46,30 @@ final public class VariableCollection {
		* Constructs a VariableCollection with the given variables and enumerations.
		* <p>
		* The VariableCollection constructed here will have the variables given, along with all the enumeration constants
		* from the given set of enumerations. Note that all enumeration constants must not conflict with each other or
		* any given variable.
		* from the partial collections.
		* <p>
		* Input and output variables are distinguished (if required by a generator), and passed in separately here.
		*
		* @param variables This variables to store in this collection.
		* @param enumerationTypes The set of enumerations for which the constants should be extracted. May be null.
		* @param inputVariables The input variables to store in this collection.
		* @param outputVariables The output variables to store in this collection.
		*/
		public VariableCollection(Map<String, Variable> variables, Set<EnumerationVariableType> enumerationTypes) {
		m_variables = variables;
		if (m_variables != null) {
		for(Map.Entry<String, Variable> var : m_variables.entrySet()) {
		m_variablesAndEnumeratedValues.put(var.getKey(), var.getValue());
		public VariableCollection(PartialVariableCollection inputVariables, PartialVariableCollection outputVariables) {
		Set<EnumerationVariableType> usedEnumerationTypes = new HashSet<EnumerationVariableType>();
		if (inputVariables != null) {
		m_inputVariables.putAll(inputVariables.m_variables);
		m_variablesAndEnumeratedValues.putAll(inputVariables.m_variables);

		usedEnumerationTypes.addAll(inputVariables.m_enumerationTypes);
		}

		if (outputVariables != null) {
		m_outputVariables.putAll(outputVariables.m_variables);
		m_variablesAndEnumeratedValues.putAll(outputVariables.m_variables);

		usedEnumerationTypes.addAll(outputVariables.m_enumerationTypes);
		}

		if (enumerationTypes != null) {
		for(EnumerationVariableType enumType : enumerationTypes) {
		for(EnumerationVariableType enumType : usedEnumerationTypes) {
		for(String enumValue : enumType.enumerationValues()) {
		if (m_variablesAndEnumeratedValues.containsKey(enumValue)) {
		throw new IllegalArgumentException("Enumerated value conflicts with existing variable!");
		@@ -73,17 +78,16 @@ final public class VariableCollection {
		}
		}
		}
		}

		/**
		* Constructs a VariableCollection with the given variables and enumerations.
		* <p>
		* The VariableCollection constructed here will have the variables given. No enumerations will be stored.
		* The VariableCollection constructed here will have the variables given. It leaves the output set of variables empty.
		*
		* @param variables This variables to store in this collection.
		* @param inputVariables The input variables to store in this collection.
		*/
		public VariableCollection(Map<String, Variable> variables) {
		this(variables, null);
		public VariableCollection(PartialVariableCollection inputVariables) {
		this(inputVariables, null);
		}

		/**
		@@ -98,15 +102,38 @@ final public class VariableCollection {
		}

		/**
		* Returns a map containing only the variables.
		* Returns a map containing only input the variables.
		* <p>
		* This ignores all the enumeration constants present.
		* @return A map of input variables.
		*/
		public Map<String, Variable> getInputVariables() {
		return Collections.unmodifiableMap(m_inputVariables);
		}

		/**
		* Returns a map containing only output the variables.
		* <p>
		* This ignores all the enumeration constants present.
		* @return A map of variables.
		* @return A map of output variables.
		*/
		public Map<String, Variable> getOutputVariables() {
		return Collections.unmodifiableMap(m_outputVariables);
		}

		/**
		* Returns a map containing all the variables.
		* <p>
		* This combines the input and output variables, ignoring all the enumeration constants present.
		* @return A map of output variables.
		*/
		public Map<String, Variable> getVariables() {
		return Collections.unmodifiableMap(m_variables);
		public Map<String, Variable> getAllVariables() {
		Map<String, Variable> variables = new LinkedHashMap<String, Variable>(m_inputVariables);
		variables.putAll(m_outputVariables);
		return Collections.unmodifiableMap(variables);
		}

		private final Map<String,Variable> m_variables;
		private final Map<String,Variable> m_inputVariables = new LinkedHashMap<String, Variable>();
		private final Map<String,Variable> m_outputVariables = new LinkedHashMap<String, Variable>();
		private final Map<String,Variable> m_variablesAndEnumeratedValues = new HashMap<String, Variable>();
		}

src/main/java/ca/mcscert/jtet/parsers/VariableParser.java

+5 −4

Original line number	Diff line number	Diff line
		@@ -31,6 +31,7 @@ package ca.mcscert.jtet.parsers;
		import ca.mcscert.jtet.expression.BooleanVariableType;
		import ca.mcscert.jtet.expression.EnumerationVariableType;
		import ca.mcscert.jtet.expression.FixedPointVariableType;
		import ca.mcscert.jtet.expression.PartialVariableCollection;
		import ca.mcscert.jtet.expression.RealVariableType;
		import ca.mcscert.jtet.expression.Variable;
		import ca.mcscert.jtet.expression.VariableCollection;
		@@ -62,7 +63,7 @@ import org.antlr.v4.runtime.tree.TerminalNode;
		*/
		final public class VariableParser {

		public VariableCollection parseVariables(String variables) {
		public PartialVariableCollection parseVariables(String variables) {
		// create a CharStream that reads from standard input
		ANTLRInputStream input = new ANTLRInputStream(variables) {

		@@ -177,19 +178,19 @@ final public class VariableParser {
		// effectively means the expression can just be emitted into the verification system to limit it.
		m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey()));

		VariableCollection variableCollection = new VariableCollection(m_variables, m_usedEnumerationTypes);
		VariableCollection variableCollection = new VariableCollection(new PartialVariableCollection(m_variables, m_usedEnumerationTypes));
		m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression));

		// Undo the variables hack, to avoid having unused variables bleed into the verification scripts!
		m_variables.remove(subtypeVar);
		}

		m_variableCollection = new VariableCollection(m_variables, m_usedEnumerationTypes);
		m_variableCollection = new PartialVariableCollection(m_variables, m_usedEnumerationTypes);
		}

		private Map<String, Variable> m_variables = new LinkedHashMap<String, Variable>();
		private Set<EnumerationVariableType> m_usedEnumerationTypes = new HashSet<EnumerationVariableType>();
		public VariableCollection m_variableCollection;
		public PartialVariableCollection m_variableCollection;

		private Map<String, limitingExpressionData> m_variableLimitingExpressions = new HashMap<String, limitingExpressionData>();
		}