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

* tests/python/streett_totgba.py: Remove superfluous comment.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2021-11-10 15:28:08 +01:00
parent d4967f20e9
commit 2f528c7190
1 changed files with 1 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
tests/python/streett_totgba.py
View file

@ -1,6 +1,6 @@
#!/usr/bin/python3 #!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*- # -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de # Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et Développement de
# l'EPITA. # l'EPITA.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -47,12 +47,6 @@ def test_aut(aut):
del os.environ["SPOT_STREETT_CONV_MIN"] del os.environ["SPOT_STREETT_CONV_MIN"]
assert sltgba.equivalent_to(slftgba) assert sltgba.equivalent_to(slftgba)
# Those automata are generated with ltl2dstar, which is NOT part of spot,
# using the following command:
# genltl --eh-patterns --dac-patterns --hkrss-patterns --sb-patterns |\
# ltldo "ltl2dstar --automata=streett --output-format=hoa\
# --ltl2nba=spin:ltl2tgba@-s %L ->%O" -F- --name=%f -H"
if shutil.which('ltl2dstar') is None: if shutil.which('ltl2dstar') is None:
sys.exit(77) sys.exit(77)