Commit 73bb562b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

complement: reset the terminal property

Reported by Thomas Medioni.

* spot/twaalgos/complement.cc: Here.
* tests/core/complement.test: Add a test case.
* NEWS: Mention it.
parent cdf699ff
......@@ -8,6 +8,10 @@ New in spot 2.3.2.dev (not yet released)
- The output of 'genltl --r-left=1 --r-right=1 --format=%F'
had typos.
- 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that
the output is "terminal" because dtwa_complement() failed to reset
that property.
New in spot 2.3.2 (2017-03-15)
Tools:
......
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
......@@ -18,7 +18,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/cleanacc.hh>
......@@ -27,9 +27,19 @@ namespace spot
twa_graph_ptr
dtwa_complement(const const_twa_graph_ptr& aut)
{
if (!is_deterministic(aut))
throw
std::runtime_error("dtwa_complement() requires a deterministic input");
// Simply complete the automaton, and complement its acceptance.
auto res = cleanup_acceptance_here(complete(aut));
res->set_acceptance(res->num_sets(), res->get_acceptance().complement());
// Complementing the acceptance is likely to break the terminal
// property, but not weakness. We make a useless call to
// prop_keep() just so we remember to update it in the future if a
// new argument is added.
res->prop_keep({true, true, true, true, true});
res->prop_terminal(trival::maybe());
return res;
}
}
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -22,12 +22,8 @@
set -e
autfilt=autfilt
ltl2tgba=ltl2tgba
randaut=randaut
$randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut
run 0 $autfilt --complement -H aut >/dev/null
randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut
run 0 autfilt --complement -H aut >/dev/null
cat >in <<EOF
HOA: v1
......@@ -36,7 +32,7 @@ Acceptance: 0 t
--BODY--
--END--
EOF
$autfilt --complement -H in >out
autfilt --complement -H in >out
cat >expected <<EOF
HOA: v1
States: 1
......@@ -54,7 +50,7 @@ EOF
diff out expected
$ltl2tgba -H 'GFa & GFb' Xa | $autfilt --complement -H >out
ltl2tgba -H 'GFa & GFb' Xa Fa | autfilt --complement -H >out
cat >expected <<EOF
HOA: v1
States: 1
......@@ -78,7 +74,7 @@ AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic terminal
properties: deterministic weak
--BODY--
State: 0
[0] 2
......@@ -90,12 +86,27 @@ State: 2 {0}
State: 3
[t] 3
--END--
HOA: v1
States: 2
Start: 1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant weak
--BODY--
State: 0 {0}
[t] 0
State: 1
[0] 0
[!0] 1
--END--
EOF
diff out expected
# The complement of a nondeterministic automaton is currently done via
# a determinization.
$ltl2tgba -H 'FGa' | $autfilt --complement >out
ltl2tgba -H 'FGa' | autfilt --complement >out
cat >expected <<EOF
HOA: v1
States: 2
......
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