prism-accumulation/prism/src/pta/DB.java

//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM 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 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM 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 PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package pta;

/**
 * Helper class for encapsulation of difference bound as an integer.
 * We use the least significant bit to encode strictness in the bound
 * (1 = non-strict, 0 = strict); the rest is for the (integer) bound.
 * Upper bound of infinity is encoded as Integer.MAX_VALUE.
 */
public class DB
{
	// Bit masks, etc.
	protected final static int NON_STRICT = 0x1;
	protected final static int DIFF_MASK = ~0x1;
	protected final static int INFTY = Integer.MAX_VALUE;
	protected final static int LEQ_ZERO = 0x1;
	protected final static int LT_ZERO = 0x0;
	protected final static int LEQ_MINUS_ONE = (-1 << 1) | NON_STRICT;

	// Created bound <=v
	protected static int createLeq(int v)
	{
		return (v << 1) | NON_STRICT;
	}

	// Create bound <v
	protected static int createLt(int v)
	{
		return (v << 1);
	}

	// Get (signed) difference part of bound
	protected static int getSignedDiff(int d)
	{
		return (DIFF_MASK & d) >> 1;
	}

	// Is bound strict?
	protected static boolean isStrict(int d)
	{
		return (NON_STRICT & d) == 0;
	}

	// Is infinity
	protected static boolean isInfty(int d)
	{
		return (d == INFTY);
	}

	// Add two bounds
	protected static int add(int d1, int d2)
	{
		// Anything + inf = inf
		if (d1 == INFTY || d2 == INFTY)
			return INFTY;
		// Both leq: <=m + <=n = <=m+n; else: <m+n
		return d1 + d2 - ((d1 & NON_STRICT) | (d2 & NON_STRICT));
	}

	// Compute dual bound: flip both strictness and sign
	protected static int dual(int d)
	{
		if (d == INFTY)
			return d;
		// TODO: probably a more efficient way to do this
		return isStrict(d) ? createLeq(-getSignedDiff(d)) : createLt(-getSignedDiff(d)); 
	}

	// Get bound as a string
	protected static String toString(int d)
	{
		if (d == INFTY)
			return "<inf";
		return (isStrict(d) ? "<" : "<=") + getSignedDiff(d);
	}

	// Get bound as a string, multiplied by -1 and flipped, e.g. "<v" -> "-v<" 
	protected static String toStringFlipped(int d)
	{
		if (d == INFTY)
			return "-inf<";
		return (-getSignedDiff(d)) + (isStrict(d) ? "<" : "<=");
	}

	// Get constraint as a string
	protected static String constraintToString(int i, int j, int d, PTA pta)
	{
		String s;
		if (i > 0) {
			// x-y < v
			if (j > 0) {
				s = pta.getClockName(i);
				// x-y < inf
				if (isInfty(d))
					s += "-" + pta.getClockName(j) + "<inf";
				// x-y < 0  ->  x < y
				else if (getSignedDiff(d) == 0)
					s += (isStrict(d) ? "<" : "<=") + pta.getClockName(j);
				// x-y < v
				else
					s += "-" + pta.getClockName(j) + (isStrict(d) ? "<" : "<=") + getSignedDiff(d);
				// x-0 < v
			} else {
				s = pta.getClockName(i);
				if (isInfty(d))
					s += "<inf";
				else
					s += (isStrict(d) ? "<" : "<=") + getSignedDiff(d);
			}
		}
		// 0-y < v  ->  y > -v
		else {
			s = pta.getClockName(j);
			if (isInfty(d))
				s += ">-inf";
			else
				s += (isStrict(d) ? ">" : ">=") + (-getSignedDiff(d));
		}
		return s;
	}

	// Get constraint pair as a string
	// (x - y < v2 and y - x < v1, i.e. -v1 < x - y < v2) where x,y are clocks i,j and vk is from dk 
	protected static String constraintPairToString(int i, int j, int d2, int d1, PTA pta)
	{
		String s;
		if (i > 0) {
			// -v1 < x-y < v2
			if (j > 0) {
				if (!isInfty(d2) && (-getSignedDiff(d1) == getSignedDiff(d2))) {
					if (getSignedDiff(d1) == 0)
						s = pta.getClockName(i) + "=" + pta.getClockName(j);
					else
						s = pta.getClockName(i) + "-" + pta.getClockName(j) + "=" + getSignedDiff(d2);
				} else {
					s = toStringFlipped(d1) + pta.getClockName(i) + "-" + pta.getClockName(j) + toString(d2);
				}
				// -v1 < x-0 < v2
			} else {
				if (!isInfty(d2) && (-getSignedDiff(d1) == getSignedDiff(d2)))
					s = pta.getClockName(i) + "=" + getSignedDiff(d2);
				else
					s = toStringFlipped(d1) + pta.getClockName(i) + toString(d2);
			}
		}
		// -v1 < 0-y < v2  ->  -v2 < y < v1
		else {
			if (!isInfty(d2) && (-getSignedDiff(d1) == getSignedDiff(d2)))
				s = pta.getClockName(j) + "=" + getSignedDiff(d1);
			else
				s = toStringFlipped(d2) + pta.getClockName(j) + toString(d1);
		}
		return s;
	}
}