documentation

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6789 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/param/ConstraintChecker.java

@@ -40,8 +40,13 @@ import java.util.HashMap;
  * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  */
 class ConstraintChecker {
+	/**
+	 * Class to store keys for the cache of the decision procedure.
+	 */
 	class DecisionEntryKey {
+		/** constraint to be stored (representing "constraint >=/> 0") */
 		Function constraint;
+		/** whether constraint should be strictly larger than zero */
 		boolean strict;
 		
 		@Override
@@ -63,8 +68,13 @@ class ConstraintChecker {
 		}
 	}
 	
+	/**
+	 * Class to store keys for the cache of the decision procedure.
+	 */
 	class DecisionEntryValue {
+		/** region this result is valid for */
 		Region region;
+		/** result, that is whether corresponding constraint holds in region */
 		boolean result;
 		
 		@Override
@@ -86,7 +96,9 @@ class ConstraintChecker {
 		}
 	}
 
+	/** number of random points to evaluate in decision procedure */
 	private int numRandomPoints;
+	/** decision cache */
 	protected HashMap<DecisionEntryKey,ArrayList<DecisionEntryValue>> decisions;
 	
 	/**
@@ -99,11 +111,30 @@ class ConstraintChecker {
 		decisions = new HashMap<DecisionEntryKey,ArrayList<DecisionEntryValue>>();
 	}
 
+	/**
+	 * Main decision check.
+	 * In this class, does nothing. Derived class could override this method
+	 * for instance by calling an external decision procedure, use a library
+	 * to decide validity in a given region, etc.
+	 * 
+	 * @param region region for which to check validity of constraint
+	 * @param constraint constraint to check (whether >=/> 0)
+	 * @param strict true iff ">" shold be checked rathern than ">="
+	 * @return true
+	 */
 	boolean mainCheck(Region region, Function constraint, boolean strict)
 	{
 		return true;
 	}
 
+	/**
+	 * Does a quick pre-check by evaluating constraint at random points.
+	 * 
+	 * @param region region for which to check validity of constraint
+	 * @param constraint constraint to check (whether >=/> 0)
+	 * @param strict true iff ">" shold be checked rathern than ">="
+	 * @return true if no counterexamples to validity found
+	 */
 	boolean preCheck(Region region, Function constraint, boolean strict)
 	{
 		ArrayList<Point> points = region.specialPoints();
@@ -123,11 +154,11 @@ class ConstraintChecker {
 	}
 	
 	/**
-	 * Checks whether 
+	 * Checks whether constraint holds in given region.
 	 * 
-	 * @param region
-	 * @param constraint
-	 * @param strict
+	 * @param region region for which to check validity of constraint
+	 * @param constraint constraint to check (whether >=/> 0)
+	 * @param strict true iff ">" shold be checked rathern than ">="
 	 * @return true iff function values are (strictly) larger than zero in whole region 
 	 */
 	boolean check(Region region, Function constraint, boolean strict)

prism/src/param/DagFunction.java

@@ -28,7 +28,7 @@ package param;
 
 /**
  * TODO implement completely
- * @author emhahn
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  */
 class DagFunction extends Function {
 	private DagFunctionFactory dagFactory;

prism/src/param/DagFunctionFactory.java

@@ -30,6 +30,10 @@ import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Random;
 
+/**
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ * TODO complete once needed
+ */
 class DagFunctionFactory extends FunctionFactory {
 	private class Number extends DagOperator {
 		private BigInteger number;

prism/src/param/DagOperator.java

@@ -28,6 +28,9 @@ package param;
 
 import java.math.BigInteger;
 
+/**
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 abstract class DagOperator {
 	private BigInteger cValue;
 	DagOperator(BigInteger cValue) {

prism/src/param/JasFunction.java

@@ -48,9 +48,13 @@ import edu.jas.ufd.Quotient;
  * @see JasFunctionFactory
  */
 final class JasFunction extends Function {
+	/** JAS object the function is wrapping */
 	private Quotient<BigInteger> jas;
+	/** numerator of function (stored if needed) */
 	Polynomial num;
+	/** denominator of function (stored if needed) */
 	Polynomial den;
+	/** type of function (rational function, infinity, etc.) */
 	int type;
 	final static int NORMAL = 0;
 	final static int INF = 1;
@@ -59,6 +63,13 @@ final class JasFunction extends Function {
 	
 	// constructors
 	
+	/**
+	 * Creates a new JAS function.
+	 * 
+	 * @param functionContext function context of this function
+	 * @param jas JAS object this function object is wrapping
+	 * @param type type of function represented
+	 */
 	JasFunction(JasFunctionFactory functionContext, Quotient<BigInteger> jas, int type) {
 		super(functionContext);
 		this.jas = jas;
@@ -103,6 +114,11 @@ final class JasFunction extends Function {
 		return jas.hashCode();
 	}
 	
+	/**
+	 * Returns JAS object this function is wrapping.
+	 * 
+	 * @return JAS object this function is wrapping
+	 */
 	Quotient<BigInteger> getJas()
 	{
 		return jas;
@@ -181,6 +197,12 @@ final class JasFunction extends Function {
 		return new JasFunction((JasFunctionFactory) factory, result, NORMAL);
 	}
 
+	/**
+	 * Transforms a JAS polynomial to a Polynomial object.
+	 * 
+	 * @param j JAS polynomial
+	 * @return polynomial of Polynomial class
+	 */
 	private Polynomial jasToPoly(GenPolynomial<BigInteger> j)
 	{
 		int numVariables = j.numberOfVariables();

prism/src/param/JasFunctionFactory.java

@@ -50,6 +50,13 @@ final class JasFunctionFactory extends FunctionFactory {
 	private JasFunction minf;
 	private JasFunction[] parameters;
 
+	/**
+	 * Creates a new function factory.
+	 * 
+	 * @param parameterNames names of parameters
+	 * @param lowerBounds lower bounds of parameters
+	 * @param upperBounds upper bounds of parameters
+	 */
 	JasFunctionFactory(String[] parameterNames, BigRational[] lowerBounds, BigRational[] upperBounds)
 	{
 		super(parameterNames, lowerBounds, upperBounds);
@@ -102,11 +109,23 @@ final class JasFunctionFactory extends FunctionFactory {
 		return minf;
 	}
 
+	/**
+	 * Get JAS ring for rational functions used by this factory.
+	 * 
+	 * @return JAS ring for rational functions used by this factory
+	 */
 	QuotientRing<BigInteger> getJasQuotRing()
 	{
 		return jasQuotRing;
 	}
 	
+	/**
+	 * Get JAS ring for polynomials used by this factory.
+	 * In JAS, rational functions are built on polynomial rings, and this
+	 * function returns this corresponding ring.
+	 * 
+	 * @return JAS ring for polynomials used by this factory
+	 */
 	GenPolynomialRing<BigInteger> getJasPolyRing()
 	{
 		return jasPolyRing;

prism/src/param/Lumper.java

@@ -30,6 +30,16 @@ import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.HashSet;
 
+/**
+ * Base class for signature-based bisimulation lumping.
+ * Derived classes could implement specific types of bisimulation,
+ * e.g. weak, strong, etc.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ * @see NullLumper
+ * @see StrongLumper
+ * @see WeakLumper
+ */
 abstract class Lumper {
 	/**
 	 * Kind of lumping to be used.
@@ -53,6 +63,11 @@ abstract class Lumper {
 	/** maps states from original to containing states in lumped model */
 	protected int[] originalToOptimised;
 
+	/**
+	 * Creates new lumper for given parametric Markov chain.
+	 * 
+	 * @param origPmc Markov chain to build lumper for
+	 */
 	Lumper(MutablePMC origPmc)
 	{
 		this.origPmc = origPmc;
@@ -63,16 +78,35 @@ abstract class Lumper {
 		buildQuotient();
 	}
 
+	/**
+	 * Creates a new lumper.
+	 * This constructor needs to be present for technical reasons.
+	 */
 	protected Lumper()
 	{
 		
 	}
 
+	/**
+	 * Stores combination of state reward and state time.
+	 * This class is used subsume states with the same reward and time.
+	 * If the time entry is irrelevant, it can be set to null.
+	 *  
+	 * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+	 */
 	class RewardEntry
 	{
+		/** reward for this entry */
 		final Function reward;
+		/** time for this entry */
 		final Function time;
 		
+		/**
+		 * Creates a new reward entry.
+		 * 
+		 * @param reward reward for this entry
+		 * @param time time for this entry.
+		 */
 		RewardEntry(Function reward, Function time) {
 			this.reward = reward;
 			this.time = time;
@@ -109,9 +143,17 @@ abstract class Lumper {
 		}
 	}
 	
+	/**
+	 * Creates an initial partitioning appropriate for analysis to perform.
+	 * For reachability, takes care that only target-states / non-target
+	 * are stored in one initial block, for reward analyses takes care
+	 * that only states with same reward are subsumed, etc. For certain types
+	 * of bisimulations, this is not enough, and the initial partition must be
+	 * refined further before starting the main refinement process. This is
+	 * the case for instance for weak bisimulation.
+	 */
 	protected void createInitialPartition()
 	{
-//		while (partition.mayChange()) {
 		HashSet<Integer> oldBlock = partition.nextChangeableBlock();
 		if (!origPmc.isUseRewards()) {
 			HashSet<Integer> safeStates = new HashSet<Integer>();
@@ -155,15 +197,25 @@ abstract class Lumper {
 			}
 			partition.addBlocks(newBlocks);
 		}
-//		}
 		partition.markAllBlocksAsNew();
 	}
 	
-	MutablePMC getOptimised()
+	/**
+	 * Return the quotient of the original model.
+	 * Before calling this method, {@code lump()} must have been called.
+	 * 
+	 * @return quotient of original model
+	 */
+	MutablePMC getQuotient()
 	{
 		return optPmc;
 	}
 	
+	/**
+	 * Enumerates the blocks after refinement is finished.
+	 * This is done as a preparation to create the quotient and the
+	 * mapping from original to quotient states.
+	 */
 	protected void mapBlocksToNumber()
 	{
 		blocks = partition.getAllBlocks();
@@ -179,11 +231,24 @@ abstract class Lumper {
 		}
 	}
 	
+	/**
+	 * Returns a mapping from original model states to quotient states.
+	 * Thus, {@result[state]} is the state of the quotient to which
+	 * {@code state} belongs.
+	 * 
+	 * @return mapping from original model states to quotient states
+	 */
 	int[] getOriginalToOptimised()
 	{
 		return originalToOptimised;
 	}
 	
+	/**
+	 * Perform the lumping process.
+	 * Refines blocks from the list of blocks to refine, it is clear that
+	 * further tries to refine blocks will not lead to the creation of any
+	 * new blocks.
+	 */
 	protected void lump()
 	{
 		ArrayList<HashSet<Integer>> newBlocks = new ArrayList<HashSet<Integer>>();
@@ -195,6 +260,20 @@ abstract class Lumper {
 		}
 	}
 	
+	/**
+	 * Refine a given block.
+	 * The exact way of how this is done depends on the type of bisimulation used.
+	 * 
+	 * @param oldBlock block to refine
+	 * @param newBlocks list of new blocks generated
+	 */
 	abstract protected void refineBlock(HashSet<Integer> oldBlock, ArrayList<HashSet<Integer>> newBlocks);
+	
+	/**
+	 * Build the quotients after refinement has finished.
+	 * Each state of the quotient will be a block of states from the original
+	 * model. The exact way of how transitions between states are computed
+	 * depends on the type of bisimulation used.
+	 */
 	abstract protected void buildQuotient();
 }

prism/src/param/NullLumper.java

@@ -29,22 +29,45 @@ package param;
 import java.util.ArrayList;
 import java.util.HashSet;
 
+/**
+ * Lumper for identity bisimulation.
+ * That is, this class does basically nothing and is there for convenience
+ * when choosing between different types of bisimulations. So, for
+ * disabling bisimulation, one can use an object of this class.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class NullLumper extends Lumper {
 
+	/**
+	 * Creates a new identity bisimulation lumper for given Markov chain.
+	 * @param origPmc parametric Markov chain to create lumper for
+	 */
 	NullLumper(MutablePMC origPmc) {
 		this.origPmc = origPmc;
 		this.optPmc = origPmc;
 	}
 
+	/**
+	 * Does not have to do anything.
+	 */
 	@Override
 	protected void refineBlock(HashSet<Integer> oldBlock,
 			ArrayList<HashSet<Integer>> newBlocks) {
 	}
 
+	/**
+	 * Does not have to do anything.
+	 */
 	@Override
 	protected void buildQuotient() {
 	}
 
+	/**
+	 * Build identity mapping.
+	 * 
+	 * @return identity mapping
+	 */
 	@Override
 	int[] getOriginalToOptimised() {
 		int[] result = new int[origPmc.getNumStates()];

prism/src/param/Optimiser.java

@@ -29,6 +29,11 @@ package param;
 
 import java.util.ArrayList;
 
+/**
+ * Searches for bounds of minimal/maximal values.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class Optimiser {
 	RegionValues values;
 	RegionValues filter;

prism/src/param/ParamModelChecker.java

@@ -74,6 +74,11 @@ import prism.PrismPrintStreamLog;
 import prism.PrismSettings;
 import prism.Result;
 
+/**
+ * Model checker for parametric Markov models.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final public class ParamModelChecker
 {
 	// Log for output (default to System.out)

prism/src/param/ParamRewardStruct.java

@@ -26,10 +26,27 @@
 
 package param;
 
+/**
+ * Reward structure for parametric model.
+ * We only consider rewards assigned to a certain nondeterministic choice,
+ * because for the properties we consider, state rewards can be stored
+ * as equivalent choice rewards.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class ParamRewardStruct {
+	/** rewards for all choices */
 	Function[] rewards;
+	/** function factory the functions used for rewards belong to */
 	FunctionFactory factory;
 	
+	/**
+	 * Constructs a new reward structure for with given number of choices.
+	 * Initially, all rewards will be zero.
+	 * 
+	 * @param factory function factory to use
+	 * @param numChoices number of different rewards
+	 */
 	ParamRewardStruct(FunctionFactory factory, int numChoices)
 	{
 		this.rewards = new Function[numChoices];
@@ -39,6 +56,11 @@ final class ParamRewardStruct {
 		}
 	}
 	
+	/**
+	 * Constructs a new reward structure which is the copy of another one.
+	 * 
+	 * @param other original to construct copy of
+	 */
 	ParamRewardStruct(ParamRewardStruct other)
 	{
 		this.rewards = new Function[other.rewards.length];
@@ -48,6 +70,15 @@ final class ParamRewardStruct {
 		this.factory = other.factory;
 	}
 	
+	/**
+	 * Instantiate reward structure at a given point.
+	 * That is, a reward structure is computed in which the corresponding
+	 * values have been inserted for each parameter, and which is thus
+	 * nonparametric.
+	 * 
+	 * @param point instantiate for these parameter values
+	 * @return non-parametric reward structure instantiated at given point
+	 */
 	ParamRewardStruct instantiate(Point point)
 	{
 		ParamRewardStruct result = new ParamRewardStruct(factory, rewards.length);
@@ -59,16 +90,34 @@ final class ParamRewardStruct {
 		return result;
 	}
 	
+	/**
+	 * Set reward for given choice.
+	 * 
+	 * @param choice choice to set reward for
+	 * @param reward reward to set
+	 */
 	void setReward(int choice, Function reward)
 	{
 		rewards[choice] = reward;
 	}
 	
+	/**
+	 * Add reward to given choice.
+	 * 
+	 * @param choice choice to add reward to
+	 * @param reward reward to add to existing reward for choice
+	 */
 	void addReward(int choice, Function reward)
 	{
 		rewards[choice] = rewards[choice].add(reward);
 	}
 	
+	/**
+	 * Get reward for given choice.
+	 * 
+	 * @param choice choice to get reward of
+	 * @return reward for given choice
+	 */
 	Function getReward(int choice)
 	{
 		return rewards[choice];

prism/src/param/Partition.java

@@ -31,8 +31,22 @@ import java.util.Comparator;
 import java.util.HashSet;
 import java.util.PriorityQueue;
 
+/**
+ * Stores a given partitioning of the states of a Markov model.
+ * This class is intended to be used in combination with signature-based
+ * partitioning refinement. In addition to storing the states, it can also
+ * compute which blocks become subject to change due to changes in other
+ * blocks.  
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class Partition {
-	final class SmallFirstComparator implements Comparator<HashSet<Integer>> {
+	/**
+	 * Comparator class comparing integer hash sets according to their size.
+	 *
+	 * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+	 */
+	final class HashSetSizeComparator implements Comparator<HashSet<Integer>> {
 		@Override
 		public int compare(HashSet<Integer> o1, HashSet<Integer> o2) {
 			int size1 = o1.size();
@@ -49,7 +63,7 @@ final class Partition {
 		
 		@Override
 		public boolean equals(Object obj) {
-			return obj instanceof SmallFirstComparator;
+			return obj instanceof HashSetSizeComparator;
 		}
 		
 		@Override
@@ -58,20 +72,32 @@ final class Partition {
 		}
 	}
 
+	/** parametric Markov chain this partition is for */
 	private MutablePMC pmc;
+	/** all blocks of this partitioning */
 	private HashSet<HashSet<Integer>> blocks;
+	/** maps states to the block they are contained in */
 	private ArrayList<HashSet<Integer>> stateToBlock;
+	/** list of blocks which might need to be refined */
 	private PriorityQueue<HashSet<Integer>> mayChange;
+	/** hash set of blocks which might need to be refined */
 	private HashSet<HashSet<Integer>> mayChangeHash;
+	/** next block to refine */
 	private HashSet<Integer> nextBlock;
 
+	/**
+	 * Creates new partitioning for given parametric Markov chain.
+	 * Initially, all states will be in the same block.
+	 * 
+	 * @param pmc parametric Markov chain to create partitioning of
+	 */
 	Partition(MutablePMC pmc)
 	{
 		this.pmc = pmc;
 		blocks = new HashSet<HashSet<Integer>>();
 		stateToBlock = new ArrayList<HashSet<Integer>>(pmc.getNumStates());
 		HashSet<Integer> initialBlock = new HashSet<Integer>(1);
-		mayChange = new PriorityQueue<HashSet<Integer>>(11, new SmallFirstComparator());
+		mayChange = new PriorityQueue<HashSet<Integer>>(11, new HashSetSizeComparator());
 		mayChangeHash = new HashSet<HashSet<Integer>>();
 		for (int state = 0; state < pmc.getNumStates(); state++) {
 			initialBlock.add(state);
@@ -82,6 +108,11 @@ final class Partition {
 		mayChangeHash.add(initialBlock);
 	}
 
+	/**
+	 * Obtain the next changeable block, according to their priority (size).
+	 * 
+	 * @return next changeable block
+	 */
 	HashSet<Integer> nextChangeableBlock()
 	{
 		nextBlock = mayChange.poll();
@@ -90,6 +121,13 @@ final class Partition {
 		return nextBlock;
 	}
 
+	/**
+	 * Add a list of new blocks to list of blocks.
+	 * Also marks existing blocks as subject to change in case they have
+	 * transitions into these new blocks, and thus might have to be split. 
+	 * 
+	 * @param newBlocks list of blocks to add
+	 */
 	void addBlocks(ArrayList<HashSet<Integer>> newBlocks)
 	{
 		blocks.addAll(newBlocks);
@@ -117,11 +155,21 @@ final class Partition {
 		}
 	}
 
+	/**
+	 * Checks whether there are blocks remaining which might need refinement.
+	 * 
+	 * @return true iff blocks are remaining which might need refinement
+	 */
 	boolean mayChange()
 	{
 		return !mayChange.isEmpty();
 	}
 	
+	/**
+	 * Obtain a list of all blocks of the partition. 
+	 * 
+	 * @return list of all blocks of the partition
+	 */
 	ArrayList<HashSet<Integer>> getAllBlocks()
 	{
 		ArrayList<HashSet<Integer>> allBlocks = new ArrayList<HashSet<Integer>>(blocks.size());
@@ -132,11 +180,20 @@ final class Partition {
 		return allBlocks;
 	}
 	
+	/**
+	 * Get the block in which a given state is contained.
+	 * 
+	 * @param state state to search containing block of
+	 * @return block state is contained in
+	 */
 	HashSet<Integer> getStateBlock(int state)
 	{
 		return stateToBlock.get(state);
 	}
 	
+	/**
+	 * Marks all blocks as being new.
+	 */
 	void markAllBlocksAsNew()
 	{
 		mayChange.clear();

prism/src/param/Polynomial.java

@@ -30,7 +30,9 @@ import java.math.BigInteger;
 import java.util.ArrayList;
 import java.util.HashMap;
 
-// TODO terms must be sorted finally, if this class is to be actually used
+// TODO terms should be sorted. will become necessary if a Function is
+// implemented which directly uses objects of this class to store
+// rational functions
 
 /**
  * A polynomial exressed as a sum of terms.

prism/src/param/RahdConstraintChecker.java

@@ -30,6 +30,10 @@ import java.io.BufferedReader;
 import java.io.IOException;
 import java.io.InputStreamReader;
 
+/**
+ * TODO complete
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class RahdConstraintChecker extends ConstraintChecker {
 	// TODO read from PrismSettings
 	final static String rahdBin = "/home/scratch/svn/pers-sb/rahd/rahd-bin";	

prism/src/param/RegionIntersection.java

@@ -26,6 +26,15 @@
 
 package param;
 
+/**
+ * Maintains the intersection of two regions.
+ * This class is to be used in combination with
+ * {@code RegionValuesIntersections} to iterate over the intersection
+ * of two {@RegionValues}.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ * @see RegionValuesIntersections
+ */
 final class RegionIntersection {
 	private Region region;
 	private StateValues values1;

prism/src/param/RegionValuesIntersections.java

@@ -29,6 +29,9 @@ package param;
 import java.util.Iterator;
 import java.util.NoSuchElementException;
 
+/**
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class RegionValuesIntersections implements Iterable<RegionIntersection> {
 	final private class RegionIntersectionOperator implements Iterator<RegionIntersection> {
 		private RegionValues regions1;

prism/src/param/RegionsTODO.java

@@ -30,6 +30,9 @@ import java.util.Comparator;
 import java.util.List;
 import java.util.PriorityQueue;
 
+/**
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class RegionsTODO {
 	class RegionsByVolumeComparator implements Comparator<Region> {
 

prism/src/param/ResultExporter.java

@@ -38,6 +38,9 @@ import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Map.Entry;
 
+/**
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class ResultExporter {
 	class PointComparator implements Comparator<Point> {
 		@Override

prism/src/param/StateEliminator.java

@@ -43,6 +43,8 @@ import java.util.ListIterator;
  * is maintained, but the state no longer has any incoming transitions,
  * except in some cases self loops. This way, after all states have been
  * treated, the value of concern can be obtained by a simple computation.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  */
 final class StateEliminator {
 	/**

prism/src/param/StrongLumper.java

@@ -32,12 +32,30 @@ import java.util.HashSet;
 import java.util.ListIterator;
 import java.util.Map.Entry;
 
+/**
+ * Strong bisimulation lumper.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class StrongLumper extends Lumper {
 
+	/**
+	 * Construct a new strong bisimulation lumper.
+	 * 
+	 * @param origPmc Markov chain to construct lumper for
+	 */
 	StrongLumper(MutablePMC origPmc) {
 		super(origPmc);
 	}
 
+	/**
+	 * Construct the strong bisimulation signature of given block.
+	 * The signature is a mapping of blocks to the probability to move
+	 * from the given state to any state of the block.
+	 * 
+	 * @param state state to compute signature of
+	 * @return signature of this state
+	 */
 	private HashMap<HashSet<Integer>, Function> stateSignature(int state)
 	{
 		HashMap<HashSet<Integer>, Function> signature = new HashMap<HashSet<Integer>, Function>();
@@ -57,6 +75,13 @@ final class StrongLumper extends Lumper {
 		return signature;
 	}
 	
+	/**
+	 * Refines a given block to a list of new blocks for strong bisimulation.
+	 * Each block will consist of the states with the same signature.
+	 * 
+	 * @param oldBlock block to refine
+	 * @param newBlocks list of new blocks generated
+	 */
 	@Override
 	protected void refineBlock(HashSet<Integer> oldBlock, ArrayList<HashSet<Integer>> newBlocks) {
 		HashMap<HashMap<HashSet<Integer>, Function>, HashSet<Integer>> signatures = new HashMap<HashMap<HashSet<Integer>, Function>, HashSet<Integer>>();
@@ -74,26 +99,31 @@ final class StrongLumper extends Lumper {
 		}
 	}
 
+	/**
+	 * Build the strong bisimulation quotient from the blocks computed.
+	 * Transition probabilities are simply derived from the signature
+	 * of an arbitrary state for each block.
+	 */
 	@Override
 	protected void buildQuotient() {
 		optPmc = new MutablePMC(origPmc.getFunctionFactory(), blocks.size(), origPmc.isUseRewards(), origPmc.isUseTime());
 		for (int newState = 0; newState < blocks.size(); newState++) {
 			HashSet<Integer> fromBlock = blocks.get(newState);
-			int someOldState = fromBlock.iterator().next();
-			HashMap<HashSet<Integer>, Function> signature = stateSignature(someOldState);
+			int someOriginalState = fromBlock.iterator().next();
+			HashMap<HashSet<Integer>, Function> signature = stateSignature(someOriginalState);
 			for (Entry<HashSet<Integer>, Function> entry : signature.entrySet()) {
 				optPmc.addTransition(newState, blockToNumber.get(entry.getKey()), entry.getValue());
 			}
 			if (origPmc.isUseRewards()) {
-				optPmc.setReward(newState, origPmc.getReward(someOldState));
+				optPmc.setReward(newState, origPmc.getReward(someOriginalState));
 				if (optPmc.getReward(newState).equals(origPmc.getFunctionFactory().getZero())) {
 					optPmc.setTargetState(newState, true);					
 				}
 				if (origPmc.isUseTime()) {
-					optPmc.setTime(newState, origPmc.getTime(someOldState));
+					optPmc.setTime(newState, origPmc.getTime(someOriginalState));
 				}
 			} else {
-				optPmc.setTargetState(newState, origPmc.isTargetState(someOldState));
+				optPmc.setTargetState(newState, origPmc.isTargetState(someOriginalState));
 			}
 			for (int oldState : fromBlock) {
 				if (origPmc.isInitState(oldState)) {

prism/src/param/SymbolicEngine.java

@@ -43,6 +43,9 @@ import prism.ModelType;
 import prism.PrismException;
 import prism.PrismLangException;
 
+/**
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 public class SymbolicEngine
 {
 	protected ModulesFile modulesFile;

prism/src/param/ValueComputer.java

@@ -582,7 +582,7 @@ final class ValueComputer
 			lumper = new StrongLumper(pmc);
 		}
 		
-		MutablePMC quot = lumper.getOptimised();
+		MutablePMC quot = lumper.getQuotient();
 		StateEliminator eliminator = new StateEliminator(quot, eliminationOrder);
 		eliminator.eliminate();
 		int[] origToCopy = lumper.getOriginalToOptimised();

prism/src/param/WeakLumper.java

@@ -34,18 +34,44 @@ import java.util.Iterator;
 import java.util.ListIterator;
 import java.util.Map.Entry;
 
+/**
+ * Weak bisimulation lumper.
+ * Notice that weak bisimulation is only valid for unbounded reachability,
+ * but must not be used for expected accumulated rewards or long-run
+ * average rewards.
+ * 
+ * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
+ */
 final class WeakLumper extends Lumper {
 
+	/**
+	 * Construct a new weak bisimulation lumper.
+	 * 
+	 * @param origPmc Markov chain to construct lumper for
+	 */
 	WeakLumper(MutablePMC origPmc) {
 		super(origPmc);
 	}
 	
+	/**
+	 * Construct the weak bisimulation signature of given block.
+	 * The signature is a mapping of blocks to the probability to move
+	 * from the given state to any state of the block under the condition
+	 * that the block is left. Thus, it is only defined for states which have
+	 * a non-zero probability of leaving the block in one step. The function
+	 * returns {@code null} for states ("silent" states) for which this is
+	 * not the case.
+	 * 
+	 * @param state state to compute signature of
+	 * @return signature of this state
+	 */
 	private HashMap<HashSet<Integer>, Function> stateSignature(int state, HashSet<Integer> ownClass)
 	{
 		HashMap<HashSet<Integer>, Function> signature = new HashMap<HashSet<Integer>, Function>();
 		ListIterator<Integer> toStateIter = origPmc.transitionTargets.get(state).listIterator();
 		ListIterator<Function> toProbIter = origPmc.transitionProbs.get(state).listIterator();
 
+		/* compute probability to remain in block in one step */
 		Function slProb = origPmc.getFunctionFactory().getZero();
 		while (toStateIter.hasNext()) {
 			int toState = toStateIter.next();
@@ -54,9 +80,11 @@ final class WeakLumper extends Lumper {
 				slProb = slProb.add(toStateProb);
 			}
 		}
+		/* for states which cannot leave their block directly, return {@code null} */
 		if (slProb.equals(origPmc.getFunctionFactory().getOne())) {
 			return null;
 		}
+		/* 1 / (1 - slProb) */
 		Function star = slProb.star();
 
 		toStateIter = origPmc.transitionTargets.get(state).listIterator();
@@ -78,6 +106,23 @@ final class WeakLumper extends Lumper {
 		return signature;
 	}
 	
+	/**
+	 * Refines a given block to a list of new blocks for weak bisimulation.
+	 * New blocks are as follows: some of the new blocks consist of the
+	 * states which can leave their block ("non-silent" states) and which
+	 * have the same signature. In addition, such a block contains the states
+	 * which cannot leave their block in one step ("silent" states) and which
+	 * can only reach states of this particular new block. Other blocks
+	 * consist of silent states which can reach more than one particular
+	 * signature block. For these kind of blocks, we have a new block for
+	 * each combination of new blocks they might reach. For instance, if
+	 * there are new blocks (based on a signature) A,B,C, we add blocks
+	 * {A,B},{B,C} and {A,B,C}, containing silent states which can reach
+	 * A and B / B and C / A, B and C. 
+	 * 
+	 * @param oldBlock block to refine
+	 * @param newBlocks list of new blocks generated
+	 */
 	@Override
 	protected void refineBlock(HashSet<Integer> oldBlock,
 			ArrayList<HashSet<Integer>> newBlocks) {
@@ -85,6 +130,9 @@ final class WeakLumper extends Lumper {
 		HashSet<Integer> silent = new HashSet<Integer>();
 		HashMap<HashMap<HashSet<Integer>, Function>, HashSet<Integer>> signatures = new HashMap<HashMap<HashSet<Integer>, Function>, HashSet<Integer>>();
 		HashMap<Integer, HashSet<Integer>> stateToBlock = new HashMap<Integer, HashSet<Integer>>();
+		/* compute signatures of states of old block and divide into silent/
+		 * nonsilent states. Silent states are states which cannot leave the
+		 * block in one step. */
 		for (int state : oldBlock) {
 			HashMap<HashSet<Integer>, Function> signature = stateSignature(state, oldBlock);
 			if (signature != null) {
@@ -101,6 +149,7 @@ final class WeakLumper extends Lumper {
 			}
 		}
 		
+		/* non-silent states reach only the new block they are contained in */
 		HashMap<Integer, HashSet<HashSet<Integer>>> reachWhichBlocks = new HashMap<Integer, HashSet<HashSet<Integer>>>();
 		for (int state : oldBlock) {
 			HashSet<HashSet<Integer>> predReachBlocks = new HashSet<HashSet<Integer>>();
@@ -110,6 +159,12 @@ final class WeakLumper extends Lumper {
 			reachWhichBlocks.put(state, predReachBlocks);
 		}
 		
+		/* collect all silent states which can reach a particular
+		 * non-silent state by performing a backwards depth-first search.
+		 * Mark silent states one comes across with the block of the
+		 * non-silent state. We can already stop the search if we know
+		 * that the state has previously been visited from another
+		 * state from the same block. */
 		for (int state : nonSilent) {
 			HashSet<Integer> block = stateToBlock.get(state);
 			ArrayDeque<Integer> stack = new ArrayDeque<Integer>();
@@ -125,6 +180,7 @@ final class WeakLumper extends Lumper {
 				}
 			}
 		}
+		/* compute new blocks, add the nonempty ones to list of new blocks */
 		HashMap<HashSet<HashSet<Integer>>, HashSet<Integer>> remap = new HashMap<HashSet<HashSet<Integer>>, HashSet<Integer>>();
 		for (Entry<Integer, HashSet<HashSet<Integer>>> entry : reachWhichBlocks.entrySet()) {
 			HashSet<Integer> sigStates = remap.get(entry.getValue());
@@ -141,6 +197,14 @@ final class WeakLumper extends Lumper {
 		}
 	}
 
+	/**
+	 * Build the weak bisimulation quotient from the blocks computed.
+	 * Transition probabilities are basically based on the weak bisimulation
+	 * signature. However, we must take care that we use a non-silent state
+	 * to compute transition probabilties from. Also, states which can never
+	 * leave their block after an arbitrary number of steps ("divergent"
+	 * states) must lead to adding a self loop in their containing block.
+	 */
 	@Override
 	protected void buildQuotient() {
 		optPmc = new MutablePMC(origPmc.getFunctionFactory(), blocks.size(), origPmc.isUseRewards(), false);
@@ -171,6 +235,14 @@ final class WeakLumper extends Lumper {
 		}
 	}
 	
+	/**
+	 * Creates an initial partitioning.
+	 * This function is based on the of the {@code Lumper} class. However,
+	 * for the weak bisimulation lumping to work correctly, for each block
+	 * of the initial partitioning, we have to split off "divergent" states.
+	 * Divergent states are states which can never leave their block, after
+	 * any number of steps.
+	 */
 	@Override
 	protected void createInitialPartition() {
 		super.createInitialPartition();