Commit ebe4ffc5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sccinfo: introduce is_rejecting()

Because scc_info does not perform a full emptiness check, it is not
always able to tell whether an SCC is accepting if the acceptance
condition use Fin primitives.  This introduce is_rejecting_scc() in
addition to to is_accepting_scc().  Only one of them may be true, but
they can both be false if scc_info has no idea whether the SCC is
accepting.

* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: Implement
is_rejecting_scc().
* src/bin/ltlcross.cc, src/tgba/acc.cc, src/tgba/acc.hh,
src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/remfin.cc, src/tgbaalgos/safety.cc,
src/tgbaalgos/sccfilter.cc: Use it.
* src/tgbaalgos/dotty.cc: Use is_rejecting_scc() and is_accepting_scc()
to color SCCs.
* doc/org/oaut.org: Document the colors used.
* src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Adjust
tests.
* src/tgbatest/sccdot.test: New test case.
* src/tgbatest/Makefile.am: Add it.
parent 86584418
...@@ -547,18 +547,22 @@ digraph G { ...@@ -547,18 +547,22 @@ digraph G {
I [label="", style=invis, height=0] I [label="", style=invis, height=0]
I -> 1 I -> 1
subgraph cluster_0 { subgraph cluster_0 {
color=green
label="" label=""
0 [label="0"] 0 [label="0"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=green
label="" label=""
3 [label="3"] 3 [label="3"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=red
label="" label=""
4 [label="4"] 4 [label="4"]
} }
subgraph cluster_3 { subgraph cluster_3 {
color=green
label="" label=""
1 [label="1"] 1 [label="1"]
2 [label="2"] 2 [label="2"]
...@@ -586,40 +590,77 @@ ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/' ...@@ -586,40 +590,77 @@ ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
#+RESULTS: oaut-dot2 #+RESULTS: oaut-dot2
#+begin_example #+begin_example
digraph G { digraph G {
label="(Gb | F!a) W c\\nInf(0)" rankdir=LR
label="Fin(2) & (Inf(0)&Inf(1))"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, height=0] I [label="", style=invis, width=0]
I -> 1 I -> 1
subgraph cluster_0 { subgraph cluster_0 {
color=grey
label="" label=""
0 [label="0"] 5 [label="5"]
6 [label="6"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=orange
label="" label=""
3 [label="3"] 0 [label="0"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=orange
label="" label=""
4 [label="4"] 9 [label="9"]
10 [label="10"]
} }
subgraph cluster_3 { subgraph cluster_3 {
color=green
label=""
8 [label="8"]
}
subgraph cluster_4 {
color=green
label=""
7 [label="7"]
}
subgraph cluster_5 {
color=black
label="" label=""
1 [label="1"]
2 [label="2"] 2 [label="2"]
} }
0 -> 0 [label="b\\n{0}"] subgraph cluster_6 {
1 -> 0 [label="a & b & !c"] color=red
1 -> 1 [label="!a & !c\\n{0}"] label=""
1 -> 2 [label="a & !c"] 4 [label="4"]
1 -> 3 [label="c"] }
2 -> 1 [label="!a & !c\\n{0}"] subgraph cluster_7 {
2 -> 2 [label="a & !c"] color=green
2 -> 3 [label="!a & c"] label=""
2 -> 4 [label="a & c"] 1 [label="1"]
3 -> 3 [label="1\\n{0}"] 3 [label="3"]
4 -> 3 [label="!a"] }
4 -> 4 [label="a"] 0 -> 0 [label="a & b\\n{0,1,2}"]
0 -> 0 [label="!a & !b\\n{2}"]
0 -> 5 [label="a\\n{2}"]
1 -> 4 [label="b"]
1 -> 3 [label="a & !b"]
2 -> 0 [label="a"]
2 -> 7 [label="b"]
3 -> 1 [label="a & b\\n{0,1}"]
4 -> 4 [label="!b\\n{1,2}"]
4 -> 2 [label="b"]
5 -> 6 [label="1"]
6 -> 5 [label="1"]
7 -> 7 [label="!a & b\\n{0,1}"]
7 -> 7 [label="a & b\\n{0,2}"]
7 -> 8 [label="1"]
8 -> 8 [label="!a & b\\n{0,2}"]
8 -> 8 [label="a & b\\n{0,1}"]
8 -> 9 [label="1"]
9 -> 9 [label="!a & b\\n{0,2}"]
9 -> 10 [label="a & b\\n{0,1}"]
10 -> 9 [label="!a & b\\n{0,1}"]
10 -> 10 [label="a & b\\n{0,2}"]
} }
#+end_example #+end_example
...@@ -634,6 +675,134 @@ The acceptance condition is displayed in the same way as in the [[http://adl.git ...@@ -634,6 +675,134 @@ The acceptance condition is displayed in the same way as in the [[http://adl.git
format]]. Here =Inf(0)= means that runs are accepting if and only if format]]. Here =Inf(0)= means that runs are accepting if and only if
they visit some the transitions in the set #0 infinitely often. they visit some the transitions in the set #0 infinitely often.
The strongly connected components are displayed using the following colors:
- *green* components contain an accepting cycle
- *red* components contain no accepting cycle
- *orange* components may or may not contain an accepting cycle. Such an indecision occur only when using =Fin= acceptance primitive, deciding that would require a better algorithm than what the output routine is using.
- *black* components are trivial (i.e., they contain no cycle)
- *gray* components are useless (i.e., they are non-accepting, and are only followed by non-accepting components)
Here is an example involving all colors:
#+NAME: oaut-dot3
#+BEGIN_SRC sh :results verbatim :exports none
autfilt --dot=cas <<EOF | sed 's/\\/\\\\/'
HOA: v1
States: 10
Start: 1
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 3 Inf(0)&Inf(1)&Fin(2)
--BODY--
State: 0 {2}
[0&1] 0 {0 1}
[!0&!1] 0
[0] 5
State: 1
[1] 4
[0&!1] 3
State: 4
[!1] 4 {1 2}
[1] 2
State: 2
[0] 0
[1] 7
State: 3
[0&1] 1 {1 0}
State: 5
[t] 6 {1}
State: 6
[t] 5
State: 7
[!0&1] 7 {0 2}
[0&1] 7 {0 1}
[t] 8
State: 8
[!0&1] 8 {0 2}
[0&1] 9 {0 1}
State: 9
[!0&1] 8 {0 1}
[0&1] 9 {0 2}
--END--
EOF
#+END_SRC
#+RESULTS: oaut-dot3
#+begin_example
digraph G {
rankdir=LR
label="Fin(2) & (Inf(0)&Inf(1))"
labelloc="t"
node [shape="circle"]
I [label="", style=invis, width=0]
I -> 1
subgraph cluster_0 {
color=grey
label=""
5 [label="5"]
6 [label="6"]
}
subgraph cluster_1 {
color=orange
label=""
0 [label="0"]
}
subgraph cluster_2 {
color=orange
label=""
8 [label="8"]
9 [label="9"]
}
subgraph cluster_3 {
color=green
label=""
7 [label="7"]
}
subgraph cluster_4 {
color=black
label=""
2 [label="2"]
}
subgraph cluster_5 {
color=red
label=""
4 [label="4"]
}
subgraph cluster_6 {
color=green
label=""
1 [label="1"]
3 [label="3"]
}
0 -> 0 [label="a & b\\n{0,1,2}"]
0 -> 0 [label="!a & !b\\n{2}"]
0 -> 5 [label="a\\n{2}"]
1 -> 4 [label="b"]
1 -> 3 [label="a & !b"]
2 -> 0 [label="a"]
2 -> 7 [label="b"]
3 -> 1 [label="a & b\\n{0,1}"]
4 -> 4 [label="!b\\n{1,2}"]
4 -> 2 [label="b"]
5 -> 6 [label="1\\n{1}"]
6 -> 5 [label="1"]
7 -> 7 [label="!a & b\\n{0,2}"]
7 -> 7 [label="a & b\\n{0,1}"]
7 -> 8 [label="1"]
8 -> 8 [label="!a & b\\n{0,2}"]
8 -> 9 [label="a & b\\n{0,1}"]
9 -> 8 [label="!a & b\\n{0,1}"]
9 -> 9 [label="a & b\\n{0,2}"]
}
#+end_example
#+BEGIN_SRC dot :file oaut-dot3.png :cmdline -Tpng :var txt=oaut-dot3 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:oaut-dot3.png]]
* Statistics * Statistics
The =--stats= option takes format string parameter to specify what and The =--stats= option takes format string parameter to specify what and
......
...@@ -673,7 +673,7 @@ namespace ...@@ -673,7 +673,7 @@ namespace
st->nondeterministic = st->nondetstates != 0; st->nondeterministic = st->nondetstates != 0;
for (unsigned n = 0; n < c; ++n) for (unsigned n = 0; n < c; ++n)
{ {
if (!m.is_accepting_scc(n)) if (m.is_rejecting_scc(n))
++st->nonacc_scc; ++st->nonacc_scc;
else if (is_terminal_scc(m, n)) else if (is_terminal_scc(m, n))
++st->terminal_scc; ++st->terminal_scc;
......
...@@ -189,6 +189,47 @@ namespace spot ...@@ -189,6 +189,47 @@ namespace spot
return false; return false;
} }
static bool
inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
{
switch (pos->op)
{
case acc_cond::acc_op::And:
{
auto sub = pos - pos->size;
while (sub < pos)
{
--pos;
if (!inf_eval(inf, pos))
return false;
pos -= pos->size;
}
return true;
}
case acc_cond::acc_op::Or:
{
auto sub = pos - pos->size;
while (sub < pos)
{
--pos;
if (inf_eval(inf, pos))
return true;
pos -= pos->size;
}
return false;
}
case acc_cond::acc_op::Inf:
return (pos[-1].mark & inf) == pos[-1].mark;
case acc_cond::acc_op::Fin:
return true;
case acc_cond::acc_op::FinNeg:
case acc_cond::acc_op::InfNeg:
SPOT_UNREACHABLE();
}
SPOT_UNREACHABLE();
return false;
}
static acc_cond::mark_t static acc_cond::mark_t
eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos) eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
{ {
...@@ -243,6 +284,13 @@ namespace spot ...@@ -243,6 +284,13 @@ namespace spot
return eval(inf, &code_.back()); return eval(inf, &code_.back());
} }
bool acc_cond::inf_satisfiable(mark_t inf) const
{
if (code_.empty())
return true;
return inf_eval(inf, &code_.back());
}
acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const
{ {
if (uses_fin_acceptance()) if (uses_fin_acceptance())
......
...@@ -843,6 +843,11 @@ namespace spot ...@@ -843,6 +843,11 @@ namespace spot
} }
bool accepting(mark_t inf) const; bool accepting(mark_t inf) const;
// Assume all Fin(x) in the condition a true. Would the resulting
// condition (involving only Inf(y)) be satisfiable?
bool inf_satisfiable(mark_t inf) const;
mark_t accepting_sets(mark_t inf) const; mark_t accepting_sets(mark_t inf) const;
std::ostream& format(std::ostream& os, mark_t m) const std::ostream& format(std::ostream& os, mark_t m) const
......
...@@ -164,10 +164,25 @@ namespace spot ...@@ -164,10 +164,25 @@ namespace spot
for (unsigned i = 0; i < sccs; ++i) for (unsigned i = 0; i < sccs; ++i)
{ {
os_ << " subgraph cluster_" << i << " {\n"; os_ << " subgraph cluster_" << i << " {\n";
// Color the SCC to indicate whether is it accepting.
if (!si->is_useful_scc(i))
os_ << " color=grey\n";
else if (si->is_trivial(i))
os_ << " color=black\n";
else if (si->is_accepting_scc(i))
os_ << " color=green\n";
else if (si->is_rejecting_scc(i))
os_ << " color=red\n";
else
os_ << " color=orange\n";
if (name_ || opt_show_acc_) if (name_ || opt_show_acc_)
// Reset the label, otherwise the graph label would {
// be inherited by the cluster. // Reset the label, otherwise the graph label would
os_ << " label=\"\"\n"; // be inherited by the cluster.
os_ << " label=\"\"\n";
}
for (auto s: si->states_of(i)) for (auto s: si->states_of(i))
process_state(s); process_state(s);
os_ << " }\n"; os_ << " }\n";
......
...@@ -136,7 +136,7 @@ namespace spot ...@@ -136,7 +136,7 @@ namespace spot
{ {
acc_cond::mark_t acc = 0U; acc_cond::mark_t acc = 0U;
unsigned scc = si.scc_of(src); unsigned scc = si.scc_of(src);
if (!si.is_accepting_scc(scc) && !si.is_trivial(scc)) if (si.is_rejecting_scc(scc) && !si.is_trivial(scc))
acc = all_acc; acc = all_acc;
// Keep track of all conditions on transition leaving state // Keep track of all conditions on transition leaving state
......
...@@ -80,9 +80,8 @@ namespace spot ...@@ -80,9 +80,8 @@ namespace spot
bool bool
is_weak_scc(scc_info& map, unsigned scc) is_weak_scc(scc_info& map, unsigned scc)
{ {
// If no cycle is accepting, the SCC is weak. // Rejecting SCCs are weak.
if (!map.is_accepting_scc(scc) if (map.is_rejecting_scc(scc))
&& !map.get_aut()->acc().uses_fin_acceptance())
return true; return true;
// If all transitions use the same acceptance set, the SCC is weak. // If all transitions use the same acceptance set, the SCC is weak.
return map.used_acc_of(scc).size() == 1; return map.used_acc_of(scc).size() == 1;
......
...@@ -292,6 +292,9 @@ namespace spot ...@@ -292,6 +292,9 @@ namespace spot
res->new_transition(s, t.dst, t.cond, res->new_transition(s, t.dst, t.cond,
(t.acc & main_sets) | main_add); (t.acc & main_sets) | main_add);
if (si.is_rejecting_scc(n))
continue;
// Create clones // Create clones
for (unsigned i = 0; i < cs; ++i) for (unsigned i = 0; i < cs; ++i)
if (m & rem[i]) if (m & rem[i])
......
...@@ -40,8 +40,12 @@ namespace spot ...@@ -40,8 +40,12 @@ namespace spot
for (auto& scc: *si) for (auto& scc: *si)
{ {
if (!scc.is_accepting()) if (scc.is_rejecting())
continue; continue;
// Non-rejecting SCCs should necessarily be accepting, because
// with only one self loop, there should be no ambiguity.
if (!scc.is_accepting())
return false;
// Accepting SCCs should have only one state. // Accepting SCCs should have only one state.
auto& st = scc.states(); auto& st = scc.states();
if (st.size() != 1) if (st.size() != 1)
......
...@@ -115,7 +115,7 @@ namespace spot ...@@ -115,7 +115,7 @@ namespace spot
// the destination in not in an accepting SCC, // the destination in not in an accepting SCC,
// or if we are between SCC with early_susp unset. // or if we are between SCC with early_susp unset.
unsigned u = this->si->scc_of(dst); unsigned u = this->si->scc_of(dst);
if (!this->si->is_accepting_scc(u) if (this->si->is_rejecting_scc(u)
|| (!early_susp && (u != this->si->scc_of(src)))) || (!early_susp && (u != this->si->scc_of(src))))
cond = bdd_exist(cond, suspvars); cond = bdd_exist(cond, suspvars);
} }
...@@ -147,7 +147,7 @@ namespace spot ...@@ -147,7 +147,7 @@ namespace spot
unsigned u = this->si->scc_of(src); unsigned u = this->si->scc_of(src);
// If the transition is between two SCCs, or in a // If the transition is between two SCCs, or in a
// non-accepting SCC. Remove the acceptance sets. // non-accepting SCC. Remove the acceptance sets.
if (!this->si->is_accepting_scc(u) || u != this->si->scc_of(dst)) if (this->si->is_rejecting_scc(u) || u != this->si->scc_of(dst))
acc = 0U; acc = 0U;
} }
...@@ -173,7 +173,7 @@ namespace spot ...@@ -173,7 +173,7 @@ namespace spot
std::tie(keep, cond, acc) = std::tie(keep, cond, acc) =
this->next_filter::trans(src, dst, cond, acc); this->next_filter::trans(src, dst, cond, acc);
if (!this->si->is_accepting_scc(this->si->scc_of(dst))) if (this->si->is_rejecting_scc(this->si->scc_of(dst)))
acc = 0U; acc = 0U;
return filtered_trans(keep, cond, acc); return filtered_trans(keep, cond, acc);
} }
...@@ -206,7 +206,7 @@ namespace spot ...@@ -206,7 +206,7 @@ namespace spot
unsigned max = 0; // Max number of useful sets unsigned max = 0; // Max number of useful sets
for (unsigned n = 0; n < scc_count; ++n) for (unsigned n = 0; n < scc_count; ++n)
{ {
if (!this->si->is_accepting_scc(n)) if (this->si->is_rejecting_scc(n))
continue; continue;
strip_[n] = acc.useless(used_acc[n].begin(), used_acc[n].end()); strip_[n] = acc.useless(used_acc[n].begin(), used_acc[n].end());
cnt[n] = acc.num_sets() - strip_[n].count(); cnt[n] = acc.num_sets() - strip_[n].count();
...@@ -218,7 +218,7 @@ namespace spot ...@@ -218,7 +218,7 @@ namespace spot
// that do not have enough. // that do not have enough.
for (unsigned n = 0; n < scc_count; ++n) for (unsigned n = 0; n < scc_count; ++n)
{ {
if (!this->si->is_accepting_scc(n)) if (this->si->is_rejecting_scc(n))
continue; continue;
if (cnt[n] < max) if (cnt[n] < max)
strip_[n].remove_some(max - cnt[n]); strip_[n].remove_some(max - cnt[n]);
...@@ -237,7 +237,7 @@ namespace spot ...@@ -237,7 +237,7 @@ namespace spot
{ {
unsigned u = this->si->scc_of(dst); unsigned u = this->si->scc_of(dst);
if (!this->si->is_accepting_scc(u)) if (this->si->is_rejecting_scc(u))
acc = 0U; acc = 0U;
else else
acc = acc.strip(strip_[u]); acc = acc.strip(strip_[u]);
......
...@@ -120,7 +120,10 @@ namespace spot ...@@ -120,7 +120,10 @@ namespace spot
node_.emplace_back(acc, triv); node_.emplace_back(acc, triv);
std::swap(node_.back().succ_, root_.front().node.succ_); std::swap(node_.back().succ_, root_.front().node.succ_);
std::swap(node_.back().states_, root_.front().node.states_); std::swap(node_.back().states_, root_.front().node.states_);
node_.back().accepting_ = !triv && aut->acc().accepting(acc); node_.back().accepting_ =
!triv && root_.front().node.accepting_;
node_.back().rejecting_ =
triv || !aut->acc().inf_satisfiable(acc);
root_.pop_front(); root_.pop_front();
// Record the transition between the SCC being popped // Record the transition between the SCC being popped
// and the previous SCC. // and the previous SCC.
...@@ -177,7 +180,7 @@ namespace spot ...@@ -177,7 +180,7 @@ namespace spot
// non-dead SCC has necessarily been crossed by our path to // non-dead SCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs // this state: there is a state S2 in our path which belongs
// to this SCC too. We are going to merge all states between // to this SCC too. We are going to merge all states between
// this S1 and S2 into this SCC. // this S1 and S2 into this SCC..
// //
// This merge is easy to do because the order of the SCC in // This merge is easy to do because the order of the SCC in
// ROOT is descending: we just have to merge all SCCs from the // ROOT is descending: we just have to merge all SCCs from the
...@@ -186,17 +189,24 @@ namespace spot ...@@ -186,17 +189,24 @@ namespace spot
int threshold = spi; int threshold = spi;
std::list<unsigned> states; std::list<unsigned> states;
scc_succs succs; scc_succs succs;
bool is_accepting = false;
// If this is a self-loop, check its acceptance alone.
if (dest == succ->src)
is_accepting = aut->acc().accepting(acc);
assert(!root_.empty());
while (threshold > root_.front().index) while (threshold > root_.front().index)
{ {
assert(!root_.empty());
acc |= root_.front().node.acc_; acc |= root_.front().node.acc_;
acc |= root_.front().in_acc; acc |= root_.front().in_acc;
is_accepting |= root_.front().node.accepting_;
states.splice(states.end(), root_.front().node.states_); states.splice(states.end(), root_.front().node.states_);
succs.insert(succs.end(),