UMB fixes

prism/src/io/UMBImporter.java

@@ -331,9 +331,6 @@ private void buildVarInfo(UMBIndex.UMBEntity entity, VarList varList) throws Pri
 				if (umbIndex.getNumValuationClasses(entity) > 1) {
 					throw new PrismException("Import of multiple valuation classes not yet supported");
 				}
-				if (!umbIndex.areValuationsUnique(entity)) {
-					throw new PrismException("UMB valuations for " + entity + " are not unique");
-				}
 			}
 			UMBBitPacking bitPacking = umbIndex.getValuationBitPacking(entity);
 			int numVars = bitPacking.getNumVariables();
@@ -356,15 +353,27 @@ private void buildVarInfo(UMBIndex.UMBEntity entity, VarList varList) throws Pri
 						int varIntMin;
 						int varIntMax;
 						if (computeRange) {
-							UMBReader.IntRange varIntRange = umbReader.getValuationIntRange(entity, bitPacking, i);
-							varIntMin = varIntRange.getMin();
-							varIntMax = varIntRange.getMax();
+							UMBReader.LongRange varLongRange = umbReader.getValuationLongRange(entity, bitPacking, i);
+							long varLongMin = varLongRange.getMin();
+							long varLongMax = varLongRange.getMax();
+							try {
+								varIntMin = SafeCast.toIntExact(varLongMin);
+								varIntMax = SafeCast.toIntExact(varLongMax);
+							} catch (ArithmeticException e) {
+								throw new PrismException("UMB variable " + var.name + " exceeds the range of an int");
+							}
 						} else {
 							// Default to min/max values for (u)ints
 							if (var.getType().type == UMBType.Type.INT) {
+								if (bitPacking.getVariableSize(i) > 32) {
+									throw new PrismException("UMB variable " + var.name + " exceeds the range of an int");
+								}
 								varIntMin = -(1 << (bitPacking.getVariableSize(i) - 1));
 								varIntMax = (1 << (bitPacking.getVariableSize(i) - 1)) -1;
 							} else {
+								if (bitPacking.getVariableSize(i) >= 32) {
+									throw new PrismException("UMB variable " + var.name + " exceeds the range of an int");
+								}
 								varIntMin = 0;
 								varIntMax = (1 << bitPacking.getVariableSize(i)) - 1;
 							}
@@ -405,7 +414,7 @@ public void extractStates(IOUtils.StateDefnConsumer storeStateDefn) throws Prism
 				try {
 					//System.out.println(s + ":" + bitPacking.decodeBitString(bitString));
 					for (int i = 0; i < numVars; i++) {
-						storeStateDefn.accept(s.get(), i, bitPacking.getVariableValue(bitString, i));
+						storeStateDefn.accept(s.get(), i, getBitStringValue(bitPacking, bitString, i));
 					}
 					s.incrementAndGet();
 				} catch (UMBException | PrismException e) {
@@ -434,7 +443,7 @@ public void extractObservationDefinitions(IOUtils.StateDefnConsumer storeObserva
 				try {
 					//System.out.println(s + ":" + bitPacking.decodeBitString(bitString));
 					for (int i = 0; i < numVars; i++) {
-						storeObservationDefn.accept(s.get(), i, bitPacking.getVariableValue(bitString, i));
+						storeObservationDefn.accept(s.get(), i, getBitStringValue(bitPacking, bitString, i));
 					}
 					s.incrementAndGet();
 				} catch (UMBException | PrismException e) {
@@ -446,6 +455,34 @@ public void extractObservationDefinitions(IOUtils.StateDefnConsumer storeObserva
 		}
 	}
 
+	/**
+	 * Get the value of the {@code i}th variable, from a bit string, as an Object
+	 */
+	private Object getBitStringValue(UMBBitPacking bitPacking, UMBBitString bitString, int i) throws UMBException
+	{
+		UMBBitPacking.BitPackedVariable var = bitPacking.getVariable(i);
+		switch (var.getType().type) {
+			case BOOL:
+				return bitPacking.getBooleanVariableValue(bitString, i);
+			case INT:
+				try {
+					return SafeCast.toIntExact(bitPacking.getLongVariableValue(bitString, i));
+				} catch (ArithmeticException e) {
+					throw new UMBException("UMB variable " + var.name + " exceeds the range of an int");
+				}
+			case UINT:
+				try {
+					return SafeCast.toIntExact(bitPacking.getULongVariableValue(bitString, i));
+				} catch (ArithmeticException e) {
+					throw new UMBException("UMB variable " + var.name + " exceeds the range of an int");
+				}
+			case DOUBLE:
+				return bitPacking.getDoubleVariableValue(bitString, i);
+			default:
+				throw new UMBException("Unknown UMB variable tyoe: " + var.getType().type);
+		}
+	}
+
 	@Override
 	public int computeMaxNumChoices() throws PrismException
 	{

prism/src/io/github/pmctools/umbj/UMBBitPacking.java

@@ -229,7 +229,9 @@ public UMBBitString newBitString()
 		return new UMBBitString(getTotalNumBytes());
 	}
 
-	/** Set the value of the {@code i}th variable, which must be a (signed) integer, in a bit string.
+	/**
+	 * Set the value of the {@code i}th variable, which must be a (signed) integer, in a bit string.
+	 * This assumes that the integer needs at most 32 bits, so that it can be stored in an {@code int}.
 	 * @param bitString The bit string to modify
 	 * @param i The index of the variable
 	 * @param value The value to set
@@ -239,7 +241,9 @@ public void setIntVariableValue(UMBBitString bitString, int i, int value) throws
 		bitString.setInt(getVariableOffset(i), getVariableSize(i), value);
 	}
 
-	/** Set the value of the {@code i}th variable, which must be an (unsigned) integer, in a bit string.
+	/**
+	 * Set the value of the {@code i}th variable, which must be an (unsigned) integer, in a bit string.
+	 * This assumes that the integer needs at most 32 bits, so that it can be stored in an {@code int}.
 	 * @param bitString The bit string to modify
 	 * @param i The index of the variable
 	 * @param value The value to set
@@ -249,6 +253,30 @@ public void setUIntVariableValue(UMBBitString bitString, int i, int value) throw
 		bitString.setUInt(getVariableOffset(i), getVariableSize(i), value);
 	}
 
+	/**
+	 * Set the value of the {@code i}th variable, which must be a (signed) integer, in a bit string.
+	 * This assumes that the integer needs at most 64 bits, so that it can be stored in a {@code long}.
+	 * @param bitString The bit string to modify
+	 * @param i The index of the variable
+	 * @param value The value to set
+	 */
+	public void setLongVariableValue(UMBBitString bitString, int i, long value) throws UMBException
+	{
+		bitString.setLong(getVariableOffset(i), getVariableSize(i), value);
+	}
+
+	/**
+	 * Set the value of the {@code i}th variable, which must be an (unsigned) integer, in a bit string.
+	 * This assumes that the integer needs at most 64 bits, so that it can be stored in a {@code long}.
+	 * @param bitString The bit string to modify
+	 * @param i The index of the variable
+	 * @param value The value to set
+	 */
+	public void setULongVariableValue(UMBBitString bitString, int i, long value) throws UMBException
+	{
+		bitString.setULong(getVariableOffset(i), getVariableSize(i), value);
+	}
+
 	/** Set the value of the {@code i}th variable, which must be a double, in a bit string.
 	 * @param bitString The bit string to modify
 	 * @param i The index of the variable
@@ -293,6 +321,7 @@ public Object getVariableValue(UMBBitString bitString, int i) throws UMBExceptio
 
 	/**
 	 * Get the value of the {@code i}th variable, which must be a (signed) integer, from a bit string.
+	 * This assumes that the integer needs at most 32 bits, so that it can be stored in an {@code int}.
 	 */
 	public int getIntVariableValue(UMBBitString bitString, int i) throws UMBException
 	{
@@ -301,12 +330,31 @@ public int getIntVariableValue(UMBBitString bitString, int i) throws UMBExceptio
 
 	/**
 	 * Get the value of the {@code i}th variable, which must be an (unsigned) integer, from a bit string.
+	 * This assumes that the integer needs at most 32 bits, so that it can be stored in an {@code int}.
 	 */
 	public int getUIntVariableValue(UMBBitString bitString, int i) throws UMBException
 	{
 		return bitString.getUInt(getVariableOffset(i), getVariableSize(i));
 	}
 
+	/**
+	 * Get the value of the {@code i}th variable, which must be a (signed) integer, from a bit string.
+	 * This assumes that the integer needs at most 64 bits, so that it can be stored in a {@code long}.
+	 */
+	public long getLongVariableValue(UMBBitString bitString, int i) throws UMBException
+	{
+		return bitString.getLong(getVariableOffset(i), getVariableSize(i));
+	}
+
+	/**
+	 * Get the value of the {@code i}th variable, which must be an (unsigned) integer, from a bit string.
+	 * This assumes that the integer needs at most 64 bits, so that it can be stored in a {@code long}.
+	 */
+	public long getULongVariableValue(UMBBitString bitString, int i) throws UMBException
+	{
+		return bitString.getULong(getVariableOffset(i), getVariableSize(i));
+	}
+
 	/**
 	 * Get the value of the {@code i}th variable, which must be a double, from a bit string.
 	 */

prism/src/io/github/pmctools/umbj/UMBBitString.java

@@ -35,6 +35,7 @@ public UMBBitString(int numBytes)
 
 	/**
 	 * Store the value of an {@code n}-bit (signed) integer in a portion of the bit string.
+	 * This assumes that the integer needs at most 32 bits, so that it can be stored in an {@code int}.
 	 * @param offset The first bit of the bitstring portion
 	 * @param n The size (in bits) of the bitstring portion
 	 * @param value The value to store
@@ -55,6 +56,7 @@ public void setInt(int offset, int n, int value) throws UMBException
 
 	/**
 	 * Store the value of an {@code n}-bit unsigned integer in a portion of the bit string.
+	 * This assumes that the integer needs at most 32 bits, so that it can be stored in an {@code int}.
 	 * @param offset The first bit of the bitstring portion
 	 * @param n The size (in bits) of the bitstring portion
 	 * @param value The value to store
@@ -68,6 +70,43 @@ public void setUInt(int offset, int n, int value) throws UMBException
 		setInt(offset, n, value);
 	}
 
+	/**
+	 * Store the value of an {@code n}-bit (signed) integer in a portion of the bit string.
+	 * This assumes that the integer needs at most 64 bits, so that it can be stored in a {@code long}.
+	 * @param offset The first bit of the bitstring portion
+	 * @param n The size (in bits) of the bitstring portion
+	 * @param value The value to store
+	 */
+	public void setLong(int offset, int n, long value) throws UMBException
+	{
+		if (n > 64) {
+			throw new UMBException("Cannot store integer of " + n + " bits (too large for Java long)");
+		}
+		// Store bits into the byte array
+		for (int i = 0; i < n; i++) {
+			// Copy the i-th (least significant) bit of value to the appropriate bit in bytes
+			char valueBitShifted = (char) (((value >>> i) & 1) << ((offset + i) & 7));
+			char byteMask = (char) ('\u0001' << ((offset + i) & 7));
+			bytes[(offset + i) >> 3] = (byte) ((bytes[(offset + i) >> 3] & ~(byteMask)) | (valueBitShifted));
+		}
+	}
+
+	/**
+	 * Store the value of an {@code n}-bit unsigned integer in a portion of the bit string.
+	 * This assumes that the integer needs at most 64 bits, so that it can be stored in a {@code long}.
+	 * @param offset The first bit of the bitstring portion
+	 * @param n The size (in bits) of the bitstring portion
+	 * @param value The value to store
+	 */
+	public void setULong(int offset, int n, long value) throws UMBException
+	{
+		if (n >= 64) {
+			throw new UMBException("Cannot store unsigned integer of " + n + " bits (too large for Java long)");
+		}
+		// Storing (including bit truncation) is the same as for signed integers
+		setLong(offset, n, value);
+	}
+
 	/**
 	 * Store the value of a (64-bit) double in a portion of the bit string.
 	 * @param offset The first bit of the bitstring portion
@@ -146,6 +185,48 @@ public int getUInt(int offset, int n) throws UMBException
 		return value;
 	}
 
+	/**
+	 * Get the value of an {@code n}-bit (signed) integer, extracted from a portion of the bit string.
+	 * If the value does not fit into a standard Java (64-bit) signed long, an exception is thrown.
+	 * @param offset The first bit of the bitstring portion
+	 * @param n The size (in bits) of the bitstring portion
+	 */
+	public long getLong(int offset, int n) throws UMBException
+	{
+		if (n > 64) {
+			throw new UMBException("Cannot extract integer of " + n + " bits (too large for Java long)");
+		}
+		// Extract bits into a long
+		long value = 0;
+		for (int i = offset + n - 1; i >= offset; i--) {
+			value = (value << 1) | ((bytes[i >> 3] & (1L << (i & 7))) != 0 ? 1 : 0);
+		}
+		// Sign extend if necessary
+		if ((value & (1 << (n - 1))) != 0) {
+			value -= (1 << n);
+		}
+		return value;
+	}
+
+	/**
+	 * Get the value of an {@code n}-bit unsigned integer, extracted from a portion of the bit string.
+	 * If the value does not fit into a standard Java (64-bit) signed long, an exception is thrown.
+	 * @param offset The first bit of the bitstring portion
+	 * @param n The size (in bits) of the bitstring portion
+	 */
+	public long getULong(int offset, int n) throws UMBException
+	{
+		if (n >= 64) {
+			throw new UMBException("Cannot extract unsigned integer of " + n + " bits (too large for Java long)");
+		}
+		// Extract bits into a long
+		long value = 0;
+		for (int i = offset + n - 1; i >= offset; i--) {
+			value = (value << 1) | ((bytes[i >> 3] & (1L << (i & 7))) != 0 ? 1 : 0);
+		}
+		return value;
+	}
+
 	/**
 	 * Get the value of a (64-bit) double, extracted from a portion of the bit string.
 	 * @param offset The first bit of the bitstring portion

prism/src/io/github/pmctools/umbj/UMBFormat.java

@@ -79,6 +79,13 @@ public class UMBFormat
 	/** Filename for storing valuation classes */
 	public static final String VALUATION_CLASSES = "valuation-to-class" + BIN_FILE_EXT;
 
+	// Default values for binary files
+
+	public enum BinFileDefaultValue
+	{
+		IDENTITY, ZERO, ONE
+	}
+
 	// Allowable compression formats
 
 	public enum CompressionFormat