Uses of Interface
edu.wis.jtlv.env.spec.Spec

Packages that use Spec

edu.wis.jtlv.env	The main package of JTLV, most creational action are usually done through static procedures in object Env.
edu.wis.jtlv.env.spec	Package dedicated to the user's specifications interface.
edu.wis.jtlv.lib.mc	The library containing all implemented model checking algorithms.
edu.wis.jtlv.lib.mc.tl
edu.wis.jtlv.old_lib.mc	The old library containing model checking algorithms.

Uses of Spec in edu.wis.jtlv.env

Methods in edu.wis.jtlv.env that return Spec

static Spec[]	Env.loadSpecFile(java.lang.String filename) Load any kind of specification from a file.
static Spec[]	Env.loadSpecInputStream(java.io.InputStream is) Load any kind of specification from a given input stream.
static Spec[]	Env.loadSpecString(java.lang.String to_parse) Load any kind of specification from a string.

Uses of Spec in edu.wis.jtlv.env.spec

Classes in edu.wis.jtlv.env.spec that implement Spec

class	SpecBDD First order specification which is parsed as an SMV expression.
class	SpecCTLRange 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.
class	SpecExp Specification expression.

Methods in edu.wis.jtlv.env.spec that return Spec

Spec	Macro.executeMacro(Spec orig)
Spec[]	SpecExp.getChildren() Get the children specification of this node.

Methods in edu.wis.jtlv.env.spec with parameters of type Spec

Spec	Macro.executeMacro(Spec orig)

Constructors in edu.wis.jtlv.env.spec with parameters of type Spec

SpecExp(Operator op, Spec e1)
Constructor for an unary specification.

SpecExp(Operator op, Spec[] el)
A general purpose constructor.

SpecExp(Operator op, Spec e1, Spec e2)
Constructor for a binary specification.

SpecExp(Operator op, Spec e1, Spec e2, Spec e3)
Constructor for a triplet specification.

Uses of Spec in edu.wis.jtlv.lib.mc

Constructors in edu.wis.jtlv.lib.mc with parameters of type Spec

SimpleInvarianceAlg(Module design, Spec prop)
A constructor for the invariance algorithm.

SimpleReactAlg(ModuleWithWeakFairness design, Spec p, Spec[] q, Spec r)
A constructor for the react algorithm.

SimpleReactAlg(ModuleWithWeakFairness design, Spec p, Spec[] q, Spec r)
A constructor for the react algorithm.

SimpleTempEntailAlg(Module design, Spec p, Spec q)
A constructor for the temp entailment algorithm.

Uses of Spec in edu.wis.jtlv.lib.mc.tl

Methods in edu.wis.jtlv.lib.mc.tl with parameters of type Spec

BDD	LTLTester.getSpec2BDD(Spec root) Returns a BDD variable representing the given specification in this tester.

Constructors in edu.wis.jtlv.lib.mc.tl with parameters of type Spec

CTLModelCheckAlg(ModuleWithStrongFairness design, Spec property)

LTLModelCheckAlg(Module design, Spec property)
Constructor for a given specification \phi (as a formula in temporal logic) which we want to decide whether \phi is valid over finite state program P, i.e.

LTLTester(Spec root_spec, boolean isWeak)
Constructor for the tester.

LTLValidAlg(SMVModule design, Spec property)
A constructor for checking a property on a design.

LTLValidAlg(Spec property)
A constructor for checking a property without a design.

Uses of Spec in edu.wis.jtlv.old_lib.mc

Methods in edu.wis.jtlv.old_lib.mc with parameters of type Spec

void	SimpleModelChecker.checkInvariance(Spec property) The invariance procedure check that a property holds on all reachable states.
void	SimpleModelChecker.checkInvarianceStrandardOutput(Spec property) The invariance procedure check that a property holds on all reachable states.
void	SimpleModelChecker.checkReact(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	SimpleModelChecker.checkReact(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	SimpleModelChecker.checkReactStrandardOutput(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	SimpleModelChecker.checkReactStrandardOutput(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	SimpleModelChecker.checkTempEntail(Spec p, Spec q) Verify whether [](p -> <>q) is valid.
void	SimpleModelChecker.checkTempEntailStrandardOutput(Spec p, Spec q) Verify whether [](p -> <>q) is valid.
BDD	LTLModelChecker.LTLTesterBuilder.getSpec2BDD(Spec root)
void	CTLModelChecker.modelCheck(Spec property) Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.
void	LTLModelChecker.modelCheck(Spec property) Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.
void	CTLModelChecker.modelCheckStandardOutput(Spec property) Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.
void	LTLModelChecker.modelCheckStandardOutput(Spec property) Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.
boolean	LTLModelChecker.modelCheckWithNoCounterExample(Spec property)
static void	LTLModelChecker.standAloneValid(Spec property) Check validity for a given LTL property without any design attached.
static void	LTLModelChecker.standAloneValidStarndardOutput(Spec property) Check validity for a given LTL property without any design attached.
void	LTLModelChecker.valid(Spec property) Check validity for a given LTL property.
void	LTLModelChecker.validStarndardOutput(Spec property) Check validity for a given LTL property.

Constructors in edu.wis.jtlv.old_lib.mc with parameters of type Spec

LTLModelChecker.LTLTesterBuilder(Spec root_spec, boolean isWeak)