edu.wis.jtlv.experimental.games
Class OldParallelGRGame

java.lang.Object
  edu.wis.jtlv.experimental.games.OldParallelGRGame

All Implemented Interfaces:

Game, TwoPlayersGame

public class OldParallelGRGame
extends java.lang.Object
implements TwoPlayersGame

Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of Reactive(1) Designs. In VMCAI, pages 364–380, Charleston, SC, Jenuary 2006.

To execute, create an object with two Modules, one for the system and the other for the environment, and then just extract the strategy through OldParallelGRGame#calculate_strategy().

Version:

"1.3.2"

Author:

yaniv sa'ar.

Nested Class Summary

class

OldParallelGRGame.InnerX

Field Summary

static java.util.HashMap<java.lang.Integer,BDD>	idx2envTrans
static java.util.HashMap<java.lang.Integer,BDD>	idx2sysTrans

Constructor Summary

OldParallelGRGame(ModuleWithWeakFairness env, ModuleWithWeakFairness sys)
for this implementation, pool_size must be set to 10.

Method Summary

void	calculate_strategy(int kind) Extracting an implementation from the set of possible strategies with the given priority to the next step.
BDD	envWinningStates() Getter for the system's winning states.
BDD	firstPlayersWinningStates()
BDD	gameInitials()
ModuleWithWeakFairness	getEnvPlayer() Getter for the environment player.
ModuleWithWeakFairness	getSysPlayer() Getter for the system player.
BDD[]	playersWinningStates()
void	printWinningStrategy() Extracting an arbitrary implementation from the set of possible strategies.
void	runIt(int j, int i, int cy, BDD X, BDD start)
BDD	secondPlayersWinningStates()
BDD	sysWinningStates() Getter for the environment's winning states.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

idx2sysTrans

public static java.util.HashMap<java.lang.Integer,BDD> idx2sysTrans

idx2envTrans

public static java.util.HashMap<java.lang.Integer,BDD> idx2envTrans

Constructor Detail

OldParallelGRGame

public OldParallelGRGame(ModuleWithWeakFairness env,
                         ModuleWithWeakFairness sys)
                  throws GameException

for this implementation, pool_size must be set to 10.
System.setProperty("pool_size", "" + 10);

Parameters:

env -

sys -

Throws:

GameException

Method Detail

runIt

public void runIt(int j,
                  int i,
                  int cy,
                  BDD X,
                  BDD start)

printWinningStrategy

public void printWinningStrategy()

Extracting an arbitrary implementation from the set of possible strategies.

Specified by:

printWinningStrategy in interface Game

calculate_strategy

public void calculate_strategy(int kind)

Extracting an implementation from the set of possible strategies with the given priority to the next step.

Possible priorities are:
3 - Z Y X.
7 - Z X Y.
11 - Y Z X.
15 - Y X Z.
19 - X Z Y.
23 - X Y Z.

Parameters:

kind - The priority kind.

getEnvPlayer

public ModuleWithWeakFairness getEnvPlayer()

Getter for the environment player.

Returns:

The environment player.

getSysPlayer

public ModuleWithWeakFairness getSysPlayer()

Getter for the system player.

Returns:

The system player.

sysWinningStates

public BDD sysWinningStates()

Getter for the environment's winning states.

Returns:

The environment's winning states.

envWinningStates

public BDD envWinningStates()

Getter for the system's winning states.

Returns:

The system's winning states.

gameInitials

public BDD gameInitials()

Specified by:

gameInitials in interface Game

playersWinningStates

public BDD[] playersWinningStates()

Specified by:

playersWinningStates in interface Game

firstPlayersWinningStates

public BDD firstPlayersWinningStates()

Specified by:

firstPlayersWinningStates in interface TwoPlayersGame

secondPlayersWinningStates

public BDD secondPlayersWinningStates()

Specified by:

secondPlayersWinningStates in interface TwoPlayersGame