Commit 1f0bb428 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

add a stutter-invariant property to automata

... and show it in the HOA output.  Fixes #60.

* src/tgba/tgba.hh: Add is_stutter_invariant().
* src/tgbaalgos/hoa.cc: Print stutter-invariant
and inherently-weak.
* src/tgbaalgos/ltl2tgba_fm.cc: Set both.
* src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/complete.cc,
src/tgbaalgos/degen.cc, src/tgbaalgos/dtgbacomp.cc,
src/tgbaalgos/mask.cc, src/tgbaalgos/minimize.cc,
src/tgbaalgos/remfin.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/stutter.cc,
src/tgbatest/hoaparse.test, src/tgbatest/ltldo.test,
src/tgbatest/monitor.test, src/tgbatest/randomize.test,
src/tgbatest/remfin.test, src/tgbatest/sbacc.test: Adjust.
parent 566118a5
...@@ -675,6 +675,7 @@ namespace spot ...@@ -675,6 +675,7 @@ namespace spot
bool state_based_acc:1; // State-based acceptance. bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Weak automaton. bool inherently_weak:1; // Weak automaton.
bool deterministic:1; // Deterministic automaton. bool deterministic:1; // Deterministic automaton.
bool stutter_inv:1; // Stutter invariant
}; };
union union
{ {
...@@ -757,16 +758,27 @@ namespace spot ...@@ -757,16 +758,27 @@ namespace spot
is.deterministic = val; is.deterministic = val;
} }
bool is_stutter_invariant() const
{
return is.stutter_inv;
}
void prop_stutter_invariant(bool val = true)
{
is.stutter_inv = val;
}
struct prop_set struct prop_set
{ {
bool state_based; bool state_based;
bool single_acc; bool single_acc;
bool inherently_weak; bool inherently_weak;
bool deterministic; bool deterministic;
bool stutter_inv;
static prop_set all() static prop_set all()
{ {
return { true, true, true, true }; return { true, true, true, true, true };
} }
}; };
...@@ -782,6 +794,8 @@ namespace spot ...@@ -782,6 +794,8 @@ namespace spot
prop_inherently_weak(other->is_inherently_weak()); prop_inherently_weak(other->is_inherently_weak());
if (p.deterministic) if (p.deterministic)
prop_deterministic(other->is_deterministic()); prop_deterministic(other->is_deterministic());
if (p.stutter_inv)
prop_stutter_invariant(other->is_stutter_invariant());
} }
void prop_keep(prop_set p) void prop_keep(prop_set p)
......
...@@ -112,7 +112,7 @@ namespace spot ...@@ -112,7 +112,7 @@ namespace spot
{ {
isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref) isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref)
{ {
ref_ = make_tgba_digraph(ref, {true, true, true, true}); ref_ = make_tgba_digraph(ref, tgba::prop_set::all());
ref_deterministic_ = ref_->is_deterministic(); ref_deterministic_ = ref_->is_deterministic();
if (!ref_deterministic_) if (!ref_deterministic_)
{ {
...@@ -144,7 +144,7 @@ namespace spot ...@@ -144,7 +144,7 @@ namespace spot
} }
} }
auto tmp = make_tgba_digraph(aut, {true, true, true, true}); auto tmp = make_tgba_digraph(aut, tgba::prop_set::all());
spot::canonicalize(tmp); spot::canonicalize(tmp);
return *tmp == *ref_; return *tmp == *ref_;
} }
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// de l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -105,11 +105,12 @@ namespace spot ...@@ -105,11 +105,12 @@ namespace spot
tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut) tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut)
{ {
auto res = make_tgba_digraph(aut, { auto res = make_tgba_digraph(aut, {
true, // state based true, // state based
true, // single acc true, // single acc
true, // inherently_weak true, // inherently_weak
true, // deterministic true, // deterministic
}); true, // stutter inv.
});
tgba_complete_here(res); tgba_complete_here(res);
return res; return res;
} }
......
...@@ -204,8 +204,8 @@ namespace spot ...@@ -204,8 +204,8 @@ namespace spot
res->set_single_acceptance_set(); res->set_single_acceptance_set();
if (want_sba) if (want_sba)
res->prop_state_based_acc(); res->prop_state_based_acc();
// Preserve determinism and weakness // Preserve determinism, weakness, and stutter-invariance
res->prop_copy(a, { false, false, true, true }); res->prop_copy(a, { false, false, true, true, true });
// Create an order of acceptance conditions. Each entry in this // Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can // vector correspond to an acceptance set. Each index can
......
...@@ -32,6 +32,7 @@ namespace spot ...@@ -32,6 +32,7 @@ namespace spot
false, // single acc false, // single acc
false, // inherently_weak false, // inherently_weak
false, // deterministic false, // deterministic
true, // stutter inv.
}); });
// Copy the old acceptance condition before we replace it. // Copy the old acceptance condition before we replace it.
acc_cond oldacc = aut->acc(); // Copy it! acc_cond oldacc = aut->acc(); // Copy it!
...@@ -120,6 +121,7 @@ namespace spot ...@@ -120,6 +121,7 @@ namespace spot
true, // single acc true, // single acc
true, // inherently weak true, // inherently weak
true, // determinisitic true, // determinisitic
true, // stutter inv.
}); });
scc_info si(res); scc_info si(res);
......
...@@ -22,6 +22,7 @@ ...@@ -22,6 +22,7 @@
#include <ostream> #include <ostream>
#include <sstream> #include <sstream>
#include <cstring>
#include <map> #include <map>
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "tgba/tgbagraph.hh" #include "tgba/tgbagraph.hh"
...@@ -296,19 +297,41 @@ namespace spot ...@@ -296,19 +297,41 @@ namespace spot
os << aut->acc().get_acceptance(); os << aut->acc().get_acceptance();
os << nl; os << nl;
os << "properties:"; os << "properties:";
// Make sure the property line is not too large,
// otherwise our test cases do not fit in 80 columns...
unsigned prop_len = 60;
auto prop = [&](const char* str)
{
if (newline)
{
auto l = strlen(str);
if (prop_len < l)
{
prop_len = 60;
os << "\nproperties:";
}
prop_len -= l;
}
os << str;
};
implicit_labels = md.use_implicit_labels; implicit_labels = md.use_implicit_labels;
if (implicit_labels) if (implicit_labels)
os << " implicit-labels"; prop(" implicit-labels");
else else
os << " trans-labels explicit-labels"; prop(" trans-labels explicit-labels");
if (acceptance == Hoa_Acceptance_States) if (acceptance == Hoa_Acceptance_States)
os << " state-acc"; prop(" state-acc");
else if (acceptance == Hoa_Acceptance_Transitions) else if (acceptance == Hoa_Acceptance_Transitions)
os << " trans-acc"; prop(" trans-acc");
if (md.is_complete) if (md.is_complete)
os << " complete"; prop(" complete");
if (md.is_deterministic) if (md.is_deterministic)
os << " deterministic"; prop(" deterministic");
if (aut->is_stutter_invariant())
prop(" stutter-invariant");
if (aut->is_inherently_weak())
prop(" inherently-weak");
os << nl; os << nl;
// If we want to output implicit labels, we have to // If we want to output implicit labels, we have to
......
...@@ -2514,6 +2514,9 @@ namespace spot ...@@ -2514,6 +2514,9 @@ namespace spot
acc.set_generalized_buchi(); acc.set_generalized_buchi();
a->prop_inherently_weak(f->is_syntactic_persistence());
a->prop_stutter_invariant(f->is_syntactic_stutter_invariant());
if (!simplifier) if (!simplifier)
// This should not be deleted before we have registered all propositions. // This should not be deleted before we have registered all propositions.
delete s; delete s;
......
...@@ -26,7 +26,7 @@ namespace spot ...@@ -26,7 +26,7 @@ namespace spot
{ {
auto res = make_tgba_digraph(in->get_dict()); auto res = make_tgba_digraph(in->get_dict());
res->copy_ap_of(in); res->copy_ap_of(in);
res->prop_copy(in, { true, false, true, true }); res->prop_copy(in, { true, false, true, true, false });
unsigned na = in->acc().num_sets(); unsigned na = in->acc().num_sets();
unsigned tr = to_remove.count(); unsigned tr = to_remove.count();
assert(tr <= na); assert(tr <= na);
...@@ -54,7 +54,7 @@ namespace spot ...@@ -54,7 +54,7 @@ namespace spot
auto res = make_tgba_digraph(in->get_dict()); auto res = make_tgba_digraph(in->get_dict());
res->copy_ap_of(in); res->copy_ap_of(in);
res->prop_copy(in, { true, true, true, true }); res->prop_copy(in, { true, true, true, true, false });
res->copy_acceptance_conditions_of(in); res->copy_acceptance_conditions_of(in);
transform_copy(in, res, [&](unsigned src, transform_copy(in, res, [&](unsigned src,
bdd& cond, bdd& cond,
......
...@@ -485,6 +485,7 @@ namespace spot ...@@ -485,6 +485,7 @@ namespace spot
// final is empty: there is no acceptance condition // final is empty: there is no acceptance condition
build_state_set(det_a, non_final); build_state_set(det_a, non_final);
auto res = minimize_dfa(det_a, final, non_final); auto res = minimize_dfa(det_a, final, non_final);
res->prop_copy(a, { false, false, false, false, true });
res->prop_deterministic(); res->prop_deterministic();
res->prop_inherently_weak(); res->prop_inherently_weak();
res->prop_state_based_acc(); res->prop_state_based_acc();
...@@ -588,6 +589,7 @@ namespace spot ...@@ -588,6 +589,7 @@ namespace spot
} }
auto res = minimize_dfa(det_a, final, non_final); auto res = minimize_dfa(det_a, final, non_final);
res->prop_copy(a, { false, false, false, false, true });
res->prop_deterministic(); res->prop_deterministic();
res->prop_inherently_weak(); res->prop_inherently_weak();
return res; return res;
......
...@@ -262,6 +262,7 @@ namespace spot ...@@ -262,6 +262,7 @@ namespace spot
unsigned nst = aut->num_states(); unsigned nst = aut->num_states();
auto res = make_tgba_digraph(aut->get_dict()); auto res = make_tgba_digraph(aut->get_dict());
res->copy_ap_of(aut); res->copy_ap_of(aut);
res->prop_copy(aut, { false, false, false, false, true });
res->new_states(nst); res->new_states(nst);
res->set_acceptance(aut->acc().num_sets() + extra_sets, new_code); res->set_acceptance(aut->acc().num_sets() + extra_sets, new_code);
res->set_init_state(aut->get_init_state_number()); res->set_init_state(aut->get_init_state_number());
......
...@@ -317,7 +317,7 @@ namespace spot ...@@ -317,7 +317,7 @@ namespace spot
scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si) scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si)
{ {
auto res = scc_filter_apply<state_filter<>>(aut, given_si); auto res = scc_filter_apply<state_filter<>>(aut, given_si);
res->prop_copy(aut, { true, true, true, true }); res->prop_copy(aut, { true, true, true, true, true });
return res; return res;
} }
...@@ -340,6 +340,7 @@ namespace spot ...@@ -340,6 +340,7 @@ namespace spot
true, true,
true, true,
true, true,
true,
}); });
return res; return res;
} }
...@@ -372,6 +373,7 @@ namespace spot ...@@ -372,6 +373,7 @@ namespace spot
true, true,
true, true,
false, // determinism may not be preserved false, // determinism may not be preserved
false, // stutter inv. of suspvars probably altered
}); });
return res; return res;
} }
......
...@@ -635,6 +635,7 @@ namespace spot ...@@ -635,6 +635,7 @@ namespace spot
false, // single acc set by set_generalized_buchi false, // single acc set by set_generalized_buchi
true, // weakness preserved, true, // weakness preserved,
false, // determinism checked and set below false, // determinism checked and set below
true, // stutter inv.
}); });
if (nb_minato == nb_satoneset && !Cosimulation) if (nb_minato == nb_satoneset && !Cosimulation)
res->prop_deterministic(); res->prop_deterministic();
......
...@@ -432,6 +432,7 @@ namespace spot ...@@ -432,6 +432,7 @@ namespace spot
true, // single_acc true, // single_acc
false, // inherently_weak false, // inherently_weak
false, // deterministic false, // deterministic
false, // stutter inv.
}); });
a->merge_transitions(); a->merge_transitions();
return a; return a;
...@@ -452,6 +453,7 @@ namespace spot ...@@ -452,6 +453,7 @@ namespace spot
true, // single_acc true, // single_acc
false, // inherently_weak false, // inherently_weak
false, // deterministic false, // deterministic
false, // stutter inv.
}); });
unsigned n = a->num_states(); unsigned n = a->num_states();
...@@ -516,7 +518,7 @@ namespace spot ...@@ -516,7 +518,7 @@ namespace spot
tgba_digraph_ptr tgba_digraph_ptr
closure(const const_tgba_digraph_ptr& a) closure(const const_tgba_digraph_ptr& a)
{ {
return closure(make_tgba_digraph(a, {true, true, true, true})); return closure(make_tgba_digraph(a, {true, true, true, true, false}));
} }
// The stutter check algorithm to use can be overridden via an // The stutter check algorithm to use can be overridden via an
......
...@@ -267,7 +267,8 @@ Start: 0 ...@@ -267,7 +267,8 @@ Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: generalized-Buchi 2 acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1) Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc complete deterministic properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 "foo" {0} State: 0 "foo" {0}
[!0&!1] 2 [!0&!1] 2
...@@ -483,7 +484,8 @@ Start: 0 ...@@ -483,7 +484,8 @@ Start: 0
AP: 3 "a" "b" "c" AP: 3 "a" "b" "c"
acc-name: generalized-Buchi 2 acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1) Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[!0&!1 | !0&!2] 0 [!0&!1 | !0&!2] 0
...@@ -566,7 +568,8 @@ Start: 0 ...@@ -566,7 +568,8 @@ Start: 0
AP: 1 "a" AP: 1 "a"
acc-name: generalized-Buchi 3 acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2) Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[0] 1 {0 1} [0] 1 {0 1}
...@@ -778,7 +781,8 @@ Start: 0 ...@@ -778,7 +781,8 @@ Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete deterministic properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[1] 1 [1] 1
...@@ -878,7 +882,8 @@ Start: 0 ...@@ -878,7 +882,8 @@ Start: 0
AP: 0 AP: 0
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete deterministic properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[t] 1 [t] 1
...@@ -1033,7 +1038,8 @@ run 2 ../ltl2tgba -XH foob 2>output.err ...@@ -1033,7 +1038,8 @@ run 2 ../ltl2tgba -XH foob 2>output.err
grep 'foob:1.1: Cannot open file foob' output.err grep 'foob:1.1: Cannot open file foob' output.err
# Make sure we can read multiple automata from stdin # Make sure we can read multiple automata from stdin
../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' > input ../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' |
sed 's/ stutter-invariant//;s/ inherently-weak//;/properties:$/d' > input
../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output ../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output
diff input output diff input output
...@@ -1366,7 +1372,8 @@ States: 2 ...@@ -1366,7 +1372,8 @@ States: 2
Start: 0 Start: 0
AP: 1 "a" AP: 1 "a"
Acceptance: 1 t Acceptance: 1 t
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 "F(a)" State: 0 "F(a)"
[0] 1 {0} [0] 1 {0}
...@@ -1379,7 +1386,8 @@ States: 1 ...@@ -1379,7 +1386,8 @@ States: 1
Start: 0 Start: 0
AP: 3 "a" "b" "c" AP: 3 "a" "b" "c"
Acceptance: 6 Inf(0)&Inf(2)&Inf(4)&Inf(5) Acceptance: 6 Inf(0)&Inf(2)&Inf(4)&Inf(5)
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[0&1&2] 0 {0 2 4} [0&1&2] 0 {0 2 4}
...@@ -1412,7 +1420,8 @@ Start: 0 ...@@ -1412,7 +1420,8 @@ Start: 0
AP: 1 "a" AP: 1 "a"
acc-name: all acc-name: all
Acceptance: 0 t Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete deterministic properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 "F(a)" State: 0 "F(a)"
[0] 1 [0] 1
...@@ -1426,7 +1435,8 @@ Start: 0 ...@@ -1426,7 +1435,8 @@ Start: 0
AP: 3 "a" "b" "c" AP: 3 "a" "b" "c"
acc-name: generalized-Buchi 4 acc-name: generalized-Buchi 4
Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3) Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[0&1&2] 0 {0 1 2} [0&1&2] 0 {0 1 2}
...@@ -1444,7 +1454,8 @@ EOF ...@@ -1444,7 +1454,8 @@ EOF
# Implicit labels # Implicit labels
../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' > out.hoa ../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' > out.hoa
../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' > out-i.hoa ../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' |
sed 's/ stutter-invariant//;/properties:$/d' > out-i.hoa
../../bin/autfilt -C -Hi out.hoa --name=%M > out-i2.hoa ../../bin/autfilt -C -Hi out.hoa --name=%M > out-i2.hoa
diff out-i.hoa out-i2.hoa diff out-i.hoa out-i2.hoa
......
...@@ -75,7 +75,8 @@ Start: 0 ...@@ -75,7 +75,8 @@ Start: 0
AP: 1 "_foo_" AP: 1 "_foo_"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[0] 0 {0} [0] 0 {0}
...@@ -95,7 +96,8 @@ Start: 0 ...@@ -95,7 +96,8 @@ Start: 0
AP: 1 "_foo_" AP: 1 "_foo_"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete deterministic properties: trans-labels explicit-labels trans-acc complete
properties: deterministic