edu.wis.jtlv.lib.games
Class GR1GameAlg

java.lang.Object
  edu.wis.jtlv.lib.games.GR1GameAlg

All Implemented Interfaces:

AlgI, GameAlgI, GameAlgTwoPlayersI

public class GR1GameAlg
extends java.lang.Object
implements GameAlgTwoPlayersI

Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. Synthesis of Reactive(1) Designs. In VMCAI, pages 364–380, Charleston, SC, January 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 GR1Game.printWinningStrategy().

Version:

"1.3.2"

Author:

yaniv sa'ar.

Field Summary

BDD[][][]	x_mem
BDD[][]	y_mem
BDD[]	z_mem

Constructor Summary

GR1GameAlg(Module env, Module sys, GeneralizedReactivePair gr_pair)

Method Summary

AlgResultI	calculate_strategy(int kind) Extracting an implementation from the set of possible strategies with the given priority to the next step.
AlgResultI	doAlgorithm() performing the GR 1 game itself, and collecting all memory.
AlgResultI	postAlgorithm() The post algorithm calculate the synthesizing implementation.
AlgResultI	preAlgorithm() Does nothing.

Methods inherited from class java.lang.Object

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

Field Detail

x_mem

public BDD[][][] x_mem

y_mem

public BDD[][] y_mem

z_mem

public BDD[] z_mem

Constructor Detail

GR1GameAlg

public GR1GameAlg(Module env,
                  Module sys,
                  GeneralizedReactivePair gr_pair)
           throws GameAlgException

Throws:

GameAlgException

Method Detail

preAlgorithm

public AlgResultI preAlgorithm()
                        throws GameAlgException

Does nothing.

Specified by:

preAlgorithm in interface AlgI

Returns:

Nothing.

Throws:

GameAlgException

See Also:

AlgI.preAlgorithm()

doAlgorithm

public AlgResultI doAlgorithm()
                       throws GameAlgException

performing the GR 1 game itself, and collecting all memory.

Specified by:

doAlgorithm in interface AlgI

Returns:

The winning state of the system player.

Throws:

GameAlgException

See Also:

AlgI.doAlgorithm()

postAlgorithm

public AlgResultI postAlgorithm()
                         throws GameAlgException

The post algorithm calculate the synthesizing implementation.

Extracting an arbitrary implementation from the set of possible strategies.

Specified by:

postAlgorithm in interface AlgI

Returns:

The synthesis of the design (in String format).

Throws:

GameAlgException

calculate_strategy

public AlgResultI 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.