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

ltlcross: report missing input/output sequence

Browse source 
* src/bin/ltlcross.cc: Fix it.
* src/tgbatest/ltlcross3.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2013-11-19 22:45:16 +01:00
parent cf91a23711
commit 686a45484d
4 changed files with 29 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/bin/ltlcross.cc
View file

@ -690,14 +690,13 @@ namespace
declare('N', &output);
declare('T', &output);
std::vector<bool> has(256);
size_t s = translators.size();
assert(s);
for (size_t n = 0; n < s; ++n)
{
// Check that each translator uses at least one input and
// one output.
has.clear();
std::vector<bool> has(256);
const translator_spec& t = translators[n];
scan(t.cmd, has);
if (!(has['f'] || has['s'] || has['l'] || has['w']