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

ltlcross: fix cross-checks for automata using Fin acceptance

Fixes #420 reported by Salomon Sickert.

* bin/ltlcross.cc: Call determine_unknown_acceptance().
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Document
that one_accepting_scc()==-1 can mean "don't know", and update
determine_unknown_acceptance() to set one_acc_scc_.
* tests/core/ltlcross3.test: Add test case.
* NEWS: Mention the fixes.
parent 4db6a342
Pipeline #20576 passed with stages
in 216 minutes and 57 seconds
......@@ -45,6 +45,15 @@ New in spot 2.9.1.dev (not yet released)
file. With this refactoring, we can retrieve both a kripke or a
kripkecube from a PINS file.
Bugs fixed:
- ltlcross --csv=... --product=N with N>0 could output spurious
diagnosics claiming that words were rejected when evaluating
the automaton on state-space.
- spot::scc_info::determine_unknown_acceptance() now also update the
result of spot::scc_info::one_accepting_scc().
New in spot 2.9.1 (2020-07-15)
Command-line tools:
......
......@@ -1568,6 +1568,7 @@ namespace
sm = new
spot::scc_info(p,
spot::scc_info_options::TRACK_STATES);
sm->determine_unknown_acceptance();
}
catch (const std::bad_alloc&)
{
......
......@@ -472,9 +472,15 @@ namespace spot
"does not support alternating automata");
auto& node = node_[s];
if (check_scc_emptiness(s))
node.rejecting_ = true;
{
node.rejecting_ = true;
}
else
node.accepting_ = true;
{
node.accepting_ = true;
if (one_acc_scc_ < 0)
one_acc_scc_ = s;
}
changed = true;
}
}
......
......@@ -535,7 +535,14 @@ namespace spot
return node_.size();
}
/// Return the number of one accepting SCC if any, -1 otherwise.
/// \brief Return the number of one accepting SCC if any, -1 otherwise.
///
/// If an accepting SCC has been found, return its number.
/// Otherwise return -1. Note that when the acceptance condition
/// contains Fin, -1 does not implies that all SCCs are rejecting:
/// it just means that no accepting SCC is known currently. In
/// that case, you might want to call
/// determine_unknown_acceptance() first.
int one_accepting_scc() const
{
return one_acc_scc_;
......
......@@ -327,6 +327,11 @@ diff foo expected
# This command used to crash. Report from František Blahoudek.
run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba'
# In spot 2.9 and 2.9.1 the following command used to report a bug
# that did not exist. Issue #420.
ltlcross --csv=/dev/null ltl2tgba 'ltl2tgba -D -G' --states=5 \
-f '(G(F(((a) & (X(X(a)))) | ((!(a)) & (X(X(!(a))))))))'
# The CSV file should not talk about product if --products=0
ltlcross --color --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv
grep product out.csv && exit 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