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

translate: add ltl-split option

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Build
automata with generic acceptance by doing product of automata for
smaller subformulas.
* bin/spot-x.cc: Mention ltl-split.
* NEWS: Mention the change, and show some results.
* tests/core/genltl.test, tests/python/_product_susp.ipynb,
tests/python/highlighting.ipynb: Adjust test cases.
* doc/org/ltl2tgba.org: Update.
* tests/core/gragsa.test: Add another formula to cover more
code.
parent 4f2e9512
......@@ -87,6 +87,35 @@ New in spot 2.5.3.dev (not yet released)
a "suspendable" automaton B. They are also optimized for
the case that A is weak.
- When 'generic' acceptance is enabled, the translation routine will
split the input formula on Boolean operators into components that
are syntactically 'obligation', 'suspendable', or 'something
else'. Those will be translated separately and combined with
product()/product_susp(). This is inspired by the ways things are
done in ltl2dstar or delag, and can be disabled by passing option
-xltl-split=0, as in ltl2tgba -G -D -xltl-split=0. Here are the
sizes of deterministic automata produced with generic acceptance
using two versions of ltl2tgba and delag for reference.
ltl2tgba -GD rabinizer 4
2.5 2.6 delag
------------- -------------
FGa0&GFb0 5 1 1
(FGa1&GFb1)|FGa0|GFb0 8 1 1
(FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 497 1 1
FGa0|GFb0 2 1 1
(FGa1|GFb1)&FGa0&GFb0 16 1 1
(FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 29 1 1
GFa1 <-> GFz 4 1 1
(GFa1 & GFa2) <-> GFz 8 1 1
(GFa1 & GFa2 & GFa3) <-> GFz 21 1 1
GFa1 -> GFz 5 1 1
(GFa1 & GFa2) -> GFz 12 1 1
(GFa1 & GFa2 & GFa3) -> GFz 41 1 1
FG(a|b)|FG(!a|Xb) 4 2 2
FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 5 4
FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 15 8
- print_dot(), used to print automata in GraphViz's format,
underwent several changes:
......@@ -219,6 +248,13 @@ New in spot 2.5.3.dev (not yet released)
Make sure to quote %L to protect the potential commas:
genltl --format='%F,"%L",%f' ...
- In Spot 2.5 and prior running "ltl2tgba --generic --det" on some
formula would attempt to translate it as deterministic TGBA or
determinize it into an automaton with parity acceptance. Version
2.5 introduced --parity to force parity acceptance on the output.
This version finally gives --generic some more natural semantics:
any acceptance condition can be used.
New in spot 2.5.3 (2018-04-20)
......
......@@ -45,6 +45,9 @@ static const argp_option options[] =
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.") },
{ 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 \
......
......@@ -18,8 +18,8 @@ a quick summary:
- =--ba= (or =-B=) outputs state-based Büchi automata
- =--monitor= (or =-M=) outputs monitors
- =--generic --deterministic= (or =-DG=) will do whatever it takes to
produce a deterministic automaton, and may output generalized Büchi,
or parity acceptance.
produce a deterministic automaton, and may use any acceptance
condition
- =--parity --deterministic= (or =-DP=) will produce a deterministic
automaton with parity acceptance.
......@@ -466,8 +466,7 @@ In particular, for properties more complex than obligations, it is
possible that no deterministic TGBA exist, and even if it exists,
=ltl2tgba= might not find it: so a non-deterministic automaton can be
returned in this case. If you absolutely want a deterministic
automaton, [[#generic][read on about the =--generic= option below]].
automaton, see [[#generic][the =--generic= option]] or [[#parity][the =--parity= option]].
An example formula where the difference between =-D= and =--small= is
flagrant is =Ga|Gb|Gc=:
......@@ -724,9 +723,15 @@ expectations.
:END:
The =--generic= (or =-G=) option allows =ltl2tgba= to use more
complex acceptance. Combined with =--deterministic= (or =-D=) this
allows the use of a determinization algorithm that produces
automata with parity acceptance.
complex acceptance conditions. This is done by splitting the LTL
formulas on Boolean connectives to recognize some subformulas that
are either to translate with different types of acceptance
conditions, and then combining everything back together.
Combined with =--deterministic= (or =-D=) this allows the use of a
determinization algorithm that produces automata with parity
acceptance. This is only used for subformulas for which we do not
know a better way to get a deterministic automaton.
For instance =FGa= is the typical formula for which not
deterministic TGBA exists.
......@@ -743,7 +748,7 @@ ltl2tgba "FGa" -D -d
#+RESULTS:
[[file:ltl2tgba-fga.svg]]
But with =--generic=, =ltl2tgba= will output the following Rabin automaton:
But with =--generic=, =ltl2tgba= will output the following co-Büchi automaton:
#+NAME: ltl2tgba-fga-D
#+BEGIN_SRC sh :results verbatim :exports code
......@@ -757,9 +762,54 @@ ltl2tgba "FGa" -G -D -d
#+RESULTS:
[[file:ltl2tgba-fga-D.svg]]
Note that determinization algorithm implemented actually outputs
parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as
=Rabin 1= or =parity min odd 2=.
If we translate =Fb|Gc= as a deterministic automaton with any
acceptance condition, we get a weak and deterministic Büchi automaton:
#+NAME: ltl2tgba-fbgc-D
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "Fb|Gc" -G -D -d
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-fbgc-D.svg :var txt=ltl2tgba-fbgc-D :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-fbgc-D.svg]]
Finally if we translate the conjunction of these two subformulas, a
product of these two automata will be made, producing:
#+NAME: ltl2tgba-fbgcfga-D
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "(Fb|Gc)&FGa" -G -D -d
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-fbgcfga-D.svg :var txt=ltl2tgba-fbgcfga-D :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-fbgcfga-D.svg]]
Disabling the splitting of the original formula LTL formulas can be
done using option =-x ltl-split=0=. In that case the formula
=(Fb|Gc)&FGa= will be translated into a single TGBA, and because this
TGBA is non-deterministic, it will then be determinized into an
automaton with parity acceptance:
#+NAME: ltl2tgba-fbgcfga-nosplit-D
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "(Fb|Gc)&FGa" -G -D -xltl-split=0 -d
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-fbgcfga-nosplit-D.svg :var txt=ltl2tgba-fbgcfga-nosplit-D :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-fbgcfga-nosplit-D.svg]]
The [[./man/spot-x.7.html][=spot-x=]](7) man page lists a few =-x= options (=det-scc=,
......@@ -785,7 +835,7 @@ would be larger if SCC-based optimizations were disabled:
#+NAME: ltl2tgba-det2
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d
ltl2tgba "F(a W FGb)" -xdet-scc=0 -G -D -d
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results
......@@ -795,11 +845,10 @@ ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d
#+RESULTS:
[[file:ltl2tgba-det2.svg]]
While the =--generic= option currently only builds automata with
generalized-Büchi or parity acceptance, this is very likely to change
in the future.
* Deterministic automata with =--parity --deterministic=
:PROPERTIES:
:CUSTOM_ID: parity
:END:
Using the =--parity= (or upper-case =-P=) option will force the
acceptance condition to be of a parity type. This has to be
......
......@@ -26,6 +26,7 @@
#include <spot/twaalgos/relabel.hh>
#include <spot/twaalgos/gfguarantee.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/product.hh>
namespace spot
{
......@@ -35,7 +36,9 @@ namespace spot
comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
relabel_bool_ = tls_impl_ = -1;
gf_guarantee_ = level_ != Low;
ltl_split_ = true;
opt_ = opt;
if (!opt)
return;
......@@ -49,6 +52,7 @@ namespace spot
}
tls_impl_ = opt->get("tls-impl", -1);
gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_);
ltl_split_ = opt->get("ltl-split", 1);
}
void translator::build_simplifier(const bdd_dict_ptr& dict)
......@@ -95,6 +99,8 @@ namespace spot
throw std::runtime_error
("tls-impl should take a value between 0 and 3");
}
if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
options.favor_event_univ = true;
simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
}
......@@ -160,37 +166,160 @@ namespace spot
twa_graph_ptr aut;
twa_graph_ptr aut2 = nullptr;
if (comp_susp_ > 0)
if (ltl_split_ && type_ == Generic && !r.is_syntactic_obligation())
{
// FIXME: Handle unambiguous_ automata?
int skel_wdba = skel_wdba_;
if (skel_wdba < 0)
skel_wdba = (pref_ & postprocessor::Deterministic) ? 1 : 2;
aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0,
skel_simul_ == 0, early_susp_ != 0,
comp_susp_ == 2, skel_wdba == 2, false);
formula r2 = r;
unsigned leading_x = 0;
while (r2.is(op::X))
{
r2 = r2[0];
++leading_x;
}
// F(q|u|f) = q|F(u)|F(f)
// G(q&e&f) = q&G(e)&G(f)
bool want_u = r2.is({op::F, op::Or});
if (want_u || r2.is({op::G, op::And}))
{
std::vector<formula> susp;
std::vector<formula> rest;
auto op1 = r2.kind();
auto op2 = r2[0].kind();
for (formula child: r2[0])
{
bool u = child.is_universal();
bool e = child.is_eventual();
if (u && e)
susp.push_back(child);
else if ((want_u && u) || (!want_u && e))
susp.push_back(formula::unop(op1, child));
else
rest.push_back(child);
}
susp.push_back(formula::unop(op1, formula::multop(op2, rest)));
r2 = formula::multop(op2, susp);
}
if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or))
goto nosplit;
bool is_and = r2.is(op::And);
// Let's classify subformulas.
std::vector<formula> oblg;
std::vector<formula> susp;
std::vector<formula> rest;
for (formula child: r2)
{
if (child.is_syntactic_obligation())
oblg.push_back(child);
else if (child.is_eventual() && child.is_universal())
susp.push_back(child);
else
rest.push_back(child);
}
option_map om;
if (opt_)
om = *opt_;
om.set("ltl-split", 0);
translator translate_without_split(simpl_, &om);
translate_without_split.set_pref(pref_);
translate_without_split.set_level(level_);
translate_without_split.set_type(type_);
auto transrun = [&](formula f)
{
if (f == r2)
return translate_without_split.run(f);
else
return run(f);
};
aut = nullptr;
// All obligations can be converted into a minimal WDBA.
if (!oblg.empty())
{
formula oblg_f = formula::multop(r2.kind(), oblg);
aut = transrun(oblg_f);
}
if (!rest.empty())
{
formula rest_f = formula::multop(r2.kind(), rest);
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);
}
if (!susp.empty())
{
twa_graph_ptr susp_aut = nullptr;
// Each suspendable formula separately
for (formula f: susp)
{
twa_graph_ptr one = transrun(f);
if (!susp_aut)
susp_aut = one;
else if (is_and)
susp_aut = product(susp_aut, one);
else
susp_aut = product_or(susp_aut, one);
}
if (aut == nullptr)
aut = susp_aut;
else if (is_and)
aut = product_susp(aut, susp_aut);
else
aut = product_or_susp(aut, susp_aut);
}
if (leading_x > 0)
{
unsigned init = aut->get_init_state_number();
do
{
unsigned tmp = aut->new_state();
aut->new_edge(tmp, init, bddtrue);
init = tmp;
}
while (--leading_x);
aut->set_init_state(init);
}
}
else
{
if (gf_guarantee_ && PREF_ != Any)
nosplit:
if (comp_susp_ > 0)
{
bool det = unambiguous || (PREF_ == Deterministic);
bool sba = type_ == BA || (pref_ & SBAcc);
if ((type_ & (BA | Parity | Generic)) || type_ == TGBA)
aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), det, sba);
if (aut2 && (type_ & (BA | Parity)) && (pref_ & Deterministic))
return finalize(aut2);
if (!aut2 && (type_ & (Generic | Parity | CoBuchi)))
// FIXME: Handle unambiguous_ automata?
int skel_wdba = skel_wdba_;
if (skel_wdba < 0)
skel_wdba = (pref_ & postprocessor::Deterministic) ? 1 : 2;
aut = compsusp(r, simpl_->get_dict(), skel_wdba == 0,
skel_simul_ == 0, early_susp_ != 0,
comp_susp_ == 2, skel_wdba == 2, false);
}
else
{
if (gf_guarantee_ && PREF_ != Any)
{
aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba);
if (aut2
&& (type_ & (CoBuchi | Parity))
bool det = unambiguous || (PREF_ == Deterministic);
bool sba = type_ == BA || (pref_ & SBAcc);
if ((type_ & (BA | Parity | Generic)) || type_ == TGBA)
aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(),
det, sba);
if (aut2 && ((type_ == BA) || (type_ & Parity))
&& (pref_ & Deterministic))
return finalize(aut2);
if (!aut2 && (type_ & (Generic | Parity | CoBuchi)))
{
aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), sba);
if (aut2
&& (type_ & (CoBuchi | Parity))
&& (pref_ & Deterministic))
return finalize(aut2);
}
}
}
bool exprop = unambiguous || level_ == postprocessor::High;
aut = ltl_to_tgba_fm(r, simpl_->get_dict(), exprop,
true, false, false, nullptr, nullptr,
......
......@@ -149,6 +149,8 @@ namespace spot
int relabel_bool_;
int tls_impl_;
bool gf_guarantee_;
bool ltl_split_;
const option_map* opt_;
};
/// @}
......
......@@ -183,29 +183,29 @@ cat >exp<<EOF
"ms-example=4,2",10
"ms-example=4,3",11
"ms-example=4,4",12
"ms-phi-r=0",2
"ms-phi-r=1",16
"ms-phi-r=2",29
"ms-phi-s=0",5
"ms-phi-s=1",8
"ms-phi-s=2",497
"ms-phi-r=0",1
"ms-phi-r=1",1
"ms-phi-r=2",1
"ms-phi-s=0",1
"ms-phi-s=1",1
"ms-phi-s=2",1
"ms-phi-h=0",1
"ms-phi-h=1",3
"ms-phi-h=2",7
"ms-phi-h=3",15
"ms-phi-h=4",31
"ms-phi-h=1",2
"ms-phi-h=2",5
"ms-phi-h=3",19
"ms-phi-h=4",83
"gf-equiv=0",1
"gf-equiv=1",4
"gf-equiv=2",8
"gf-equiv=3",21
"gf-equiv=4",81
"gf-equiv=5",431
"gf-equiv=1",1
"gf-equiv=2",1
"gf-equiv=3",1
"gf-equiv=4",1
"gf-equiv=5",1
"gf-implies=0",1
"gf-implies=1",5
"gf-implies=2",12
"gf-implies=3",41
"gf-implies=4",186
"gf-implies=5",1047
"gf-implies=1",1
"gf-implies=2",1
"gf-implies=3",1
"gf-implies=4",1
"gf-implies=5",1
"gf-equiv-xn=1",2
"gf-equiv-xn=2",4
"gf-equiv-xn=3",8
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche
# Copyright (C) 2016, 2018 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -21,8 +21,10 @@
. ./defs
set -e
# formula 'XX((Fa|Gb)&FGc)' tests the X removal of the ltl-split path
randltl -n 100 p1 p2 p3 --tree-size 5..15 --seed=200 |
ltlcross --timeout=60 \
ltlcross -F- -f 'XX((Fa|Gb)&FGc)' --timeout=60 \
"ltl2tgba %f > %T" \
"ltl2tgba -G -D %f > %T" \
"ltl2tgba -G -D %f | autfilt --gsa=unique-fin > %T" \
......
This diff is collapsed.
This diff is collapsed.
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