Commit 406e3b4f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

exclusive_ap::constrain does not improve determism

Fixes #363.

* spot/tl/exclusive.cc: Fix the prop_copy() call.
* tests/core/exclusive-tgba.test: Test it.
* NEWS: Mention the issue.
parent 1b92a8e6
......@@ -14,6 +14,12 @@ New in spot 2.6.1.dev (not yet released)
colors 0-7, and that higher color numbers cycle into this 16-color
palette.
Bugs fixed:
- exclusive_ap::constrain() (called by autfilt --exclusive-ap=...)
would incorrectly copy the "universal" property of the input
automaton, causing print_hoa() to fail.
New in spot 2.6.1 (2018-08-04)
Command-line tools:
......
......@@ -178,7 +178,7 @@ namespace spot
twa_graph_ptr res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut);
res->prop_copy(aut, { true, true, false, true, false, true });
res->prop_copy(aut, { true, true, false, false, false, true });
res->copy_acceptance_of(aut);
if (simplify_guards)
{
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
# Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -173,3 +173,9 @@ test "5,22,10" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' |
ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' |
autfilt --small --exclusive-ap=a,b,c --simplify-ex --ap=3 > out
test "5,21,10" = `autfilt out --stats='%s,%t,%e' --ap=2`
# Issue #363.
ltl2tgba 'a U b' |
autfilt --exclusive-ap=a,b,c --simplify-exclusive-ap > out
test "2,8,3" = `autfilt out --stats='%s,%t,%e' --ap=2`
Supports Markdown
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