documentation, and some minor sonar warning fixes

trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/Marking.java

@@ -153,10 +153,16 @@ public <LETTER> boolean isTransitionEnabled(final Transition<LETTER, PLACE> tran
 	}
 
 	/**
+	 * Computes the marking reached from this marking by firing the given transition.
+	 *
+	 * This method assumes that the transition is enabled (see {@link #isTransitionEnabled(Transition)}). Calling the
+	 * method for a non-enabled transition produces incorrect results.
+	 *
 	 * @param transition
 	 *            The transition.
 	 * @return The marking to which the occurrence of the specified transition leads.
 	 * @throws PetriNetNot1SafeException
+	 *             if firing the transition puts multiple tokens in some place
 	 */
 	public <LETTER> Marking<PLACE> fireTransition(final Transition<LETTER, PLACE> transition)
 			throws PetriNetNot1SafeException {
@@ -183,7 +189,7 @@ public <LETTER> Marking<PLACE> fireTransition(final Transition<LETTER, PLACE> tr
 
 	@Override
 	public String toString() {
-		return this.mPlaces.toString();
+		return mPlaces.toString();
 	}
 
 	public Stream<PLACE> stream() {

trunk/source/Library-Automata/src/de/uni_freiburg/informatik/ultimate/automata/petrinet/PetriNetRun.java

@@ -67,8 +67,8 @@ public PetriNetRun(final Marking<PLACE> m0) {
 	 *
 	 * @param m0
 	 *            initial marking
-	 * @param symbol
-	 *            first symbol
+	 * @param transition
+	 *            first transition
 	 * @param m1
 	 *            next marking
 	 */

trunk/source/Library-CHC/src/de/uni_freiburg/informatik/ultimate/lib/chc/ChcSolution.java

@@ -32,7 +32,11 @@
 import de.uni_freiburg.informatik.ultimate.logic.Model;
 import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
 
-public class ChcSolution extends BasePayloadContainer {
+/**
+ * Represents the output of a CHC solver, consisting of a satisfiabilitya verdict (represented as {@see LBool}), and
+ * possibly additional information such as a model, a derivation or an UNSAT core.
+ */
+public final class ChcSolution extends BasePayloadContainer {
 	private static final long serialVersionUID = -4389502364282768199L;
 
 	private final LBool mSatisfiability;
@@ -48,14 +52,35 @@ private ChcSolution(final LBool satisfiability, final Model model, final Derivat
 		mUnsatCore = unsatCore;
 	}
 
+	/**
+	 * Create a new solution representing a {@code SAT} verdict.
+	 *
+	 * @param model
+	 *            Optionally, a model produced by the solver. May be null.
+	 * @return the new instance
+	 */
 	public static ChcSolution sat(final Model model) {
 		return new ChcSolution(LBool.SAT, model, null, null);
 	}
 
+	/**
+	 * Create a new solution representing an {@code UNSAT} verdict.
+	 *
+	 * @param derivation
+	 *            Optionally, a derivation produced by the solver. May be null.
+	 * @param unsatCore
+	 *            Optionally, an UNSAT core produced by the solver. May be null.
+	 * @return the new instance
+	 */
 	public static ChcSolution unsat(final Derivation derivation, final Set<HornClause> unsatCore) {
 		return new ChcSolution(LBool.UNSAT, null, derivation, unsatCore);
 	}
 
+	/**
+	 * Create a new solution representing an {@code UNKNOWN} verdict.
+	 *
+	 * @return the new instance
+	 */
 	public static ChcSolution unknown() {
 		return new ChcSolution(LBool.UNKNOWN, null, null, null);
 	}

trunk/source/Library-CHC/src/de/uni_freiburg/informatik/ultimate/lib/chc/GolemChcScript.java

@@ -42,6 +42,11 @@
 import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
 import de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor;
 
+/**
+ * Runs the "golem" tool to solve CHC systems.
+ *
+ * See <https://github.com/usi-verification-and-security/golem/>.
+ */
 public class GolemChcScript implements IChcScript {
 	private static final boolean ADD_CLAUSE_NAMES = false;
 	private static final boolean ADD_COMMENTS = false;
@@ -52,15 +57,36 @@ public class GolemChcScript implements IChcScript {
 	private final ManagedScript mMgdScript;
 	private final long mDefaultQueryTimeout;
 
-	private boolean mProduceModels = false;
+	// defaults to false
+	private boolean mProduceModels;
 
+	// initially null
+	private Model mLastModel;
 	private LBool mLastResult;
-	private Model mLastModel = null;
 
+	/**
+	 * Create a new instance. The new instance can be used to solve multiple CHC systems. By default, the solver is run
+	 * without a time limit.
+	 *
+	 * @param services
+	 *            Ultimate services
+	 * @param mgdScript
+	 *            A managed script used to convert between CHC and SMT terms
+	 */
 	public GolemChcScript(final IUltimateServiceProvider services, final ManagedScript mgdScript) {
 		this(services, mgdScript, -1L);
 	}
 
+	/**
+	 * Create a new instance with a default time limit. The new instance can be used to solve multiple CHC systems.
+	 *
+	 * @param services
+	 *            Ultimate services
+	 * @param mgdScript
+	 *            A managed script used to convert between CHC and SMT terms
+	 * @param defaultTimeout
+	 *            A maximum time limit for all solver calls
+	 */
 	public GolemChcScript(final IUltimateServiceProvider services, final ManagedScript mgdScript,
 			final long defaultTimeout) {
 		mServices = services;

trunk/source/Library-CHC/src/de/uni_freiburg/informatik/ultimate/lib/chc/results/ChcUnknownResult.java

@@ -38,6 +38,14 @@ public class ChcUnknownResult implements IResult {
 	private final String mPlugin;
 	private final String mLongDescription;
 
+	/**
+	 * Create a new result.
+	 *
+	 * @param plugin
+	 *            The ID of the plugin that produced this result.
+	 * @param description
+	 *            A description of the result.
+	 */
 	public ChcUnknownResult(final String plugin, final String description) {
 		mPlugin = plugin;
 		mLongDescription = description;

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/IcfgUtils.java

@@ -441,7 +441,7 @@ public static boolean canReachCached(final IcfgLocation sourceLoc, final Predica
 
 			// When reachability was confirmed, do not search any further.
 			if (canReach != LBool.SAT) {
-				successors.stream().forEach(worklist::add);
+				worklist.addAll(successors);
 			}
 		}
 

trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/ProofAnnotation.java

@@ -41,7 +41,7 @@
  *
  * @author Dominik Klumpp ([email protected])
  */
-public class ProofAnnotation extends ModernAnnotations {
+public final class ProofAnnotation extends ModernAnnotations {
 	private static final long serialVersionUID = -9142656546325935187L;
 
 	private static final String KEY = ProofAnnotation.class.getName();

trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/FloydHoareUtils.java

@@ -132,7 +132,7 @@ public static void createInvariantResults(final String pluginName, final IIcfg<I
 			final var invResult =
 					new InvariantResult<IIcfgElement, Object>(pluginName, locNode, translatedInvariant, checks);
 			reporter.accept(invResult);
-			new WitnessInvariant(invResult.getInvariant()).annotate(locNode);
+			new WitnessInvariant<>(invResult.getInvariant()).annotate(locNode);
 		}
 	}
 

trunk/source/Library-Proofs/src/de/uni_freiburg/informatik/ultimate/lib/proofs/floydhoare/IcfgFloydHoareValidityCheck.java

@@ -94,7 +94,7 @@ public IcfgFloydHoareValidityCheck(final IUltimateServiceProvider services, fina
 
 	@Override
 	protected Iterable<Pair<IInternalAction, LOC>> getInternalSuccessors(final LOC state) {
-		return getSuccessors(state, IInternalAction.class, this::isNoTrivialSummary);
+		return getSuccessors(state, IInternalAction.class, IcfgFloydHoareValidityCheck::isNoTrivialSummary);
 	}
 
 	@Override
@@ -110,7 +110,7 @@ protected Iterable<Triple<IReturnAction, LOC, LOC>> getReturnSuccessors(final LO
 				.collect(Collectors.toList());
 	}
 
-	private boolean isNoTrivialSummary(final IInternalAction action) {
+	private static boolean isNoTrivialSummary(final IInternalAction action) {
 		return !(action instanceof IIcfgSummaryTransition<?>
 				&& ((IIcfgSummaryTransition<?>) action).calledProcedureHasImplementation());
 	}
@@ -125,4 +125,4 @@ private <A extends IAction> Iterable<Pair<A, LOC>> getSuccessors(final LOC state
 				.map(e -> new Pair<>(clazz.cast(e), (LOC) e.getTarget())).filter(p -> filter.test(p.getFirst()))
 				.collect(Collectors.toList());
 	}
-}
+}

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/partialorder/PartialOrderReductionFacade.java

@@ -484,9 +484,9 @@ public IStatisticsDataProvider getStatistics() {
 		return mStatistics;
 	}
 
-	private final class Statistics extends AbstractStatisticsDataProvider {
-		private int mIndependenceStatisticsCounter = 0;
-		private int mPersistentSetStatisticsCounter = 0;
+	private static final class Statistics extends AbstractStatisticsDataProvider {
+		private int mIndependenceStatisticsCounter;
+		private int mPersistentSetStatisticsCounter;
 
 		private void reportIndependenceStatistics(final IIndependenceRelation<?, ?> relation) {
 			final StatisticsData data = new StatisticsData();

trunk/source/Library-TraceCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/tracecheckerutils/partialorder/independence/abstraction/VarAbsConstraints.java

@@ -64,7 +64,7 @@ public class VarAbsConstraints<L extends IAction> {
 	 *
 	 * Use with care! The given maps as well as all sets stored within them are expected to never be modified! In many
 	 * cases, it is better to use the methods {@link Lattice#getBottom()}, {@link Lattice#getTop()} and
-	 * {{@link #withModifiedConstraints(IAction, Set, Set)} to create new constraints.
+	 * {@link #withModifiedConstraints(IAction, Set, Set)} to create new constraints.
 	 *
 	 * @param in
 	 *            maps letters to the set of constrained inVars