Commit 80ce0e21 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

satminimization: do not assume the initial state is 0

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
parent 5d8f16da
...@@ -395,9 +395,12 @@ namespace spot ...@@ -395,9 +395,12 @@ namespace spot
} }
dout << "(2) the initial state is reachable\n"; dout << "(2) the initial state is reachable\n";
dout << state_pair(0, 0) << '\n'; {
out << d.prodid[state_pair(0, 0)] << " 0\n"; unsigned init = ref->get_init_state_number();
dout << state_pair(0, init) << '\n';
out << d.prodid[state_pair(0, init)] << " 0\n";
++nclauses; ++nclauses;
}
for (std::map<state_pair, int>::const_iterator pit = d.prodid.begin(); for (std::map<state_pair, int>::const_iterator pit = d.prodid.begin();
pit != d.prodid.end(); ++pit) pit != d.prodid.end(); ++pit)
......
...@@ -527,9 +527,12 @@ namespace spot ...@@ -527,9 +527,12 @@ namespace spot
} }
dout << "(9) the initial state is reachable\n"; dout << "(9) the initial state is reachable\n";
dout << path(0, 0) << '\n'; {
out << d.pathid[path(0, 0)] << " 0\n"; unsigned init = ref->get_init_state_number();
dout << path(0, init) << '\n';
out << d.pathid[path(0, init)] << " 0\n";
++nclauses; ++nclauses;
}
for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
for (unsigned q1p = 0; q1p < ref_size; ++q1p) for (unsigned q1p = 0; q1p < ref_size; ++q1p)
...@@ -732,11 +735,9 @@ namespace spot ...@@ -732,11 +735,9 @@ namespace spot
transition_acc transition_acc
ta(q2, l, ta(q2, l,
d.cacc.mark(m), q3); d.cacc.mark(m), q3);
int tai = d.transaccid[ta];
const char* not_ = "¬"; const char* not_ = "¬";
if (d.cacc.has(biga_, m)) if (d.cacc.has(biga_, m))
not_ = ""; not_ = "";
out << tai << ' ';
out << " ∧ " << not_ out << " ∧ " << not_
<< ta << "FC"; << ta << "FC";
} }
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment