From 7b5f80d46d5f631353d2fdbfee891df5b2cb26f9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 31 Jan 2015 17:49:02 +0100 Subject: [PATCH] tgbatest: get rid of tgbaread since it's only purpose is to test a parser we want to get rid of (#1) * src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: Delete. * src/tgbatest/Makefile.am: Adjust. --- src/tgbatest/Makefile.am | 5 +-- src/tgbatest/tgbaread.cc | 76 -------------------------------------- src/tgbatest/tgbaread.test | 57 ---------------------------- 3 files changed, 1 insertion(+), 137 deletions(-) delete mode 100644 src/tgbatest/tgbaread.cc delete mode 100755 src/tgbatest/tgbaread.test diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 359f92508..7a5e82431 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -44,8 +44,7 @@ check_PROGRAMS = \ maskacc \ powerset \ readsat \ - taatgba \ - tgbaread + taatgba # Keep this sorted alphabetically. acc_SOURCES = acc.cc @@ -65,7 +64,6 @@ powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc readsat_SOURCES = readsat.cc taatgba_SOURCES = taatgba.cc -tgbaread_SOURCES = tgbaread.cc # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. @@ -75,7 +73,6 @@ TESTS = \ bitvect.test \ ltlcross3.test \ taatgba.test \ - tgbaread.test \ renault.test \ nondet.test \ det.test \ diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc deleted file mode 100644 index c519eeb89..000000000 --- a/src/tgbatest/tgbaread.cc +++ /dev/null @@ -1,76 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include -#include -#include "tgbaparse/public.hh" -#include "tgbaalgos/dotty.hh" -#include "ltlast/allnodes.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " [-d] filename" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - if (argc < 2) - syntax(argv[0]); - - { - bool debug = false; - int filename_index = 1; - - if (!strcmp(argv[1], "-d")) - { - debug = true; - if (argc < 3) - syntax(argv[0]); - filename_index = 2; - } - - auto dict = spot::make_bdd_dict(); - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::tgba_parse_error_list pel; - auto a = spot::tgba_parse(argv[filename_index], pel, dict, env, debug); - - if (spot::format_tgba_parse_errors(std::cerr, argv[filename_index], pel)) - return 2; - - if (a) - spot::dotty_reachable(std::cout, a); - else - return 1; - } - - assert(spot::ltl::atomic_prop::instance_count() == 0); - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - return 0; -} diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test deleted file mode 100755 index d34dd0723..000000000 --- a/src/tgbatest/tgbaread.test +++ /dev/null @@ -1,57 +0,0 @@ -#!/bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2009, 2014, 2015 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - - -. ./defs - -set -e - -cat >input < stdout - -cat >expected < 0 - 0 [label="0"] - 0 -> 1 [label="a & !b\n{0,1}"] - 1 [label="1"] - 1 -> 2 [label="a\n{0}"] - 2 [label="2"] - 2 -> 0 [label="1"] -} -EOF - -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout -diff stdout expected - -rm input stdout expected