alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sat: more debug.

Browse source 
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: More debuging
code.
This commit is contained in:
Alexandre Duret-Lutz 2013-12-17 15:55:23 +01:00
parent 9c98975c19
commit b4d0b9ee42
2 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/tgbaalgos/dtbasat.cc
View file

@ -18,6 +18,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream> #include <iostream>
#include <fstream>
#include <sstream> #include <sstream>
#include "dtbasat.hh" #include "dtbasat.hh"
#include "reachiter.hh" #include "reachiter.hh"
@ -901,6 +902,8 @@ namespace spot
satdict.prodid.begin(); pit != satdict.prodid.end(); ++pit) satdict.prodid.begin(); pit != satdict.prodid.end(); ++pit)
if (positive.find(pit->second) != positive.end()) if (positive.find(pit->second) != positive.end())
dout << pit->second << "\t" << pit->first << "\n"; dout << pit->second << "\t" << pit->first << "\n";
else
dout << -pit->second << "\t¬" << pit->first << "C\n";
dout << "--- pathid_cand variables ---\n"; dout << "--- pathid_cand variables ---\n";
for (std::map<path, int>::const_iterator pit = for (std::map<path, int>::const_iterator pit =
@ -908,6 +911,9 @@ namespace spot
pit != satdict.pathid_cand.end(); ++pit) pit != satdict.pathid_cand.end(); ++pit)
if (positive.find(pit->second) != positive.end()) if (positive.find(pit->second) != positive.end())
dout << pit->second << "\t" << pit->first << "C\n"; dout << pit->second << "\t" << pit->first << "C\n";
else
dout << -pit->second << "\t¬" << pit->first << "C\n";
dout << "--- pathid_ref variables ---\n"; dout << "--- pathid_ref variables ---\n";
for (std::map<path, int>::const_iterator pit = for (std::map<path, int>::const_iterator pit =
@ -915,6 +921,18 @@ namespace spot
pit != satdict.pathid_ref.end(); ++pit) pit != satdict.pathid_ref.end(); ++pit)
if (positive.find(pit->second) != positive.end()) if (positive.find(pit->second) != positive.end())
dout << pit->second << "\t" << pit->first << "R\n"; dout << pit->second << "\t" << pit->first << "R\n";
else
dout << -pit->second << "\t¬" << pit->first << "C\n";
dout << "--- pathcand variables ---\n";
for (std::map<state_pair, int>::const_iterator pit =
satdict.pathcand.begin();
pit != satdict.pathcand.end(); ++pit)
if (positive.find(pit->second) != positive.end())
dout << pit->second << "\t" << pit->first << "C\n";
else
dout << -pit->second << "\t¬" << pit->first << "C\n";
#endif #endif
a->merge_transitions(); a->merge_transitions();

1
src/tgbaalgos/dtgbasat.cc
View file

@ -18,6 +18,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream> #include <iostream>
#include <fstream>
#include <sstream> #include <sstream>
#include "dtgbasat.hh" #include "dtgbasat.hh"
#include "reachiter.hh" #include "reachiter.hh"