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

S

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

Save a BDD to the file system.

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

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

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

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 ModelCheckingTest

simpleCheckInvariance() - Static method in class ModelCheckingTest

simpleCheckReact() - Static method in class ModelCheckingTest

simpleCheckTempEntail() - Static method in class ModelCheckingTest

SimpleModelChecker - Class in edu.wis.jtlv.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.lib.mc.SimpleModelChecker

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

Simulation - Class in edu.wis.jtlv.lib

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

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

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

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

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

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

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

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

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

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

SpecManualTest - Class in <Unnamed>

SpecManualTest() - Constructor for class SpecManualTest

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

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

standAloneValidStarndardOutput(Spec) - Static method in class edu.wis.jtlv.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, this procedure return all states which can be reached in a single step from these 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(SMVModule) - Method in class edu.wis.jtlv.env.module.SMVModule

sysWinningStates() - Method in class edu.wis.jtlv.lib.games.GRGame

Getter for the environment's winning states.