DiaDes
0.1
DIAgnosis of Discrete-Event System
|
#include <Formula.hh>
Classes | |
class | CubeNode |
Public Types | |
typedef Diades::Utils::Exception< FormulaFactory > | Exception |
Public Member Functions | |
FormulaFactory () | |
FormulaFactory (const VariableVector &varSet) | |
void | reset (const VariableVector &varSet) |
~FormulaFactory () | |
const BDD & | noContext () const |
const Formula & | context () const |
const Formula & | newFormula (const Variable &variable, const Value &value) const |
const Formula & | newFormula (int *cube) |
const Formula & | newSwapFormula (const Formula &f, const VariableVector &var, const VariableVector &newVar) |
void | extractAssignments (int *cube, const Variable &var, FormulaVector &assignments) const |
void | extractValues (const int *cube, const Variable &var, ValueVector &values) const |
const Value & | nullValue () const |
const Formula & | newAndFormula (const Formula &f1, const Formula &f2) |
const Formula & | newOrFormula (const Formula &f1, const Formula &f2) |
const Formula & | newNotFormula (const Formula &f) |
const Formula & | isTrue () const |
const Formula & | isFalse () const |
const Formula & | nullFormula () const |
void | printInfoFactory () const |
BDD | getBDD (bool positive, BDD var) const |
void | increment (vector< bool > &encoding) const |
void | bddFormulaToDot (DdNode *rootNode, const string &fileName) const |
void | destroy () |
Variable & | getVariable (const string &name) |
const VariableVector & | variables () const |
bool | operator== (const FormulaFactory &factory) const |
Cudd & | bddManager () |
const Cudd & | bddManager () const |
bool | valid () const |
void | addVariables (const vector< unsigned > &indexes, VariableVector &variables) const |
const BDD & | getPositiveCube (const Variable &var) const |
void | getModels (const Formula &formula, FormulaVector &models) |
void | pickupModel (const Formula &formula, FormulaBox &model) |
void | pickupModel (const Formula &formula, ValueVector &values) |
Static Public Member Functions | |
static string | typeName () |
Static Public Attributes | |
static FormulaFactory | nullFactory |
Private Member Functions | |
const Formula & | newFormula (const BDD &bdd) |
const Formula & | createFormulaFromCube (const vector< int > &cube, const vector< BDD > &newVars) |
BDD | encode (Variable &var, int &indexBDD) |
void | searchAssignments (const int *cube, const Variable &var, list< CubeNode::Pointer > &leaves) const |
Private Attributes | |
Cudd * | _mgr |
vector< FormulaVector > | _assignments |
vector< Formula::Pointer > | _allocatedFormulas |
vector< int > | _indexesToVar |
vector< vector< int > > | _varIndexes |
vector< CubeNode *> | _rootCubeNode |
vector< BDD > | _positiveCube |
Formula::Pointer | _isNull |
Formula::Pointer | _isTrue |
Formula::Pointer | _isFalse |
Formula::Pointer | _context |
BDD | _nocontext |
unordered_map< string, Variable::Reference > | _variableOfLabel |
VariableVector | _varSet |
Friends | |
class | Formula |
This class is the factory from which we can get any set of formulae based on a given set of variables.
Suppose now the following cube = 2 0 1, it represents (v1=red || v1=blue) && (v2 = n0). Suppose now the following cube = 2 1 2, it represents (v1=yellow). Suppose now the following cube = 2 2 2, it represents TRUE. Suppose now the following cube = 0 0 0, it represents (v1=red) && (v2=yes). With this encoding (v1=red) || (v1=blue) || (v1=yellow) is true and any conjunction like (v1=red) && (v1=blue) is False The BDD complement of an assignment Formula is also a Formula
Definition at line 509 of file Formula.hh.
Definition at line 673 of file Formula.hh.
Diades::Sdmdl::FormulaFactory::FormulaFactory | ( | ) |
Default constructor
Diades::Sdmdl::FormulaFactory::FormulaFactory | ( | const VariableVector & | varSet | ) |
Constructor
varSet | the set of Variable involved in the encoding formulas created by this Factory |
Diades::Sdmdl::FormulaFactory::~FormulaFactory | ( | ) |
Destructor
void Diades::Sdmdl::FormulaFactory::addVariables | ( | const vector< unsigned > & | indexes, |
VariableVector & | variables | ||
) | const |
add the set of Variables supported by the bdd variables of indexes
indexes | the set of indexes associated to bdd variables |
variables | the resulting set of Variable supported by the bdd variables |
void Diades::Sdmdl::FormulaFactory::bddFormulaToDot | ( | DdNode * | rootNode, |
const string & | fileName | ||
) | const |
rootNode | |
fileName |
|
inline |
|
inline |
|
inline |
Definition at line 747 of file Formula.hh.
References Diades::Sdmdl::Formula::value(), and Diades::Sdmdl::Formula::variable().
|
private |
Creation of a Formula from a cube
cube | the cube that corresponds to the encoding of the Assignment |
newVars | the support of the encoded Assignment |
void Diades::Sdmdl::FormulaFactory::destroy | ( | ) |
Destroy the Factory
Referenced by Diades::Sdmdl::Experimental::BddStateMachine::~BddStateMachine().
|
private |
encode the set of variable assignments with a set of bdd variables starting at index indexBDD
var | the variable to encode |
indexBDD | the starting index |
void Diades::Sdmdl::FormulaFactory::extractAssignments | ( | int * | cube, |
const Variable & | var, | ||
FormulaVector & | assignments | ||
) | const |
Creation of the set of assignment Formula based on a cube for a given Variable
cube | the given cube (an array of size bddManager().ReadSize() containing 0's 1's and 2's) cube[i] = 0 means the bddVar(i) is complemented cube[i] = 1 means the bddVar(i) is not complemented and cube[i] = 2 means the bddVar(i) is not involved in the bdd |
var | the Variable |
assignments | the returned assignment Formulas. |
void Diades::Sdmdl::FormulaFactory::extractValues | ( | const int * | cube, |
const Variable & | var, | ||
ValueVector & | values | ||
) | const |
Get the values based on a cube for a given Variable
cube | the given cube (an array of size bddManager().ReadSize() containing 0's 1's and 2's) cube[i] = 0 means the bddVar(i) is complemented cube[i] = 1 means the bddVar(i) is not complemented and cube[i] = 2 means the bddVar(i) is not involved in the bdd |
var | the Variable |
assignments | the returned assignment Formulas. |
BDD Diades::Sdmdl::FormulaFactory::getBDD | ( | bool | positive, |
BDD | var | ||
) | const |
positive | |
var |
void Diades::Sdmdl::FormulaFactory::getModels | ( | const Formula & | formula, |
FormulaVector & | models | ||
) |
Model enumerations
formula | a given formula |
models | the set of full/complete assignments F such that F is a model of 'formula' |
const BDD& Diades::Sdmdl::FormulaFactory::getPositiveCube | ( | const Variable & | var | ) | const |
var | a Variable |
Variable& Diades::Sdmdl::FormulaFactory::getVariable | ( | const string & | name | ) |
name | name of the Variable to look for |
void Diades::Sdmdl::FormulaFactory::increment | ( | vector< bool > & | encoding | ) | const |
encoding | the boolean counter to increment |
|
inline |
Definition at line 884 of file Formula.hh.
Referenced by Diades::Sdmdl::Experimental::BddStateMachine::BddStateMachine(), Diades::Sdmdl::Experimental::BddStateMachine::resetInternalFormulaFactory(), and runGlobalDiagnosisProblem().
|
inline |
Definition at line 874 of file Formula.hh.
const Formula& Diades::Sdmdl::FormulaFactory::newFormula | ( | const Variable & | variable, |
const Value & | value | ||
) | const |
Assignment formula
Referenced by Diades::Sdmdl::Experimental::encodeInitialStates(), and Diades::Sdmdl::Experimental::encodeTransitions().
const Formula& Diades::Sdmdl::FormulaFactory::newFormula | ( | int * | cube | ) |
Creation of a Formula based on a cube
cube | the given cube (an array of size bddManager().ReadSize() containing 0's 1's and 2's) cube[i] = 0 means the bddVar(i) is complemented cube[i] = 1 means the bddVar(i) is not complemented and cube[i] = 2 means the bddVar(i) is not involved in the bdd |
|
private |
Creation of a Formula from a BDD
bdd | a predefined BDD |
f | a Formula |
const Formula& Diades::Sdmdl::FormulaFactory::newSwapFormula | ( | const Formula & | f, |
const VariableVector & | var, | ||
const VariableVector & | newVar | ||
) |
|
inline |
Definition at line 733 of file Formula.hh.
|
inline |
Definition at line 893 of file Formula.hh.
Referenced by Diades::Sdmdl::FormulaFactory::CubeNode::getAssignment().
|
inline |
Definition at line 834 of file Formula.hh.
References Diades::Sdmdl::ValueFactory::nullValue(), and Diades::Sdmdl::Value::owner().
Referenced by Diades::Sdmdl::FormulaFactory::CubeNode::getValue().
|
inline |
void Diades::Sdmdl::FormulaFactory::pickupModel | ( | const Formula & | formula, |
FormulaBox & | model | ||
) |
Pickup a model
formula | a given formula |
model | a complete set of assignments F such that F is a model of 'formula', empty if such a model does not exist |
void Diades::Sdmdl::FormulaFactory::pickupModel | ( | const Formula & | formula, |
ValueVector & | values | ||
) |
Pickup a model
formula | a given formula |
values | the set of values assigned to variables() to get the model |
void Diades::Sdmdl::FormulaFactory::printInfoFactory | ( | ) | const |
void Diades::Sdmdl::FormulaFactory::reset | ( | const VariableVector & | varSet | ) |
varSet | the new Variable set involved in the encoding formulas created by this Factory |
Referenced by Diades::Sdmdl::Experimental::BddStateMachine::resetInternalFormulaFactory().
|
private |
Search assignments from a cube
cube | a cube |
var | the variable involved in the assignments to look for |
leaves | the CubeNode that contains the assignments to look for |
|
inlinestatic |
Definition at line 670 of file Formula.hh.
|
inline |
Definition at line 1003 of file Formula.hh.
References Diades::Sdmdl::Formula::bdd(), Diades::Sdmdl::Experimental::encode(), and Diades::Sdmdl::Formula::getModels().
|
inline |
Definition at line 960 of file Formula.hh.
|
friend |
Definition at line 1107 of file Formula.hh.
|
private |
Definition at line 679 of file Formula.hh.
|
private |
Definition at line 678 of file Formula.hh.
|
private |
Definition at line 687 of file Formula.hh.
|
private |
Definition at line 680 of file Formula.hh.
|
private |
Definition at line 686 of file Formula.hh.
|
private |
Definition at line 684 of file Formula.hh.
|
private |
Definition at line 685 of file Formula.hh.
|
private |
Definition at line 677 of file Formula.hh.
|
private |
Definition at line 688 of file Formula.hh.
|
private |
Definition at line 683 of file Formula.hh.
|
private |
Definition at line 682 of file Formula.hh.
|
private |
Definition at line 689 of file Formula.hh.
|
private |
Definition at line 681 of file Formula.hh.
|
private |
_varSet
the current set of declared Variables
Definition at line 695 of file Formula.hh.
|
static |
Definition at line 674 of file Formula.hh.