From a6677c2984f08edee913263213cdee1c321a8ad3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Nov 2010 15:38:00 +0100 Subject: [PATCH] Do not output a counterexample by default in ltl2tgba, introduce options -C and -CR for that. * src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control whether we want the accepting run to be printed or replayed. * src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test, src/tgbatest/emptchk.test, src/tgbatest/emptchke.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR. --- ChangeLog | 11 +++++ src/tgbatest/dfs.test | 14 +++--- src/tgbatest/eltl2tgba.test | 6 +-- src/tgbatest/emptchk.test | 82 ++++++++++++++++++------------------ src/tgbatest/emptchke.test | 16 +++---- src/tgbatest/ltl2tgba.cc | 32 ++++++++++++-- src/tgbatest/ltlcounter.test | 8 ++-- 7 files changed, 103 insertions(+), 66 deletions(-) diff --git a/ChangeLog b/ChangeLog index ad5ecfb2b..522aab474 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-11-06 Alexandre Duret-Lutz + + Do not output a counterexample by default in ltl2tgba, introduce + options -C and -CR for that. + + * src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control + whether we want the accepting run to be printed or replayed. + * src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test, + src/tgbatest/emptchk.test, src/tgbatest/emptchke.test, + src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR. + 2010-11-06 Alexandre Duret-Lutz Make sure the neverclaim parser works on the output of spin and diff --git a/src/tgbatest/dfs.test b/src/tgbatest/dfs.test index fed7014c3..694166b69 100755 --- a/src/tgbatest/dfs.test +++ b/src/tgbatest/dfs.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -79,8 +79,8 @@ s9, s8,,; s9, s9,,; EOF -run 0 ../ltl2tgba -eSE05 -X blue_counter -run 0 ../ltl2tgba -eTau03_opt -X blue_counter +run 0 ../ltl2tgba -CR -eSE05 -X blue_counter +run 0 ../ltl2tgba -CR -eTau03_opt -X blue_counter # s1->s2->s3->(large composant from s4 to s9) # ^ || @@ -131,8 +131,8 @@ s9, s8,,; s9, s9,,; EOF -run 0 ../ltl2tgba -eSE05 -X blue_last -run 0 ../ltl2tgba -eTau03_opt -X blue_last +run 0 ../ltl2tgba -CR -eSE05 -X blue_last +run 0 ../ltl2tgba -CR -eTau03_opt -X blue_last # _______ # | | @@ -187,7 +187,7 @@ s9, s8,,; s9, s9,,; EOF -run 0 ../ltl2tgba -eSE05 -X red -run 0 ../ltl2tgba -eTau03_opt -X red +run 0 ../ltl2tgba -CR -eSE05 -X red +run 0 ../ltl2tgba -CR -eTau03_opt -X red rm -f red blue_counter blue_last diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test index 76671557d..7b683e60b 100755 --- a/src/tgbatest/eltl2tgba.test +++ b/src/tgbatest/eltl2tgba.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -33,11 +33,11 @@ check_construct() # translated using FM. check_true() { - run 0 ../ltl2tgba -e -Poutput -f "$1" + run 0 ../ltl2tgba -CR -e -Poutput -f "$1" } check_false() { - run 1 ../ltl2tgba -e -Poutput -f "$1" + run 1 ../ltl2tgba -CR -e -Poutput -f "$1" } # Create the prelude file. diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 02ad9a00f..9a6e9b2ed 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -35,52 +35,54 @@ expect_ce_do() expect_ce() { - expect_ce_do -e -l "$1" - expect_ce_do -e -l -D "$1" - expect_ce_do -e -f "$1" - expect_ce_do -e -f -D "$1" - expect_ce_do -e'Cou99(shy)' -l "$1" - expect_ce_do -e'Cou99(shy)' -l -D "$1" - expect_ce_do -e'Cou99(shy)' -f "$1" - expect_ce_do -e'Cou99(shy)' -f -D "$1" - expect_ce_do -eCVWY90 -l "$1" - expect_ce_do -eCVWY90 -f "$1" - run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -l "$1" - run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -f "$1" - run 0 ../ltl2tgba -eSE05 -l "$1" - run 0 ../ltl2tgba -eSE05 -f "$1" - run 0 ../ltl2tgba -e'SE05(bsh=10M)' -l "$1" - run 0 ../ltl2tgba -e'SE05(bsh=10M)' -f "$1" - run 0 ../ltl2tgba -eTau03_opt -f "$1" - run 0 ../ltl2tgba -eGV04 -f "$1" + expect_ce_do -CR -e -l "$1" + expect_ce_do -CR -e -l -D "$1" + expect_ce_do -CR -e -f "$1" + expect_ce_do -CR -e -f -D "$1" + expect_ce_do -CR -e'Cou99(shy)' -l "$1" + expect_ce_do -CR -e'Cou99(shy)' -l -D "$1" + expect_ce_do -CR -e'Cou99(shy)' -f "$1" + expect_ce_do -CR -e'Cou99(shy)' -f -D "$1" + expect_ce_do -CR -eCVWY90 -l "$1" + expect_ce_do -CR -eCVWY90 -f "$1" + run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -l "$1" + run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -f "$1" + run 0 ../ltl2tgba -CR -eSE05 -l "$1" + run 0 ../ltl2tgba -CR -eSE05 -f "$1" + run 0 ../ltl2tgba -CR -e'SE05(bsh=10M)' -l "$1" + run 0 ../ltl2tgba -CR -e'SE05(bsh=10M)' -f "$1" + run 0 ../ltl2tgba -CR -eTau03_opt -f "$1" + run 0 ../ltl2tgba -CR -eGV04 -f "$1" # Expect multiple accepting runs - test `../ltl2tgba -e'CVWY90(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2 - test `../ltl2tgba -e'SE05(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2 + test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "$1" | + grep Prefix: | wc -l` -ge $2 + test `../ltl2tgba -CR -e'SE05(repeated)' -l "$1" | + grep Prefix: | wc -l` -ge $2 } expect_no() { - run 0 ../ltl2tgba -E -l "$1" - run 0 ../ltl2tgba -E -l -D "$1" - run 0 ../ltl2tgba -E -f "$1" - run 0 ../ltl2tgba -E -f -D "$1" - run 0 ../ltl2tgba -E'Cou99(shy)' -l "$1" - run 0 ../ltl2tgba -E'Cou99(shy)' -l -D "$1" - run 0 ../ltl2tgba -E'Cou99(shy)' -f "$1" - run 0 ../ltl2tgba -E'Cou99(shy)' -f -D "$1" - run 0 ../ltl2tgba -ECVWY90 -l "$1" - run 0 ../ltl2tgba -ECVWY90 -f "$1" - run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -l "$1" - run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -f "$1" - run 0 ../ltl2tgba -ESE05 -l "$1" - run 0 ../ltl2tgba -ESE05 -f "$1" - run 0 ../ltl2tgba -E'SE05(bsh=10M)' -l "$1" - run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1" - run 0 ../ltl2tgba -ETau03_opt -f "$1" - run 0 ../ltl2tgba -EGV04 -f "$1" - test `../ltl2tgba -e'CVWY90(repeated)' -l "!($1)" | + run 0 ../ltl2tgba -CR -E -l "$1" + run 0 ../ltl2tgba -CR -E -l -D "$1" + run 0 ../ltl2tgba -CR -E -f "$1" + run 0 ../ltl2tgba -CR -E -f -D "$1" + run 0 ../ltl2tgba -CR -E'Cou99(shy)' -l "$1" + run 0 ../ltl2tgba -CR -E'Cou99(shy)' -l -D "$1" + run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f "$1" + run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f -D "$1" + run 0 ../ltl2tgba -CR -ECVWY90 -l "$1" + run 0 ../ltl2tgba -CR -ECVWY90 -f "$1" + run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -l "$1" + run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -f "$1" + run 0 ../ltl2tgba -CR -ESE05 -l "$1" + run 0 ../ltl2tgba -CR -ESE05 -f "$1" + run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -l "$1" + run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -f "$1" + run 0 ../ltl2tgba -CR -ETau03_opt -f "$1" + run 0 ../ltl2tgba -CR -EGV04 -f "$1" + test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "!($1)" | grep Prefix: | wc -l` -ge $2 - test `../ltl2tgba -e'SE05(repeated)' -l "!($1)" | + test `../ltl2tgba -CR -e'SE05(repeated)' -l "!($1)" | grep Prefix: | wc -l` -ge $2 } diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index e1f5b8ece..e398ee497 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -29,14 +29,14 @@ set -e expect_ce() { - run 0 ../ltl2tgba -e -X "$1" - run 0 ../ltl2tgba -e -D -X "$1" - run 0 ../ltl2tgba -e'Cou99(shy)' -X "$1" - run 0 ../ltl2tgba -e'Cou99(shy)' -D -X "$1" - run 0 ../ltl2tgba -eCVWY90 -X "$1" - run 0 ../ltl2tgba -eGV04 -X "$1" - run 0 ../ltl2tgba -eSE05 -X "$1" - run 0 ../ltl2tgba -eTau03 -X "$1" + run 0 ../ltl2tgba -CR -e -X "$1" + run 0 ../ltl2tgba -CR -e -D -X "$1" + run 0 ../ltl2tgba -CR -e'Cou99(shy)' -X "$1" + run 0 ../ltl2tgba -CR -e'Cou99(shy)' -D -X "$1" + run 0 ../ltl2tgba -CR -eCVWY90 -X "$1" + run 0 ../ltl2tgba -CR -eGV04 -X "$1" + run 0 ../ltl2tgba -CR -eSE05 -X "$1" + run 0 ../ltl2tgba -CR -eTau03 -X "$1" } cat >input <<'EOF' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5c5f39b3d..37b62c4c2 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -214,6 +214,10 @@ syntax(char* prog) << "accepting run" << std::endl << " -E[ALGO] run emptiness check, expect no accepting run" << std::endl + << " -C compute an accepting run (Counterexample) if it exists" + << std::endl + << " -CR compute and replay an accepting run (implies -C)" + << std::endl << " -g graph the accepting run on the automaton (requires -e)" << std::endl << " -G graph the accepting run seen as an automaton " @@ -287,6 +291,8 @@ main(int argc, char** argv) spot::emptiness_check_instantiator* echeck_inst = 0; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool expect_counter_example = false; + bool accepting_run = false; + bool accepting_run_replay = false; bool from_file = false; bool read_neverclaim = false; int reduc_aut = spot::Reduce_None; @@ -341,6 +347,15 @@ main(int argc, char** argv) containment = true; translation = TransTAA; } + else if (!strcmp(argv[formula_index], "-C")) + { + accepting_run = true; + } + else if (!strcmp(argv[formula_index], "-CR")) + { + accepting_run = true; + accepting_run_replay = true; + } else if (!strcmp(argv[formula_index], "-d")) { debug_opt = true; @@ -440,10 +455,12 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-g")) { + accepting_run = true; graph_run_opt = true; } else if (!strcmp(argv[formula_index], "-G")) { + accepting_run = true; graph_run_tgba_opt = true; } else if (!strcmp(argv[formula_index], "-k")) @@ -1111,7 +1128,7 @@ main(int argc, char** argv) std::cout << std::endl; break; } - else + else if (accepting_run) { tm.start("computing accepting run"); @@ -1148,14 +1165,21 @@ main(int argc, char** argv) else { spot::print_tgba_run(std::cout, a, run); - if (!spot::replay_tgba_run(std::cout, a, run, - true)) - exit_code = 1; + + if (accepting_run_replay + && !spot::replay_tgba_run(std::cout, a, run, + true)) + exit_code = 1; } delete run; tm.stop("printing accepting run"); } } + else + { + std::cout << "an accepting run exists " + << "(use -C to print it)" << std::endl; + } } delete res; } diff --git a/src/tgbatest/ltlcounter.test b/src/tgbatest/ltlcounter.test index 46218c037..05274b8a0 100755 --- a/src/tgbatest/ltlcounter.test +++ b/src/tgbatest/ltlcounter.test @@ -1,6 +1,6 @@ #!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement de +# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de # l'EPITA (LRDE) # # This file is part of Spot, a model checking library. @@ -36,10 +36,10 @@ run='run 0' check_formula() { # First, check the satisfiability of the formula with Spot - $run ../ltl2tgba -e -x -f "$1" >/dev/null + $run ../ltl2tgba -CR -e -x -f "$1" >/dev/null # Also check the satisfiability of the degeneralized formula - $run ../ltl2tgba -e -D -x -f "$1" >/dev/null - $run ../ltl2tgba -e -DS -x -f "$1" >/dev/null + $run ../ltl2tgba -CR -e -D -x -f "$1" >/dev/null + $run ../ltl2tgba -CR -e -DS -x -f "$1" >/dev/null } # Kristin Y. Rozier reported that the formulae with n=10 were badly