|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use Context | |
---|---|
de.upb.swt.mcie.formulas | This package implements formulas, which can be state formulas, transition formulas or temporal formulas. |
de.upb.swt.mcie.mc | This package implements models with the corresponding model checking procedures, and the main method for invoking the model checker. |
de.upb.swt.mcie.parser | This package implements a parser and compiler for formulas and models. |
de.upb.swt.mcie.robdds | This package implements reduced ordered binary decision diagrams (ROBDDs). |
Uses of Context in de.upb.swt.mcie.formulas |
---|
Methods in de.upb.swt.mcie.formulas with parameters of type Context | |
---|---|
ROBDD |
Variable.toROBDD(Context context)
Returns the ROBDD that represents the set of all states in which this formula is valid. |
ROBDD |
UnaryOp.toROBDD(Context context)
Returns the ROBDD representation of the set of all states satisfying the formula. |
abstract ROBDD |
Formula.toROBDD(Context context)
Returns the ROBDD representation of the set of all states respectively the set of transitions satisfying the formula. |
ROBDD |
Constant.toROBDD(Context context)
Returns the ROBDD that represents the set of all states in which this formula is valid. |
ROBDD |
BinaryOp.toROBDD(Context context)
Returns the ROBDD representation of the set of all states respectively the set of transitions satisfying the formula. |
Uses of Context in de.upb.swt.mcie.mc |
---|
Fields in de.upb.swt.mcie.mc declared as Context | |
---|---|
private Context |
Transitionsystem.context
The context associated with this transition system. |
private Context |
Kripkestructure.context
The context associated with this Kripkestructure. |
Methods in de.upb.swt.mcie.mc that return Context | |
---|---|
Context |
Transitionsystem.getContext()
Returns the context associated with this Kripke structure. |
abstract Context |
Model.getContext()
Must implement an operation that returns the Context associated with this
model. |
Context |
Kripkestructure.getContext()
Returns the context associated with this Kripke structure. |
Context |
FairModel.getContext()
Returns the context associated with this fair model structure. |
Methods in de.upb.swt.mcie.mc with parameters of type Context | |
---|---|
static ROBDD |
Procedures.transClosure(Context context,
ROBDD r)
This method calculates the transitive closure of a given relation. |
Constructors in de.upb.swt.mcie.mc with parameters of type Context | |
---|---|
FairModel(Context context)
Constructs an empty fair Model. |
|
Kripkestructure(Context context)
Constructs an empty Kripke structure. |
|
Kripkestructure(Context context,
ROBDD init,
ROBDD relation)
Constructs a Kripke structure from the provided ROBDDs for the initial condition and the transition relation. |
|
Transitionsystem(Context context)
Constructs an empty transition structure. |
|
Transitionsystem(Context context,
ROBDD init,
ROBDD[] transitions,
ChangeSet[] changeSets)
Constructs a transition structure from the provided ROBDDs for the initial condition and an array of transition relation (along with the set of variables that may be change by a transition). |
Uses of Context in de.upb.swt.mcie.parser |
---|
Methods in de.upb.swt.mcie.parser with parameters of type Context | |
---|---|
FairModel |
Parser.parseFairKripkestructure(Context context)
Parses a fair Kripke structure and returns it as result. |
FairModel |
Parser.parseFairTransitionsystem(Context context)
Parses a fair transition system and returns it as result. |
Kripkestructure |
Parser.parseKripkestructure(Context context)
Parses a Kripke structure and returns it as result. |
Transitionsystem |
Parser.parseTransitionsystem(Context context)
Parses a transition system and returns it as result. |
Uses of Context in de.upb.swt.mcie.robdds |
---|
Fields in de.upb.swt.mcie.robdds declared as Context | |
---|---|
(package private) Context |
Variable.context
The context in which this variable is defined. |
(package private) Context |
ROBDD.context
The context of the ROBDD. |
private Context |
HashAssignment.context
The context of the assignment. |
(package private) Context |
ChangeSet.context
The context. |
private Context |
BinOp.context
The context for this binary operation. |
Methods in de.upb.swt.mcie.robdds that return Context | |
---|---|
Context |
HashAssignment.getContext()
Returns the context of the assignment. |
Context |
Assignment.getContext()
Returns the context of the assignment. |
Constructors in de.upb.swt.mcie.robdds with parameters of type Context | |
---|---|
BinOp(Context context,
boolean[][] truthTable)
Creates a new binary operation from the truth table. |
|
ChangeSet(Context context)
Constructs an empty change set for a given context. |
|
ChangeSet(Context context,
Variable[] variables)
Constructs a set of variables in a given context. |
|
HashAssignment(Context context)
Constructs an empty assignment, i.e. a mapping that assigns don't care values (null) to each variable. |
|
TerminalNode(Context context,
int t)
Creates a terminal node for the given truth value (0 or 1 for false and true). |
|
Variable(Context context,
java.lang.String name,
int number,
boolean isprimed)
Constructs a variable. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |