libgsjj  1
Deterministic finite automata learning library
HeuleVerwerNonCNFMethod.cpp
Go to the documentation of this file.
1 
7 #include "gsjj/passive/NonCNF/HeuleVerwerNonCNFMethod.h"
8 
9 #include <iostream>
10 #include <utility>
11 #include <cmath>
12 #include <vector>
13 #include <fstream>
14 #include <math.h>
15 #include <boost/algorithm/string.hpp>
16 
17 namespace gsjj {
18  namespace passive {
19  namespace NonCNF {
20  HeuleVerwerNonCNFMethod::HeuleVerwerNonCNFMethod(const std::set<std::string> &SpSet, const std::set<std::string> &SmSet, const std::set<std::string> &SSet, const std::set<std::string> &prefixesSet, const std::set<char> &alphabetSet, unsigned int n) :
21  SATNonCNFMethod(SpSet, SmSet, SSet, prefixesSet, alphabetSet, n)
22  {
23  s_registered = s_registered;
24  }
25 
26  HeuleVerwerNonCNFMethod::~HeuleVerwerNonCNFMethod()
27  {
28  }
29 
30  std::string HeuleVerwerNonCNFMethod::getFactoryName() {
31  return "heuleNonCNF";
32  }
33 
34  bool HeuleVerwerNonCNFMethod::createFormula(std::ostream &stream){
35  std::string formula = "";
36  //Equation 4.5.1
37  if (m_numberStates > 1) {
38  for (unsigned int p = 0; p < m_numberStates; p++){
39  formula += " ( ";
40  for (const char &a : m_alphabet){
41  formula += " ( ";
42  for (unsigned int q = 0; q < m_numberStates; q++){
43  for (unsigned int r = 0; r < m_numberStates; r++){
44  //r is q' in the report
45  if (q != r){
46  formula += "! ( d_" + std::to_string(p) + "_" + a + "_" + std::to_string(q) +
47  " & d_" + std::to_string(p) + "_" + a + "_" + std::to_string(r) + " )";
48  formula += " &\n";
49  }
50  }
51  }
52  formula = formula.substr(0, formula.length() - 3);
53  formula += " ) &\n";
54  }
55  formula = formula.substr(0, formula.length() - 3);
56  formula += " ) &\n";
57  }
58 
59  formula = formula.substr(0, formula.length() - 3);
60  stream << formula;
61 
62  formula = " &\n";
63  }
64 
65  //Equation 4.5.2
66  for (const auto &u : m_prefixes) {
67  formula += " ( ";
68  for (unsigned int q = 0 ; q < m_numberStates ; q++) {
69  formula += "x_" + u + "_" + std::to_string(q);
70  if (q != m_numberStates - 1){
71  formula += " | ";
72  }
73  }
74  formula += " ) &\n";
75  }
76 
77  formula = formula.substr(0, formula.length() - 3);
78  stream << formula;
79 
80  //Equation 4.5.3
81  formula = " &\n";
82  for (const auto &ua : m_prefixes) {
83  if (ua.size() > 0) {
84  const std::string &u = ua.substr(0, ua.size() - 1);
85  const char &a = ua.at(ua.size() - 1);
86 
87  for (unsigned int p = 0 ; p < m_numberStates ; p++) {
88  for (unsigned int q = 0 ; q < m_numberStates ; q++) {
89  formula += "( ( x_" + u + "_" + std::to_string(p) +
90  " & d_" + std::to_string(p) + "_" + a + "_" + std::to_string(q) + " ) -> x_" +
91  ua + "_" + std::to_string(q) + " )";
92  formula += " &\n";
93  }
94  }
95  }
96  }
97 
98  formula = formula.substr(0, formula.length() - 3);
99  stream << formula;
100 
101  //Equation 4.5.4
102  formula = " &\n";
103  for (unsigned int q = 0; q < m_numberStates; q++){
104  for (const auto &u : m_Sp){
105  formula += "( x_" + u + "_" + std::to_string(q) + " -> f_" + std::to_string(q) + " )";
106  formula += " &\n";
107  }
108 
109  for (const auto &u : m_Sm){
110  formula += "( x_" + u + "_" + std::to_string(q) + " -> ! f_" + std::to_string(q) + " )";
111  formula += " &\n";
112  }
113  }
114 
115  formula = formula.substr(0, formula.length() - 3);
116  stream << formula;
117 
118  //Equation 4.5.5
119  formula = " &\n";
120  for (unsigned int p = 0; p < m_numberStates; p++){
121  for (const char &a : m_alphabet){
122  formula += "( ";
123  for (unsigned int q = 0; q < m_numberStates; q++){
124  formula += "d_" + std::to_string(p) + "_" + a + "_" + std::to_string(q);
125  formula += " | ";
126  }
127  formula = formula.substr(0, formula.length() - 3);
128  formula += ") &\n";
129  }
130  }
131 
132  formula = formula.substr(0, formula.length() - 3);
133  stream << formula;
134 
135  //Equation 4.5.6
136  formula = " &\n";
137  for (const auto &u : m_prefixes) {
138  for (unsigned int p = 0 ; p < m_numberStates ; p++) {
139  for (unsigned int q = 0 ; q < m_numberStates ; q++) {
140  if (p != q) {
141  formula += "( ! ( x_" + u + "_" + std::to_string(p) + " & x_" +
142  u + "_" + std::to_string(q) + " ) )";
143  formula += " &\n";
144  }
145  }
146  }
147  }
148 
149  formula = formula.substr(0, formula.length() - 3);
150  stream << formula;
151 
152  //Equation 4.5.7
153  formula = " &\n";
154  for (const auto &ua : m_prefixes) {
155  if (ua.size() > 0) {
156  const std::string &u = ua.substr(0, ua.size() - 1);
157  const char &a = ua.at(ua.size() - 1);
158 
159  for (unsigned int p = 0 ; p < m_numberStates ; p++) {
160  for (unsigned int q = 0 ; q < m_numberStates ; q++) {
161  formula += "( ( x_" + u + "_" + std::to_string(p) + " & " + "x_" + ua + "_" + std::to_string(q) + " ) "
162  + "-> d_" + std::to_string(p) + "_" + a + "_" + std::to_string(q) + " ) ";
163  formula += "&\n";
164  }
165  }
166  }
167  }
168 
169  formula = formula.substr(0, formula.length() - 3);
170  stream << formula;
171 
172  return true;
173  }
174 
175  std::unique_ptr<DFA<char>> HeuleVerwerNonCNFMethod::toDFA(std::istream &stream) const
176  {
177  //First, we have to read the solution
178  std::string line;
179  // std::map<std::string, unsigned int> words_states;
180  // std::vector<unsigned int> final_states;
181  std::vector<std::vector<std::string>> d_vars;
182  std::vector<unsigned int> f_vars;
183 
184  std::unique_ptr<DFA<char>> dfa;
185 
186  while(std::getline(stream, line)){
187  //If there is a variable on this line
188  if (line.at(0) == 'x'){
189  std::vector<std::string> results;
190  std::vector<std::string> results_2;
191  //We split the line to get var - = - assignationOfTheVar
192  boost::split(results, line, [](char c){return c == ' ';});
193  //We split the var to get x - pref - stateNumber
194  boost::split(results_2, results[0], [](char c){return c == '_';});
195  // auto pair = std::make_pair(results_2[1], std::stoi(results_2[2]));
196  // m_state_bit.emplace(state(pair, std::stoi(results[2])));
197  if (std::stoi(results[2]) == 1 && results_2[1] == ""){
198  dfa = std::make_unique<DFA<char>>(std::stoi(results_2[2]), m_Sp.find("") != m_Sp.end());
199  }
200  }
201  if (line.at(0) == 'd'){
202  std::vector<std::string> results;
203  std::vector<std::string> results_2;
204  //We split the line to get var - = - assignationOfTheVar
205  boost::split(results, line, [](char c){return c == ' ';});
206  //We split the var to get d - p - a - q
207  boost::split(results_2, results[0], [](char c){return c == '_';});
208  // auto pair = std::make_pair(results_2[1], std::stoi(results_2[2]));
209  // m_state_bit.emplace(state(pair, std::stoi(results[2])));
210  if(std::stoi(results[2]) == 1){
211  std::vector<std::string> my_vec;
212  my_vec.push_back(results_2[1]);
213  my_vec.push_back(results_2[2]);
214  my_vec.push_back(results_2[3]);
215  d_vars.push_back(my_vec);
216  }
217  }
218  if (line.at(0) == 'f'){
219  std::vector<std::string> results;
220  std::vector<std::string> results_2;
221  //We split the line to get var - = - assignationOfTheVar
222  boost::split(results, line, [](char c){return c == ' ';});
223  //We split the var to get f - q
224  boost::split(results_2, results[0], [](char c){return c == '_';});
225  // auto pair = std::make_pair(results_2[1], std::stoi(results_2[2]));
226  // m_state_bit.emplace(state(pair, std::stoi(results[2])));
227  if (std::stoi(results[2]) == 1){
228  f_vars.push_back(std::stoi(results_2[1]));
229  }
230  }
231  }
232 
233  for(unsigned int i = 0; i < m_numberStates; i++){
234  if(std::find(f_vars.begin(), f_vars.end(), i) != f_vars.end()){
235  dfa->addState(i, true);
236  }
237  else{
238  dfa->addState(i, false);
239  }
240  }
241 
242  for(const auto &vec : d_vars){
243  const char *a = vec.at(1).c_str();
244  dfa->addTransition(std::stoi(vec.at(0)), a[0], std::stoi(vec.at(2)));
245  }
246 
247  return dfa;
248  }
249 
250  std::string HeuleVerwerNonCNFMethod::getFileName() const {
251  return "heule";
252  }
253  }
254  }
255 }
gsjj::passive::Method::m_alphabet
const std::set< char > m_alphabet
Definition: Method.h:121
gsjj
The namespace of the library.
Definition: binary.h:11
gsjj::passive::Method::m_Sm
const std::set< std::string > m_Sm
The set of words to reject .
Definition: Method.h:105
gsjj::passive::Method::m_prefixes
const std::set< std::string > m_prefixes
Definition: Method.h:117
HeuleVerwerNonCNFMethod.h
This file declares the Heule and Verwer method that relies on non CNF SAT solver. ...
gsjj::passive::NonCNF::HeuleVerwerNonCNFMethod::toDFA
std::unique_ptr< DFA< char > > toDFA(std::istream &stream) const override
Effectively creates the DFA.
Definition: HeuleVerwerNonCNFMethod.cpp:175
gsjj::passive::RegisterInFactory< HeuleVerwerNonCNFMethod >::s_registered
static bool s_registered
Useful to make sure the template is correctly used by the compiler.
Definition: MethodFactory.h:97
gsjj::passive::NonCNF::HeuleVerwerNonCNFMethod::getFileName
virtual std::string getFileName() const override
Gives the name of the file in which the boolean formula must be written.
Definition: HeuleVerwerNonCNFMethod.cpp:250
gsjj::passive::NonCNF::HeuleVerwerNonCNFMethod::createFormula
virtual bool createFormula(std::ostream &stream) override
Creates the boolean formula (must not be in CNF) and writes it in the stream.
Definition: HeuleVerwerNonCNFMethod.cpp:34
gsjj::passive::Method::m_numberStates
const unsigned int m_numberStates
The number of states in the DFA to construct.
Definition: Method.h:109
gsjj::passive::NonCNF::SATNonCNFMethod
Base class for every method that relies on a non-CNF SAT solver.
Definition: SATNonCNFMethod.h:26
gsjj::passive::Method::m_Sp
const std::set< std::string > m_Sp
The set of words to accept .
Definition: Method.h:101
Generated by   doxygen 1.8.13