DiaDes  0.1
DIAgnosis of Discrete-Event System
Formula.hh
Go to the documentation of this file.
1 #ifndef __DIADES__SDMDL__FORMULA_HH
2 #define __DIADES__SDMDL__FORMULA_HH
3 #include <vector>
4 #include <list>
5 #include <unordered_map>
6 #include <string>
7 #include <cuddObj.hh>
10 #include <diades/utils/Verbose.hh>
11 #include <diades/sdmdl/Variable.hh>
12 
13 
24 using std::vector;
25 using std::list;
26 using std::pair;
27 using std::string;
28 using std::unordered_map;
29 using Diades::Utils::Msg;
31 namespace Diades {
32 
33  namespace Sdmdl {
34 
35  class FormulaFactory;
36 
42  class Formula {
43  public:
44 
49  typedef enum {
50  OrOp = 0, AndOp = 1
52 
57  typedef enum {
58  NotOp = 0
59  } UnaryOperator;
60 
61 
62 
63 
64 
65  public:
67 
68  static string typeName() {
69  return "Diades::Sdmdl::Formula";
70  }
71 
72  public:
73  typedef std::reference_wrapper<Formula const> ConstReference;
74  typedef std::vector<ConstReference> FormulaVector;
75  typedef Formula * Pointer;
76 
77  private:
81  BDD _bdd;
90 
97 
103  mutable bool _supportNotComputed;
104 
111 
112 
113  private:
114 
120  _bdd(),
121  _dataIndex(-1),
122  _owner(&owner),
123  _support(), _supportNotComputed(true), _value() {
124  }
125 
133  Formula(const BDD & bdd, int index, FormulaFactory & owner) :
134  _bdd(bdd), _dataIndex(index), _owner(&owner), _support(), _supportNotComputed(true), _value() {
135  }
136 
137 
138  public:
139 
149  void getModels(FormulaVector & models) const;
150 
151 
152 
153 
173  const Formula & existAbstract(const VariableVector & variables, bool complementSet = false) const;
174 
180  bool isAssignment() const {
181  return (support().size() == 1) && (!value().isNull());
182  }
183 
190  const VariableVector & support() const;
191 
192 
193 
201  const Value & value() const;
202 
210  const Variable & variable() const {
211  return support().front();
212  }
213 
214 
215 
222  bool isFalse() const;
223 
231  bool isTrue() const;
232 
233 
245  void primes(FormulaVector & result) const;
246 
254  bool operator==(const Formula & f) const {
255  return this == &f;
256  }
257 
265  bool operator!=(const Formula & f) const {
266  return !(*this == f);
267  }
268 
273  virtual ~Formula() {
274  }
275 
280  const Cudd & bddManager() const;
281 
288  const BDD & bdd() const {
289  return _bdd;
290  }
291 
292 
300  const Formula & operator||(const Formula & f) const;
301 
302 
310  const Formula & operator&&(const Formula & f) const;
311 
312 
319  const Formula & operator!() const;
320 
321 
330  const Formula & apply(BinaryOperator op, const Formula & f) const;
331 
332 
340  const Formula & apply(UnaryOperator op) const;
341 
342 
343 
344 
352  bool entails(const Formula & f) const;
353 
354 
362  bool satisfies(const Formula & f) const;
363 
364 
365 
372  bool isCube() const;
373 
381  bool equivalent(const Formula & f) const;
382 
383 
390  string textify() const;
391 
398  string latexify() const;
399 
400 
404  bool isNull() const;
405 
406 
413  FormulaFactory & owner() const;
414 
415 
424  friend ostream & operator<<(ostream & os, const Formula & f);
425 
426 
427 
428  friend class FormulaFactory;
429  };
430 
435 
439  class FormulaBox {
440  private:
441  FormulaVector _box;
442 
443  public:
444 
445  FormulaBox() : _box() {
446  _box.reserve(1);
447  }
448 
449  FormulaBox(const FormulaBox & box) : _box(box._box) {
450  }
451 
452  FormulaBox & operator=(const FormulaBox & box) {
453  if (this != &box) {
454  if (box.empty()) {
455  _box.clear();
456  } else {
457  put(box.get());
458  }
459  }
460  return *this;
461  }
462 
463  FormulaBox(const Formula & formula) : _box() {
464  _box.push_back(formula);
465  }
466 
467  const Formula & get() const {
468  return _box.back().get();
469  }
470 
471  const Formula & put(const Formula & formula) {
472  _box.clear();
473  _box.push_back(formula);
474  return get();
475  }
476 
477  bool empty() const {
478  return _box.empty();
479  }
480  };
481 
510  private:
511 
519  class CubeNode {
520  public:
521  typedef CubeNode * Pointer;
522 
523  private:
527  vector<Pointer> _children;
531  FormulaVector _assignment;
532 
537 
542 
543  public:
544 
549  CubeNode(FormulaFactory & factory) : _children(), _assignment(), _value(), _factory(factory) {
550  }
551 
557  destroy();
558  }
559 
560 
565  void destroy();
566 
567 
573  void newCubeNode(unsigned i);
574 
580  void setAssignment(const Formula & assignment) {
581  _assignment.clear();
582  _assignment.push_back(assignment);
583  }
584 
590  void setValue(const Value & value) {
591  _value.clear();
592  _value.push_back(value);
593  }
594 
601  const Formula & getAssignment() {
602  if (_assignment.empty()) {
603  return _factory.nullFormula();
604  }
605  return _assignment[0];
606  }
607 
614  const Value & getValue() {
615  if (_value.empty()) {
616  return _factory.nullValue();
617  }
618  return _value[0];
619  }
620 
631  Pointer chain(const vector<int> & cube,
632  unsigned lower, unsigned upper);
633 
641  Pointer child(unsigned i) {
642  if (_children.size() > i) {
643  return _children[i];
644  }
645  return nullptr;
646  }
647 
654  bool validChild(unsigned i) const {
655  return _children.size() > i && _children[i] != nullptr;
656  }
657 
658 
663  void print(unsigned level) const;
664 
665  };
666 
667 
668  public:
669 
670  static string typeName() {
671  return "Diades::Sdmdl::FormulaFactory";
672  }
675 
676  private:
677  Cudd * _mgr;
678  vector< FormulaVector > _assignments;
679  vector<Formula::Pointer> _allocatedFormulas;
680  vector<int> _indexesToVar;
681  vector< vector<int> > _varIndexes;
682  vector< CubeNode * > _rootCubeNode;
683  vector< BDD > _positiveCube;
689  unordered_map<string, Variable::Reference> _variableOfLabel;
690 
696 
697 
698 
699 
700  public:
704  FormulaFactory();
705 
711  FormulaFactory(const VariableVector & varSet);
712 
713 
719  void reset(const VariableVector & varSet);
720 
721 
726  ~FormulaFactory();
727 
733  const BDD & noContext() const {
734  return _nocontext;
735  }
736 
747  const Formula & context() const {
748  return *_context;
749  }
750 
751 
760  const Formula & newFormula(const Variable & variable, const Value & value) const;
761 
762 
763 
764 
773  const Formula & newFormula(int * cube);
774 
775 
782  const Formula & newSwapFormula(const Formula & f,
783  const VariableVector & var,
784  const VariableVector & newVar);
785 
786 
805  void extractAssignments(int * cube, const Variable & var, FormulaVector & assignments) const;
806 
807 
826  void extractValues(const int * cube, const Variable & var, ValueVector & values) const;
827 
834  const Value & nullValue() const {
835  return _varSet[0].get().domain().front().get().owner().nullValue();
836  }
837 
846  const Formula & newAndFormula(const Formula & f1, const Formula & f2);
847 
848 
857  const Formula & newOrFormula(const Formula & f1, const Formula & f2);
858 
866  const Formula & newNotFormula(const Formula & f);
867 
874  const Formula & isTrue() const {
875  return *_isTrue;
876  }
877 
884  const Formula & isFalse() const {
885  return *_isFalse;
886  }
887 
893  const Formula & nullFormula() const {
894  return *_isNull;
895  }
896 
897 
902  void printInfoFactory() const;
903 
904 
905 
914  BDD getBDD(bool positive, BDD var) const;
915 
921  void increment(vector<bool> & encoding) const;
922 
923 
924 
931  void bddFormulaToDot(DdNode * rootNode, const string & fileName) const;
932 
933 
934 
939  void destroy();
940 
941 
942 
943 
952  Variable & getVariable(const string & name);
953 
960  const VariableVector & variables() const {
961  return _varSet;
962  }
963 
971  bool operator==(const FormulaFactory & factory) const {
972  return this == &factory;
973  }
974 
981  Cudd & bddManager() {
982  require(Exception, valid(), "bddManager: invalid factory");
983  return *_mgr;
984  }
985 
992  const Cudd & bddManager() const {
993  require(Exception, valid(), "bddManager: invalid factory");
994  return *_mgr;
995  }
996 
1003  bool valid() const {
1004  return _mgr != nullptr;
1005  }
1006 
1007 
1008 
1009 
1016  void addVariables(const vector<unsigned> & indexes, VariableVector & variables) const;
1017 
1018 
1019 
1020 
1029  const BDD & getPositiveCube(const Variable & var) const;
1030 
1031 
1032 
1033  private:
1034 
1039  const Formula & newFormula(const BDD & bdd);
1040 
1041 
1042 
1051  const Formula & createFormulaFromCube(const vector<int> & cube,
1052  const vector<BDD> & newVars);
1053 
1063  BDD encode(Variable & var, int & indexBDD);
1064 
1072  void searchAssignments(const int * cube, const Variable & var,
1073  list<CubeNode::Pointer> & leaves) const;
1074 
1075  public:
1076 
1087  void getModels(const Formula & formula, FormulaVector & models);
1088 
1089 
1097  void pickupModel(const Formula & formula, FormulaBox & model);
1098 
1105  void pickupModel(const Formula & formula, ValueVector & values);
1106 
1107  friend class Formula;
1108  };
1109 
1110 
1111  /*********************************** EXTERNAL FORMULA UTILS *******************************/
1112 
1113 
1120  void printFormula(const Formula & formula, ostream & os);
1121 
1122  /****************************** TEMPLATES *********************************************/
1123 
1124  template <Formula::BinaryOperator OP>
1127 
1128  static string typeName() {
1129  return "Diades::Sdmdl::FormulaBinaryOperator";
1130  }
1131 
1132  const Formula & operator()(const Formula & f1, const Formula & f2) const {
1133  try {
1134  return f1.apply(OP, f2);
1135  } catch (exception & e) {
1136  throw (Exception(Msg("Failure to apply a binary operator between '%1%' and '%2%'.")
1137  % f1 % f2, e));
1138  }
1139  return f1;
1140  }
1141  };
1142 
1143  /*************************************************************************************/
1144 
1145  template <Formula::UnaryOperator OP>
1148 
1149  static string typeName() {
1150  return "Diades::Sdmdl::FormulaUnaryOperator";
1151  }
1152 
1153  const Formula & operator()(const Formula & f) const {
1154  try {
1155  return f.apply(OP);
1156  } catch (exception & e) {
1157  throw (Exception(Msg("Failure to apply a unary operator on '%1%'.")
1158  % f, e));
1159  }
1160  return f;
1161  }
1162  };
1163 
1164  /*************************************************************************************/
1165 
1166  template<Formula::UnaryOperator UnaryOp>
1167  FormulaVector & applyUnaryOperator(FormulaVector & formulas) {
1168  FormulaVector tmp;
1169  for (const Formula & f : formulas) {
1170  tmp.push_back(f);
1171  }
1172  formulas.clear();
1174  for (const Formula & f : tmp) {
1175  formulas.push_back(unOp(f));
1176  }
1177  return formulas;
1178  }
1179 
1180  /*************************************************************************************/
1181 
1187  inline FormulaVector & notF(FormulaVector & formulas) {
1188  return applyUnaryOperator<Formula::UnaryOperator::NotOp>(formulas);
1189  }
1190 
1191  /*************************************************************************************/
1192 
1193  template<Formula::BinaryOperator BinaryOp>
1194  FormulaVector & applyBinaryOperator(FormulaVector & formulas, const Formula & f2) {
1195  FormulaVector tmp;
1196  for (const Formula & f1 : formulas) {
1197  tmp.push_back(f1);
1198  }
1199  formulas.clear();
1201  for (const Formula & f1 : tmp) {
1202  formulas.push_back(binOp(f1, f2));
1203  }
1204  return formulas;
1205  }
1206 
1207 
1208  /*************************************************************************************/
1209 
1216  inline FormulaVector & andF(FormulaVector & formulas, const Formula & f) {
1217  return applyBinaryOperator<Formula::BinaryOperator::AndOp>(formulas, f);
1218  }
1219 
1220  /*************************************************************************************/
1221 
1228  inline FormulaVector & orF(FormulaVector & formulas, const Formula & f) {
1229  return applyBinaryOperator<Formula::BinaryOperator::OrOp>(formulas, f);
1230  }
1231 
1232 
1233  };
1234 
1235 
1236 };
1237 #endif /*FORMULA_H_*/
FormulaBox(const FormulaBox &box)
Definition: Formula.hh:449
FormulaVector & notF(FormulaVector &formulas)
Definition: Formula.hh:1187
const Formula & operator()(const Formula &f1, const Formula &f2) const
Definition: Formula.hh:1132
VariableVector _support
Definition: Formula.hh:96
Formula::Pointer _isFalse
Definition: Formula.hh:686
CubeNode(FormulaFactory &factory)
Definition: Formula.hh:549
const Value & nullValue() const
Definition: Formula.hh:834
const Formula & operator()(const Formula &f) const
Definition: Formula.hh:1153
Formula(FormulaFactory &owner)
Definition: Formula.hh:119
vector< Formula::Pointer > _allocatedFormulas
Definition: Formula.hh:679
bool operator==(const FormulaFactory &factory) const
Definition: Formula.hh:971
const Formula & get() const
Definition: Formula.hh:467
friend ostream & operator<<(ostream &os, const Formula &f)
BddStateMachine & encode(const Diades::Automata::Experimental::StateMachine< StateProperty, FaultProperty > &component, Variable &stateVar, Variable &nextStateVar, Variable &event, BddStateMachine &result)
FormulaVector & orF(FormulaVector &formulas, const Formula &f)
Definition: Formula.hh:1228
void setAssignment(const Formula &assignment)
Definition: Formula.hh:580
const Formula & apply(BinaryOperator op, const Formula &f) const
Utils::Exception< Formula > Exception
Definition: Formula.hh:66
const Formula & nullFormula() const
Definition: Formula.hh:893
const Formula & isTrue() const
Definition: Formula.hh:874
const BDD & noContext() const
Definition: Formula.hh:733
FormulaVector & applyBinaryOperator(FormulaVector &formulas, const Formula &f2)
Definition: Formula.hh:1194
std::vector< ConstReference > FormulaVector
Definition: Formula.hh:74
const Formula & context() const
Definition: Formula.hh:747
FormulaBox(const Formula &formula)
Definition: Formula.hh:463
static string typeName()
Definition: Formula.hh:670
const Cudd & bddManager() const
const Formula & operator &&(const Formula &f) const
FormulaVector & andF(FormulaVector &formulas, const Formula &f)
Definition: Formula.hh:1216
bool isNull() const
const Value & value() const
bool entails(const Formula &f) const
vector< FormulaVector > _assignments
Definition: Formula.hh:678
string textify() const
FormulaFactory & owner() const
FormulaFactory * _owner
Definition: Formula.hh:89
string latexify() const
bool isAssignment() const
Definition: Formula.hh:180
const VariableVector & variables() const
Definition: Formula.hh:960
Utils::Exception< FormulaUnaryOperator< OP > > Exception
Definition: Formula.hh:1147
Variable::VariableVector VariableVector
Definition: Variable.hh:403
Diades::Utils::Exception< FormulaFactory > Exception
Definition: Formula.hh:673
const Formula & put(const Formula &formula)
Definition: Formula.hh:471
const Variable & variable() const
Definition: Formula.hh:210
Formula(const BDD &bdd, int index, FormulaFactory &owner)
Definition: Formula.hh:133
#define require(Exception, expr, message)
Definition: Assertion.hh:90
bool validChild(unsigned i) const
Definition: Formula.hh:654
Namespace of the Diades project.
void getModels(FormulaVector &models) const
vector< int > _indexesToVar
Definition: Formula.hh:680
FormulaBox & operator=(const FormulaBox &box)
Definition: Formula.hh:452
static FormulaFactory nullFactory
Definition: Formula.hh:674
const Formula & operator||(const Formula &f) const
FormulaVector _box
Definition: Formula.hh:441
FormulaVector & applyUnaryOperator(FormulaVector &formulas)
Definition: Formula.hh:1167
const Formula & isFalse() const
Definition: Formula.hh:884
bool operator!=(const Formula &f) const
Definition: Formula.hh:265
Value::ValueVector ValueVector
Definition: Value.hh:187
const VariableVector & support() const
const BDD & bdd() const
Definition: Formula.hh:288
void setValue(const Value &value)
Definition: Formula.hh:590
const Cudd & bddManager() const
Definition: Formula.hh:992
const ValueFactory & owner() const
Definition: Value.hh:162
friend class FormulaFactory
Definition: Formula.hh:428
bool satisfies(const Formula &f) const
vector< CubeNode *> _rootCubeNode
Definition: Formula.hh:682
const Formula & operator!() const
void primes(FormulaVector &result) const
Utils::Exception< FormulaBinaryOperator< OP > > Exception
Definition: Formula.hh:1126
vector< BDD > _positiveCube
Definition: Formula.hh:683
boost::format Msg
Definition: Verbose.hh:42
const Value & nullValue() const
Definition: Value.hh:294
Formula::Pointer _context
Definition: Formula.hh:687
vector< vector< int > > _varIndexes
Definition: Formula.hh:681
ValueVector _value
Definition: Formula.hh:110
Formula::Pointer _isNull
Definition: Formula.hh:684
Formula::Pointer _isTrue
Definition: Formula.hh:685
std::reference_wrapper< Formula const > ConstReference
Definition: Formula.hh:73
bool equivalent(const Formula &f) const
const Formula & existAbstract(const VariableVector &variables, bool complementSet=false) const
bool operator==(const Formula &f) const
Definition: Formula.hh:254
void printFormula(const Formula &formula, ostream &os)
static string typeName()
Definition: Formula.hh:68
unordered_map< string, Variable::Reference > _variableOfLabel
Definition: Formula.hh:689