From 3b3a1965267597a17e4609f9d911979354ff56c1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 18 Feb 2005 10:03:01 +0000 Subject: [PATCH] * src/tgbatest/ltl2tgba.cc: Simplify using emptiness_check_instantiator. * src/tgba/tgba.cc, src/tgba/tgba.hh (tgba::number_of_acceptance_conditions): Return an unsigned. * bench/emptchk/algorithms, bench/emptchk/README, src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust references to algorithms. * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Quote variables properly. --- ChangeLog | 12 ++ bench/emptchk/README | 30 ++-- bench/emptchk/algorithms | 10 +- bench/emptchk/pml-clserv.sh | 6 +- bench/emptchk/pml-eeaean.sh | 6 +- src/tgba/tgba.cc | 6 +- src/tgba/tgba.hh | 4 +- src/tgbatest/emptchk.test | 42 ++--- src/tgbatest/emptchke.test | 6 +- src/tgbatest/ltl2tgba.cc | 296 +++++++++--------------------------- 10 files changed, 141 insertions(+), 277 deletions(-) diff --git a/ChangeLog b/ChangeLog index 3ae44b0a4..edc337752 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2005-02-18 Alexandre Duret-Lutz + + * src/tgbatest/ltl2tgba.cc: Simplify using + emptiness_check_instantiator. + * src/tgba/tgba.cc, src/tgba/tgba.hh + (tgba::number_of_acceptance_conditions): Return an unsigned. + * bench/emptchk/algorithms, bench/emptchk/README, + src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust + references to algorithms. + * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Quote + variables properly. + 2005-02-17 Alexandre Duret-Lutz * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc diff --git a/bench/emptchk/README b/bench/emptchk/README index 1f22c456e..29e3c77f5 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -176,20 +176,22 @@ This directory contains: ========================== Here are the short names for the algorithms used in the outputs. + ltl-*.sh tests use names from the left column, and pml-*.sh tests + use names from the right column. - Cou99 - Cou99_shy- - Cou99_shy - > Cou99_rem - > Cou99_rem_shy- - > Cou99_rem_shy - > CVWY90 - CVWY90_bsh - > GV04 - > SE05 - SE05_bsh - > Tau03 - > Tau03_opt + Cou99 Cou99 + Cou99_shy- Cou99(shy !group) + Cou99_shy Cou99(shy group) + > Cou99_rem Cou99(poprem) + > Cou99_rem_shy- Cou99(poprem shy !group) + > Cou99_rem_shy Cou99(poprem shy group) + > CVWY90 CVWY90 + CVWY90_bsh CVWY90(bsh=4K) + > GV04 GV04 + > SE05 SE05 + SE05_bsh SE05(bsh=4K) + > Tau03 Tau03 + > Tau03_opt Tau03_opt Only the algorithms marked with a `>' have been shown in the paper. `bsh' stands for `bit-state hashing'. @@ -197,7 +199,7 @@ This directory contains: `Cou99_rem*' algorithms are using the `rem' field to remove the SCC without recomputing the SCC as described in the paper. The other `Cou99*' algorithms are not. (Beware that in the paper - we showed the `Cou99_rem*' variants and called them `Cou99*'.) + we presented the `Cou99_rem*' variants and called them `Cou99*'.) The ltl-*.sh tests output look as follows: diff --git a/bench/emptchk/algorithms b/bench/emptchk/algorithms index be8d65906..f2f3085cc 100644 --- a/bench/emptchk/algorithms +++ b/bench/emptchk/algorithms @@ -1,9 +1,9 @@ Cou99 -Cou99_shy- -Cou99_shy -Cou99_rem -Cou99_rem_shy- -Cou99_rem_shy +Cou99(shy !group) +Cou99(shy group) +Cou99(poprem) +Cou99(poprem shy !group) +Cou99(poprem shy group) GV04 CVWY90 SE05 diff --git a/bench/emptchk/pml-clserv.sh b/bench/emptchk/pml-clserv.sh index 9f410f228..d5d1409a0 100644 --- a/bench/emptchk/pml-clserv.sh +++ b/bench/emptchk/pml-clserv.sh @@ -34,13 +34,13 @@ do echo " $model" echo "+++++++++++++++++++++" - cat $FORMULAE | + cat "$FORMULAE" | while read formula; do echo "-----------------------------------------------------------" # echo "### formula: $formula" - cat $ALGORITHMS | + cat "$ALGORITHMS" | while read algo; do - $LTL2TGBA -0 -e$algo $opts -Pmodels/$model "$formula" + "$LTL2TGBA" -0 -e"$algo" $opts -Pmodels/$model "$formula" done done done diff --git a/bench/emptchk/pml-eeaean.sh b/bench/emptchk/pml-eeaean.sh index 010cb96c2..82e51d35a 100644 --- a/bench/emptchk/pml-eeaean.sh +++ b/bench/emptchk/pml-eeaean.sh @@ -34,13 +34,13 @@ do echo " $model" echo "+++++++++++++++++++++" - cat $FORMULAE | + cat "$FORMULAE" | while read formula; do echo "-----------------------------------------------------------" echo "### formula: $formula" - cat $ALGORITHMS | + cat "$ALGORITHMS" | while read algo; do - $LTL2TGBA -0 -e$algo $opts -Pmodels/$model "$formula" + "$LTL2TGBA" -0 -e"$algo" $opts -Pmodels/$model "$formula" done done done diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index b9cb9009a..19a7383c1 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -76,13 +76,13 @@ namespace spot return ""; } - int + unsigned int tgba::number_of_acceptance_conditions() const { if (num_acc_ < 0) { bdd all = all_acceptance_conditions(); - int n = 0; + unsigned int n = 0; while (all != bddfalse) { ++n; diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 4de8344a2..78b12d921 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -188,7 +188,7 @@ namespace spot virtual bdd all_acceptance_conditions() const = 0; /// The number of acceptance conditions. - virtual int number_of_acceptance_conditions() const; + virtual unsigned int number_of_acceptance_conditions() const; /// \brief Return the conjuction of all negated acceptance /// variables. diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index a1df1b2e3..0666bd274 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -37,23 +37,23 @@ expect_ce() expect_ce_do -e -D "$1" expect_ce_do -e -f "$1" expect_ce_do -e -f -D "$1" - expect_ce_do -eCou99_shy "$1" - expect_ce_do -eCou99_shy -D "$1" - expect_ce_do -eCou99_shy -f "$1" - expect_ce_do -eCou99_shy -f -D "$1" + expect_ce_do -e'Cou99(shy)' "$1" + expect_ce_do -e'Cou99(shy)' -D "$1" + expect_ce_do -e'Cou99(shy)' -f "$1" + expect_ce_do -e'Cou99(shy)' -f -D "$1" expect_ce_do -eCVWY90 "$1" expect_ce_do -eCVWY90 -f "$1" - run 0 ./ltl2tgba -eCVWY90_bsh "$1" - run 0 ./ltl2tgba -eCVWY90_bsh -f "$1" + run 0 ./ltl2tgba -e'CVWY90(bsh=10M)' "$1" + run 0 ./ltl2tgba -e'CVWY90(bsh=10M)' -f "$1" run 0 ./ltl2tgba -eSE05 "$1" run 0 ./ltl2tgba -eSE05 -f "$1" - run 0 ./ltl2tgba -eSE05_bsh "$1" - run 0 ./ltl2tgba -eSE05_bsh -f "$1" + run 0 ./ltl2tgba -e'SE05(bsh=10M)' "$1" + run 0 ./ltl2tgba -e'SE05(bsh=10M)' -f "$1" run 0 ./ltl2tgba -eTau03_opt -f "$1" run 0 ./ltl2tgba -eGV04 -f "$1" # Expect multiple accepting runs - test `./ltl2tgba -eCVWY90_repeated "$1" | grep Prefix: | wc -l` -ge $2 - test `./ltl2tgba -eSE05_repeated "$1" | grep Prefix: | wc -l` -ge $2 + test `./ltl2tgba -e'CVWY90(repeated)' "$1" | grep Prefix: | wc -l` -ge $2 + test `./ltl2tgba -e'SE05(repeated)' "$1" | grep Prefix: | wc -l` -ge $2 } expect_no() @@ -62,23 +62,23 @@ expect_no() run 0 ./ltl2tgba -E -D "$1" run 0 ./ltl2tgba -E -f "$1" run 0 ./ltl2tgba -E -f -D "$1" - run 0 ./ltl2tgba -ECou99_shy "$1" - run 0 ./ltl2tgba -ECou99_shy -D "$1" - run 0 ./ltl2tgba -ECou99_shy -f "$1" - run 0 ./ltl2tgba -ECou99_shy -f -D "$1" + run 0 ./ltl2tgba -E'Cou99(shy)' "$1" + run 0 ./ltl2tgba -E'Cou99(shy)' -D "$1" + run 0 ./ltl2tgba -E'Cou99(shy)' -f "$1" + run 0 ./ltl2tgba -E'Cou99(shy)' -f -D "$1" run 0 ./ltl2tgba -ECVWY90 "$1" run 0 ./ltl2tgba -ECVWY90 -f "$1" - run 0 ./ltl2tgba -ECVWY90_bsh "$1" - run 0 ./ltl2tgba -ECVWY90_bsh -f "$1" + run 0 ./ltl2tgba -E'CVWY90(bsh=10M)' "$1" + run 0 ./ltl2tgba -E'CVWY90(bsh=10M)' -f "$1" run 0 ./ltl2tgba -ESE05 "$1" run 0 ./ltl2tgba -ESE05 -f "$1" - run 0 ./ltl2tgba -ESE05_bsh "$1" - run 0 ./ltl2tgba -ESE05_bsh -f "$1" + run 0 ./ltl2tgba -E'SE05(bsh=10M)' "$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 -eCVWY90_repeated "!($1)" | + test `./ltl2tgba -e'CVWY90(repeated)' "!($1)" | grep Prefix: | wc -l` -ge $2 - test `./ltl2tgba -eSE05_repeated "!($1)" | + test `./ltl2tgba -e'SE05(repeated)' "!($1)" | grep Prefix: | wc -l` -ge $2 } diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 5503e6b59..d4858a2a2 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -29,8 +29,8 @@ expect_ce() { run 0 ./ltl2tgba -e -X "$1" run 0 ./ltl2tgba -e -D -X "$1" - run 0 ./ltl2tgba -eCou99_shy -X "$1" - run 0 ./ltl2tgba -eCou99_shy -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" } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 260de9426..a1272d194 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -38,14 +38,7 @@ #include "tgbaalgos/lbtt.hh" #include "tgba/tgbatba.hh" #include "tgba/tgbaproduct.hh" -#include "tgbaalgos/gv04.hh" -#include "tgbaalgos/magic.hh" #include "tgbaalgos/reducerun.hh" -#include "tgbaalgos/se05.hh" -#include "tgbaalgos/tau03.hh" -#include "tgbaalgos/tau03opt.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/gtec/ce.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/neverclaim.hh" @@ -133,27 +126,12 @@ syntax(char* prog) << "(implies -f)" << std::endl << std::endl << "Where ALGO should be one of:" << std::endl - << " Cou99 (the default)" << std::endl - << " Cou99_shy-" << std::endl - << " Cou99_shy" << std::endl - << " Cou99_rem" << std::endl - << " Cou99_rem_shy-" << std::endl - << " Cou99_rem_shy" << std::endl - << " CVWY90" << std::endl - << " CVWY90_repeated" << std::endl - << " CVWY90_bsh[(heap size in Mo - 10Mo by default)]" - << std::endl - << " CVWY90_bsh_repeated[(heap size in MB - 10MB" - << " by default)]" << std::endl - << " GV04" << std::endl - << " SE05" << std::endl - << " SE05_repeated" << std::endl - << " SE05_bsh[(heap size in MB - 10MB by default)]" - << std::endl - << " SE05_bsh_repeated[(heap size in MB - 10MB" - << " by default)]" << std::endl - << " Tau03" << std::endl - << " Tau03_opt" << std::endl; + << " Cou99(OPTIONS) (the default)" << std::endl + << " CVWY90(OPTIONS)" << std::endl + << " GV04(OPTIONS)" << std::endl + << " SE05(OPTIONS)" << std::endl + << " Tau03(OPTIONS)" << std::endl + << " Tau03_opt(OPTIONS)" << std::endl; exit(2); } @@ -165,22 +143,15 @@ main(int argc, char** argv) bool debug_opt = false; bool paper_opt = false; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; - bool degeneralize_maybe = false; bool fm_opt = false; bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; bool file_opt = false; int output = 0; int formula_index = 0; - std::string echeck_algo; - enum { None, Couvreur, Couvreur2, MagicSearch, Se05Search, - Tau03Search, Tau03OptSearch, Gv04 } echeck = None; + const char* echeck_algo = 0; + spot::emptiness_check_instantiator* echeck_inst = 0; enum { NoneDup, BFS, DFS } dupexp = NoneDup; - bool couv_group = true; - bool poprem = false; - bool search_many = false; - bool bit_state_hashing = false; - int heap_size = 10*1024*1024; bool expect_counter_example = false; bool from_file = false; int reduc_aut = spot::Reduce_None; @@ -237,29 +208,37 @@ main(int argc, char** argv) } else if (!strncmp(argv[formula_index], "-e", 2)) { - if (argv[formula_index][2] != 0) - { - char *p = strchr(argv[formula_index], '('); - if (p && sscanf(p+1, "%d)", &heap_size) == 1) - *p = '\0'; - echeck_algo = argv[formula_index] + 2; - } - else - echeck_algo = "Cou99"; + echeck_algo = 2 + argv[formula_index]; + if (!*echeck_algo) + echeck_algo = "Cou99"; + + const char* err; + echeck_inst = + spot::emptiness_check_instantiator::construct(echeck_algo, &err); + if (!echeck_inst) + { + std::cerr << "Failed to parse argument of -e near `" + << err << "'" << std::endl; + exit(2); + } expect_counter_example = true; output = -1; } else if (!strncmp(argv[formula_index], "-E", 2)) { - if (argv[formula_index][2] != 0) - { - char *p = strchr(argv[formula_index], '('); - if (p && sscanf(p+1, "%d)", &heap_size) == 1) - *p = '\0'; - echeck_algo = argv[formula_index] + 2; - } - else - echeck_algo = "Cou99"; + const char* echeck_algo = 2 + argv[formula_index]; + if (!*echeck_algo) + echeck_algo = "Cou99"; + + const char* err; + echeck_inst = + spot::emptiness_check_instantiator::construct(echeck_algo, &err); + if (!echeck_inst) + { + std::cerr << "Failed to parse argument of -e near `" + << err << "'" << std::endl; + exit(2); + } expect_counter_example = false; output = -1; } @@ -416,109 +395,8 @@ main(int argc, char** argv) } } - if (echeck_algo != "") - { - if (echeck_algo == "Cou99") - { - echeck = Couvreur; - } - else if (echeck_algo == "Cou99_shy") - { - echeck = Couvreur2; - couv_group = true; - } - else if (echeck_algo == "Cou99_shy-") - { - echeck = Couvreur2; - couv_group = false; - } - else if (echeck_algo == "Cou99_rem") - { - echeck = Couvreur; - poprem = true; - } - else if (echeck_algo == "Cou99_rem_shy") - { - echeck = Couvreur2; - couv_group = true; - poprem = true; - } - else if (echeck_algo == "Cou99_rem_shy-") - { - echeck = Couvreur2; - couv_group = false; - poprem = true; - } - else if (echeck_algo == "CVWY90") - { - echeck = MagicSearch; - degeneralize_maybe = true; - } - else if (echeck_algo == "CVWY90_repeated") - { - echeck = MagicSearch; - degeneralize_maybe = true; - search_many = true; - } - else if (echeck_algo == "CVWY90_bsh") - { - echeck = MagicSearch; - degeneralize_maybe = true; - bit_state_hashing = true; - } - else if (echeck_algo == "CVWY90_bsh_repeated") - { - echeck = MagicSearch; - degeneralize_maybe = true; - bit_state_hashing = true; - search_many = true; - } - else if (echeck_algo == "SE05") - { - echeck = Se05Search; - degeneralize_maybe = true; - } - else if (echeck_algo == "SE05_repeated") - { - echeck = Se05Search; - degeneralize_maybe = true; - search_many = true; - } - else if (echeck_algo == "SE05_bsh") - { - echeck = Se05Search; - degeneralize_maybe = true; - bit_state_hashing = true; - } - else if (echeck_algo == "SE05_bsh_repeated") - { - echeck = Se05Search; - degeneralize_maybe = true; - bit_state_hashing = true; - search_many = true; - } - else if (echeck_algo == "Tau03") - { - echeck = Tau03Search; - } - else if (echeck_algo == "Tau03_opt") - { - echeck = Tau03OptSearch; - } - else if (echeck_algo == "GV04") - { - echeck = Gv04; - degeneralize_maybe = true; - } - else - { - std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl; - syntax(argv[0]); - } - } - if ((graph_run_opt || graph_run_tgba_opt) - && (echeck_algo == "" || !expect_counter_example)) + && (!echeck_inst || !expect_counter_example)) { std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl; exit(1); @@ -601,9 +479,11 @@ main(int argc, char** argv) spot::tgba_tba_proxy* degeneralized = 0; - if (degeneralize_maybe + unsigned int n_acc = a->number_of_acceptance_conditions(); + if (echeck_inst && degeneralize_opt == NoDegen - && a->number_of_acceptance_conditions() > 1) + && n_acc > 1 + && echeck_inst->max_acceptance_conditions() < n_acc) degeneralize_opt = DegenTBA; if (degeneralize_opt == DegenTBA) a = degeneralized = new spot::tgba_tba_proxy(a); @@ -681,9 +561,12 @@ main(int argc, char** argv) if (system) { a = product = product_to_free = new spot::tgba_product(system, a); - if (degeneralize_maybe - && degeneralize_opt == NoDegen - && product->number_of_acceptance_conditions() > 1) + + unsigned int n_acc = a->number_of_acceptance_conditions(); + if (echeck_inst + && degeneralize_opt == NoDegen + && n_acc > 1 + && echeck_inst->max_acceptance_conditions() < n_acc) degeneralize_opt = DegenTBA; if (degeneralize_opt == DegenTBA) a = product = product_degeneralized = @@ -693,6 +576,24 @@ main(int argc, char** argv) new spot::tgba_sba_proxy(product); } + if (echeck_inst + && (a->number_of_acceptance_conditions() + < echeck_inst->min_acceptance_conditions())) + { + if (!paper_opt) + { + std::cerr << echeck_algo << " requires at least " + << echeck_inst->min_acceptance_conditions() + << " acceptance conditions." << std::endl; + exit(1); + } + else + { + std::cout << std::endl; + exit(0); + } + } + switch (output) { case -1: @@ -744,70 +645,18 @@ main(int argc, char** argv) assert(!"unknown output option"); } - spot::option_map o; - o.set("poprem", poprem); - o.set("group", couv_group); - - spot::emptiness_check* ec = 0; - switch (echeck) - { - case None: - break; - - case Couvreur: - ec = new spot::couvreur99_check(a, o); - break; - - case Couvreur2: - ec = new spot::couvreur99_check_shy(a, o); - break; - - case MagicSearch: - if (bit_state_hashing) - ec = spot::bit_state_hashing_magic_search(a, heap_size); - else - ec = spot::explicit_magic_search(a); - break; - - case Se05Search: - if (bit_state_hashing) - ec = spot::bit_state_hashing_se05_search(a, heap_size); - else - ec = spot::explicit_se05_search(a); - break; - - case Tau03Search: - if (a->number_of_acceptance_conditions() == 0) - { - if (!paper_opt) - std::cout << "To apply Tau03, the automaton must have at" - << " least one accepting condition. Try with another" - << " algorithm." << std::endl; - else - std::cout << std::endl; - } - else - { - ec = spot::explicit_tau03_search(a); - } - break; - case Tau03OptSearch: - ec = spot::explicit_tau03_opt_search(a); - break; - case Gv04: - ec = spot::explicit_gv04_check(a); - break; - } - - if (ec) + if (echeck_inst) { + spot::emptiness_check* ec = echeck_inst->instantiate(a); + bool search_many = echeck_inst->options().get("repeated"); + assert(ec); do { spot::emptiness_check_result* res = ec->check(); if (paper_opt) { std::ios::fmtflags old = std::cout.flags(); - std::cout << std::left << std::setw(20) + std::cout << std::left << std::setw(25) << echeck_algo << ", "; spot::tgba_statistics a_size = spot::stats_reachable(ec->automaton()); @@ -841,17 +690,17 @@ main(int argc, char** argv) if (!graph_run_opt && !graph_run_tgba_opt) ec->print_stats(std::cout); if (expect_counter_example != !!res && - (!bit_state_hashing || !expect_counter_example)) + (!expect_counter_example || ec->safe())) exit_code = 1; if (!res) { std::cout << "no accepting run found"; - if (bit_state_hashing && expect_counter_example) + if (!ec->safe() && expect_counter_example) { std::cout << " even if expected" << std::endl; - std::cout << "this is maybe due to the use of the bit" - << " state hashing technic" << std::endl; + std::cout << "this may be due to the use of the bit" + << " state hashing technique" << std::endl; std::cout << "you can try to increase the heap size " << "or use an explicit storage" << std::endl; @@ -913,6 +762,7 @@ main(int argc, char** argv) delete degeneralized; delete aut_red; delete to_free; + delete echeck_inst; } else {