alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

product: fix handling of operand with false acceptance

Browse source 
* NEWS: Mention the issue.
* spot/twaalgos/product.cc: Fix it.
* tests/python/prodexpt.py: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-06 23:23:13 +01:00
parent 7f0ef7ad59
commit d8a0f307eb
3 changed files with 73 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -91,6 +91,13 @@ New in spot 2.8.6.dev (not yet released)
- car() is a new variant of LAR algorithm that combines several
strategies for paritazing any automaton.
Bugs fixed:
- Building a product between two complete automata where one operand
had false acceptance could create a incomplete automaton
incorrectly tagged as complete, causing the print_hoa() function
to raise an exception.
New in spot 2.8.6 (2020-02-19)
Bugs fixed:

49
spot/twaalgos/product.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -285,21 +285,34 @@ namespace spot
if (!res) // aborted
return nullptr;
// The product of two non-deterministic automata could be
// deterministic. Likewise for non-complete automata.
if (left->prop_universal() && right->prop_universal())
res->prop_universal(true);
if (left->prop_complete() && right->prop_complete())
res->prop_complete(true);
if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
res->prop_stutter_invariant(true);
if (left->prop_inherently_weak() && right->prop_inherently_weak())
res->prop_inherently_weak(true);
if (left->prop_weak() && right->prop_weak())
res->prop_weak(true);
if (left->prop_terminal() && right->prop_terminal())
res->prop_terminal(true);
res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc());
if (res->acc().is_f())
{
assert(res->num_edges() == 0);
res->prop_universal(true);
res->prop_complete(false);
res->prop_stutter_invariant(true);
res->prop_terminal(true);
res->prop_state_acc(true);
}
else
{
// The product of two non-deterministic automata could be
// deterministic. Likewise for non-complete automata.
if (left->prop_universal() && right->prop_universal())
res->prop_universal(true);
if (left->prop_complete() && right->prop_complete())
res->prop_complete(true);
if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
res->prop_stutter_invariant(true);
if (left->prop_inherently_weak() && right->prop_inherently_weak())
res->prop_inherently_weak(true);
if (left->prop_weak() && right->prop_weak())
res->prop_weak(true);
if (left->prop_terminal() && right->prop_terminal())
res->prop_terminal(true);
res->prop_state_acc(left->prop_state_acc()
&& right->prop_state_acc());
}
return res;
}
}
@ -450,6 +463,10 @@ namespace spot
{
auto res = make_twa_graph(left->get_dict());
res->new_state();
res->prop_terminal(true);
res->prop_stutter_invariant(true);
res->prop_universal(true);
res->prop_complete(false);
return res;
}
return make_twa_graph(left, twa::prop_set::all());

35
tests/python/prodexpt.py
View file

@ -1,6 +1,6 @@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2016-2017, 2019 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2016-2017, 2019-2020 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -102,3 +102,34 @@ res = spot.product(left, right, spot.output_aborter(900, 9000))
assert res is None
res = spot.product(left, right, spot.output_aborter(1000, 9000))
assert res is not None
a, b = spot.automata("""HOA: v1 States: 1 Start: 0 AP: 0 acc-name: all
Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0
--END-- HOA: v1 States: 1 Start: 0 AP: 0 acc-name: none Acceptance: 0 f
properties: trans-labels explicit-labels state-acc complete properties:
deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 --END--""")
out = spot.product(a, b).to_str()
assert out == """HOA: v1
States: 1
Start: 0
AP: 0
acc-name: none
Acceptance: 0 f
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0
--END--"""
out = spot.product_susp(a, b).to_str()
assert out == """HOA: v1
States: 1
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0
--END--"""