A B C D E F G H I J K L M N O P Q R S T U V X Y Z _

R

r - Variable in class edu.wis.jtlv.old_lib.games.RkGame.ImplicationEntity

reachable() - Method in class edu.wis.jtlv.env.module.Module

Calculate all reachable states form the initial states.

ReactivePair - Class in edu.wis.jtlv.lib.games

A pair of BDD's representing a reactive property where if 'assumption', and 'guarantee' are given, then the specification is "[]<>assumption -> []<>guarantee".

ReactivePair(BDD, BDD) - Constructor for class edu.wis.jtlv.lib.games.ReactivePair

RealTimeCTLOp - Static variable in enum edu.wis.jtlv.env.spec.Operator

recursive_find_intersect(BDD, Memory.Permutation, Memory.Permutation, int) - Method in class edu.wis.jtlv.old_lib.games.Memory

recursive_next_intersect(BDD, BDD, Memory.Permutation, Memory.Permutation, int) - Method in class edu.wis.jtlv.old_lib.games.Memory

register_domain_module_values(SMVModule, BDDDomain, String[]) - Method in class edu.wis.jtlv.env.Env.JTLVBDDToString

register_domain_module_values(SMVModule, BDDDomain, int, int) - Method in class edu.wis.jtlv.env.Env.JTLVBDDToString

registerErrorListener(ErrorListener) - Static method in class edu.wis.jtlv.env.Env

Register an error listener to be invoked on every error which is thrown in the JTLV environment.

releventVars() - Method in interface edu.wis.jtlv.env.spec.Spec

Get the domain of this specification.

releventVars() - Method in class edu.wis.jtlv.env.spec.SpecBDD

releventVars() - Method in class edu.wis.jtlv.env.spec.SpecCTLRange

releventVars() - Method in class edu.wis.jtlv.env.spec.SpecExp

removeAllIniRestrictions() - Method in class edu.wis.jtlv.env.module.FDSModule

removeAllIniRestrictions() - Method in class edu.wis.jtlv.env.module.Module

Remove all restrictions from the initial states.

removeAllIniRestrictions() - Method in class edu.wis.jtlv.env.module.SMVModule

removeAllTransRestrictions() - Method in class edu.wis.jtlv.env.module.FDSModule

removeAllTransRestrictions() - Method in class edu.wis.jtlv.env.module.Module

Remove all restrictions from the transitions.

removeAllTransRestrictions() - Method in class edu.wis.jtlv.env.module.SMVModule

removeErrorListener(ErrorListener) - Static method in class edu.wis.jtlv.env.Env

Remove an error listener from the queue of listeners.

removeIniRestriction(int) - Method in class edu.wis.jtlv.env.module.FDSModule

removeIniRestriction(int) - Method in class edu.wis.jtlv.env.module.Module

Remove a restriction from the initial states.

removeIniRestriction(int) - Method in class edu.wis.jtlv.env.module.SMVModule

removeInstanceVar(SMVModule) - Method in class edu.wis.jtlv.env.module.SMVModule

Removes and inner composed module.

removeRunningVar() - Method in class edu.wis.jtlv.env.module.SMVModule

Remove the "running variable if is there (NuSMV compatibility)

removeTransRestriction(int) - Method in class edu.wis.jtlv.env.module.FDSModule

removeTransRestriction(int) - Method in class edu.wis.jtlv.env.module.Module

Remove a restriction from the transitions.

removeTransRestriction(int) - Method in class edu.wis.jtlv.env.module.SMVModule

resetCopyTime() - Method in class edu.wis.jtlv.env.JTLVThread

Reset the time this thread spent on copying.

resetEnv() - Static method in class edu.wis.jtlv.env.Env

Reset the environment.

restrictIni(BDD) - Method in class edu.wis.jtlv.env.module.FDSModule

restrictIni(BDD) - Method in class edu.wis.jtlv.env.module.Module

Add a restriction to the initial states.

restrictIni(BDD) - Method in class edu.wis.jtlv.env.module.SMVModule

restrictTrans(BDD) - Method in class edu.wis.jtlv.env.module.FDSModule

restrictTrans(BDD) - Method in class edu.wis.jtlv.env.module.Module

Add a restriction to the transitions.

restrictTrans(BDD) - Method in class edu.wis.jtlv.env.module.SMVModule

resultObject() - Method in class edu.wis.jtlv.lib.AlgResultBDD

A BDD object representation of the results.

resultObject() - Method in class edu.wis.jtlv.lib.AlgResultBoolean

A Boolean object representation of the results.

resultObject() - Method in interface edu.wis.jtlv.lib.AlgResultI

An object representation of the results.

resultObject() - Method in class edu.wis.jtlv.lib.AlgResultModule

A Module object representation of the results.

resultObject() - Method in class edu.wis.jtlv.lib.AlgResultPath

A BDD[] object representation of the results.

resultObject() - Method in class edu.wis.jtlv.lib.AlgResultString

A String object representation of the results.

resultString() - Method in class edu.wis.jtlv.lib.AlgResultBDD

resultString() - Method in class edu.wis.jtlv.lib.AlgResultBoolean

resultString() - Method in interface edu.wis.jtlv.lib.AlgResultI

A string representation of the results.

resultString() - Method in class edu.wis.jtlv.lib.AlgResultModule

resultString() - Method in class edu.wis.jtlv.lib.AlgResultPath

resultString() - Method in class edu.wis.jtlv.lib.AlgResultString

RkGame - Class in edu.wis.jtlv.old_lib.games

Nir Piterman, Amir Pnueli.

RkGame(Module, Module, Set<RkGame.ImplicationEntity>) - Constructor for class edu.wis.jtlv.old_lib.games.RkGame

RkGame.ImplicationEntity - Class in edu.wis.jtlv.old_lib.games

RkGame.ImplicationEntity(BDD, BDD) - Constructor for class edu.wis.jtlv.old_lib.games.RkGame.ImplicationEntity

RkGameAlg - Class in edu.wis.jtlv.lib.games

Nir Piterman, Amir Pnueli.

RkGameAlg(Module, Module, Set<ReactivePair>) - Constructor for class edu.wis.jtlv.lib.games.RkGameAlg

A constructor for the R[k] Game and synthesis.

run() - Method in class edu.wis.jtlv.lib.AlgRunnerThread

NOTE that when not using the sequential mode, the user should take care of BDD synchronization issue - see the following link for more details JTLVThread

runSequential() - Method in class edu.wis.jtlv.lib.AlgRunnerThread

Execute in sequential mode.
NOTE that when not using the sequential mode, the user should take care of BDD synchronization issue - see the following link for more details JTLVThread