/*
 * Copyright (C) 2014, United States Government, as represented by the
 * Administrator of the National Aeronautics and Space Administration.
 * All rights reserved.
 *
 * The Java Pathfinder core (jpf-core) platform is licensed under the
 * Apache License, Version 2.0 (the "License"); you may not use this file except
 * in compliance with the License. You may obtain a copy of the License at
 *
 *        http://www.apache.org/licenses/LICENSE-2.0.
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
//package gov.nasa.jpf.search;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.annotation.JPFOption;
import gov.nasa.jpf.annotation.JPFOptions;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.VM;
import gov.nasa.jpf.vm.RestorableVMState;

/**
 * This search strategy traverses paths.  For each path, it starts in the 
 * initial state.  Paths are selected randomly.  Each path is traversed at
 * most once.
 * 
 * The JPF property search.path_limit specifies the maximum number of
 * paths this search strategy will traverse.  Its default value is
 * Integer.MAX_VALUE.
 * 
 * This search strategy does not support backtracking.
 * 
 * @author Alexander Aolaritei
 * @author Abasifreke James
 * @author Siraj Rauff
 * @author Anton Sitkovets
 * @author Mina Zaki
 * @author Franck van Breugel
 */
@JPFOptions({@JPFOption(type = "int", key = "search.path_limit", defaultValue = "Integer.MAX_VALUE", comment = "maximum number of paths searched")})
public class RandomPathsSearch extends Search {
	private final int PATH_LIMIT;

	/**
	 * Initializes this search.
	 * 
	 * @param config JPF's configuration
	 * @param vm JPF's virtual machine
	 */
	public RandomPathsSearch (Config config, VM vm) {
		super(config, vm);
		PATH_LIMIT = config.getInt("search.path_limit", Integer.MAX_VALUE);
	}

	/**
	 * The strategy of this search.
	 */
	@Override
	public void search() {
		notifySearchStarted();
		
		int paths = 0;
		RestorableVMState initialState = vm.getRestorableState();

		while (paths < PATH_LIMIT) {
			if (isNewState()) {
				while (forward()) {
					backtrack();
				}
			}
				
			paths++;
			vm.restoreState(initialState);
		}
		
		notifySearchFinished();
	}

	/**
	 * Tests whether this search supports requests for backtracking.
	 * 
	 * @return false
	 */
	public boolean supportsBacktrack() {
		return false;
	}
}