src/creator/Aiger.java
public static ArrayList<Boolean> successor(Game game, int state, int label) {
		assert(game != null);
		assert(game.states.containsKey(state));
		if (game.states.get(state).player == 1) {
			// Player1 state
			assert(label >= 0 && label < Util.bitpower(game.varActionP1no()));
			ArrayList<Boolean> result = new ArrayList<Boolean>(game.varStateP2no());
			for (int j=0; j<latchbits; j++) result.add(game.states.get(state).values.get(j));
			int lhelp = label;
			for (int j=0; j<envbits; j++) {
				result.add((lhelp % 2) == 1);
				lhelp /= 2;
			}
			assert(lhelp == 0);
			return result;
			
		} else {
			// Player2 state
			assert(label >= 0 && label < Util.bitpower(game.varActionP2no()));
			ArrayList<Boolean> oldstate = new ArrayList<Boolean>(latchbits);
			for (int j=0; j<latchbits; j++) oldstate.add(game.states.get(state).values.get(j));
			ArrayList<Boolean> einput = new ArrayList<Boolean>(envbits);
			for (int j=latchbits; j<latchbits+envbits; j++) einput.add(game.states.get(state).values.get(j));
			
			ArrayList<Boolean> cinput = new ArrayList<Boolean>(contbits);
			int lhelp = label;
			for (int j=0; j<contbits; j++) {
				cinput.add((lhelp % 2) == 1);
				lhelp /= 2;
			}
			assert(lhelp == 0);
			
			assert(AigerCircuit.getInstance() != null);
			Pair<Boolean,ArrayList<Boolean>> circuitr = AigerCircuit.getInstance().compute(einput, cinput, oldstate);
			ArrayList<Boolean> result = new ArrayList<Boolean>(game.varStateP1no());
			for (int j=0; j<latchbits; j++) result.add(circuitr.second().get(j));
			result.add(circuitr.first());
			return result;
		}
	}
/**
	 * Computes successor state given a state-action pair
	 * @param game	Compute in this game
	 * @param state	Move from this state
	 * @param label	Move using this action
	 * @return		Values of successor state
	 */
Computes successor state given a state-action pair
@param game  Compute in this game
@param state Move from this state
@param label Move using this action
@return              Values of successor state
Computes successor state given a state - action pair @param game Compute in this game @param state Move from this state @param label Move using this action @return Values of successor state
public static ArrayList<Boolean> successor(Game game, int state, int label) {
		assert(game != null);
		assert(game.states.containsKey(state));
		if (game.states.get(state).player == 1) {
			assert(label >= 0 && label < Util.bitpower(game.varActionP1no()));
			ArrayList<Boolean> result = new ArrayList<Boolean>(game.varStateP2no());
			for (int j=0; j<latchbits; j++) result.add(game.states.get(state).values.get(j));
			int lhelp = label;
			for (int j=0; j<envbits; j++) {
				result.add((lhelp % 2) == 1);
				lhelp /= 2;
			}
			assert(lhelp == 0);
			return result;
		} else {
			assert(label >= 0 && label < Util.bitpower(game.varActionP2no()));
			ArrayList<Boolean> oldstate = new ArrayList<Boolean>(latchbits);
			for (int j=0; j<latchbits; j++) oldstate.add(game.states.get(state).values.get(j));
			ArrayList<Boolean> einput = new ArrayList<Boolean>(envbits);
			for (int j=latchbits; j<latchbits+envbits; j++) einput.add(game.states.get(state).values.get(j));
			ArrayList<Boolean> cinput = new ArrayList<Boolean>(contbits);
			int lhelp = label;
			for (int j=0; j<contbits; j++) {
				cinput.add((lhelp % 2) == 1);
				lhelp /= 2;
			}
			assert(lhelp == 0);
			assert(AigerCircuit.getInstance() != null);
			Pair<Boolean,ArrayList<Boolean>> circuitr = AigerCircuit.getInstance().compute(einput, cinput, oldstate);
			ArrayList<Boolean> result = new ArrayList<Boolean>(game.varStateP1no());
			for (int j=0; j<latchbits; j++) result.add(circuitr.second().get(j));
			result.add(circuitr.first());
			return result;
		}
	}
public static ArrayList < Boolean > successor ( Game game , int state , int label ) { assert ( game != null ) ; assert ( game . states . containsKey ( state ) ) ; if ( game . states . get ( state ) . player == 1 ) { assert ( label >= 0 && label < Util . bitpower ( game . varActionP1no ( ) ) ) ; ArrayList < Boolean > result = new ArrayList < Boolean > ( game . varStateP2no ( ) ) ; for ( int j = 0 ; j < latchbits ; j ++ ) result . add ( game . states . get ( state ) . values . get ( j ) ) ; int lhelp = label ; for ( int j = 0 ; j < envbits ; j ++ ) { result . add ( ( lhelp % 2 ) == 1 ) ; lhelp /= 2 ; } assert ( lhelp == 0 ) ; return result ; } else { assert ( label >= 0 && label < Util . bitpower ( game . varActionP2no ( ) ) ) ; ArrayList < Boolean > oldstate = new ArrayList < Boolean > ( latchbits ) ; for ( int j = 0 ; j < latchbits ; j ++ ) oldstate . add ( game . states . get ( state ) . values . get ( j ) ) ; ArrayList < Boolean > einput = new ArrayList < Boolean > ( envbits ) ; for ( int j = latchbits ; j < latchbits + envbits ; j ++ ) einput . add ( game . states . get ( state ) . values . get ( j ) ) ; ArrayList < Boolean > cinput = new ArrayList < Boolean > ( contbits ) ; int lhelp = label ; for ( int j = 0 ; j < contbits ; j ++ ) { cinput . add ( ( lhelp % 2 ) == 1 ) ; lhelp /= 2 ; } assert ( lhelp == 0 ) ; assert ( AigerCircuit . getInstance ( ) != null ) ; Pair < Boolean , ArrayList < Boolean > > circuitr = AigerCircuit . getInstance ( ) . compute ( einput , cinput , oldstate ) ; ArrayList < Boolean > result = new ArrayList < Boolean > ( game . varStateP1no ( ) ) ; for ( int j = 0 ; j < latchbits ; j ++ ) result . add ( circuitr . second ( ) . get ( j ) ) ; result . add ( circuitr . first ( ) ) ; return result ; } }
Computes successor state given a state-action pair
 @param game  Compute in this game
 @param state Move from this state
 @param label Move using this action
 @return              Values of successor state
Computes successor state given a state - action pair @param game Compute in this game @param state Move from this state @param label Move using this action @return Values of successor state
// Player1 state // Player2 state