package tlc2.tool.liveness;

import java.io.IOException;

import tlc2.tool.StateVec;
import tlc2.tool.TLCState;
import tlc2.tool.Tool;
import tlc2.util.LongVec;
import tlc2.util.statistics.IBucketStatistics;

public interface ILiveCheck {

	/**
	 * This method records that state is an initial state in the behavior graph.
	 * It is called when a new initial state is generated.
	 */
	void addInitState(TLCState state, long stateFP);

	/**
	 * This method adds new nodes into the behavior graph induced by s0. It is
	 * called after the successors of s0 are computed.
	 */
	void addNextState(TLCState s0, long fp0, StateVec nextStates, LongVec nextFPs) throws IOException;
	
	/**
	 * true iff a call to {@link ILiveCheck#check(boolean)} would indeed result in liveness checking.
	 */
	boolean doLiveCheck();
	
	/**
	 * Check liveness properties for the current (potentially partial) state graph. Returns
	 * true iff it finds no errors.
	 * 
	 * @param forceCheck
	 *            Always checks liveness if true, otherwise heuristics about the
	 *            partial graph are taken into account if it is worthwhile to
	 *            check liveness.
	 * @return true iff it finds no errors or if liveness has not been checked
	 *         on the partial graph because it was deemed worthless.
	 */
	boolean check(boolean forceCheck) throws Exception;

	/**
	 * No states can be added with add*State once finalCheck has been called.
	 * 
	 * @see ILiveCheck#check()
	 * @return
	 * @throws Exception
	 */
	boolean finalCheck() throws Exception;

	/* simulation mode */
	
	/**
	 * This method is the mutual exclusive counterpart to addInitState and
	 * addNextState. Where the two each take a single state and its successors,
	 * checkTrace expects a sequence of TLCStates. The first state in this sequence
	 * is seen as the init state whereas the remaining states in the sequence belong
	 * to the behavior started by the init state.
	 * <p>
	 * checkTrace behaves similar to adding the sequence's first state with addInitState
	 * and the others with addNextState. However, checkTrace is meant to be used
	 * in simulation mode (see Simulator) only. Don't call check or finalCheck, it
	 * is done as part of checkTrace.
	 * <p>
	 * checkTrace can be called multiple times until ILiveCheck has been closed (see close()).
	 * 
	 * @param trace
	 * @throws IOException
	 * @throws InterruptedException
	 */
	void checkTrace(final StateVec trace) throws IOException, InterruptedException;
	
	/* auxiliary methods */
	
	String getMetaDir();

	Tool getTool();

	IBucketStatistics getOutDegreeStatistics();

	ILiveChecker getChecker(int idx);

	int getNumChecker();

	/* Close all the files for disk graphs. */
	void close() throws IOException;

	/* Checkpoint. */
	void beginChkpt() throws IOException;

	void commitChkpt() throws IOException;

	void recover() throws IOException;

	IBucketStatistics calculateInDegreeDiskGraphs(IBucketStatistics aGraphStats) throws IOException;

	IBucketStatistics calculateOutDegreeDiskGraphs(IBucketStatistics aGraphStats) throws IOException;

	void reset() throws IOException;
}
@@ -1,8 +1,1419 @@
+/*******************************************************************************%0A * Copyright (c) 2015 Microsoft Research. All rights reserved. %0A *%0A * The MIT License (MIT)%0A * %0A * Permission is hereby granted, free of charge, to any person obtaining a copy %0A * of this software and associated documentation files (the %22Software%22), to deal%0A * in the Software without restriction, including without limitation the rights%0A * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies%0A * of the Software, and to permit persons to whom the Software is furnished to do%0A * so, subject to the following conditions:%0A *%0A * The above copyright notice and this permission notice shall be included in all%0A * copies or substantial portions of the Software. %0A * %0A * THE SOFTWARE IS PROVIDED %22AS IS%22, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR%0A * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS%0A * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR%0A * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN%0A * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION%0A * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.%0A *%0A * Contributors:%0A *   Markus Alexander Kuppe - initial API and implementation%0A ******************************************************************************/%0A
 package 

Add missing copyright header