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

translate: enable a restricted form of ltl-split for TGBA/BA

Fixes #267

* spot/twaalgos/gfguarantee.cc: Fix a typo when comparing automata
sizes.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Use
ltl-split even for BA/TGBA, but only of conjunctions with GF(..)
in those cases.
* tests/core/ltl2tgba2.test: Adjust and add the example of #267.
* tests/core/degenid.test, tests/core/parity2.test,
tests/core/stutter-tgba.test, tests/python/automata.ipynb,
tests/python/highlighting.ipynb, tests/python/stutter-inv.ipynb,
bin/spot-x.cc: Adjust.
parent 4235b007
Pipeline #2646 passed with stages
in 155 minutes and 4 seconds
......@@ -46,8 +46,7 @@ more rules based on automata-based implication checks. The default value \
depends on the --low/--medium/--high settings.") },
{ nullptr, 0, nullptr, 0, "Translation options:", 0 },
{ DOC("ltl-split", "Set to 0 to disable the translation of automata \
as product or sum of subformulas. This is currently used only when \
building automata with generic acceptance conditions.") },
as product or sum of subformulas.") },
{ DOC("comp-susp", "Set to 1 to enable compositional suspension, \
as described in our SPIN'13 paper (see Bibliography below). Set to 2, \
to build only the skeleton TGBA without composing it. Set to 0 (the \
......
......@@ -418,7 +418,7 @@ namespace spot
if (!is_terminal_automaton(aut, &si2, true))
return reduced;
do_g_f_terminal_inplace(si2, state_based);
if (aut->num_states() <= reduced->num_states())
if (aut->num_states() < reduced->num_states())
return aut;
}
return reduced;
......
......@@ -105,7 +105,8 @@ namespace spot
simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
}
twa_graph_ptr translator::run(formula* f)
twa_graph_ptr translator::run_aux(formula r)
{
#define PREF_ (pref_ & (Small | Deterministic))
......@@ -118,49 +119,6 @@ namespace spot
set_pref(pref_ | postprocessor::Deterministic);
}
// Do we want to relabel Boolean subformulas?
// If we have a huge formula such as
// (a1 & a2 & ... & an) U (b1 | b2 | ... | bm)
// then it is more efficient to translate
// a U b
// and then fix the automaton. We use relabel_bse() to find
// sub-formulas that are Boolean but do not have common terms.
//
// This rewriting is enabled only if the formula
// 1) has some Boolean subformula
// 2) has more than relabel_bool_ atomic propositions (the default
// is 4, but this can be changed)
// 3) relabel_bse() actually reduces the number of atomic
// propositions.
relabeling_map m;
formula to_work_on = *f;
if (relabel_bool_ > 0)
{
bool has_boolean_sub = false; // that is not atomic
std::set<formula> aps;
to_work_on.traverse([&](const formula& f)
{
if (f.is(op::ap))
aps.insert(f);
else if (f.is_boolean())
has_boolean_sub = true;
return false;
});
unsigned atomic_props = aps.size();
if (has_boolean_sub && (atomic_props >= (unsigned) relabel_bool_))
{
formula relabeled = relabel_bse(to_work_on, Pnn, &m);
if (m.size() < atomic_props)
to_work_on = relabeled;
else
m.clear();
}
}
formula r = simpl_->simplify(to_work_on);
if (to_work_on == *f)
*f = r;
// This helps ltl_to_tgba_fm() to order BDD variables in a more
// natural way (improving the degeneralization).
simpl_->clear_as_bdd_cache();
......@@ -168,8 +126,7 @@ namespace spot
twa_graph_ptr aut;
twa_graph_ptr aut2 = nullptr;
if (ltl_split_ && (type_ == Generic
|| (type_ & Parity)) && !r.is_syntactic_obligation())
if (ltl_split_ && !r.is_syntactic_obligation())
{
formula r2 = r;
unsigned leading_x = 0;
......@@ -178,11 +135,11 @@ namespace spot
r2 = r2[0];
++leading_x;
}
if (type_ == Generic)
if (type_ == Generic || type_ == TGBA)
{
// F(q|u|f) = q|F(u)|F(f)
// F(q|u|f) = q|F(u)|F(f) only for generic acceptance
// G(q&e&f) = q&G(e)&G(f)
bool want_u = r2.is({op::F, op::Or});
bool want_u = r2.is({op::F, op::Or}) && (type_ == Generic);
if (want_u || r2.is({op::G, op::And}))
{
std::vector<formula> susp;
......@@ -204,7 +161,12 @@ namespace spot
r2 = formula::multop(op2, susp);
}
}
if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or))
if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or) ||
// For TGBA/BA we only do conjunction. There is nothing wrong
// with disjunction, but it seems to generated larger automata
// in many cases and it needs to be further investigated. Maybe
// this could be relaxed in the case of deterministic output.
(r2.is(op::Or) && (type_ == TGBA || type_ == BA)))
goto nosplit;
bool is_and = r2.is(op::And);
......@@ -212,16 +174,38 @@ namespace spot
std::vector<formula> oblg;
std::vector<formula> susp;
std::vector<formula> rest;
bool want_g = type_ == TGBA || type_ == BA;
for (formula child: r2)
{
if (child.is_syntactic_obligation())
oblg.push_back(child);
else if (child.is_eventual() && child.is_universal()
&& (type_ == Generic))
&& (!want_g || child.is(op::G)))
susp.push_back(child);
else
rest.push_back(child);
}
if (!susp.empty())
{
// The only cases where we accept susp and rest to be both
// non-empty is when doing arbitrary acceptance, or when doing
// Generic or TGBA.
if (!rest.empty() && !(type_ == Generic || type_ == TGBA))
{
rest.insert(rest.end(), susp.begin(), susp.end());
susp.clear();
}
// For Parity, we want to translate all suspendable
// formulas at once.
if (rest.empty() && type_ & Parity)
susp = { formula::multop(r2.kind(), susp) };
}
// For TGBA and BA, we only split if there is something to
// suspend.
if (susp.empty() && (type_ == TGBA || type_ == BA))
goto nosplit;
option_map om;
if (opt_)
om = *opt_;
......@@ -238,34 +222,26 @@ namespace spot
return run(f);
};
// std::cerr << "splitting\n";
aut = nullptr;
// All obligations can be converted into a minimal WDBA.
if (!oblg.empty())
{
formula oblg_f = formula::multop(r2.kind(), oblg);
//std::cerr << "oblg: " << oblg_f << '\n';
aut = transrun(oblg_f);
}
if (!rest.empty())
{
formula rest_f = formula::multop(r2.kind(), rest);
// In case type_ is Parity, all suspendable formulas have
// been put into rest_f. But if the entire rest_f is
// suspendable, we want to handle it like so.
if (rest_f.is_eventual() && rest_f.is_universal())
{
assert(susp.empty());
susp.push_back(rest_f);
}
//std::cerr << "rest: " << rest_f << '\n';
twa_graph_ptr rest_aut = transrun(rest_f);
if (aut == nullptr)
aut = rest_aut;
else if (is_and)
aut = product(aut, rest_aut);
else
{
twa_graph_ptr rest_aut = transrun(rest_f);
if (aut == nullptr)
aut = rest_aut;
else if (is_and)
aut = product(aut, rest_aut);
else
aut = product_or(aut, rest_aut);
}
aut = product_or(aut, rest_aut);
}
if (!susp.empty())
{
......@@ -273,6 +249,7 @@ namespace spot
// Each suspendable formula separately
for (formula f: susp)
{
//std::cerr << "susp: " << f << '\n';
twa_graph_ptr one = transrun(f);
if (!susp_aut)
susp_aut = one;
......@@ -370,6 +347,56 @@ namespace spot
aut = std::move(aut2);
}
return aut;
}
twa_graph_ptr translator::run(formula* f)
{
// Do we want to relabel Boolean subformulas?
// If we have a huge formula such as
// (a1 & a2 & ... & an) U (b1 | b2 | ... | bm)
// then it is more efficient to translate
// a U b
// and then fix the automaton. We use relabel_bse() to find
// sub-formulas that are Boolean but do not have common terms.
//
// This rewriting is enabled only if the formula
// 1) has some Boolean subformula
// 2) has more than relabel_bool_ atomic propositions (the default
// is 4, but this can be changed)
// 3) relabel_bse() actually reduces the number of atomic
// propositions.
relabeling_map m;
formula to_work_on = *f;
if (relabel_bool_ > 0)
{
bool has_boolean_sub = false; // that is not atomic
std::set<formula> aps;
to_work_on.traverse([&](const formula& f)
{
if (f.is(op::ap))
aps.insert(f);
else if (f.is_boolean())
has_boolean_sub = true;
return false;
});
unsigned atomic_props = aps.size();
if (has_boolean_sub && (atomic_props >= (unsigned) relabel_bool_))
{
formula relabeled = relabel_bse(to_work_on, Pnn, &m);
if (m.size() < atomic_props)
to_work_on = relabeled;
else
m.clear();
}
}
formula r = simpl_->simplify(to_work_on);
if (to_work_on == *f)
*f = r;
auto aut = run_aux(r);
if (!m.empty())
relabel_here(aut, &m);
return aut;
......
......@@ -138,6 +138,7 @@ namespace spot
protected:
void setup_opt(const option_map* opt);
void build_simplifier(const bdd_dict_ptr& dict);
twa_graph_ptr run_aux(formula f);
private:
tl_simplifier* simpl_;
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2011, 2013, 2014, 2015, 2017 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
# Copyright (C) 2011, 2013, 2014, 2015, 2017, 2018 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -239,7 +239,9 @@ properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant
--BODY--
State: 0
[0] 1
[0&1&2] 1
[0&!2] 2
[0&!1&2] 3
State: 1 {0}
[1&2] 1
[!2] 2
......
......@@ -362,12 +362,14 @@ EOF
diff output expected
# These four formulas appear in a NEWS entry for Spot 2.6
# The first four formulas appear in a NEWS entry for Spot 2.6
# The 5th one is from issue #267.
cat >formulas <<EOF
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30
GF(((a & Xb) | XXc) & Xd), 4,60, 4,64, 4,68, 5,80
GF(((a & Xb) | XXc) & Xd), 4,64, 4,64, 5,80, 5,80
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12
G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8
EOF
ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
......
......@@ -426,7 +426,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 6
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: Buchi
......@@ -435,23 +435,21 @@ properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 0
[t] 2
[0&1&2] 3
[!0] 1
[0&1&2] 2
State: 1
[2] 4
State: 2
[t] 3
[1&2] 4
[t] 5
State: 2
[!0] 1
[0&!1&2] 2
[0&1&2] 2 {0}
State: 3
[2] 1
[0&!1&2] 3
[0&1&2] 3 {0}
[0] 3
[0&1&2] 4
State: 4
[0&!1&2] 4
[0&1&2] 4 {0}
State: 5
[0&1&2] 4
[0] 5
--END--
HOA: v1
name: "FGa"
......@@ -489,7 +487,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 6
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: Rabin 1
......@@ -498,23 +496,21 @@ properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 0
[t] 2
[0&1&2] 3
[!0] 1
[0&1&2] 2
State: 1
[2] 4
State: 2
[t] 3
[1&2] 4
[t] 5
State: 2
[!0] 1
[0&!1&2] 2
[0&1&2] 2 {1}
State: 3
[2] 1
[0&!1&2] 3
[0&1&2] 3 {1}
[0] 3
[0&1&2] 4
State: 4
[0&!1&2] 4
[0&1&2] 4 {1}
State: 5
[0&1&2] 4
[0] 5
--END--
HOA: v1
name: "FGa"
......@@ -552,7 +548,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 6
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: Buchi
......@@ -561,23 +557,21 @@ properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 0
[t] 2
[0&1&2] 3
[!0] 1
[0&1&2] 2
State: 1
[2] 4
State: 2
[t] 3
[1&2] 4
[t] 5
State: 2
[!0] 1
[0&!1&2] 2
[0&1&2] 2 {0}
State: 3
[2] 1
[0&!1&2] 3
[0&1&2] 3 {0}
[0] 3
[0&1&2] 4
State: 4
[0&!1&2] 4
[0&1&2] 4 {0}
State: 5
[0&1&2] 4
[0] 5
--END--
HOA: v1
name: "FGa"
......@@ -615,7 +609,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 6
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: Streett 1
......@@ -624,23 +618,21 @@ properties: trans-labels explicit-labels trans-acc colored
--BODY--
State: 0
[0] 0 {0}
[t] 2 {0}
[0&1&2] 3 {0}
[!0] 1 {0}
[0&1&2] 2 {0}
State: 1
[2] 4 {0}
State: 2
[t] 3 {0}
[1&2] 4 {0}
[t] 5 {0}
State: 2
[!0] 1 {0}
[0&!1&2] 2 {0}
[0&1&2] 2 {1}
State: 3
[2] 1 {0}
[0&!1&2] 3 {0}
[0&1&2] 3 {1}
[0] 3 {0}
[0&1&2] 4 {0}
State: 4
[0&!1&2] 4 {0}
[0&1&2] 4 {1}
State: 5
[0&1&2] 4 {0}
[0] 5 {0}
--END--
HOA: v1
name: "FGa"
......@@ -678,7 +670,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 6
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: parity min odd 3
......@@ -687,23 +679,21 @@ properties: trans-labels explicit-labels trans-acc colored
--BODY--
State: 0
[0] 0 {2}
[t] 2 {2}
[0&1&2] 3 {2}
[!0] 1 {2}
[0&1&2] 2 {2}
State: 1
[2] 4 {2}
State: 2
[t] 3 {2}
[1&2] 4 {2}
[t] 5 {2}
State: 2
[!0] 1 {2}
[0&!1&2] 2 {2}
[0&1&2] 2 {1}
State: 3
[2] 1 {2}
[0&!1&2] 3 {2}
[0&1&2] 3 {1}
[0] 3 {2}
[0&1&2] 4 {2}
State: 4
[0&!1&2] 4 {2}
[0&1&2] 4 {1}
State: 5
[0&1&2] 4 {2}
[0] 5 {2}
--END--
HOA: v1
name: "FGa"
......@@ -741,7 +731,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 6
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: parity max even 3
......@@ -750,23 +740,21 @@ properties: trans-labels explicit-labels trans-acc colored
--BODY--
State: 0
[0] 0 {1}
[t] 2 {1}
[0&1&2] 3 {1}
[!0] 1 {1}
[0&1&2] 2 {1}
State: 1
[2] 4 {1}
State: 2
[t] 3 {1}
[1&2] 4 {1}
[t] 5 {1}
State: 2
[!0] 1 {1}
[0&!1&2] 2 {1}
[0&1&2] 2 {2}
State: 3
[2] 1 {1}
[0&!1&2] 3 {1}
[0&1&2] 3 {2}
[0] 3 {1}
[0&1&2] 4 {1}
State: 4
[0&!1&2] 4 {1}
[0&1&2] 4 {2}
State: 5
[0&1&2] 4 {1}
[0] 5 {1}
--END--
EOF
diff expected2 res2
......@@ -1182,7 +1170,7 @@ State: 1
--END--
HOA: v1
name: "(p0 W XXGp0) & G(Fp1 & FGp2)"
States: 10
States: 5
Start: 0
AP: 3 "p0" "p1" "p2"
acc-name: Rabin 1
......@@ -1190,46 +1178,24 @@ Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0&!1 | 0&!2] 0
[!0] 1
[0&!1 | 0&!2] 2
[0&1&2] 3
[0&1&2] 2
State: 1
[!1 | !2] 4
[1&2] 5
[!1 | !2] 3
[1&2] 4
State: 2
[!0&!1 | !0&!2] 1
[0&!1 | 0&!2] 2
[0&1&2] 3
[!0&1&2] 6
[0&!2] 0 {0}
[!0] 1
[0&!1&2] 2
[0&1&2] 2 {1}
State: 3
[!0&!2] 1
[0&!2] 2 {0}
[!0&!1&2] 7
[!0&1&2] 8
[0&!1&2] 9
[0&1&2] 9 {1}
[0&!1 | 0&!2] 3
[0&1&2] 4
State: 4
[0&!1 | 0&!2] 4
[0&1&2] 5
State: 5
[0&!2] 4 {0}
[0&!1&2] 5
[0&1&2] 5 {1}
State: 6
[!0&!1 | !2] 4
[0&2 | 1&2] 5