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 _

P

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

Parse the given file and add it to the system.

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

pCompassionAt(int) - Method in class edu.wis.jtlv.env.module.ModuleWithStrongFairness

Getter for a P part of the compassion condition defined at the given index in the module.

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

perm - Variable in class edu.wis.jtlv.old_lib.games.Memory.Permutation

playersWinningStates() - Method in interface edu.wis.jtlv.old_lib.games.Game

playersWinningStates() - Method in class edu.wis.jtlv.old_lib.games.GR1Game

playersWinningStates() - Method in class edu.wis.jtlv.old_lib.games.RkGame

popLastCompassion() - Method in class edu.wis.jtlv.env.module.ModuleWithStrongFairness

Removes the last compassion added to this module.

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

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

popLastJustice() - Method in class edu.wis.jtlv.env.module.ModuleWithWeakFairness

Removes the last justice added to this module.

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

postAlgorithm() - Method in interface edu.wis.jtlv.lib.AlgI

Post algorithm phase.

postAlgorithm() - Method in class edu.wis.jtlv.lib.games.GR1GameAlg

The post algorithm calculate the synthesizing implementation.

postAlgorithm() - Method in class edu.wis.jtlv.lib.games.RkGameAlg

The post algorithm calculate the synthesizing implementation.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleDeadlockAlg

Does nothing.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleInvarianceAlg

Does nothing.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleReactAlg

Does Nothing.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleTempEntailAlg

Does nothing.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.CTLModelCheckAlg

Does nothing.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.LTLModelCheckAlg

If instantiated with a user tester, then returning it to its previous state.

postAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.LTLValidAlg

Does nothing.

preAlgorithm() - Method in interface edu.wis.jtlv.lib.AlgI

Pre algorithm phase.

preAlgorithm() - Method in class edu.wis.jtlv.lib.games.GR1GameAlg

Does nothing.

preAlgorithm() - Method in class edu.wis.jtlv.lib.games.RkGameAlg

Does nothing.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleDeadlockAlg

Does nothing.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleInvarianceAlg

Does nothing.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleReactAlg

Does Nothing.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleTempEntailAlg

Does nothing.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.CTLModelCheckAlg

Check that the property is a CTL property.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.LTLModelCheckAlg

Preparing the LTL tester.

preAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.LTLValidAlg

Preparing the LTL tester.

pred(BDD, BDD) - Static method in class edu.wis.jtlv.env.Env

Given a set of state and a transitions, the procedure return all states which can lead in a single step to the given states.

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

Given a set of state, this procedure return all states which can lead in a single module step to these states.

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

Construct a BDD representing the idle transition of this module and its synchronous sub modules.

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

Given a BDD, returns the same BDD in its prime version of the variables.

prime(BDD, ModuleBDDField[]) - Static method in class edu.wis.jtlv.env.Env

Given a BDD, returns the same BDD with the prime version of the given array of fields.

prime() - Method in class edu.wis.jtlv.env.module.ModuleBDDField

Get the prime version of this field.

printWinningStrategy() - Method in interface edu.wis.jtlv.old_lib.games.Game

printWinningStrategy() - Method in class edu.wis.jtlv.old_lib.games.GR1Game

Extracting an arbitrary implementation from the set of possible strategies.

printWinningStrategy() - Method in class edu.wis.jtlv.old_lib.games.RkGame

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

putModule(String, Module) - Static method in class edu.wis.jtlv.env.Env

Add a new module to the collection of all modules, and associate it with the given string.