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 Specifications interface.
edu.wis.jtlv.lib.mc	A library containing all implemented 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()

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)

SpecExp(Operator op, Spec[] el)

SpecExp(Operator op, Spec e1, Spec e2)

SpecExp(Operator op, Spec e1, Spec e2, Spec e3)

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

Methods in edu.wis.jtlv.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.
net.sf.javabdd.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.
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.lib.mc with parameters of type Spec

LTLModelChecker.LTLTesterBuilder(Spec root_spec, boolean isWeak)