Commit 6bfa9793 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

translate: improve handling of Xor and Equiv at top-level for -G -D

* spot/tl/formula.hh: Add variant of formula::is that support 4
arguments.
* spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
to preserve Xor and Equiv at the top-level.
* spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
Equiv for the -D -G case.
* NEWS: Mention that.
* tests/core/ltl2tgba2.test: Add test case.
* tests/python/simstate.py: Adjust expected result.
parent 3ab2dd17
Pipeline #18927 passed with stage
in 86 minutes
New in spot 2.9.0.dev (not yet released)
Command-line tools:
- 'ltl2tgba -G -D' is now better at handling formulas that use
'<->' and 'xor' operators at the top level. For instance
ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe'
now produces a 16-state automaton (instead of 31 in Spot 2.9).
Library:
- product_xor() and product_xnor() are two new versions of the
......@@ -8,6 +15,11 @@ New in spot 2.9.0.dev (not yet released)
respectively the symmetric difference of the operands, and the
complement of that.
- tl_simplifier_options::keep_top_xor is a new option to keep Xor
and Equiv operator that appear at the top of LTL formulas (maybe
below other Boolean or X operators). This is used by the
spot::translator class when creating deterministic automata with
generic acceptance.
New in spot 2.9 (2020-04-30)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -186,18 +186,27 @@ namespace spot
std::string kindstr() const;
/// \see formula::is
/// @{
bool is(op o) const
{
return op_ == o;
}
/// \see formula::is
bool is(op o1, op o2) const
{
return op_ == o1 || op_ == o2;
}
/// \see formula::is
bool is(op o1, op o2, op o3) const
{
return op_ == o1 || op_ == o2 || op_ == o3;
}
bool is(op o1, op o2, op o3, op o4) const
{
return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
}
bool is(std::initializer_list<op> l) const
{
const fnode* n = this;
......@@ -209,6 +218,7 @@ namespace spot
}
return true;
}
/// @}
/// \see formula::get_child_of
const fnode* get_child_of(op o) const
......@@ -1333,6 +1343,19 @@ namespace spot
return ptr_->is(o1, o2);
}
/// Return true if the formula is of kind \a o1 or \a o2 or \a o3
bool is(op o1, op o2, op o3) const
{
return ptr_->is(o1, o2, o3);
}
/// Return true if the formula is of kind \a o1 or \a o2 or \a o3
/// or \a a4.
bool is(op o1, op o2, op o3, op o4) const
{
return ptr_->is(o1, o2, o3, o4);
}
/// Return true if the formulas nests all the operators in \a l.
bool is(std::initializer_list<op> l) const
{
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011-2019 Laboratoire de Recherche et Developpement
// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -417,22 +417,25 @@ namespace spot
//////////////////////////////////////////////////////////////////////
formula
nenoform_rec(formula f, bool negated, tl_simplifier_cache* c);
nenoform_rec(formula f, bool negated, tl_simplifier_cache* c,
bool deep);
formula equiv_or_xor(bool equiv, formula f1, formula f2,
tl_simplifier_cache* c)
tl_simplifier_cache* c, bool deep)
{
auto rec = [c](formula f, bool negated)
auto rec = [c, deep](formula f, bool negated)
{
return nenoform_rec(f, negated, c);
return nenoform_rec(f, negated, c, deep);
};
if (equiv)
{
// Rewrite a<=>b as (a&b)|(!a&!b)
auto recurse_f1_true = rec(f1, true);
auto recurse_f1_false = rec(f1, false);
auto recurse_f2_true = rec(f2, true);
if (!deep && c->options.keep_top_xor)
return formula::Equiv(recurse_f1_true, recurse_f2_true);
auto recurse_f1_false = rec(f1, false);
auto recurse_f2_false = rec(f2, false);
auto left = formula::And({recurse_f1_false, recurse_f2_false});
auto right = formula::And({recurse_f1_true, recurse_f2_true});
......@@ -442,8 +445,10 @@ namespace spot
{
// Rewrite a^b as (a&!b)|(!a&b)
auto recurse_f1_true = rec(f1, true);
auto recurse_f1_false = rec(f1, false);
auto recurse_f2_true = rec(f2, true);
if (!deep && c->options.keep_top_xor)
return formula::Xor(recurse_f1_true, recurse_f2_true);
auto recurse_f1_false = rec(f1, false);
auto recurse_f2_false = rec(f2, false);
auto left = formula::And({recurse_f1_false, recurse_f2_true});
auto right = formula::And({recurse_f1_true, recurse_f2_false});
......@@ -451,8 +456,11 @@ namespace spot
}
}
// The deep argument indicate whether we are under a temporal
// operator (except X).
formula
nenoform_rec(formula f, bool negated, tl_simplifier_cache* c)
nenoform_rec(formula f, bool negated, tl_simplifier_cache* c,
bool deep)
{
if (f.is(op::Not))
{
......@@ -474,9 +482,9 @@ namespace spot
}
else
{
auto rec = [c](formula f, bool neg)
auto rec = [c, &deep](formula f, bool neg)
{
return nenoform_rec(f, neg, c);
return nenoform_rec(f, neg, c, deep);
};
switch (op o = f.kind())
......@@ -504,21 +512,25 @@ namespace spot
break;
case op::F:
// !Fa == G!a
deep = true;
result = formula::unop(negated ? op::G : op::F,
rec(f[0], negated));
break;
case op::G:
// !Ga == F!a
deep = true;
result = formula::unop(negated ? op::F : op::G,
rec(f[0], negated));
break;
case op::Closure:
deep = true;
result = formula::unop(negated ?
op::NegClosure : op::Closure,
rec(f[0], false));
break;
case op::NegClosure:
case op::NegClosureMarked:
deep = true;
result = formula::unop(negated ? op::Closure : o,
rec(f[0], false));
break;
......@@ -539,17 +551,18 @@ namespace spot
case op::Xor:
{
// !(a ^ b) == a <=> b
result = equiv_or_xor(negated, f[0], f[1], c);
result = equiv_or_xor(negated, f[0], f[1], c, deep);
break;
}
case op::Equiv:
{
// !(a <=> b) == a ^ b
result = equiv_or_xor(!negated, f[0], f[1], c);
result = equiv_or_xor(!negated, f[0], f[1], c, deep);
break;
}
case op::U:
{
deep = true;
// !(a U b) == !a R !b
auto f1 = rec(f[0], negated);
auto f2 = rec(f[1], negated);
......@@ -558,6 +571,7 @@ namespace spot
}
case op::R:
{
deep = true;
// !(a R b) == !a U !b
auto f1 = rec(f[0], negated);
auto f2 = rec(f[1], negated);
......@@ -566,6 +580,7 @@ namespace spot
}
case op::W:
{
deep = true;
// !(a W b) == !a M !b
auto f1 = rec(f[0], negated);
auto f2 = rec(f[1], negated);
......@@ -574,6 +589,7 @@ namespace spot
}
case op::M:
{
deep = true;
// !(a M b) == !a W !b
auto f1 = rec(f[0], negated);
auto f2 = rec(f[1], negated);
......@@ -604,15 +620,16 @@ namespace spot
// !(a*) etc. should never occur.
{
assert(!negated);
result = f.map([c](formula f)
result = f.map([c, deep](formula f)
{
return nenoform_rec(f, false, c);
return nenoform_rec(f, false, c, deep);
});
break;
}
case op::EConcat:
case op::EConcatMarked:
{
deep = true;
// !(a <>-> b) == a[]-> !b
auto f1 = f[0];
auto f2 = f[1];
......@@ -622,6 +639,7 @@ namespace spot
}
case op::UConcat:
{
deep = true;
// !(a []-> b) == a<>-> !b
auto f1 = f[0];
auto f2 = f[1];
......@@ -4048,9 +4066,9 @@ namespace spot
if (f2.is_sere_formula() && !f2.is_boolean())
return false;
if (right)
f2 = nenoform_rec(f2, true, this);
f2 = nenoform_rec(f2, true, this, false);
else
f1 = nenoform_rec(f1, true, this);
f1 = nenoform_rec(f1, true, this, false);
return syntactic_implication(f1, f2);
}
......@@ -4085,7 +4103,7 @@ namespace spot
formula
tl_simplifier::negative_normal_form(formula f, bool negated)
{
return nenoform_rec(f, negated, cache_);
return nenoform_rec(f, negated, cache_, false);
}
bool
......
// -*- coding: utf-8 -*-
// Copyright (C) 2011-2017, 2019 Laboratoire de Recherche et Developpement
// Copyright (C) 2011-2017, 2019, 2020 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -30,14 +30,15 @@ namespace spot
{
public:
tl_simplifier_options(bool basics = true,
bool synt_impl = true,
bool event_univ = true,
bool containment_checks = false,
bool containment_checks_stronger = false,
bool nenoform_stop_on_boolean = false,
bool reduce_size_strictly = false,
bool boolean_to_isop = false,
bool favor_event_univ = false)
bool synt_impl = true,
bool event_univ = true,
bool containment_checks = false,
bool containment_checks_stronger = false,
bool nenoform_stop_on_boolean = false,
bool reduce_size_strictly = false,
bool boolean_to_isop = false,
bool favor_event_univ = false,
bool keep_top_xor = false)
: reduce_basics(basics),
synt_impl(synt_impl),
event_univ(event_univ),
......@@ -46,7 +47,8 @@ namespace spot
nenoform_stop_on_boolean(nenoform_stop_on_boolean),
reduce_size_strictly(reduce_size_strictly),
boolean_to_isop(boolean_to_isop),
favor_event_univ(favor_event_univ)
favor_event_univ(favor_event_univ),
keep_top_xor(keep_top_xor)
{
}
......@@ -87,6 +89,10 @@ namespace spot
bool boolean_to_isop;
// Try to isolate subformulae that are eventual and universal.
bool favor_event_univ;
// Keep Xor and Equiv at the top of the formula, possibly under
// &,|, and X operators. Only rewrite Xor and Equiv under
// temporal operators.
bool keep_top_xor;
};
// fwd declaration to hide technical details.
......
......@@ -108,6 +108,8 @@ namespace spot
}
if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
options.favor_event_univ = true;
if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
options.keep_top_xor = true;
simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
}
......@@ -167,15 +169,16 @@ 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,
op::Xor, op::Equiv) ||
// For TGBA/BA we only do conjunction. There is nothing wrong
// with disjunction, but it seems to generate 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)))
(!r2.is(op::And) && (type_ == TGBA || type_ == BA)))
goto nosplit;
bool is_and = r2.is(op::And);
op topop = r2.kind();
// Let's classify subformulas.
std::vector<formula> oblg;
std::vector<formula> susp;
......@@ -270,10 +273,16 @@ namespace spot
twa_graph_ptr rest_aut = transrun(rest_f);
if (aut == nullptr)
aut = rest_aut;
else if (is_and)
else if (topop == op::And)
aut = product(aut, rest_aut);
else
else if (topop == op::Or)
aut = product_or(aut, rest_aut);
else if (topop == op::Xor)
aut = product_xor(aut, rest_aut);
else if (topop == op::Equiv)
aut = product_xnor(aut, rest_aut);
else
SPOT_UNREACHABLE();
}
if (!susp.empty())
{
......@@ -285,10 +294,16 @@ namespace spot
twa_graph_ptr one = transrun(f);
if (!susp_aut)
susp_aut = one;
else if (is_and)
else if (topop == op::And)
susp_aut = product(susp_aut, one);
else
else if (topop == op::Or)
susp_aut = product_or(susp_aut, one);
else if (topop == op::Xor)
susp_aut = product_xor(susp_aut, one);
else if (topop == op::Equiv)
susp_aut = product_xnor(susp_aut, one);
else
SPOT_UNREACHABLE();
}
if (susp_aut->prop_universal().is_true())
{
......@@ -311,10 +326,14 @@ namespace spot
}
if (aut == nullptr)
aut = susp_aut;
else if (is_and)
else if (topop == op::And)
aut = product_susp(aut, susp_aut);
else
else if (topop == op::Or)
aut = product_or_susp(aut, susp_aut);
else if (topop == op::Xor) // No suspension here
aut = product_xor(aut, susp_aut);
else if (topop == op::Equiv) // No suspension here
aut = product_xnor(aut, susp_aut);
//if (aut && susp_aut)
// {
// print_hoa(std::cerr << "AUT\n", aut) << '\n';
......
......@@ -451,4 +451,11 @@ f='(GFp0 | FGp1) & (GF!p1 | FGp2) & (GF!p2 | FG!p0)'
test 1,8,3 = `ltl2tgba -G -D "$f" --stats=%s,%e,%a`
test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a`
# Handling of Xor and <-> by ltl-split and -D -G.
res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) <-> GFe)' --stats='%s %g'`
test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
:
......@@ -178,13 +178,13 @@ b.copy_state_names_from(a)
assert b.to_str() == """HOA: v1
States: 1
Start: 0
AP: 2 "p0" "p1"
AP: 2 "p1" "p0"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0 "[1,7]"
[!1] 0 {0}
[1] 0
[!0] 0 {0}
[0] 0
--END--"""
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment