From 7760b459e719f3dd532401440bba6cd683b23c5f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Aug 2011 14:00:39 +0200 Subject: [PATCH] * src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D. --- ChangeLog | 4 ++++ src/tgbatest/ltl2tgba.cc | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 4a02bc62b..679def516 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2011-08-17 Alexandre Duret-Lutz + + * src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D. + 2011-07-26 Alexandre Duret-Lutz * iface/dve2/dve2check.cc: Add option -W and simplify formulae. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 98ed72f38..2afffc858 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -265,10 +265,10 @@ syntax(char* prog) << " -K dump the graph of SCCs in dot format" << std::endl << " -KV verbosely dump the graph of SCCs in dot format" << std::endl - << " -N output the never clain for Spin (implies -D)" + << " -N output the never clain for Spin (implies -DS)" << std::endl << " -NN output the never clain for Spin, with commented states" - << " (implies -D)" << std::endl + << " (implies -DS)" << std::endl << " -O tell if a formula represents a safety, guarantee, " << "or obligation property" << std::endl