From bacd5a0ac2f72dbcabc726f3bee0401a6d686e70 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Jun 2003 12:02:36 +0000 Subject: [PATCH] * src/tgba/bddprint.cc (print_handler): Quote promises when !want_prom. * src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or identifiers. Discard empty strings. * src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod. (mixprod_SOURCES): New variable. (TESTS): Add mixprod.test. --- ChangeLog | 11 ++++++++ src/tgba/bddprint.cc | 13 +++++++--- src/tgbaparse/tgbaparse.yy | 10 ++++--- src/tgbatest/.cvsignore | 1 + src/tgbatest/Makefile.am | 10 +++++-- src/tgbatest/mixprod.cc | 53 ++++++++++++++++++++++++++++++++++++++ src/tgbatest/mixprod.test | 24 +++++++++++++++++ 7 files changed, 112 insertions(+), 10 deletions(-) create mode 100644 src/tgbatest/mixprod.cc create mode 100755 src/tgbatest/mixprod.test diff --git a/ChangeLog b/ChangeLog index 1506606f1..105866bca 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2003-06-18 Alexandre Duret-Lutz + + * src/tgba/bddprint.cc (print_handler): Quote promises + when !want_prom. + * src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or + identifiers. Discard empty strings. + * src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file. + * src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod. + (mixprod_SOURCES): New variable. + (TESTS): Add mixprod.test. + 2003-06-17 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 0c7996024..22e70345a 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -25,10 +25,15 @@ namespace spot if (isi != dict->prom_formula_map.end()) { if (want_prom) - o << "Prom["; - to_string(isi->second, o); - if (want_prom) - o << "]"; + { + o << "Prom["; + to_string(isi->second, o) << "]"; + } + else + { + o << "\""; + to_string(isi->second, o) << "\""; + } } else { diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index 15af160e7..fdeb9e9ae 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -69,15 +69,17 @@ prop_list: { $$ = new std::list; } - | prop_list IDENT + | prop_list strident { - $1->push_back(pair(false, parse_environment.require(*$2))); + if (*$2 != "") + $1->push_back(pair(false, parse_environment.require(*$2))); delete $2; $$ = $1; } - | prop_list '!' IDENT + | prop_list '!' strident { - $1->push_back(pair(true, parse_environment.require(*$3))); + if (*$3 != "") + $1->push_back(pair(true, parse_environment.require(*$3))); delete $3; $$ = $1; } diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore index 096d7bc17..b74d25e91 100644 --- a/src/tgbatest/.cvsignore +++ b/src/tgbatest/.cvsignore @@ -13,3 +13,4 @@ explprod *.ps *.dot tripprod +mixprod diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e3e9c85b9..0e4fe37b3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -11,18 +11,23 @@ check_PROGRAMS = \ ltlprod \ bddprod \ explprod \ - tripprod + tripprod \ + mixprod +# Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT explicit_SOURCES = explicit.cc explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc +mixprod_SOURCES = mixprod.cc readsave_SOURCES = readsave.cc tgbaread_SOURCES = tgbaread.cc tripprod_SOURCES = tripprod.cc +# Keep this sorted by STRENGTH. Test basic things first, +# because such failures will be easier to diagnose and fix. TESTS = \ explicit.test \ tgbaread.test \ @@ -31,7 +36,8 @@ TESTS = \ ltlprod.test \ bddprod.test \ explprod.test \ - tripprod.test + tripprod.test \ + mixprod.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc new file mode 100644 index 000000000..910a7348e --- /dev/null +++ b/src/tgbatest/mixprod.cc @@ -0,0 +1,53 @@ +#include +#include +#include "ltlvisit/destroy.hh" +#include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgba/ltl2tgba.hh" +#include "tgba/tgbaproduct.hh" +#include "tgba/tgbabddconcreteproduct.hh" +#include "tgbaparse/public.hh" +#include "tgbaalgos/save.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " formula file" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc != 3) + syntax(argv[0]); + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + + spot::ltl::parse_error_list pel1; + spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); + if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1)) + return 2; + + spot::tgba_parse_error_list pel2; + spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env); + if (spot::format_tgba_parse_errors(std::cerr, pel2)) + return 2; + + { + spot::tgba_bdd_concrete a1 = spot::ltl_to_tgba(f1); + spot::ltl::destroy(f1); + spot::tgba_product p(a1, *a2); + + spot::tgba_save_reachable(std::cout, p); + } + + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + delete a2; + assert(spot::ltl::atomic_prop::instance_count() == 0); + return exit_code; +} diff --git a/src/tgbatest/mixprod.test b/src/tgbatest/mixprod.test new file mode 100755 index 000000000..cb094b0fb --- /dev/null +++ b/src/tgbatest/mixprod.test @@ -0,0 +1,24 @@ +#!/bin/sh + +. ./defs + +set -e + +# We don't check the output, but just running this might be enough to +# trigger assertions or I/O errors. + +cat >input1 <stdout +cat stdout + +# Make sure we can read the produced output + +./mixprod 'G!a' stdout + +rm input1 stdout