diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index c950547d9..ae23a3d23 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,17 @@ +2012-05-21 Tomáš Babiak + + Count deterministic automata and deterministic states. + + * src/BuchiAutomaton.h, src/BuchiAutomaton.cc + (BuchiState::isDeterministic, BuchiAutomaton::isDeterministic, + BuchiAutomaton::nondeterminismIndex): New methods. + * src/TestOperations.cc (generateBuchiAutomaton): Collect + nondeterminism indices, and count deterministic automata. + * src/TestStatistics.cc, src/TestStatistics.h: Add storage + for these statistics. + * src/StatDisplay.cc (printBuchiAutomatonStats, + printCollectiveStats): Display these statistics. + 2012-04-27 Alexandre Duret-Lutz * doc/gpl.texi: Fix make pdf for newer texinfo.tex. @@ -336,7 +350,7 @@ * src/Product.h, src/SccCollection.h: New files. * src/BuchiProduct.h, src/BuchiProduct.cc, src/StateSpaceProduct.h: New files for providing specializations of the general product - computation operation applicable to Büchi automata and state + computation operation applicable to Büchi automata and state spaces. * src/Makefile.am: Add BuchiProduct.h, BuchiProduct.cc, @@ -381,7 +395,7 @@ Product interface for constructing the product and checking it for emptiness. (performBuchiIntersectionCheck): Use the Product interface - for constructing the intersection of Büchi automata and + for constructing the intersection of Büchi automata and checking it for emptiness. * src/UserCommandReader.cc: Do not include the @@ -412,12 +426,12 @@ analyzing a witness for the nonemptiness of a product automaton. (printAutomatonAnalysisResults): Use the Product interface for constructing and analyzing a witness for the nonemptiness - of the intersection of two Büchi automata. + of the intersection of two Büchi automata. (printPath): Update parameter list and documentation. Standardize the output to resemble that produced by printAcceptingCycle. (printAcceptingCycle): Update parameter list and documentation. Display all relevant information about an accepting execution - of a Büchi automaton. + of a Büchi automaton. 2004-05-18 Heikki Tauriainen @@ -1053,7 +1067,7 @@ 2003-07-18 Heikki Tauriainen * UserCommands.cc (printAutomatonAnalysisResults): Ensure that - the states in a witness for the nonemptiness of two Bûchi + the states in a witness for the nonemptiness of two Bûchi automata are distinct to prevent the truth valuation for the atomic propositions from being defined multiple times in any state of the witness. diff --git a/lbtt/src/BuchiAutomaton.cc b/lbtt/src/BuchiAutomaton.cc index 318c75b67..7a77dd383 100644 --- a/lbtt/src/BuchiAutomaton.cc +++ b/lbtt/src/BuchiAutomaton.cc @@ -214,7 +214,7 @@ void BuchiAutomaton::read(istream& input_stream) clear(); - try + try { /* Read the number of states in the generalized Büchi automaton. */ @@ -271,7 +271,7 @@ void BuchiAutomaton::read(istream& input_stream) acceptance_sets_on_states = true; acceptance_sets_on_transitions = false; } - + BitArray acc_sets(number_of_acceptance_sets); /* @@ -358,7 +358,7 @@ void BuchiAutomaton::read(istream& input_stream) state_mapping.second++; } - /* + /* * Check whether the current state is an initial state. (There must be * exactly one initial state.) */ @@ -506,7 +506,7 @@ void BuchiAutomaton::read(istream& input_stream) if (!initial_state_fixed) throw AutomatonParseException("no initial state specified"); - + if (number_of_processed_states != number_of_states) throw AutomatonParseException("incomplete automaton definition"); } @@ -535,7 +535,7 @@ void BuchiAutomaton::print * Arguments: stream -- A reference to an output stream. * indent -- Number of spaces to leave to the left of output. * fmt -- Determines the format of the output. - * + * * Returns: Nothing. * * ------------------------------------------------------------------------- */ @@ -641,7 +641,85 @@ void BuchiAutomaton::print estream.flush(); } +/* ========================================================================= */ +bool BuchiAutomaton::BuchiState::isDeterministic() const +/* ---------------------------------------------------------------------------- + * + * Description: Checks whether there is any nondeterminism + * on the outgoing transitions. + * + * Arguments: None. + * + * Returns: True iff the state is deterministic. + * + * ------------------------------------------------------------------------- */ +{ + size_type size = edges().size(); + if (size <= 1) + return true; + + for (int i = 0; i < size - 1; i++) + { + for (int j = i + 1; j < size; j++) + { + Ltl::LtlFormula *f = + &Ltl::And::construct((static_cast (edges()[i]))->guard(), + (static_cast (edges()[j]))->guard()); + if (f->satisfiable()) + { + Ltl::LtlFormula::destruct(f); + return false; + } + else + { + Ltl::LtlFormula::destruct(f); + } + } + } + return true; +} + +/* ========================================================================= */ +bool BuchiAutomaton::isDeterministic() const +/* ---------------------------------------------------------------------------- + * + * Description: Checks whether the automaton is deterministic. + * + * Arguments: None. + * + * Returns: True iff the automaton is deterministic. + * + * ------------------------------------------------------------------------- */ +{ + unsigned long int index = 0; + vector::const_iterator node; + for (node = nodes.begin(); node != nodes.end(); ++node) + if (!(static_cast(*node))->isDeterministic()) + return false; + return true; +} + +/* ========================================================================= */ +unsigned long int BuchiAutomaton::nondeterminismIndex() const +/* ---------------------------------------------------------------------------- + * + * Description: Computes the nondeterminism index for the automaton. + * I.e., the number for nondeterministic states. + * + * Arguments: None. + * + * Returns: Nondeterminism index. + * + * ------------------------------------------------------------------------- */ +{ + unsigned long int index = 0; + vector::const_iterator node; + for (node = nodes.begin(); node != nodes.end(); ++node) + if (!(static_cast(*node))->isDeterministic()) + index++; + return index; +} /****************************************************************************** * @@ -753,7 +831,7 @@ void BuchiAutomaton::BuchiState::print * number_of_acceptance_sets -- Number of acceptance sets in * the automaton in which the * state belongs. - * + * * Returns: Nothing. * * ------------------------------------------------------------------------ */ diff --git a/lbtt/src/BuchiAutomaton.h b/lbtt/src/BuchiAutomaton.h index cfd212323..c025f33ee 100644 --- a/lbtt/src/BuchiAutomaton.h +++ b/lbtt/src/BuchiAutomaton.h @@ -69,10 +69,10 @@ public: ~BuchiState(); /* Destructor. */ /* `edges' inherited from Graph::Node */ - + BitArray& acceptanceSets(); /* Tell the acceptance */ const BitArray& acceptanceSets() const; /* status of the state. */ - + void print /* Writes information */ (ostream& stream, /* about the state to a */ const int indent, /* stream. */ @@ -84,7 +84,12 @@ public: const GraphOutputFormat fmt, const unsigned long int number_of_acceptance_sets) - const; + const; + + bool isDeterministic() const; /* Checks wheter there is + * any nondeterminism on + * outgoing transitions. + */ private: BuchiState(const BuchiState&); /* Prevent copying and */ @@ -182,6 +187,13 @@ public: * (determined by the * `fmt' argument). */ + bool isDeterministic() const; /* Checks whether + * the automaton + * is deterministic. + */ + unsigned long int nondeterminismIndex() const; /* Computes the + * nondeterminism index. + */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ @@ -225,7 +237,7 @@ public: ~BuchiTransition(); /* Destructor. */ /* `targetNode' inherited from Graph::Edge */ - + bool enabled /* These functions test */ (const BitArray& truth_assignment, /* whether the */ const unsigned long int assignment_size) /* transition is */ @@ -249,7 +261,7 @@ public: (ostream& stream, /* about the transition */ const int indent, /* (as a plain graph */ const GraphOutputFormat fmt) const; /* edge) to a stream. */ - + void print /* Writes information */ (ostream& stream, /* about the transition */ const int indent, /* to a stream in */ @@ -534,7 +546,7 @@ inline BuchiAutomaton::BuchiTransition::BuchiTransition * Description: Constructor for class BuchiAutomaton::BuchiTransition. * Initializes a new transition to a BuchiState, guarded by an * LtlFormula (which is actually a propositional formula). - * + * * Arguments: target -- Identifier of the target state of the * automaton. * formula -- A pointer to a propositional formula guarding @@ -553,7 +565,7 @@ inline BuchiAutomaton::BuchiTransition::BuchiTransition /* ========================================================================= */ inline BuchiAutomaton::BuchiTransition::~BuchiTransition() /* ---------------------------------------------------------------------------- - * + * * Description: Destructor for class BuchiAutomaton::BuchiTransition. * * Arguments: None. @@ -651,7 +663,7 @@ inline bool BuchiAutomaton::BuchiTransition::enabled * the truth assignment. * * ------------------------------------------------------------------------- */ -{ +{ return guard_formula->evaluate(truth_assignment, assignment_size); } @@ -670,7 +682,7 @@ inline bool BuchiAutomaton::BuchiTransition::enabled * the truth assignment. * * ------------------------------------------------------------------------- */ -{ +{ return enabled(truth_assignment, truth_assignment.capacity()); } @@ -754,7 +766,7 @@ inline void BuchiAutomaton::BuchiTransition::print /* ========================================================================= */ inline BuchiAutomaton::BuchiState::BuchiState - (const unsigned long int num_of_acceptance_sets) : + (const unsigned long int num_of_acceptance_sets) : Node(), acceptance_sets(num_of_acceptance_sets) /* ---------------------------------------------------------------------------- * @@ -867,7 +879,7 @@ inline BuchiAutomaton::AutomatonParseException::AutomatonParseException * error message. * * Returns: Nothing. - * + * * ------------------------------------------------------------------------- */ { } diff --git a/lbtt/src/StatDisplay.cc b/lbtt/src/StatDisplay.cc index 8f8b772d0..97c38eadf 100644 --- a/lbtt/src/StatDisplay.cc +++ b/lbtt/src/StatDisplay.cc @@ -26,6 +26,7 @@ #include "StatDisplay.h" #include "StringUtil.h" #include "TestRoundInfo.h" +#include "Graph.h" namespace StatDisplay { @@ -101,13 +102,13 @@ void printBuchiAutomatonStats { Exceptional_ostream estream(&stream, ios::failbit | ios::badbit); - const AutomatonStats& automaton_stats = + const AutomatonStats& automaton_stats = test_results[algorithm].automaton_stats[result_id]; if (configuration.global_options.verbosity <= 2) { if (!automaton_stats.buchiAutomatonComputed()) - estream << " N/A N/A N/A N/A"; + estream << " N/A N/A N/A N/A N/A"; else { if (automaton_stats.buchi_generation_time >= 0.0) @@ -130,6 +131,9 @@ void printBuchiAutomatonStats changeStreamFormatting(stream, 4, 0, ios::right); estream << automaton_stats.number_of_acceptance_sets; restoreStreamFormatting(stream); + changeStreamFormatting(stream, 9, 0, ios::right); + estream << automaton_stats.nondeterminism_index; + restoreStreamFormatting(stream); } estream << ' '; } @@ -148,9 +152,14 @@ void printBuchiAutomatonStats + '\n' + string(indent, ' ') + "acceptance sets:" + string(7, ' ') + toString(automaton_stats.number_of_acceptance_sets) + + '\n' + string(indent, ' ') + "is deterministic:" + + string(6, ' ') + + (automaton_stats.is_deterministic?"Yes":"No") + + '\n' + string(indent, ' ') + "nondeterminism index: " + + toString(automaton_stats.nondeterminism_index) + '\n' + string(indent, ' ') + "computation time:" + string(6, ' '); - + if (automaton_stats.buchi_generation_time != -1.0) { changeStreamFormatting(stream, 9, 2, ios::fixed | ios::left); @@ -595,7 +604,7 @@ void printBuchiIntersectionCheckStats } else estream << " "; - + estream << ' ' + configuration.algorithmString(*alg_1); if (*alg_1 != alg_2) @@ -621,7 +630,7 @@ void printBuchiIntersectionCheckStats estream << "\n"; estream.flush(); } - + /* ========================================================================= */ void printAllStats (ostream& stream, int indent, @@ -723,7 +732,7 @@ void printCollectiveCrossComparisonStats * Returns: Nothing. * * ------------------------------------------------------------------------- */ -{ +{ Exceptional_ostream estream(&stream, ios::failbit | ios::badbit); estream << ' '; @@ -783,11 +792,11 @@ void printCollectiveCrossComparisonStats changeStreamFormatting(stream, 0, 2, ios::fixed); estream << percentage; restoreStreamFormatting(stream); - + estream << "%)"; if (percentage < 100.0) - estream << ' '; + estream << ' '; if (percentage < 10.0) estream << ' '; } @@ -1015,7 +1024,7 @@ void printCollectiveStats(ostream& stream, int indent) + '\n'; symbol_name_string = symbol_number_string = symbol_distribution_string = ""; - } + } else { symbol_name_string += string(12 - name_string.length(), ' '); @@ -1089,6 +1098,8 @@ void printCollectiveStats(ostream& stream, int indent) unsigned long int number_of_successful_instances; BIGUINT total_number_of_states; BIGUINT total_number_of_transitions; + BIGUINT total_nondeterminism_index; + int total_deterministic_count; const TestStatistics& stats = final_statistics[algorithm]; @@ -1243,14 +1254,18 @@ void printCollectiveStats(ostream& stream, int indent) double buchi_generation_time; estream << '\n' + string(22 + indent, ' ') - + "| Number of | Time consumed |\n" + + "| Number of | Time consumed |" + + " Number of | Nondeterminism |\n" + string(22 + indent, ' ') - + "| acceptance sets | (seconds) |\n" + + "| acceptance sets | (seconds) |" + + " determ. aut | index |\n" + string(7 + indent, ' ') + string(15, '-') + '+'; - for (int j = 0; j < 2; j++) + for (int j = 0; j < 3; j++) estream << string(17, '-') + '+'; + estream << string(16, '-') + '+'; + for (int j = 0; j < 3; j++) { estream << '\n' + string(8 + indent, ' '); @@ -1273,6 +1288,10 @@ void printCollectiveStats(ostream& stream, int indent) buchi_generation_time = stats.total_buchi_generation_time[j]; total_number_of_acceptance_sets = stats.total_number_of_acceptance_sets[j]; + total_deterministic_count + = stats.total_deterministic_count[j]; + total_nondeterminism_index + = stats.total_nondeterminism_index[j]; } else { @@ -1292,6 +1311,12 @@ void printCollectiveStats(ostream& stream, int indent) total_number_of_acceptance_sets = stats.total_number_of_acceptance_sets[0] + stats.total_number_of_acceptance_sets[1]; + total_deterministic_count + = stats.total_deterministic_count[0] + + stats.total_deterministic_count[1]; + total_nondeterminism_index + = stats.total_nondeterminism_index[0] + + stats.total_nondeterminism_index[1]; } number_of_successful_instances = @@ -1331,6 +1356,40 @@ void printCollectiveStats(ostream& stream, int indent) restoreStreamFormatting(stream); } + estream << " | "; + + if (number_of_successful_instances == 0) + estream << string(15, ' '); + else + { + changeStreamFormatting(stream, 15, 2, + ios::fixed | ios::right); + if (z == 0) + estream << total_deterministic_count; + else + estream << total_deterministic_count + / static_cast + (number_of_successful_instances); + restoreStreamFormatting(stream); + } + + estream << " | "; + + if (number_of_successful_instances == 0) + estream << string(14, ' '); + else + { + changeStreamFormatting(stream, 14, 2, + ios::fixed | ios::right); + if (z == 0) + estream << total_nondeterminism_index; + else + estream << total_nondeterminism_index + / static_cast + (number_of_successful_instances); + restoreStreamFormatting(stream); + } + estream << " |"; if (z == 0) estream << '\n' + string(indent + 15, ' ') + "(avg.) | "; @@ -1343,7 +1402,7 @@ void printCollectiveStats(ostream& stream, int indent) if (algorithm + 1 < round_info.number_of_translators) estream << '\n'; - + break; } diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index e2560313e..a2c461d53 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -1336,6 +1336,10 @@ void generateBuchiAutomaton automaton_stats.number_of_buchi_transitions = buchi_stats.second; automaton_stats.number_of_acceptance_sets = automaton_stats.buchi_automaton->numberOfAcceptanceSets(); + automaton_stats.nondeterminism_index + = automaton_stats.buchi_automaton->nondeterminismIndex(); + automaton_stats.is_deterministic + = automaton_stats.buchi_automaton->isDeterministic(); /* * Update Büchi automaton statistics for the given algorithm. @@ -1347,6 +1351,10 @@ void generateBuchiAutomaton += automaton_stats.number_of_buchi_transitions; final_statistics[algorithm_id].total_number_of_acceptance_sets[f] += automaton_stats.number_of_acceptance_sets; + final_statistics[algorithm_id].total_nondeterminism_index[f] + += automaton_stats.nondeterminism_index; + if (automaton_stats.is_deterministic) + final_statistics[algorithm_id].total_deterministic_count[f]++; if (final_statistics[algorithm_id].total_buchi_generation_time[f] < 0.0 || automaton_stats.buchi_generation_time < 0.0) diff --git a/lbtt/src/TestStatistics.cc b/lbtt/src/TestStatistics.cc index 053df05b0..55663b7c1 100644 --- a/lbtt/src/TestStatistics.cc +++ b/lbtt/src/TestStatistics.cc @@ -84,6 +84,7 @@ void AlgorithmTestResults::fullReset() automaton_stats[i].number_of_buchi_transitions = 0; automaton_stats[i].number_of_acceptance_sets = 0; automaton_stats[i].number_of_msccs = 0; + automaton_stats[i].nondeterminism_index = 0; automaton_stats[i].buchi_generation_time = 0.0; for (vector::iterator it diff --git a/lbtt/src/TestStatistics.h b/lbtt/src/TestStatistics.h index e6a16500c..5bb19c108 100644 --- a/lbtt/src/TestStatistics.h +++ b/lbtt/src/TestStatistics.h @@ -102,6 +102,13 @@ struct AutomatonStats * automaton. */ + unsigned long int nondeterminism_index; /* Nondeterminism index + */ + + bool is_deterministic; /* True if the automaton + * is deterministic + */ + double buchi_generation_time; /* Time used to generate a * Büchi automaton. */ @@ -284,6 +291,14 @@ struct TestStatistics * automata. */ + BIGUINT total_nondeterminism_index[2]; /* Total nondetereminism + * index for all the + * generated Büchi automata. + */ + int total_deterministic_count[2]; /* Total number of + * deterministic automata + */ + double total_buchi_generation_time[2]; /* Total time used when * generating Büchi * automata. @@ -349,10 +364,10 @@ struct TestStatistics inline AutomatonStats::AutomatonStats (vector::size_type number_of_algorithms, StateSpace::size_type max_statespace_size) : - buchi_automaton(0), number_of_buchi_states(0), + buchi_automaton(0), number_of_buchi_states(0), nondeterminism_index(0), number_of_buchi_transitions(0), number_of_acceptance_sets(0), number_of_msccs(0), buchi_generation_time(0.0), number_of_product_states(0), - number_of_product_transitions(1), + number_of_product_transitions(1), is_deterministic(false), emptiness_check_result(max_statespace_size), emptiness_check_performed(false), cross_comparison_stats(number_of_algorithms, make_pair(false, 0)), @@ -541,6 +556,8 @@ inline TestStatistics::TestStatistics total_number_of_buchi_states[i] = 0; total_number_of_buchi_transitions[i] = 0; total_number_of_acceptance_sets[i] = 0; + total_nondeterminism_index[i] = 0; + total_deterministic_count[i] = 0; total_number_of_product_states[i] = 0; total_number_of_product_transitions[i] = 0; total_buchi_generation_time[i] = 0.0;