improve support for LTLf semantics
* spot/twaalgos/remprop.cc, spot/twaalgos/remprop.hh (to_finite): New function. * bin/autfilt.cc (--to-finite): Add it. * doc/org/tut12.org: Update to use it. * spot/twa/twagraph.cc (purge_dead_states): Also remove false edges. * spot/parseaut/parseaut.yy: Do not ignore false self-loops, and add false self-loop on accepting states without successors. * NEWS: List the above changes. * tests/core/ltlf.test: New file. * tests/Makefile.am: Add it. * tests/core/complete.test: Adjust expected output.
This commit is contained in:
Alexandre Duret-Lutz
parent
9b0a20412b
commit
a3753e608b
10 changed files with 416 additions and 83 deletions
|
|
@ -38,11 +38,14 @@ finite semantics) property. The plan is as follows:
|
|||
#+END_SRC
|
||||
#+RESULTS:
|
||||
[[file:tut12a.svg]]
|
||||
4. Remove the =alive= property, and, while we are at it, simplify the
|
||||
Büchi automaton:
|
||||
4. Remove the =alive= property, after marking as accepting all states
|
||||
with an outgoing edge labeled by =!alive=. (Note that since Spot
|
||||
does not actually support state-based acceptance, it needs to keep
|
||||
a false self-loop on any accepting state without a successor in
|
||||
order to mark it as accepting.)
|
||||
#+name: tut12b
|
||||
#+begin_src sh :exports none
|
||||
ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | autfilt --remove-ap=alive -B --small -d
|
||||
ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | autfilt --to-finite -d
|
||||
#+end_src
|
||||
#+BEGIN_SRC dot :file tut12b.svg :var txt=tut12b :exports results
|
||||
$txt
|
||||
|
|
@ -66,22 +69,21 @@ The first four steps of the above sequence of operations can be
|
|||
executed as follows. Transforming LTLf to LTL can be done using
|
||||
[[file:ltlfilt.org][=ltlfilt=]]'s =--from-ltlf= option, translating the resulting formula
|
||||
into a Büchi automaton is obviously done with [[file:ltl2tgba.org][=ltl2tgba=]], and removing
|
||||
an atomic proposition from an automaton can be done using [[file:autfilt.org][=autfilt=]]'s
|
||||
=--remove-ap= option (adding =--small= will also simplify the
|
||||
automaton). Interpreting the resulting Büchi automaton as a finite
|
||||
automaton is out of scope for Spot.
|
||||
an atomic proposition while adapting the accepting states can be done
|
||||
with [[file:autfilt.org][=autfilt=]]'s =--to-finite= option. Interpreting the resulting
|
||||
Büchi automaton as a finite automaton is out of scope for Spot.
|
||||
|
||||
#+begin_src sh
|
||||
ltlfilt --from-ltlf -f "(a U b) & Fc" |
|
||||
ltl2tgba -B |
|
||||
autfilt --remove-ap=alive -B --small
|
||||
autfilt --to-finite
|
||||
#+end_src
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 4
|
||||
Start: 1
|
||||
Start: 2
|
||||
AP: 3 "b" "a" "c"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
|
|
@ -90,17 +92,17 @@ properties: very-weak
|
|||
--BODY--
|
||||
State: 0
|
||||
[!2] 0
|
||||
[2] 3
|
||||
State: 1
|
||||
[0&!2] 0
|
||||
[!0&1&!2] 1
|
||||
[!0&1&2] 2
|
||||
[0&2] 3
|
||||
[2] 1
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[!0&1] 2
|
||||
[0] 3
|
||||
State: 3 {0}
|
||||
[t] 3
|
||||
[0&!2] 0
|
||||
[0&2] 1
|
||||
[!0&1&!2] 2
|
||||
[!0&1&2] 3
|
||||
State: 3
|
||||
[0] 1
|
||||
[!0&1] 3
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
|
|
@ -111,51 +113,42 @@ automaton is output.
|
|||
|
||||
In Python, we use the =from_ltlf()= function to convert from LTLf to
|
||||
LTL and translate the result into a Büchi automaton using
|
||||
=translate()= [[file:tut10.org][as usual]]. Then we need to use the =remove_ap()= object,
|
||||
which we must first setup with some atomic propositions to remove.
|
||||
Finally we call the =postprocess()= function for automata
|
||||
simplifications. (Note that =postprocess()= is already called by
|
||||
=translate()=, but in this case removing the atomic proposition allows
|
||||
more simplification opportunities.)
|
||||
=translate()= [[file:tut10.org][as usual]]. Then we need to call the =to_finite()=
|
||||
function.
|
||||
|
||||
#+begin_src python
|
||||
import spot
|
||||
# Translate LTLf to Büchi.
|
||||
aut = spot.from_ltlf('(a U b) & Fc').translate('small', 'buchi', 'sbacc')
|
||||
# Remove "alive" atomic proposition
|
||||
rem = spot.remove_ap()
|
||||
rem.add_ap('alive')
|
||||
aut = rem.strip(aut)
|
||||
# Simplify result and print it. Use postprocess('ba', 'det')
|
||||
# if you always want a deterministic automaton.
|
||||
aut = spot.postprocess(aut, 'ba')
|
||||
print(aut.to_str('hoa'))
|
||||
f = spot.from_ltlf('(a U b) & Fc')
|
||||
aut = f.translate('small', 'buchi', 'sbacc')
|
||||
# Remove "alive" atomic propositions and print result.
|
||||
print(spot.to_finite(aut).to_str('hoa'))
|
||||
#+end_src
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 4
|
||||
Start: 1
|
||||
Start: 2
|
||||
AP: 3 "b" "a" "c"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
properties: terminal
|
||||
properties: very-weak
|
||||
--BODY--
|
||||
State: 0
|
||||
[!2] 0
|
||||
[2] 3
|
||||
State: 1
|
||||
[0&!2] 0
|
||||
[!0&1&!2] 1
|
||||
[!0&1&2] 2
|
||||
[0&2] 3
|
||||
[2] 1
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[!0&1] 2
|
||||
[0] 3
|
||||
State: 3 {0}
|
||||
[t] 3
|
||||
[0&!2] 0
|
||||
[0&2] 1
|
||||
[!0&1&!2] 2
|
||||
[!0&1&2] 3
|
||||
State: 3
|
||||
[0] 1
|
||||
[!0&1] 3
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
|
|
@ -166,9 +159,9 @@ print of an automaton]].
|
|||
* C++ version
|
||||
|
||||
The C++ version is straightforward adaptation of the Python version.
|
||||
The Python functions =translate()= and =postprocess()= are convenient
|
||||
wrappers around the =spot::translator= and =spot::postprocessor=
|
||||
objects that we need to use here.
|
||||
(The Python function =translate()= is a convenient Python-only
|
||||
wrappers around the =spot::translator= object that we need to use
|
||||
here.)
|
||||
|
||||
#+begin_src C++
|
||||
#include <iostream>
|
||||
|
|
@ -189,17 +182,7 @@ objects that we need to use here.
|
|||
trans.set_pref(spot::postprocessor::SBAcc
|
||||
| spot::postprocessor::Small);
|
||||
spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f));
|
||||
|
||||
spot::remove_ap rem;
|
||||
rem.add_ap("alive");
|
||||
aut = rem.strip(aut);
|
||||
|
||||
spot::postprocessor post;
|
||||
post.set_type(spot::postprocessor::Buchi);
|
||||
post.set_pref(spot::postprocessor::SBAcc
|
||||
| spot::postprocessor::Small); // or ::Deterministic
|
||||
aut = post.run(aut);
|
||||
|
||||
aut = spot::to_finite(aut);
|
||||
print_hoa(std::cout, aut) << '\n';
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -209,26 +192,26 @@ objects that we need to use here.
|
|||
#+begin_example
|
||||
HOA: v1
|
||||
States: 4
|
||||
Start: 1
|
||||
Start: 2
|
||||
AP: 3 "b" "a" "c"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
properties: terminal
|
||||
properties: very-weak
|
||||
--BODY--
|
||||
State: 0
|
||||
[!2] 0
|
||||
[2] 3
|
||||
State: 1
|
||||
[0&!2] 0
|
||||
[!0&1&!2] 1
|
||||
[!0&1&2] 2
|
||||
[0&2] 3
|
||||
[2] 1
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
State: 2
|
||||
[!0&1] 2
|
||||
[0] 3
|
||||
State: 3 {0}
|
||||
[t] 3
|
||||
[0&!2] 0
|
||||
[0&2] 1
|
||||
[!0&1&!2] 2
|
||||
[!0&1&2] 3
|
||||
State: 3
|
||||
[0] 1
|
||||
[!0&1] 3
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
|
|
@ -252,12 +235,48 @@ When working with LTLf, there are two different semantics for the next
|
|||
operator:
|
||||
- The weak next: =X a= is true if =a= hold in the next step or if
|
||||
there are no next step. In particular, =X(0)= is true iff there are
|
||||
no successor. (By the way, you cannot write =X0= because that as an
|
||||
no successor. (By the way, you cannot write =X0= because that is an
|
||||
atomic proposition: use =X(0)= or =X 0=.)
|
||||
- The strong next: =X[!] a= is true if =a= hold in the next step *and*
|
||||
there must be a next step. In particular =X[!]1= asserts that
|
||||
there is a successor.
|
||||
|
||||
To see the difference between =X= and =X[!]=, consider the following translation
|
||||
of =(a & Xa) | (b & X[!]b)=:
|
||||
#+name: tut12c
|
||||
#+begin_src sh :exports none
|
||||
f="(a & Xa) | (b & X[!]b)"
|
||||
ltlfilt --from-ltlf -f "$f" | ltl2tgba -B | autfilt --name="$f" --to-finite -d.nA
|
||||
#+end_src
|
||||
#+BEGIN_SRC dot :file tut12c.svg :var txt=tut12c :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
[[file:tut12c.svg]]
|
||||
|
||||
|
||||
Note that because in reality Spot supports only transitions-based
|
||||
acceptance, and the above automaton is really stored as a Büchi
|
||||
automaton that *we* decide to interpret as a finite automaton, there
|
||||
is a bit of trickery involved to represent an "accepting state"
|
||||
without any successor. While such a state makes sense in finite
|
||||
automata, it makes no sense in ω-automata: we fake it by adding a
|
||||
self-loop labeled by *false* (internally, this extra edge is carrying
|
||||
the acceptance mark that is displayed on the state). For instance:
|
||||
#+name: tut12d
|
||||
#+begin_src sh :exports none
|
||||
f="a | (b & X(0))"
|
||||
ltlfilt --from-ltlf -f "$f" | ltl2tgba -B | autfilt --name="$f" --to-finite -d.nA
|
||||
#+end_src
|
||||
#+BEGIN_SRC dot :file tut12d.svg :var txt=tut12d :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
[[file:tut12d.svg]]
|
||||
|
||||
|
||||
# LocalWords: utf LTLf html args ltlf src ltlfilt Fc tgba svg txt
|
||||
# LocalWords: ap De Giacomo Vardi IJCAI Dutta Memocode acc Buchi ba
|
||||
# LocalWords: postprocess aut det str NFA DFA ltsmin iff
|
||||
# LocalWords: postprocess aut det str NFA DFA ltsmin iff LTL Büchi
|
||||
# LocalWords: automata ltl autfilt HOA buchi sbacc iostream hoa Xa
|
||||
# LocalWords: Kripke nA
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue