alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[lbtt] Fix issues reported by Clang++ 3.1.

Browse source 
* src/Graph.h.in (PathElement::hasEdge): Check the correct
pointer, not the address of some member function.
* src/BuchiAutomaton.cc, src/Configuration.cc,
src/TestOperations.cc, src/TestOperations.h: Recode these files in
utf-8.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-27 18:07:42 +02:00
parent 141baae57e
commit 3793454864
7 changed files with 76 additions and 62 deletions
Download patch file Download diff file Expand all files Collapse all files

10
lbtt/ChangeLog
View file

@ -1,3 +1,13 @@
2012-06-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix issues reported by Clang++ 3.1.
* src/Graph.h.in (PathElement::hasEdge): Check the correct
pointer, not the address of some member function.
* src/BuchiAutomaton.cc, src/Configuration.cc,
src/TestOperations.cc, src/TestOperations.hh: Recode these files in
utf-8.
2012-06-19 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2012-06-19 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Adjust parsers to accommodate old and new versions of Automake. Adjust parsers to accommodate old and new versions of Automake.

2
lbtt/NEWS
View file

@ -22,7 +22,7 @@ Copyright (C) 2008 Heikki Tauriainen
Version 1.2.1a Version 1.2.1a
* Fix compilation with newer versions of Bison. * Fix compilation with newer versions of Bison.
* Fix compilation on Intel's icpc, and with recent version of G++. * Fix compilation on Intel's icpc, and recent version of G++ and Clang++.
* Fix compilation with newer versions of Automake. * Fix compilation with newer versions of Automake.
* Fix construction of manual ("make dvi" and "make pdf") for recent * Fix construction of manual ("make dvi" and "make pdf") for recent
version of texinfo. version of texinfo.

23
lbtt/src/BuchiAutomaton.cc
View file

@ -1,4 +1,5 @@
/* /* -*- coding: utf-8 -*-
*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
@ -199,7 +200,7 @@ void BuchiAutomaton::read(istream& input_stream)
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Reads an automaton description (which may represent a * Description: Reads an automaton description (which may represent a
* generalized Büchi automaton) from a stream and stores it * generalized Büchi automaton) from a stream and stores it
* into the automaton object. * into the automaton object.
* *
* Argument: input_stream -- A reference to an input stream. * Argument: input_stream -- A reference to an input stream.
@ -216,7 +217,7 @@ void BuchiAutomaton::read(istream& input_stream)
try try
{ {
/* Read the number of states in the generalized Büchi automaton. */ /* Read the number of states in the generalized Büchi automaton. */
einput_stream >> number_of_states; einput_stream >> number_of_states;
@ -275,8 +276,8 @@ void BuchiAutomaton::read(istream& input_stream)
BitArray acc_sets(number_of_acceptance_sets); BitArray acc_sets(number_of_acceptance_sets);
/* /*
* Allocate space for the regular Büchi automaton that will be constructed * Allocate space for the regular Büchi automaton that will be constructed
* from the generalized Büchi automaton. * from the generalized Büchi automaton.
*/ */
nodes.reserve(number_of_states); nodes.reserve(number_of_states);
@ -352,7 +353,7 @@ void BuchiAutomaton::read(istream& input_stream)
if (state_mapping.second >= number_of_states) if (state_mapping.second >= number_of_states)
throw AutomatonParseException("number of different state " throw AutomatonParseException("number of different state "
"identifiers does not match the size" "identifiers does not match the size"
" of the Büchi automaton"); " of the Büchi automaton");
current_state = state_mapping.second; current_state = state_mapping.second;
state_mapping.second++; state_mapping.second++;
@ -440,7 +441,7 @@ void BuchiAutomaton::read(istream& input_stream)
if (state_mapping.second >= number_of_states) if (state_mapping.second >= number_of_states)
throw AutomatonParseException("number of different state " throw AutomatonParseException("number of different state "
"identifiers does not match the size" "identifiers does not match the size"
" of the Büchi automaton"); " of the Büchi automaton");
neighbor_state = state_mapping.second; neighbor_state = state_mapping.second;
state_mapping.second++; state_mapping.second++;
@ -548,7 +549,7 @@ void BuchiAutomaton::print
if (nodes.empty()) if (nodes.empty())
{ {
if (fmt == NORMAL) if (fmt == NORMAL)
estream << string(indent, ' ') + "The Büchi automaton is empty.\n"; estream << string(indent, ' ') + "The Büchi automaton is empty.\n";
} }
else else
{ {
@ -558,7 +559,7 @@ void BuchiAutomaton::print
pair<size_type, unsigned long int> reachable_part_statistics pair<size_type, unsigned long int> reachable_part_statistics
= subgraphStats(initial_state); = subgraphStats(initial_state);
estream << string(indent, ' ') + "The Büchi automaton consists of\n" estream << string(indent, ' ') + "The Büchi automaton consists of\n"
+ string(indent + 4, ' ') + string(indent + 4, ' ')
<< statistics.first << statistics.first
<< " states and\n" + string(indent + 4, ' ') << " states and\n" + string(indent + 4, ' ')
@ -734,7 +735,7 @@ void BuchiAutomaton::BuchiTransition::print
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Writes information about a transition between two states of * Description: Writes information about a transition between two states of
* a Büchi automaton. * a Büchi automaton.
* *
* Arguments: stream -- A reference to an output * Arguments: stream -- A reference to an output
* stream. * stream.
@ -820,7 +821,7 @@ void BuchiAutomaton::BuchiState::print
const unsigned long int number_of_acceptance_sets) const const unsigned long int number_of_acceptance_sets) const
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Writes information about a state of a Büchi automaton. * Description: Writes information about a state of a Büchi automaton.
* *
* Arguments: stream -- A reference to an output * Arguments: stream -- A reference to an output
* stream. * stream.

7
lbtt/src/Configuration.cc
View file

@ -1,4 +1,5 @@
/* /* -*- coding: utf-8 -*-
*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
@ -1048,7 +1049,7 @@ void Configuration::print(ostream& stream, int indent) const
"Model checking result consistency check\n"; "Model checking result consistency check\n";
if (global_options.do_intr_test) if (global_options.do_intr_test)
estream << string(indent + 4, ' ') + estream << string(indent + 4, ' ') +
"Büchi automata intersection emptiness check\n"; "Büchi automata intersection emptiness check\n";
} }
else else
estream << "All automata correctness tests disabled.\n"; estream << "All automata correctness tests disabled.\n";
@ -1396,7 +1397,7 @@ void Configuration::showCommandLineHelp(const char* program_name)
"(`always', `onerror', \n" "(`always', `onerror', \n"
" `never', `onbreak')\n" " `never', `onbreak')\n"
" --intersectiontest[=VALUE], --nointersectiontest\n" " --intersectiontest[=VALUE], --nointersectiontest\n"
" Enable or disable the Büchi " " Enable or disable the Büchi "
"automata\n" "automata\n"
" intersection emptiness test\n" " intersection emptiness test\n"
" --localmodelcheck Use local model checking in tests" " --localmodelcheck Use local model checking in tests"

2
lbtt/src/Graph.h.in
View file

@ -1616,7 +1616,7 @@ inline bool Graph<EdgeContainer>::PathElement::hasEdge() const
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
return (edge != 0); return edge_pointer != 0;
} }
/* ========================================================================= */ /* ========================================================================= */

45
lbtt/src/TestOperations.cc
View file

