code cleanup, documentation

Author: nmacedo

src/main/java/kodkod/engine/AbstractKodkodSolver.java

@@ -72,7 +72,7 @@
  * @modified Nuno Macedo // [HASLab] model finding hierarchy
  */
 //[HASLab] solver hierarchy
-public abstract class AbstractKodkodSolver<B extends Bounds, O extends Options> implements KodkodSolver<B,O> { 
+public abstract class AbstractKodkodSolver<B extends Bounds, O extends Options> implements KodkodSolver<B,O>, IterableSolver<B, O> { 
 
 	/**
 	 * {@inheritDoc}

src/main/java/kodkod/engine/ElectrodSolver.java

@@ -67,6 +67,8 @@
  * restarting the solver.
  * </p>
  * 
+ * As or Pardinus 1.2, SMV iteration is disabled due to issues on the backends.
+ * 
  * @author Nuno Macedo // [HASLab] unbounded temporal model finding
  */
 public class ElectrodSolver implements UnboundedSolver<ExtendedOptions>,

src/main/java/kodkod/engine/ExplorableSolver.java

@@ -27,31 +27,28 @@
 import kodkod.instance.Bounds;
 
 /**
- * Å relational constraint solver interface that support solution iteration,
- * independent of the underlying technology (bounded vs. unbounded) and
- * functionalities (temporal, target-oriented, decomposed, symbolic).
+ * A relational constraint solver interface that support solution advanced
+ * iteration operations, independent of the underlying technology (bounded vs.
+ * unbounded) and functionalities (temporal, target-oriented, decomposed,
+ * symbolic).
  * 
  * @author Nuno Macedo // [HASLab] model finding hierarchy
  *
- * @param <B>
- *            the class of bounds required by a concrete solver
- * @param <O>
- *            the class of options required by a concrete solver
+ * @param <B> the class of bounds required by a concrete solver
+ * @param <O> the class of options required by a concrete solver
  */
-public interface ExplorableSolver<B extends Bounds, O extends PardinusOptions>
-		extends IterableSolver<B, O> {
+public interface ExplorableSolver<B extends Bounds, O extends PardinusOptions> extends IterableSolver<B, O> {
 
 	/**
 	 * Attempts to find a set of solutions to the given {@code formula} and
-	 * {@code bounds} with respect to the set options or, optionally, to
-	 * prove the formula's unsatisfiability. If the operation is successful, the
-	 * method returns an iterator over {@link Solution} objects. If there is
-	 * more than one solution, the outcome of all of them is SAT or trivially
-	 * SAT. If the problem is unsatisfiable, the iterator will produce a single
-	 * {@link Solution} whose outcome is UNSAT or trivially UNSAT. The set of
-	 * returned solutions must be non-empty, but it is not required to be
-	 * complete; a solver could simply return a singleton set containing just
-	 * the first available solution.
+	 * {@code bounds} with respect to the set options or, optionally, to prove the
+	 * formula's unsatisfiability. If the operation is successful, the method
+	 * returns an iterator over {@link Solution} objects. If there is more than one
+	 * solution, the outcome of all of them is SAT or trivially SAT. If the problem
+	 * is unsatisfiable, the iterator will produce a single {@link Solution} whose
+	 * outcome is UNSAT or trivially UNSAT. The set of returned solutions must be
+	 * non-empty, but it is not required to be complete; a solver could simply
+	 * return a singleton set containing just the first available solution.
 	 */
 	public Explorer<Solution> solveAll(Formula formula, B bounds);
 

src/main/java/kodkod/engine/Explorer.java

@@ -1,3 +1,25 @@
+/* 
+ * Kodkod -- Copyright (c) 2005-present, Emina Torlak
+ * Pardinus -- Copyright (c) 2013-present, Nuno Macedo, INESC TEC
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE.
+ */
 package kodkod.engine;
 
 import java.util.Iterator;
@@ -17,30 +39,47 @@
 public interface Explorer<T> extends Iterator<T> {
 
 	/**
-	 * Produces an alternative solution by iterating over the selected {@code state}
-	 * of the trace, fixing all previous states. A set {@code ignore} of relations
-	 * can be specified so that their valuations are ignored during iteration.
-	 * Iteration may or not {@code exclude} the state at the selected position from
-	 * future iterations, and that of higher positions is reset.
+	 * Produces an alternative solution by iterating over the static relations,
+	 * i.e., the configuration, while leaving the mutable ones free to adapt.
 	 * 
-	 * @param state   the state which will be iterated.
-	 * @param steps TODO
-	 * @param ignore  relations whose valuation will be ignored in iteration of 
-	 * 				  {@code state}.
-	 * @param force   fixed valuations for a set of relations that will be changed
-	 *                at {@code state}.
-	 * @param exclude whether the current value of the {@code state} is to be
-	 *                excluded from future iterations.
 	 * @return the next branching solution
 	 */
 	public T nextC();
 
+	/**
+	 * Produces an alternative solution by iterating over the mutable relations
+	 * while fixing the static ones, i.e., the configuration.
+	 * 
+	 * @return the next branching solution
+	 */
 	public T nextP();
 
+	/**
+	 * Produces an alternative solution by iterating over the selected {@code state}
+	 * of the trace, fixing all previous states. A set {@code change} of relations
+	 * can be specified on which a change must occur.
+	 * 
+	 * @param state  the state which will be iterated.
+	 * @param delta  the number of states from <state>, inclusive, in which the
+	 *               change must occur
+	 * @param change a set of relations in which the change must occur
+	 * @return the next branching solution
+	 */
 	public T nextS(int state, int delta, Set<Relation> change);
-	
-	public boolean hasNextP();
-	
+
+	/**
+	 * Whether there is a next configuration.
+	 * 
+	 * @return true if another configuration
+	 */
 	public boolean hasNextC();
 
+	/**
+	 * Whether there is a next path for the current configuration. Is reseted by a
+	 * new configuration.
+	 * 
+	 * @return true if another path for this configuration
+	 */
+	public boolean hasNextP();
+
 }

src/main/java/kodkod/engine/IterableSolver.java

@@ -29,7 +29,7 @@
 import kodkod.instance.Bounds;
 
 /**
- * Å relational constraint solver interface that support solution iteration,
+ * A relational constraint solver interface that support solution iteration,
  * independent of the underlying technology (bounded vs. unbounded) and
  * functionalities (temporal, target-oriented, decomposed, symbolic).
  * 

src/main/java/kodkod/engine/PardinusSolver.java

@@ -192,7 +192,7 @@ public Explorer<Solution> solveAll(Formula formula, PardinusBounds bounds) throw
 //		assert options.solver().incremental();
 
 		if (solver instanceof IterableSolver<?,?>) {
-			Iterator<Solution> it = ((IterableSolver) solver).solveAll(formula, bounds);
+			Iterator<Solution> it = ((IterableSolver<PardinusBounds, ExtendedOptions>) solver).solveAll(formula, bounds);
 			if (it instanceof Explorer)
 				return (Explorer<Solution>) it;
 			else {