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 _

S

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

Save a BDD to the file system.

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

secondPlayersWinningStates() - Method in interface edu.wis.jtlv.old_lib.games.TwoPlayersGame

setAllIniRestrictions(Vector<BDD>) - Method in class edu.wis.jtlv.env.module.FDSModule

setAllIniRestrictions(Vector<BDD>) - Method in class edu.wis.jtlv.env.module.Module

Set all restrictions for the initial states.

setAllIniRestrictions(Vector<BDD>) - Method in class edu.wis.jtlv.env.module.SMVModule

setAllTransRestrictions(Vector<BDD>) - Method in class edu.wis.jtlv.env.module.FDSModule

setAllTransRestrictions(Vector<BDD>) - Method in class edu.wis.jtlv.env.module.Module

Set all restrictions for the transitions.

setAllTransRestrictions(Vector<BDD>) - Method in class edu.wis.jtlv.env.module.SMVModule

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

Set the print mode for the toString procedure.

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

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

Set the initial condition with the given condition.

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

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

Compute the shortest path from source to destination.

simpleCheckDeadlock() - Static method in class AlgorithmRunnerMain

simpleCheckDeadlock() - Static method in class ModelCheckingTest

simpleCheckInvariance() - Static method in class AlgorithmRunnerMain

simpleCheckInvariance() - Static method in class ModelCheckingTest

simpleCheckReact() - Static method in class AlgorithmRunnerMain

simpleCheckReact() - Static method in class ModelCheckingTest

simpleCheckTempEntail() - Static method in class AlgorithmRunnerMain

simpleCheckTempEntail() - Static method in class ModelCheckingTest

SimpleDeadlockAlg - Class in edu.wis.jtlv.lib.mc

An algorithm for performing deadlock check.

SimpleDeadlockAlg(Module) - Constructor for class edu.wis.jtlv.lib.mc.SimpleDeadlockAlg

A constructor for the deadlock algorithm.

SimpleInvarianceAlg - Class in edu.wis.jtlv.lib.mc

An algorithm for performing an invariance check.

SimpleInvarianceAlg(Module, Spec) - Constructor for class edu.wis.jtlv.lib.mc.SimpleInvarianceAlg

A constructor for the invariance algorithm.

SimpleModelChecker - Class in edu.wis.jtlv.old_lib.mc

A wrapper to a SMVModule which knows how to check simple properties for the given module.

SimpleModelChecker(SMVModule) - Constructor for class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

SimpleModelChecker(SMVModule, boolean) - Constructor for class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

SimpleReactAlg - Class in edu.wis.jtlv.lib.mc

An algorithm for performing the react check.

SimpleReactAlg(ModuleWithWeakFairness, Spec, Spec[], Spec) - Constructor for class edu.wis.jtlv.lib.mc.SimpleReactAlg

A constructor for the react algorithm.

SimpleTempEntailAlg - Class in edu.wis.jtlv.lib.mc

An algorithm for performing the temp entailment check.

SimpleTempEntailAlg(Module, Spec, Spec) - Constructor for class edu.wis.jtlv.lib.mc.SimpleTempEntailAlg

A constructor for the temp entailment algorithm.

Simulation - Class in edu.wis.jtlv.lib

Simulation - NOT YET IMPLEMENTED.

Simulation() - Constructor for class edu.wis.jtlv.lib.Simulation

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

size() - Method in class edu.wis.jtlv.old_lib.games.Memory

SMVModule - Class in edu.wis.jtlv.env.module

An object which represent an SMV module.

SMVModule(String) - Constructor for class edu.wis.jtlv.env.module.SMVModule

A constructor for an object representing SMV modules.

SMVModule(String, String[], String[]) - Constructor for class edu.wis.jtlv.env.module.SMVModule

A constructor for an object representing SMV modules.

SMVModule(SMVModuleInfo, String) - Constructor for class edu.wis.jtlv.env.module.SMVModule

A constructor for an object representing SMV modules.

SMVModule(SMVModuleInfo, String, String[], String[]) - Constructor for class edu.wis.jtlv.env.module.SMVModule

An object representing SMV modules.

SMVModule.SyncStatus - Enum in edu.wis.jtlv.env.module

Enum class to distinguish between synchronous and asynchronous sub module composition.

Spec - Interface in edu.wis.jtlv.env.spec

A general interface for all kinds of specifications.

SpecBDD - Class in edu.wis.jtlv.env.spec

First order specification which is parsed as an SMV expression.

SpecBDD(String, BDD) - Constructor for class edu.wis.jtlv.env.spec.SpecBDD

A constructor for a leaf BDD specification, with a string representation.

SpecBDD(BDD) - Constructor for class edu.wis.jtlv.env.spec.SpecBDD

A constructor for a leaf BDD specification, without a string representation.

SpecCTLRange - Class in edu.wis.jtlv.env.spec

This node is a range node for the Real Time CTL operators.
Simple ranges are not assigned with such a node, and are evaluated as a smv expressions.
For consistency, this is not regarded as a temporal operator in the queries.

SpecCTLRange(int, int) - Constructor for class edu.wis.jtlv.env.spec.SpecCTLRange

A constructor for (Real Time) CTL range.

SpecException - Exception in edu.wis.jtlv.env.spec

An exception dedicated for all kind of specifications issues.

SpecException(String) - Constructor for exception edu.wis.jtlv.env.spec.SpecException

SpecExp - Class in edu.wis.jtlv.env.spec

Specification expression.

SpecExp(Operator, Spec[]) - Constructor for class edu.wis.jtlv.env.spec.SpecExp

A general purpose constructor.

SpecExp(Operator, Spec) - Constructor for class edu.wis.jtlv.env.spec.SpecExp

Constructor for an unary specification.

SpecExp(Operator, Spec, Spec) - Constructor for class edu.wis.jtlv.env.spec.SpecExp

Constructor for a binary specification.

SpecExp(Operator, Spec, Spec, Spec) - Constructor for class edu.wis.jtlv.env.spec.SpecExp

Constructor for a triplet specification.

SpecManualTest - Class in <Unnamed>

SpecManualTest() - Constructor for class SpecManualTest

standAloneValid(Spec) - Static method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

Check validity for a given LTL property without any design attached.

standAloneValidStarndardOutput(Spec) - Static method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

Check validity for a given LTL property without any design attached.

stringer - Static variable in class edu.wis.jtlv.env.Env

An object responsible for associating BDD variables to their names.

strongEquals(Object) - Method in class edu.wis.jtlv.env.module.ModuleEntity

Check whether this object is completely identical to the give object.

succ(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 be reached in a single step from the given states.

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

This procedure return all states which the module can reach in a single step from given a set of state.

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

Get the set of BDD variables which construct the domain for this field.

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

This functionality is not implemented for FDSModule yet.

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

add synchronous composition to this module.

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

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

Getter for the environment's winning states.

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

Getter for the environment's winning states.