Commit 95d732e3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

specialize scc_filter for inherently_weak automata

Part of issue #351.

* spot/twaalgos/sccfilter.cc, spot/twaalgos/sccfilter.hh: Specialize
for inherently-weak automata.
* spot/twaalgos/postproc.cc: Simplify.
* tests/core/dca2.test, tests/core/parity2.test,
tests/core/prodor.test, tests/core/randomize.test,
tests/python/automata.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/python/remfin.py,
tests/python/stutter-inv.ipynb: Adjust.
* NEWS: Mention it.
parent 2fad1ff6
Pipeline #2235 passed with stage
in 62 minutes and 26 seconds
......@@ -122,6 +122,12 @@ New in spot 2.5.3.dev (not yet released)
to update an external structure that references states of the twa
that we want to purge.
- spot::scc_filter() now automatically turns automata marked as
inherently-weak into weak automata with state-based acceptance.
The acceptance condition is set to Büchi unless the input had
co-Büchi or t acceptance. spot::scc_filter_states() will pass
inherently-weak automata to spot::scc_filter().
- spot::cleanup_parity() and spot::cleanup_parity_here() are smarter
and now remove from the acceptance condition the parity colors
that are not used in the automaton.
......
......@@ -38,7 +38,6 @@
#include <spot/twaalgos/alternation.hh>
#include <spot/twaalgos/parity.hh>
#include <spot/twaalgos/cobuchi.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/rabin2parity.hh>
namespace spot
......@@ -166,10 +165,7 @@ namespace spot
{
if (scc_filter_ == 0)
return a;
// If the automaton is weak, using transition-based acceptance
// won't help, so let's preserve state-based acceptance.
if ((state_based_ || a->prop_inherently_weak().is_true())
&& a->prop_state_acc().is_true())
if (state_based_ && a->prop_state_acc().is_true())
return scc_filter_states(a, arg);
else
return scc_filter(a, arg);
......
......@@ -124,6 +124,53 @@ namespace spot
}
};
// Transform inherently weak automata into weak Büchi automata.
template <bool buchi, class next_filter = id_filter>
struct weak_filter: next_filter
{
acc_cond::mark_t acc_m = {0};
acc_cond::mark_t rej_m = {};
template<typename... Args>
weak_filter(scc_info* si, Args&&... args)
: next_filter(si, std::forward<Args>(args)...)
{
if (!buchi)
{
acc_m = {};
if (si->get_aut()->acc().is_co_buchi())
rej_m = {0};
}
}
filtered_trans trans(unsigned src, unsigned dst,
bdd cond, acc_cond::mark_t acc)
{
bool keep;
std::tie(keep, cond, acc) =
this->next_filter::trans(src, dst, cond, acc);
if (keep)
{
unsigned ss = this->si->scc_of(src);
if (this->si->is_accepting_scc(ss))
acc = acc_m;
else
acc = rej_m;
}
return filtered_trans(keep, cond, acc);
}
void fix_acceptance(const twa_graph_ptr& out)
{
if (buchi)
out->set_buchi();
else
out->copy_acceptance_of(this->si->get_aut());
}
};
// Remove acceptance conditions from all edges outside of
// non-accepting SCCs. If "RemoveAll" is false, keep those on
// transitions entering accepting SCCs. If "PreserveSBA", is set
......@@ -160,7 +207,7 @@ namespace spot
unsigned v = this->si->scc_of(dst);
// The basic rules are as follows:
//
// - If an edge is between two SCCs, is OK to remove
// - If an edge is between two SCCs, it is OK to remove
// all acceptance sets, as this edge cannot be part
// of any loop.
// - If an edge is in an non-accepting SCC, we can only
......@@ -370,6 +417,10 @@ namespace spot
scc_info* given_si)
{
twa_graph_ptr res;
// For weak automata, scc_filter() is already doing the right
// thing and preserves state-based acceptance.
if (aut->prop_inherently_weak())
return scc_filter(aut, remove_all_useless, given_si);
if (remove_all_useless)
res = scc_filter_apply<state_filter
<acc_filter_mask<true, true>>>(aut, given_si);
......@@ -385,9 +436,18 @@ namespace spot
scc_info* given_si)
{
twa_graph_ptr res;
// acc_filter_simplify only works for generalized Büchi
if (aut->acc().is_generalized_buchi())
if (aut->prop_inherently_weak())
{
if (aut->acc().is_t() || aut->acc().is_co_buchi())
res =
scc_filter_apply<state_filter<weak_filter<false>>>(aut, given_si);
else
res =
scc_filter_apply<state_filter<weak_filter<true>>>(aut, given_si);
}
else if (aut->acc().is_generalized_buchi())
{
// acc_filter_simplify only works for generalized Büchi
if (remove_all_useless)
res =
scc_filter_apply<state_filter
......@@ -421,6 +481,11 @@ namespace spot
false,
true,
});
if (aut->prop_inherently_weak())
{
res->prop_weak(true);
res->prop_state_acc(true);
}
return res;
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de
// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2018 Laboratoire de
// Recherche et Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -50,13 +50,18 @@ namespace spot
/// degeneralization) will work better if transitions going to an
/// accepting SCC are accepting.
///
/// If the input is inherently weak, the output will be a weak
/// automaton with state-based acceptance. The acceptance condition
/// is set to Büchi unless the input was co-Büchi or t (in which
/// case we keep this acceptance).
///
/// If \a given_sm is supplied, the function will use its result
/// without computing a map of its own.
///
/// \warning Calling scc_filter on a TωA that has the SBA property
/// (i.e., transitions leaving accepting states are all marked as
/// accepting) may destroy this property. Use scc_filter_states()
/// instead.
/// \warning Calling scc_filter on a TωA that is not inherently weak
/// and has the SBA property (i.e., transitions leaving accepting
/// states are all marked as accepting) may destroy this property.
/// Use scc_filter_states() instead.
SPOT_API twa_graph_ptr
scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless = false,
scc_info* given_si = nullptr);
......
......@@ -67,7 +67,11 @@ while read l_f; do
autfilt -q --acceptance-is=Streett-like and.hoa
# Streett | Streett
autfilt r.hoa --name="($l_f)|!($r_f)" --product-or=l.hoa -S > or.hoa
autfilt -q -v --acceptance-is=Streett-like or.hoa
if ! grep -q ' weak' l.hoa; then
if ! grep -q ' weak' r.hoa; then
autfilt -q -v --acceptance-is=Streett-like or.hoa || exit 1
fi
fi
autcross --language-preserved --verbose -F or.hoa -F and.hoa \
'autfilt %H --stats=%M | ltl2tgba >%O' \
......
......@@ -236,7 +236,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
properties: weak
--BODY--
State: 0
[t] 0
......@@ -270,7 +270,7 @@ AP: 1 "a"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
properties: weak
--BODY--
State: 0
[t] 0
......@@ -304,7 +304,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
properties: weak
--BODY--
State: 0
[t] 0
......@@ -338,7 +338,7 @@ AP: 1 "a"
acc-name: Streett 1
Acceptance: 2 Fin(0) | Inf(1)
properties: trans-labels explicit-labels state-acc colored
properties: stutter-invariant inherently-weak
properties: stutter-invariant weak
--BODY--
State: 0 {0}
[t] 0
......@@ -372,7 +372,7 @@ AP: 1 "a"
acc-name: parity min odd 3
Acceptance: 3 Fin(0) & (Inf(1) | Fin(2))
properties: trans-labels explicit-labels state-acc colored
properties: stutter-invariant inherently-weak
properties: stutter-invariant weak
--BODY--
State: 0 {2}
[t] 0
......@@ -406,7 +406,7 @@ AP: 1 "a"
acc-name: parity max even 3
Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))
properties: trans-labels explicit-labels state-acc colored
properties: stutter-invariant inherently-weak
properties: stutter-invariant weak
--BODY--
State: 0 {1}
[t] 0
......
......@@ -57,23 +57,24 @@ HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) | Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 0 {1}
[0] 0 {0}
[!0&1] 1
[0&1] 1 {1}
[0&1] 1 {0}
State: 1
[!0&1] 1 {0}
[0&1] 1 {0 1}
[0&1] 1 {0}
[!0&!1] 2 {0}
[0&!1] 2 {0 1}
[0&!1] 2 {0}
State: 2
[!0] 2
[0] 2 {1}
[0] 2 {0}
--END--
EOF
diff por.hoa exp
......@@ -88,18 +89,18 @@ HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0
[!0] 0
[0] 0 {1}
[0] 0
[!0&1] 1
[0&1] 1 {1}
[0&1] 1
State: 1
[!0&1] 1 {0}
[0&1] 1 {0 1}
[!0&1] 1
[0&1] 1 {0}
--END--
EOF
diff pand.hoa exp
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
# Copyright (C) 2014, 2015, 2017, 2018 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -33,7 +33,7 @@ AP: 4 "a" "b" "c" "d"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: inherently-weak
properties: weak
--BODY--
State: 0
[0] 1
......
This diff is collapsed.
%% Cell type:code id: tags:
``` python
import spot
spot.setup()
from IPython.display import display
```
%% Cell type:markdown id: tags:
This notebook shows you different ways in which states or transitions can be highlighted in Spot.
It should be noted that highlighting works using some special [named properties](https://spot.lrde.epita.fr/concepts.html#named-properties): basically, two maps that are attached to the automaton, and associated state or edge numbers to color numbers. This named properties are fragile: they will be lost if the automaton is transformed into a new automaton, and they can become meaningless of the automaton is modified in place (e.g., if the transitions or states are reordered).
Nonetheless, highlighting is OK to use right before displaying or printing the automaton. The `dot` and `hoa` printer both know how to represent highlighted states and transitions.
# Manual highlighting
%% Cell type:code id: tags:
``` python
a = spot.translate('a U b U c')
```
%% Cell type:markdown id: tags:
The `#` option of `print_dot()` can be used to display the internal number of each transition
%% Cell type:code id: tags:
``` python
a.show('.#')
```
%% Output
<IPython.core.display.SVG object>
%% Cell type:markdown id: tags:
Using these numbers you can selectively hightlight some transitions. The second argument is a color number (from a list of predefined colors).
%% Cell type:code id: tags:
``` python
a.highlight_edges([2, 4, 5], 1)
```
%% Output
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0128edca50> >
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7feca4075120> >
%% Cell type:markdown id: tags:
Note that these `highlight_` functions work for edges and states, and come with both singular (changing the color of single state or edge) and plural versions.
They modify the automaton in place.
%% Cell type:code id: tags:
``` python
a.highlight_edge(6, 2).highlight_states((0, 1), 0)
```
%% Output
<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7f0128e4cd50> >
<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fec96f528d0> >
%% Cell type:markdown id: tags:
The plural version can take a list or tuple of state numbers (as above) or of Booleans (as below). In the latter case the indices of the True values give the states to highlight.
%% Cell type:code id: tags:
``` python
a.highlight_states([False, True, True], 5)
```
%% Output
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0128edca50> >
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7feca4075120> >
%% Cell type:markdown id: tags:
# Saving to HOA 1.1
When saving to HOA format, the highlighting is only output if version 1.1 of the format is selected, because the headers `spot.highlight.edges` and `spot.highlight.states` contain dots, which are disallowed in version 1. Compare these two outputs:
%% Cell type:code id: tags:
``` python
print(a.to_str('HOA', '1'))
print()
print(a.to_str('HOA', '1.1'))
```
%% Output
HOA: v1
States: 3
Start: 2
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[2] 0
[1&!2] 1
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2
--END--
HOA: v1.1
States: 3
Start: 2
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic stutter-invariant terminal
spot.highlight.states: 0 0 1 5 2 5
spot.highlight.edges: 2 1 4 1 5 1 6 2
--BODY--
State: 0 {0}
[t] 0
State: 1
[2] 0
[1&!2] 1
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2
--END--
%% Cell type:markdown id: tags:
# Highlighting a run
One use of this highlighting is to highlight a run in an automaton.
The following few command generate an automaton, then an accepting run on this automaton, and highlight that accepting run on the automaton. Note that a run knows the automaton from which it was generated, so calling `highlight()` will directly decorate that automaton.
%% Cell type:code id: tags:
``` python
b = spot.translate('X (F(Ga <-> b) & GF!b)'); b
```
%% Output
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0128e4cab0> >
<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fec96f528a0> >
%% Cell type:code id: tags:
``` python
r = b.accepting_run(); r
```
%% Output
Prefix:
0
| 1
1
| !a & !b
Cycle:
2
| !b {0}
%% Cell type:code id: tags:
``` python
r.highlight(5) # the parameter is a color number
```
%% Cell type:markdown id: tags:
The call of `highlight(5)` on the accepting run `r` modified the original automaton `b`:
%% Cell type:code id: tags:
``` python
b
```
%% Output