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

fix is_generalized_rabin() and is_generalized_streett()

* spot/twa/acc.cc: Fix detection of single-pairs gen-Rabin and
gen-Streett.
* tests/core/randaut.test: Add test case.
* NEWS: Mention this issue.
parent 9365f8de
......@@ -14,6 +14,10 @@ New in spot 2.8.5.dev (not yet released)
- Some formulas with Boolean sub-formulas equivalent to true or
false could be translated into automata with false labels.
- The HOA printer would incorrectly output the condition such
'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)'
due to a bug in the is_generalized_rabin() matching function.
New in spot 2.8.5 (2020-01-04)
Bugs fixed:
......
......@@ -681,14 +681,20 @@ namespace spot
// generalized Rabin should start with Or, unless
// it has a single pair.
bool singlepair = false;
{
auto topop = code_.back().sub.op;
if (topop == acc_op::And)
// Probably single-pair generalized-Rabin. Shift the source
// by one position as if we had an invisible Or in front.
++s;
{
// Probably single-pair generalized-Rabin. Shift the source
// by one position as if we had an invisible Or in front.
++s;
singlepair = true;
}
else if (topop != acc_op::Or)
return false;
{
return false;
}
}
// Each pair is the position of a Fin followed
......@@ -752,7 +758,8 @@ namespace spot
}
for (auto i: p)
pairs.emplace_back(i.second);
return (!(seen_fin & seen_inf)
return ((!singlepair || pairs.size() == 1)
&& !(seen_fin & seen_inf)
&& (seen_fin | seen_inf) == all_sets());
}
......@@ -776,14 +783,20 @@ namespace spot
// generalized Streett should start with And, unless
// it has a single pair.
bool singlepair = false;
{
auto topop = code_.back().sub.op;
if (topop == acc_op::Or)
// Probably single-pair generalized-Streett. Shift the source
// by one position as if we had an invisible And in front.
++s;
{
// Probably single-pair generalized-Streett. Shift the source
// by one position as if we had an invisible And in front.
++s;
singlepair = true;
}
else if (topop != acc_op::And)
return false;
{
return false;
}
}
......@@ -847,7 +860,8 @@ namespace spot
}
for (auto i: p)
pairs.emplace_back(i.second);
return (!(seen_inf & seen_fin)
return ((!singlepair || pairs.size() == 1)
&& !(seen_inf & seen_fin)
&& (seen_inf | seen_fin) == all_sets());
}
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -221,4 +221,12 @@ grep 'randaut:.*end of acceptance.*invalid range' stderr
randaut -Q0 1 2>stderr && exit 1
grep '0 states' stderr
# This catch a bug where 'Fin(1) & Inf(2) & Fin(0)' was
# incorrectly detected a generalized-Rabin and output a
# 'Fin(0) | Fin(1) & Inf(2)'.
randaut -Q1 -A 'Fin(1) & Inf(2) & Fin(0)' 2 > out.hoa
grep 'Acceptance:' out.hoa > out.acc
echo 'Acceptance: 3 Fin(1) & Inf(2) & Fin(0)' > out.exp
diff out.acc out.exp
:
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