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

ltlcross: fix missing check for complement of negative automata

* src/bin/ Fix it.
* src/tgbatest/ltl2dstar.test: Test it.
* NEWS: Mention it.
parent 49a09978
......@@ -4,6 +4,15 @@ New in spot 1.2.5a (not yet released)
- ltlcross --verbose is a new option to see what is being done
* Bug fixes:
- When the automaton resulting from the translation of a positive
formula is deterministic, ltlcross will compute its complement
to perform additional checks against other translations of the
positive formula. The same procedure should be performed with
automata obtained from negated formulas, but because of a typo
this was not the case.
New in spot 1.2.5 (2014-08-21)
* New features:
......@@ -1473,7 +1473,7 @@ namespace
problems +=
check_empty_prod(pos[i], comp_pos[j],
i, j, false, true);
if (i != j && comp_neg[i] && !comp_neg[i])
if (i != j && comp_neg[i] && !comp_pos[i])
problems +=
check_empty_prod(comp_neg[i], neg[j],
i, j, true, false);
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et
# Copyright (C) 2013, 2014 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# This file is part of Spot, a model checking library.
......@@ -61,3 +61,17 @@ grep '"in_type"' out.csv
grep '"DSA"' out.csv
grep '"DRA"' out.csv
grep ',,,,' out.csv
# A bug in ltlcross <=1.2.5 caused it to not use the complement of the
# negative automaton. So running ltlcross with GFa would check one
# complement (the positive one), but running with FGa would ignore
# the negative complement.
$ltlcross -f 'GFa' --verbose \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
test `grep -c 'info: check_empty.*Comp' err` = 1
$ltlcross -f 'FGa' --verbose \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
test `grep -c 'info: check_empty.*Comp' err` = 1
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