@ -1,4 +1,5 @@
/* /* -*- coding: utf-8 -*-
*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
@ -830,12 +831,12 @@ void generateBuchiAutomaton
* *
* Description: Constructs a BuchiAutomaton by invoking an external program * Description: Constructs a BuchiAutomaton by invoking an external program
* that will perform the conversion of a LTL formula (stored * that will perform the conversion of a LTL formula (stored
* into a file) into a Büchi automaton. * into a file) into a Büchi automaton.
* *
* Arguments: f -- Indicates the formula to be converted into * Arguments: f -- Indicates the formula to be converted into
* an automaton. 0 corresponds to the positive * an automaton. 0 corresponds to the positive
* and 1 to the negated formula. * and 1 to the negated formula.
* algorithm_id -- Identifier of the LTL-to-Büchi translator * algorithm_id -- Identifier of the LTL-to-Büchi translator
* to use. * to use.
* *
* Returns: Nothing. The result is stored in * Returns: Nothing. The result is stored in
@ -850,10 +851,10 @@ void generateBuchiAutomaton
= test_results[algorithm_id].automaton_stats[f]; = test_results[algorithm_id].automaton_stats[f];
if (automaton_stats.buchiAutomatonComputed()) if (automaton_stats.buchiAutomatonComputed())
printText("Büchi automaton (cached):\n", 3, 8); printText("Büchi automaton (cached):\n", 3, 8);
else else
{ {
printText("Büchi automaton:\n", 3, 8); printText("Büchi automaton:\n", 3, 8);
const Configuration::AlgorithmInformation& algorithm const Configuration::AlgorithmInformation& algorithm
= configuration.algorithms[algorithm_id]; = configuration.algorithms[algorithm_id];
@ -910,7 +911,7 @@ void generateBuchiAutomaton
/* Execute the external program. */ /* Execute the external program. */
if (!printText("<executing translator>", 5, 10)) if (!printText("<executing translator>", 5, 10))
printText("<computing Büchi automaton>", 4, 10); printText("<computing Büchi automaton>", 4, 10);
int error_number; int error_number;
int error_pipe[2]; /* used for communicating errors in exec() */ int error_pipe[2]; /* used for communicating errors in exec() */
@ -1201,7 +1202,7 @@ void generateBuchiAutomaton
printText("\n\n", 1); printText("\n\n", 1);
if (round_info.transcript_file.is_open()) if (round_info.transcript_file.is_open())
writeToTranscript("User break while generating Büchi automaton (" writeToTranscript("User break while generating Büchi automaton ("
+ configuration.algorithmString(algorithm_id) + configuration.algorithmString(algorithm_id)
+ ", " + ", "
+ (f == 0 ? "posi" : "nega") + "tive formula)\n"); + (f == 0 ? "posi" : "nega") + "tive formula)\n");
@ -1210,7 +1211,7 @@ void generateBuchiAutomaton
} }
if (round_info.transcript_file.is_open()) if (round_info.transcript_file.is_open())
writeToTranscript("Büchi automaton generation failed (" writeToTranscript("Büchi automaton generation failed ("
+ configuration.algorithmString(algorithm_id) + configuration.algorithmString(algorithm_id)
+ ", " + ", "
+ (f == 0 ? "posi" : "nega") + (f == 0 ? "posi" : "nega")
@ -1308,7 +1309,7 @@ void generateBuchiAutomaton
if (translator_process != 0) /* fatal error, lbtt should be terminated */ if (translator_process != 0) /* fatal error, lbtt should be terminated */
throw Exception throw Exception
("fatal internal error while generating Büchi automaton"); ("fatal internal error while generating Büchi automaton");
throw BuchiAutomatonGenerationException(); throw BuchiAutomatonGenerationException();
} }
@ -1342,7 +1343,7 @@ void generateBuchiAutomaton
= automaton_stats.buchi_automaton->isDeterministic(); = automaton_stats.buchi_automaton->isDeterministic();
/* /*
* Update Büchi automaton statistics for the given algorithm. * Update Büchi automaton statistics for the given algorithm.
*/ */
final_statistics[algorithm_id].total_number_of_buchi_states[f] final_statistics[algorithm_id].total_number_of_buchi_states[f]
@ -1378,14 +1379,14 @@ void performEmptinessCheck
* *
* Description: Performs the emptiness check on a ProductAutomaton, i.e., * Description: Performs the emptiness check on a ProductAutomaton, i.e.,
* finds the states of the original state space from which an * finds the states of the original state space from which an
* accepting cycle of the Büchi automaton can be reached. * accepting cycle of the Büchi automaton can be reached.
* *
* Arguments: f -- Indicates the formula originally used for * Arguments: f -- Indicates the formula originally used for
* constructing the given product automaton. * constructing the given product automaton.
* 0 corresponds to the automaton obtained * 0 corresponds to the automaton obtained
* from the positive, 1 to the one obtained * from the positive, 1 to the one obtained
* from the negated formula. * from the negated formula.
* algorithm_id -- Identifier of the LTL-to-Büchi translator * algorithm_id -- Identifier of the LTL-to-Büchi translator
* originally used for generating the given * originally used for generating the given
* product automaton. * product automaton.
* *
@ -1503,7 +1504,7 @@ void performConsistencyCheck
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Checks the model checking results for consistency for a * Description: Checks the model checking results for consistency for a
* particular LTL-to-Büchi conversion algorithm implementation, * particular LTL-to-Büchi conversion algorithm implementation,
* i.e., verifies that the model checking results for a formula * i.e., verifies that the model checking results for a formula
* and its negation are not contradictory. * and its negation are not contradictory.
* *
@ -1576,7 +1577,7 @@ void compareResults()
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Compares the model checking results obtained using different * Description: Compares the model checking results obtained using different
* LTL->Büchi conversion algorithm implementations with each * LTL->Büchi conversion algorithm implementations with each
* other. * other.
* *
* Arguments: None. * Arguments: None.
@ -1685,7 +1686,7 @@ void compareResults()
void performBuchiIntersectionCheck() void performBuchiIntersectionCheck()
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Tests the intersection of the Büchi automata constructed for * Description: Tests the intersection of the Büchi automata constructed for
* the formula and its negation for emptiness. * the formula and its negation for emptiness.
* *
* Arguments: None. * Arguments: None.
@ -1694,10 +1695,10 @@ void performBuchiIntersectionCheck()
* *
* ------------------------------------------------------------------------- */ * ------------------------------------------------------------------------- */
{ {
if (printText("Büchi automata intersection emptiness check:\n", 3, 4)) if (printText("Büchi automata intersection emptiness check:\n", 3, 4))
printText("<checking Büchi automata intersections for emptiness>\n", 4, 6); printText("<checking Büchi automata intersections for emptiness>\n", 4, 6);
else else
printText("Checking Büchi automata intersections for emptiness", 2, 4); printText("Checking Büchi automata intersections for emptiness", 2, 4);
bool result = true; bool result = true;
@ -1726,7 +1727,7 @@ void performBuchiIntersectionCheck()
8); 8);
/* /*
* Compute the intersection of two Büchi automata constructed for * Compute the intersection of two Büchi automata constructed for
* the positive and the negative formula, respectively. * the positive and the negative formula, respectively.
*/ */
@ -1802,7 +1803,7 @@ void performBuchiIntersectionCheck()
if (round_info.transcript_file.is_open()) if (round_info.transcript_file.is_open())
{ {
writeToTranscript("User break during Büchi automata intersection " writeToTranscript("User break during Büchi automata intersection "
"emptiness check"); "emptiness check");
round_info.transcript_file << string(8, ' ') + "(+) " round_info.transcript_file << string(8, ' ') + "(+) "
+ configuration.algorithmString(alg_1) + configuration.algorithmString(alg_1)
@ -1850,7 +1851,7 @@ void performBuchiIntersectionCheck()
if (round_info.transcript_file.is_open()) if (round_info.transcript_file.is_open())
{ {
writeToTranscript("Out of memory during Büchi automata " writeToTranscript("Out of memory during Büchi automata "
"intersection emptiness check"); "intersection emptiness check");
round_info.transcript_file << string(8, ' ') + "(+) " round_info.transcript_file << string(8, ' ') + "(+) "
+ configuration.algorithmString(alg_1) + configuration.algorithmString(alg_1)
@ -1871,7 +1872,7 @@ void performBuchiIntersectionCheck()
if (round_info.transcript_file.is_open()) if (round_info.transcript_file.is_open())
{ {
writeToTranscript("Büchi automata intersection emptiness check failed"); writeToTranscript("Büchi automata intersection emptiness check failed");
printBuchiIntersectionCheckStats printBuchiIntersectionCheckStats
(round_info.transcript_file, 8, algorithms); (round_info.transcript_file, 8, algorithms);
round_info.transcript_file << '\n'; round_info.transcript_file << '\n';

15
lbtt/src/TestOperations.h
View file

@ -1,4 +1,5 @@
/* /* -*- coding: utf-8 -*-
*
* Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005 * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004, 2005
* Heikki Tauriainen <Heikki.Tauriainen@tkk.fi> * Heikki Tauriainen <Heikki.Tauriainen@tkk.fi>
* *
@ -93,11 +94,11 @@ void verifyFormulaOnPath(); /* Evaluates the LTL
void writeFormulaeToFiles(); /* Writes LTL formulas */ void writeFormulaeToFiles(); /* Writes LTL formulas */
/* into a file. */ /* into a file. */
void generateBuchiAutomaton /* Generates a Büchi */ void generateBuchiAutomaton /* Generates a Büchi */
(int f, /* automaton from a LTL */ (int f, /* automaton from a LTL */
vector<Configuration::AlgorithmInformation> /* formula stored in a */ vector<Configuration::AlgorithmInformation> /* formula stored in a */
::size_type /* given file, using a */ ::size_type /* given file, using a */
algorithm_id); /* given LTL-to-Büchi algorithm_id); /* given LTL-to-Büchi
* translation algorithm * translation algorithm
* for the conversion. * for the conversion.
*/ */
@ -118,7 +119,7 @@ void performConsistencyCheck /* Performs a */
void compareResults(); /* Compares the model void compareResults(); /* Compares the model
* checking results * checking results
* obtained using some * obtained using some
* LTL-to-Büchi conversion * LTL-to-Büchi conversion
* algorithm with the * algorithm with the
* results given by the * results given by the
* other algorithms. * other algorithms.
@ -126,7 +127,7 @@ void compareResults(); /* Compares the model
void performBuchiIntersectionCheck(); /* Performs pairwise void performBuchiIntersectionCheck(); /* Performs pairwise
* emptiness checks on the * emptiness checks on the
* Büchi automata * Büchi automata
* constructed by the * constructed by the
* different algorithms * different algorithms
* from a formula and its * from a formula and its
@ -179,7 +180,7 @@ public:
/****************************************************************************** /******************************************************************************
* *
* A class for reporting Büchi automaton generation errors. * A class for reporting Büchi automaton generation errors.
* *
*****************************************************************************/ *****************************************************************************/
@ -361,7 +362,7 @@ FormulaGenerationException::operator=(const FormulaGenerationException& e)
/* ========================================================================= */ /* ========================================================================= */
inline BuchiAutomatonGenerationException::BuchiAutomatonGenerationException() : inline BuchiAutomatonGenerationException::BuchiAutomatonGenerationException() :
Exception("Büchi automaton generation failed") Exception("Büchi automaton generation failed")
/* ---------------------------------------------------------------------------- /* ----------------------------------------------------------------------------
* *
* Description: Constructor for class BuchiAutomatonGenerationException. * Description: Constructor for class BuchiAutomatonGenerationException.