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

ltl-split: translate any "safety" with "rest"

Browse source 
* tests/core/ltl2tgba2.test: Add a test-case reported by Maximilien.
* spot/twaalgos/translate.cc: Translate any "safety" formula with
"rest".
* tests/python/highlighting.ipynb: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2018-07-26 18:15:19 +02:00
parent a14f96813d
commit 3303b86a89
3 changed files with 204 additions and 243 deletions
Download patch file Download diff file Expand all files Collapse all files

15
spot/twaalgos/translate.cc
View file

@ -186,6 +186,21 @@ namespace spot
rest.push_back(child);
}
// Safety formulas are quite easy to translate since they do
// not introduce marks. If rest is non-empty, it seems
// preferable to translate the safety inside rest, as this may
// constrain the translation.
if (!rest.empty() && !oblg.empty())
{
auto safety = [](formula f)
{
return f.is_syntactic_safety();
};
auto i = std::remove_if(oblg.begin(), oblg.end(), safety);
rest.insert(rest.end(), i, oblg.end());
oblg.erase(i, oblg.end());
}
if (!susp.empty())
{
// The only cases where we accept susp and rest to be both