Commit 87c2b291 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

tgba_digraph: force selection of properties kept on copy

* src/tgba/tgba.hh: Declare a prop_set to specify the types.
* src/tgba/tgbagraph.hh: Use prop_set for all copy constructors.
* iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc,
src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc,
src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc,
src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
parent 77cb836e
......@@ -602,7 +602,8 @@ namespace spot
public:
spins_kripke(const spins_interface* d, const bdd_dict_ptr& dict,
const prop_set* ps, const ltl::formula* dead, int compress)
const spot::prop_set* ps, const ltl::formula* dead,
int compress)
: kripke(dict),
d_(d),
state_size_(d_->get_state_size()),
......@@ -723,14 +724,13 @@ namespace spot
compute_state_condition_aux(const int* vars) const
{
bdd res = bddtrue;
for (prop_set::const_iterator i = ps_->begin();
i != ps_->end(); ++i)
for (auto& i: *ps_)
{
int l = vars[i->var_num];
int r = i->val;
int l = vars[i.var_num];
int r = i.val;
bool cond = false;
switch (i->op)
switch (i.op)
{
case OP_EQ:
cond = (l == r);
......@@ -753,9 +753,9 @@ namespace spot
}
if (cond)
res &= bdd_ithvar(i->bddvar);
res &= bdd_ithvar(i.bddvar);
else
res &= bdd_nithvar(i->bddvar);
res &= bdd_nithvar(i.bddvar);
}
return res;
}
......@@ -922,7 +922,7 @@ namespace spot
bdd_dict_ptr dict_;
const char** vname_;
bool* format_filter_;
const prop_set* ps_;
const spot::prop_set* ps_;
bdd alive_prop;
bdd dead_prop;
void (*compress_)(const int*, size_t, int*, size_t&);
......@@ -1130,7 +1130,7 @@ namespace spot
return 0;
}
prop_set* ps = new prop_set;
spot::prop_set* ps = new spot::prop_set;
int errors = convert_aps(to_observe, d, dict, dead, *ps);
if (errors)
{
......
......@@ -574,8 +574,9 @@ namespace
// If --stats or --name is used, duplicate the automaton so we
// never modify the original automaton (e.g. with
// merge_transitions()) and the statistics about it make sense.
auto aut = ((format == Stats) || opt_name) ?
spot::make_tgba_digraph(haut->aut) : haut->aut;
auto aut = ((format == Stats) || opt_name)
? spot::make_tgba_digraph(haut->aut, spot::tgba::prop_set::all())
: haut->aut;
// Preprocessing.
......@@ -599,7 +600,9 @@ namespace
matched &= aut->is_empty();
if (opt_uniq)
{
auto tmp = spot::canonicalize(make_tgba_digraph(aut));
auto tmp =
spot::canonicalize(make_tgba_digraph(aut,
spot::tgba::prop_set::all()));
matched = opt_uniq->emplace(tmp->transition_vector().begin() + 1,
tmp->transition_vector().end()).second;
}
......
......@@ -311,7 +311,9 @@ main(int argc, char** argv)
if (opt_uniq)
{
auto tmp = make_tgba_digraph(spot::canonicalize(aut));
auto tmp =
spot::canonicalize(make_tgba_digraph(aut,
spot::tgba::prop_set::all()));
std::vector<tr_t> trans(tmp->transition_vector().begin() + 1,
tmp->transition_vector().end());
if (opt_uniq->emplace(trans).second)
......
......@@ -35,84 +35,184 @@ run 0 ../tgbagraph | tee stdout
cat >expected <<EOF
digraph G {
rankdir=LR
0 [label="", style=invis, width=0]
0 -> 1
1 [label="0"]
1 -> 1 [label="0"]
1 -> 2 [label="p1"]
1 -> 3 [label="p2\n{1}"]
2 [label="1"]
2 -> 3 [label="p1 & p2\n{0}"]
3 [label="2"]
3 -> 1 [label="p1 | p2\n{0,1}"]
3 -> 2 [label="!p1 | p2"]
3 -> 3 [label="1\n{0,1}"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="0"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
2 -> 0 [label="p1 | p2\n{0,1}"]
2 -> 1 [label="!p1 | p2"]
2 -> 2 [label="1\n{0,1}"]
}
digraph G {
rankdir=LR
0 [label="", style=invis, width=0]
0 -> 1
1 [label="0"]
1 -> 1 [label="0"]
1 -> 2 [label="p1"]
1 -> 3 [label="p2\n{1}"]
2 [label="1"]
2 -> 3 [label="p1 & p2\n{0}"]
3 [label="2"]
3 -> 1 [label="p1 | p2\n{0,1}"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="0"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
2 -> 0 [label="p1 | p2\n{0,1}"]
}
digraph G {
rankdir=LR
0 [label="", style=invis, width=0]
0 -> 1
1 [label="0"]
1 -> 1 [label="0"]
1 -> 2 [label="p1"]
1 -> 3 [label="p2\n{1}"]
2 [label="1"]
2 -> 3 [label="p1 & p2\n{0}"]
3 [label="2"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="0"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
}
digraph G {
rankdir=LR
0 [label="", style=invis, width=0]
0 -> 1
1 [label="0"]
1 -> 1 [label="0"]
1 -> 2 [label="p1"]
1 -> 3 [label="p2\n{1}"]
2 [label="1"]
2 -> 3 [label="p1 & p2\n{0}"]
3 [label="2"]
3 -> 1 [label="p1 | p2\n{0,1}"]
3 -> 2 [label="!p1 | p2"]
3 -> 1 [label="1\n{0,1}"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 0 [label="0"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
2 -> 0 [label="p1 | p2\n{0,1}"]
2 -> 1 [label="!p1 | p2"]
2 -> 0 [label="1\n{0,1}"]
}
digraph G {
rankdir=LR
0 [label="", style=invis, width=0]
0 -> 1
1 [label="0"]
1 -> 2 [label="p1"]
1 -> 3 [label="p2\n{1}"]
2 [label="1"]
2 -> 3 [label="p1 & p2\n{0}"]
3 [label="2"]
3 -> 1 [label="1\n{0,1}"]
3 -> 2 [label="!p1 | p2"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
2 -> 0 [label="1\n{0,1}"]
2 -> 1 [label="!p1 | p2"]
}
digraph G {
rankdir=LR
0 [label="", style=invis, width=0]
0 -> 1
1 [label="0"]
1 -> 2 [label="p1"]
1 -> 3 [label="p2\n{1}"]
2 [label="1"]
2 -> 3 [label="p1 & p2\n{0}"]
3 [label="2"]
3 -> 1 [label="1\n{0,1}"]
3 -> 2 [label="!p1 | p2"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="p1"]
0 -> 2 [label="p2\n{1}"]
1 [label="1"]
1 -> 2 [label="p1 & p2\n{0}"]
2 [label="2"]
2 -> 0 [label="1\n{0,1}"]
2 -> 1 [label="!p1 | p2"]
3 [label="3"]
4 [label="4"]
5 [label="5"]
6 [label="6"]
7 [label="7"]
8 [label="8"]
9 [label="9"]
10 [label="10"]
11 [label="11"]
12 [label="12"]
13 [label="13"]
14 [label="14"]
15 [label="15"]
16 [label="16"]
17 [label="17"]
18 [label="18"]
19 [label="19"]
20 [label="20"]
21 [label="21"]
22 [label="22"]
23 [label="23"]
24 [label="24"]
25 [label="25"]
26 [label="26"]
27 [label="27"]
28 [label="28"]
29 [label="29"]
30 [label="30"]
31 [label="31"]
32 [label="32"]
33 [label="33"]
34 [label="34"]
35 [label="35"]
36 [label="36"]
37 [label="37"]
38 [label="38"]
39 [label="39"]
40 [label="40"]
41 [label="41"]
42 [label="42"]
43 [label="43"]
44 [label="44"]
45 [label="45"]
46 [label="46"]
47 [label="47"]
48 [label="48"]
49 [label="49"]
50 [label="50"]
51 [label="51"]
52 [label="52"]
53 [label="53"]
54 [label="54"]
55 [label="55"]
56 [label="56"]
57 [label="57"]
58 [label="58"]
59 [label="59"]
60 [label="60"]
61 [label="61"]
62 [label="62"]
63 [label="63"]
64 [label="64"]
65 [label="65"]
66 [label="66"]
67 [label="67"]
68 [label="68"]
69 [label="69"]
70 [label="70"]
71 [label="71"]
72 [label="72"]
73 [label="73"]
74 [label="74"]
75 [label="75"]
76 [label="76"]
77 [label="77"]
78 [label="78"]
79 [label="79"]
80 [label="80"]
81 [label="81"]
82 [label="82"]
83 [label="83"]
84 [label="84"]
85 [label="85"]
86 [label="86"]
87 [label="87"]
88 [label="88"]
89 [label="89"]
90 [label="90"]
91 [label="91"]
92 [label="92"]
93 [label="93"]
94 [label="94"]
95 [label="95"]
96 [label="96"]
97 [label="97"]
98 [label="98"]
99 [label="99"]
100 [label="100"]
101 [label="101"]
102 [label="102"]
}
EOF
......
......@@ -29,6 +29,7 @@
#include <memory>
#include <unordered_map>
#include <functional>
#include <array>
#include "misc/casts.hh"
#include "misc/hash.hh"
......@@ -734,24 +735,45 @@ namespace spot
is.deterministic = val;
}
// This is no default value here on purpose. This way any time we
// add a new property we cannot to update every call to prop_copy().
void prop_copy(const const_tgba_ptr& other,
bool state_based,
bool single_acc,
bool inherently_weak,
bool deterministic)
struct prop_set
{
if (state_based)
bool state_based;
bool single_acc;
bool inherently_weak;
bool deterministic;
static prop_set all()
{
return { true, true, true, true };
}
};
// There is no default value here on purpose. This way any time we
// add a new property we have to update every call to prop_copy().
void prop_copy(const const_tgba_ptr& other, prop_set p)
{
if (p.state_based)
prop_state_based_acc(other->has_state_based_acc());
if (single_acc)
if (p.single_acc)
prop_single_acc_set(other->has_single_acc_set());
if (inherently_weak)
if (p.inherently_weak)
prop_inherently_weak(other->is_inherently_weak());
if (deterministic)
if (p.deterministic)
prop_deterministic(other->is_deterministic());
}
void prop_keep(prop_set p)
{
if (!p.state_based)
prop_state_based_acc(false);
if (!p.single_acc)
prop_single_acc_set(false);
if (!p.inherently_weak)
prop_inherently_weak(false);
if (!p.deterministic)
prop_deterministic(false);
}
};
/// \addtogroup tgba_representation TGBA representations
......
......@@ -186,13 +186,13 @@ namespace spot
{
}
explicit tgba_digraph(const const_tgba_digraph_ptr& other)
explicit tgba_digraph(const const_tgba_digraph_ptr& other, prop_set p)
: tgba(other->get_dict()),
g_(other->g_), init_number_(other->init_number_)
{
copy_acceptance_conditions_of(other);
copy_ap_of(other);
prop_copy(other, true, true, true, true);
prop_copy(other, p);
}
virtual ~tgba_digraph()
......@@ -489,23 +489,26 @@ namespace spot
return std::make_shared<tgba_digraph>(dict);
}
inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut)
inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut,
tgba::prop_set p)
{
return std::make_shared<tgba_digraph>(aut);
return std::make_shared<tgba_digraph>(aut, p);
}
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut)
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut,
tgba::prop_set p)
{
return std::make_shared<tgba_digraph>(aut);
return std::make_shared<tgba_digraph>(aut, p);
}
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut)
inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut,
tgba::prop_set p)
{
auto p = std::dynamic_pointer_cast<const tgba_digraph>(aut);
if (p)
return std::make_shared<tgba_digraph>(p);
auto a = std::dynamic_pointer_cast<const tgba_digraph>(aut);
if (a)
return std::make_shared<tgba_digraph>(a, p);
else
return tgba_dupexp_dfs(aut);
return tgba_dupexp_dfs(aut, p);
}
}
......
......@@ -110,7 +110,7 @@ namespace spot
{
isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref)
{
ref_ = make_tgba_digraph(ref);
ref_ = make_tgba_digraph(ref, {true, true, true, true});
ref_deterministic_ = ref_->is_deterministic();
if (!ref_deterministic_)
{
......@@ -142,7 +142,7 @@ namespace spot
}
}
auto tmp = make_tgba_digraph(aut);
auto tmp = make_tgba_digraph(aut, {true, true, true, true});
spot::canonicalize(tmp);
return *tmp == *ref_;
}
......
......@@ -28,6 +28,12 @@ namespace spot
tgba_digraph_ptr
closure(tgba_digraph_ptr&& a)
{
a->prop_keep({false, // state_based
true, // single_acc
false, // inherently_weak
false, // deterministic
});
unsigned n = a->num_states();
std::vector<unsigned> todo;
std::vector<std::vector<unsigned> > dst2trans(n);
......@@ -90,6 +96,6 @@ namespace spot
tgba_digraph_ptr
closure(const const_tgba_digraph_ptr& a)
{
return closure(make_tgba_digraph(a));
return closure(make_tgba_digraph(a, {true, true, true, true}));
}
}
......@@ -104,12 +104,12 @@ namespace spot
tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut)
{
auto res = make_tgba_digraph(aut);
res->prop_copy(aut,
true, // state based
true, // single acc
true, // inherently_weak
true); // deterministic
auto res = make_tgba_digraph(aut, {
true, // state based
true, // single acc
true, // inherently_weak
true, // deterministic
});
tgba_complete_here(res);
return res;
}
......
......@@ -203,7 +203,7 @@ namespace spot
if (want_sba)
res->prop_state_based_acc();
// Preserve determinism and weakness
res->prop_copy(a, false, false, true, true);
res->prop_copy(a, { false, false, true, true });
// Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can
......
......@@ -281,7 +281,7 @@ namespace spot
return os;
}
dotty_output d(os, options);
auto aut = make_tgba_digraph(g);
auto aut = make_tgba_digraph(g, tgba::prop_set::all());
if (assume_sba)
aut->prop_state_based_acc();
d.print(aut);
......
......@@ -25,12 +25,12 @@ namespace spot
tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_ptr& aut)
{
// Clone the original automaton.
auto res = make_tgba_digraph(aut);
res->prop_copy(aut,
false, // state based
false, // single acc
false, // inherently_weak
false); // deterministic
auto res = make_tgba_digraph(aut,
{ false, // state based
false, // single acc
false, // inherently_weak
false, // deterministic
});
// Copy the old acceptance condition before we replace it.
acc_cond oldacc = aut->acc(); // Copy it!
......@@ -113,13 +113,12 @@ namespace spot
tgba_digraph_ptr dtgba_complement_weak(const const_tgba_ptr& aut)
{
// Clone the original automaton.
auto res = make_tgba_digraph(aut);
res->prop_copy(aut,
true, // state based
true, // single acc
true, // inherently_weak
true); // deterministic
auto res = make_tgba_digraph(aut,
{ true, // state based
true, // single acc
true, // inherently weak
true, // determinisitic
});
scc_info si(res);
// We will modify res in place, and the resulting
......
......@@ -36,12 +36,12 @@ namespace spot
class dupexp_iter: public T
{
public:
dupexp_iter(const const_tgba_ptr& a)
dupexp_iter(const const_tgba_ptr& a, tgba::prop_set p)
: T(a), out_(make_tgba_digraph(a->get_dict()))
{
out_->copy_acceptance_conditions_of(a);
out_->copy_ap_of(a);
out_->prop_copy(a, true, true, true, true);
out_->prop_copy(a, p);
}
tgba_digraph_ptr
......@@ -77,8 +77,9 @@ namespace spot
{
public:
dupexp_iter_save(