From 4741dc02bf5fdca6a17aba06257b13c5bbaff214 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 16 Feb 2004 12:09:29 +0000 Subject: [PATCH] * lbtt/: Merge lbtt 1.0.3. --- ChangeLog | 4 + lbtt/ChangeLog | 89 +++-- lbtt/doc/.cvsignore | 2 +- lbtt/doc/lbtt.texi | 433 +++++++++++----------- lbtt/src/BuchiAutomaton.h | 8 +- lbtt/src/Config-parse.yy | 2 +- lbtt/src/Configuration.cc | 614 +++++++++++++++---------------- lbtt/src/Configuration.h | 348 +++++++++--------- lbtt/src/DispUtil.cc | 8 +- lbtt/src/Exception.h | 24 +- lbtt/src/ExternalTranslator.cc | 4 - lbtt/src/ExternalTranslator.h | 12 +- lbtt/src/FormulaRandomizer.h | 8 +- lbtt/src/Graph.h.in | 4 +- lbtt/src/LtlFormula.h | 8 +- lbtt/src/Makefile.am | 2 +- lbtt/src/NeverClaimAutomaton.h | 8 +- lbtt/src/ObstackAlloc.h | 166 --------- lbtt/src/PathEvaluator.h | 8 +- lbtt/src/ProductAutomaton.h | 8 +- lbtt/src/SccIterator.h | 4 +- lbtt/src/SharedTestData.h | 4 +- lbtt/src/StatDisplay.h | 8 +- lbtt/src/StateSpace.h | 8 +- lbtt/src/StateSpaceRandomizer.cc | 8 +- lbtt/src/StringUtil.h | 8 +- lbtt/src/TestOperations.cc | 4 - lbtt/src/TestOperations.h | 8 +- lbtt/src/TestRoundInfo.h | 4 +- lbtt/src/TestStatistics.h | 8 +- lbtt/src/UserCommandReader.h | 8 +- lbtt/src/UserCommands.h | 8 +- lbtt/src/main.cc | 4 +- lbtt/src/translate.cc | 6 +- 34 files changed, 817 insertions(+), 1033 deletions(-) delete mode 100644 lbtt/src/ObstackAlloc.h diff --git a/ChangeLog b/ChangeLog index d676c4274..077d5925f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2004-02-16 Alexandre Duret-Lutz + + * lbtt/: Merge lbtt 1.0.3. + 2004-02-13 Alexandre Duret-Lutz * src/tgbatest/ltl2baw.pl (END): Ensure LTL2TGBA is always diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 9421fdd1d..d4fb12b87 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -10,23 +10,6 @@ * src/TestOperations.cc: Include sys/wait.h. - * src/Alloc.h: Rename as ... - * src/ObstackAlloc.h: ... this. The problem is that alloc.h is a - system header in g++ < 3.0, and Darwin has a case-insensitive - filesystem. System headers that include alloc.h pick the local - Alloc.h version. - * BuchiAutomaton.h, Configuration.h, DispUtil.cc, - ExternalTranslator.h, FormulaRandomizer.h, Graph.h.in, - LtlFormula.h, Makefile.am, NeverClaimAutomaton.h, PathEvaluator.h, - ProductAutomaton.h, SccIterator.h, SharedTestData.h, - StatDisplay.h, StateSpace.h, StateSpaceRandomizer.cc, - StringUtil.h, TestOperations.h, TestRoundInfo.h, TestStatistics.h, - UserCommandReader.h, UserCommands.h, main.cc: Adjust includes. - -2003-12-29 Alexandre Duret-Lutz - - * doc/texinfo.tex: New upstream version. - 2003-07-29 Alexandre Duret-Lutz * src/TestOperations.cc (generateBuchiAutomaton): Forward SIGINT @@ -35,11 +18,6 @@ * src/main.cc (main): Do not intercept SIGINT in non-interactive runs. -2003-07-13 Alexandre Duret-Lutz - - * doc/lbtt.texi: Never use @-commands in @node names, recent Texinfo - versions are stricter on this. - 2003-07-10 Alexandre Duret-Lutz Spot wants `^', not `xor'. @@ -59,13 +37,74 @@ * src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc and SpotWrapper.h. * src/translate.cc (main): Add the --spot option, and build - a SpotWrapper of required. + a SpotWrapper if required. + +2004-02-13 Heikki Tauriainen + + * src/BitArray.{h,cc}, src/BuchiAutomaton.{h,cc}, + src/Configuration.{h,cc}, src/DispUtil.{h,cc}, + src/ExternalTranslator.{h,cc}, src/FormulaRandomizer.{h,cc}, + src/LtlFormula.{h,cc}, src/NeverClaimAutomaton.{h,cc}, + src/PathEvaluator.{h,cc}, src/PathIterator.{h,cc}, + src/ProductAutomaton.{h,cc}, src/SpinWrapper.{h,cc}, + src/StatDisplay.{h,cc}, src/StateSpace.{h,cc}, + src/StateSpaceRandomizer.{h,cc}, src/StringUtil.{h,cc}, + src/TestOperations.{h,cc}, src/TestStatistics.{h,cc}, + src/translate.{h,cc}, src/UserCommandReader.{h,cc}, + src/UserCommands.{h,cc}: Remove all #pragmas. + +2004-02-12 Heikki Tauriainen + + * doc/texinfo.tex: New upstream version. + + * doc/lbtt.texi: Update edition to 1.0.2. + Remove node names with commands to fix dvi file generation. + Move the node about the lbtt-translate utility to correct menu. + Reformat the automata file format section to avoid overfull lines + in dvi generation. + Fix description of the Algorithm block used with lbtt-translate. + + * doc/testprocedure.txt, doc/intersectioncheck.txt: Add initial + newlines. + +2004-02-11 Heikki Tauriainen + + * src/UserCommandReader.cc [HAVE_ISATTY]: Include the unistd.h + header. + (executeUserCommands) Stop waiting for new commands if an EOF is + detected. [HAVE_ISATTY]: If standard input is not connected to a + terminal, echo the input line. + +2004-02-10 Heikki Tauriainen + + * configure.ac: Remove duplicate checks for headers. + (GLIBC_OBSTACK_WORKAROUND): New config.h macro for checking for a + version of the obstack.h header that requires a workaround to be + compiled with g++. + Add check for the `isatty' library function. + Include the stdio.h header when testing for readline libraries. + + * src/Alloc.h: Rename to LbttAlloc.h to avoid a name conflict with + system header files on Darwin. + [GLIBC_OBSTACK_WORKAROUND] (__INT_TO_PTR): Redefine macro to + work around a C++ bug in the obstack.h header file in glibc 2.3.2. + Thanks to Alexandre Duret-Lutz for the original patch. + + * src/BuchiAutomaton.h, src/Configuration.h, src/DispUtil.cc, + src/ExternalTranslator.h, src/FormulaRandomizer.h, src/Graph.h.in, + src/LtlFormula.h, src/main.cc, src/Makefile.am, + src/NeverClaimAutomaton.h, src/PathEvaluator.h, + src/ProductAutomaton.h, src/SccIterator.h, src/SharedTestData.h, + src/StatDisplay.h, src/StateSpace.h, src/StateSpaceRandomizer.cc, + src/StringUtil.h, src/TestOperations.h, src/TestRoundInfo.h, + src/TestStatistics.h, src/UserCommandReader.h, + src/UserCommands.h: Adjust includes. + + * Update copyright information in source files. 2003-07-04 Alexandre Duret-Lutz * src/Config-parse.yy: Remove stray `,' in %token arguments. - * src/Alloc.h (__INT_TO_PTR): Redefine to work around glibc 2.3. - * doc/texinfo.tex: New upstream version. 2003-07-18 Heikki Tauriainen diff --git a/lbtt/doc/.cvsignore b/lbtt/doc/.cvsignore index 8e6345189..1e7fcf77d 100644 --- a/lbtt/doc/.cvsignore +++ b/lbtt/doc/.cvsignore @@ -1,3 +1,3 @@ Makefile.in Makefile -*.info* \ No newline at end of file +*.info* diff --git a/lbtt/doc/lbtt.texi b/lbtt/doc/lbtt.texi index 6bbccadf1..ae5b65b91 100644 --- a/lbtt/doc/lbtt.texi +++ b/lbtt/doc/lbtt.texi @@ -14,7 +14,7 @@ This file documents how to use the LTL-to-B@"uchi translator testbench @command{lbtt}. -Copyright @copyright{} 2003 Heikki Tauriainen +Copyright @copyright{} 2004 Heikki Tauriainen @ifinfo @email{heikki.tauriainen@@hut.fi} @end ifinfo @@ -68,7 +68,7 @@ under the above conditions for modified versions. @author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> @page @vskip 0pt plus 1filll -Copyright @copyright{} 2003 Heikki Tauriainen +Copyright @copyright{} 2004 Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}> The latest version of this manual can be obtained from@* @@ -96,14 +96,14 @@ under the above conditions for modified versions. @end iftex @ifnottex -@node Top, Copying, (dir), (dir) +@node Top, Copying, , (dir) @top @command{lbtt} @command{lbtt} is a tool for testing implementations of algorithms for translating propositional linear temporal logic formulas into B@"uchi automata. -This is edition 1.0.1 of the @command{lbtt} documentation. This edition +This is edition 1.0.2 of the @command{lbtt} documentation. This edition applies to @command{lbtt} versions 1.0.x. @command{lbtt} is free software, you may change and redistribute it @@ -115,20 +115,21 @@ comes with NO WARRANTY. See @ref{Copying} for details. * Overview:: A short introduction to @command{lbtt}. * Test methods:: Description of the tests @command{lbtt} - performs. + performs. * Invocation:: How to run the program. * Interpreting the output:: Explanation of @command{lbtt}'s output messages. * Analyzing test results:: Working with @command{lbtt}'s internal - commands. + commands. * Interfacing with lbtt:: Interfacing LTL-to-B@"uchi translators - with @command{lbtt}. + with @command{lbtt}. + * References:: List of references. * Definitions:: A reference of the formal definitions of - the various objects that @command{lbtt} - manipulates. + the various objects that @command{lbtt} + manipulates. * Configuration file option index:: * Command line option index:: @@ -255,24 +256,24 @@ for more information. @menu * Random input generation:: How @command{lbtt} generates input for the - tests. + tests. * Testing procedure:: Outline of @command{lbtt}'s testing - procedure. + procedure. * Model checking result cross-comparison test:: - Model checking the same LTL formula in - a fixed state space using different - LTL-to-B@"uchi translators should - give the same model checking result. + Model checking the same LTL formula in + a fixed state space using different + LTL-to-B@"uchi translators should + give the same model checking result. * Model checking result consistency check:: - Model checking two complementary LTL - formulas in the same state space using - an LTL-to-B@"uchi translator should - give consistent results. -* Buchi automata intersection emptiness check:: - The intersection of the languages - accepted by two B@"uchi automata - constructed from two complementary - LTL formulas should be empty. + Model checking two complementary LTL + formulas in the same state space using + an LTL-to-B@"uchi translator should + give consistent results. +* Automata intersection emptiness check:: + The intersection of the languages + accepted by two B@"uchi automata + constructed from two complementary + LTL formulas should be empty. @end menu @@ -302,9 +303,9 @@ the input generation algorithms. @menu * Random LTL formulas:: How @command{lbtt} generates random - LTL formulas. + LTL formulas. * Random state spaces:: How @command{lbtt} generates random - state spaces. + state spaces. @end menu @@ -609,7 +610,7 @@ pseudocode description of the algorithm used for generating random LTL formulas. @end ifnottex -@node The formula generation algorithm, , Random LTL formulas, Random LTL formulas +@node The formula generation algorithm, , Random LTL formulas, Random LTL formulas @subsubsection The formula generation algorithm @cindex random LTL formula, generation algorithm @@ -879,7 +880,7 @@ for more information. -@node Random state spaces, , Random LTL formulas, Random input generation +@node Random state spaces, , Random LTL formulas, Random input generation @subsection Random state spaces @cindex state space @@ -1016,7 +1017,7 @@ acceptable limits. -@node Algorithm for generating connected graphs, , Random state spaces, Random state spaces +@node Algorithm for generating connected graphs, , Random state spaces, Random state spaces @subsubsection Algorithm for generating connected graphs @cindex random connected graph, generation algorithm @@ -1028,7 +1029,7 @@ graphs: @smallexample @r{1} function RandomGraph(@var{n} : Integer; @var{d} : Real in [0.0,1.0]; - @var{t} : Real in [0.0,1.0]) : Graph; + @var{t} : Real in [0.0,1.0]) : Graph; @r{2} @var{S} := @{s1, s2, ..., sn@}; @r{3} @var{NodesToProcess} := @{s1@}; @r{4} @var{UnreachableNodes} := @{s2, s3, ..., sn@}; @@ -1055,7 +1056,7 @@ graphs: @r{25} end; @r{26} end; @r{27} if @r{there is no edge} (@var{state},@var{state'}) @r{in} @var{Edges} - @r{for any} @var{state'} @r{in} @var{S} then + @r{for any} @var{state'} @r{in} @var{S} then @r{28} @r{insert} (@var{state},@var{state}) @r{into} @var{Edges}; @r{29} end; @r{30} return <@var{S}, @var{Edges}, s1, @var{Label}>; @@ -1125,11 +1126,10 @@ and the model checking result consistency check (@pxref{Model checking result consistency check}) on the model checking results, and reports all detected failures. -The B@"uchi automata intersection emptiness check (@pxref{Buchi -automata intersection emptiness check}) operates as follows (note that -the LTL-to-B@"uchi translation phase is repeated in this figure only -for completeness; in reality, @command{lbtt} performs this phase only -once): +The B@"uchi automata intersection emptiness check +(@pxref{Automata intersection emptiness check}) operates as follows (note that +the LTL-to-B@"uchi translation phase is repeated in this figure only for +completeness; in reality, @command{lbtt} performs this phase only once): @ifhtml @* @end ifhtml @@ -1198,7 +1198,7 @@ providing an additional implementation to include in the tests. -@node Model checking result consistency check, Buchi automata intersection emptiness check, Model checking result cross-comparison test, Test methods +@node Model checking result consistency check, Automata intersection emptiness check, Model checking result cross-comparison test, Test methods @section Model checking result consistency check @cindex model checking result consistency check @@ -1236,8 +1236,8 @@ section. @end iftex -@node Buchi automata intersection emptiness check, , Model checking result consistency check, Test methods -@section Buchi automata intersection emptiness check +@node Automata intersection emptiness check, , Model checking result consistency check, Test methods +@section Automata intersection emptiness check @cindex B@"uchi automata intersection emptiness check @cindex tests, B@"uchi automata intersection emptiness check @@ -1288,7 +1288,7 @@ how to use @command{lbtt}'s internal commands). @menu * Configuration file:: Description of the configuration file - format. + format. * Command line options:: List of command line options. @end menu @@ -1351,17 +1351,17 @@ section specifying an LTL-to-B@"uchi translator. The other sections are optional and can be used to override the default testing parameters. @menu -* Algorithm section:: Each LTL-to-B@"uchi translator to be - tested requires a separate - @samp{Algorithm} section in the - configuration file. -* GlobalOptions section:: Options for changing the general - behavior of @command{lbtt}. -* FormulaOptions section:: Options controlling the way random - LTL formulas are generated. -* StateSpaceOptions section:: Options controlling the way random - state spaces are generated. -* Sample configuration file:: An example of a configuration file. +* Algorithm section:: Each LTL-to-B@"uchi translator to be + tested requires a separate + @samp{Algorithm} section in the + configuration file. +* GlobalOptions section:: Options for changing the general + behavior of @command{lbtt}. +* FormulaOptions section:: Options controlling the way random + LTL formulas are generated. +* StateSpaceOptions section:: Options controlling the way random + state spaces are generated. +* Sample configuration file:: An example of a configuration file. @end menu @@ -1477,9 +1477,9 @@ The default value for this option is @samp{Always}. @cindex enabling and disabling tests @findex IntersectionCheck @r{[}GlobalOptions@r{]} @findex IntersectionTest @r{[}GlobalOptions@r{]} -This option can be used to enable or disable the B@"uchi automata -intersection emptiness check (@pxref{Buchi automata intersection -emptiness check}). The test is enabled by default. +This option can be used to enable or disable the B@"uchi automata intersection +emptiness check (@pxref{Automata intersection emptiness check}). The test is +enabled by default. @item ModelCheck = Local @r{|} Global @findex ModelCheck @r{[}GlobalOptions@r{]} @@ -1669,16 +1669,16 @@ The following table illustrates the effects of the @t{ @r{LTL formula} @r{Can} f @r{be} OutputMode@r{'s effect on the} f @r{generated if} @r{formula passed to the} - GenerateMode @r{LTL-to-B@"uchi translators} - =NNF @r{?} + GenerateMode @r{LTL-to-B@"uchi translators} + =NNF @r{?} ------------------------------------------------------------- (p1 V ! p0) @r{Yes} Normal@r{/}NNF@r{:} (p1 V ! p0) - [] p0 -> <> p1 @r{Yes*} Nor@r{:} [] p0 -> <> p1 - NNF@r{:} (true U ! p0) \/ (true U p1) + [] p0 -> <> p1 @r{Yes*} Nor@r{:} [] p0 -> <> p1 + NNF@r{:} (true U ! p0) \/ (true U p1) ! <> p0 @r{No} Nor@r{:} ! <> p0 - NNF@r{:} (false V ! p0) + NNF@r{:} (false V ! p0) @r{* only if} AbbreviatedOperators=Yes } @@ -1851,12 +1851,7 @@ the generated state spaces. The default value is 5. Usually this should probably be the same as the maximum number of different atomic propositions in the generated formulas -@ifnottex (@pxref{FormulaOptions section}). -@end ifnottex -@iftex -(see the previous section). -@end iftex If the number of propositions attached to each state of the state spaces is less than the maximum number of different propositions that may occur in the generated formulas, all ``extra'' propositions in the formulas @@ -1900,7 +1895,7 @@ in any state of the state space. Note: This option has no effect if @end table -@node Sample configuration file, , StateSpaceOptions section, Configuration file +@node Sample configuration file, , StateSpaceOptions section, Configuration file @subsection Sample configuration file @cindex configuration file, example @@ -1915,7 +1910,7 @@ Algorithm @{ Name = "Translator 1" Path = "~/lbtt/bin/t-1" # location of the translator - # executable + # executable Enabled = Yes @} @@ -1924,7 +1919,7 @@ Algorithm Name = "Translator 2" Path = "~/lbtt/bin/t-2" Parameters = "-x -y 3 -v 0" # parameters to be passed to the - # `~/lbtt/bin/t-2' executable + # `~/lbtt/bin/t-2' executable Enabled = Yes @} @@ -1941,8 +1936,8 @@ GlobalOptions IntersectionTest = No # emptiness test ModelCheck = Local # perform the tests only in a - # single state of each state - # space + # single state of each state + # space @} FormulaOptions @@ -1952,15 +1947,15 @@ FormulaOptions OutputMode = Normal ChangeInterval = 1 # new formula after each test - # round + # round RandomSeed = 4632912 # random seed Size = 5...15 # 5 to 15 nodes in the parse - # tree of each formula + # tree of each formula Propositions = 3 # max. 3 different propositions - # in each LTL formula + # in each LTL formula PropositionPriority = 50 # priorities for propositional TruePriority = 1 # symbols @@ -1975,38 +1970,38 @@ FormulaOptions ReleasePriority = 5 DefaultOperatorPriority = 0 # disable all the remaining - # operators + # operators @} StatespaceOptions @{ GenerateMode = RandomGraph # generate random (not - # necessarily connected) graphs - # as state spaces + # necessarily connected) graphs + # as state spaces ChangeInterval = 10 # new state space after every - # 10th test round + # 10th test round RandomSeed = 37620 # random seed Size = 50 # 50 states in each state space Propositions = 3 # 3 propositions in each state - # of each state space + # of each state space EdgeProbability = 0.1 # approximate probability of - # having a transition between - # any two states + # having a transition between + # any two states TruthProbability = 0.5 # probability with which any - # atomic proposition is true in - # a state + # atomic proposition is true in + # a state @} @end smallexample -@node Command line options, , Configuration file, Invocation +@node Command line options, , Configuration file, Invocation @section Command line options This section lists the command line options that may be used when @@ -2017,16 +2012,16 @@ there is no direct equivalent in the configuration file options. @menu * Special options:: Options available only as command line - parameters. + parameters. * Global options:: Options corresponding to the - @samp{GlobalOptions} section of the - configuration file. + @samp{GlobalOptions} section of the + configuration file. * LTL formula options:: Options corresponding to the - @samp{FormulaOptions} section of the - configuration file. + @samp{FormulaOptions} section of the + configuration file. * State space options:: Options corresponding to the - @samp{StateSpaceOptions} section of the - configuration file. + @samp{StateSpaceOptions} section of the + configuration file. @end menu @@ -2194,8 +2189,8 @@ between test rounds to wait for user input. @cindex enabling and disabling tests @vindex --intersectiontest @vindex --nointersectiontest -These options enable or disable the B@"uchi automata intersection -emptiness check (@pxref{Buchi automata intersection emptiness check}). +These options enable or disable the B@"uchi automata intersection emptiness +check (@pxref{Automata intersection emptiness check}). @item --localmodelcheck @vindex --localmodelcheck @@ -2441,7 +2436,7 @@ them randomly. -@node State space options, , LTL formula options, Command line options +@node State space options, , LTL formula options, Command line options @subsection State space options The following command line options affect the way in which @command{lbtt} @@ -2523,7 +2518,7 @@ This option can be used to change the size of the generated state spaces. @vindex --truthprobability This option sets the probability that @command{lbtt} uses for choosing the valuation for each atomic proposition in each state of the randomly generated -state spaces. (This option has no effect is using enumerated paths as state +state spaces. (This option has no effect if using enumerated paths as state spaces.) @end table @@ -2541,9 +2536,9 @@ messages will be suppressed; higher verbosity modes show information about @menu * Configuration information:: The current configuration is shown - before starting tests. + before starting tests. * Test round messages:: Conventions for reporting test - results and test failures. + results and test failures. * Test statistics:: Shown at the end of testing. @end menu @@ -2727,11 +2722,11 @@ of the formulas into a B@"uchi automaton correctly. @end enumerate -The output of phases 4---8 will be repeated for each implementation -included in the tests. After this @command{lbtt} proceeds to the model -checking result cross-comparison test (@pxref{Model checking result -cross-comparison test}) and the B@"uchi automata intersection -emptiness test (@pxref{Buchi automata intersection emptiness check}). +The output of phases 4---8 will be repeated for each implementation included in +the tests. After this @command{lbtt} proceeds to the model checking result +cross-comparison test (@pxref{Model checking result cross-comparison test}) and +the B@"uchi automata intersection emptiness test +(@pxref{Automata intersection emptiness check}). The model checking result cross-comparison test might result in the following output: @@ -2788,7 +2783,7 @@ format specified above. -@node Test statistics, , Test round messages, Interpreting the output +@node Test statistics, , Test round messages, Interpreting the output @section Test statistics @cindex tests, statistics @@ -2858,9 +2853,9 @@ a single fixed state of each generated state space (called the ``initial'' state of the state space). @item -Number of failures in the B@"uchi automata intersection emptiness -check (@pxref{Buchi automata intersection emptiness check}) for each -pair of implementations. +Number of failures in the B@"uchi automata intersection emptiness check +(@pxref{Automata intersection emptiness check}) for each pair of +implementations. @end itemize Note that the pairwise inconsistency results form a symmetric matrix (although @@ -2895,13 +2890,13 @@ showing a prompt of the form @menu * Command conventions:: Conventions for entering commands. * Getting help:: Use the @samp{help} command to access - on-line help. + on-line help. * Test control commands:: Commands for continuing testing, - skipping tests or enabling or disabling - implementations. + skipping tests or enabling or disabling + implementations. * Data display commands:: Commands for displaying information - about B@"uchi automata, state spaces, - and LTL formulas. + about B@"uchi automata, state spaces, + and LTL formulas. * Failure analysis commands:: Commands for analyzing test failures. @end menu @@ -3167,7 +3162,7 @@ the output that is displayed. -@node Failure analysis commands, , Data display commands, Analyzing test results +@node Failure analysis commands, , Data display commands, Analyzing test results @section Failure analysis commands The first part of this section introduces the commands available for @@ -3185,7 +3180,7 @@ automata correctness tests. The second part describes the conventions that @cindex failure analysis, B@"uchi automata intersection check @cindex analyzing test failures, B@"uchi automata intersection emptiness check Analyze a failure in the B@"uchi automata intersection emptiness check -(@pxref{Buchi automata intersection emptiness check}). +(@pxref{Automata intersection emptiness check}). The two implementation identifiers select the B@"uchi automata for which to perform the analysis. The B@"uchi automata intersection emptiness check always involves automata constructed from the positive and the negative @@ -3288,10 +3283,10 @@ itself indefinitely. The witness might look as follows: @smallexample Execution M: prefix: < s0 @{p0, p4@}, - s2 @{p1, p2, p3, p4@} > + s2 @{p1, p2, p3, p4@} > cycle: < s34 @{p0, p1, p2, p3, p4@}, - s42 @{p4@}, - s44 @{p1, p4@} > + s42 @{p4@}, + s44 @{p1, p4@} > @end smallexample @noindent @@ -3321,7 +3316,7 @@ $S = \{s_0, s_2, s_{34}, s_{42}, s_{44}\}$, @iftex @tex $\rho = \{(s_0, s_2), (s_2, s_{34}), (s_{34}, s_{42}), (s_{42}, s_{44}), - (s_{44}, s_{34})\}$, + (s_{44}, s_{34})\}$, @end tex @end iftex @ifnottex @@ -3360,17 +3355,17 @@ LTL and might look as follows: +-> M, |== (p1 U p4) : | +-> M, |== p4 +-> M, |== (! p1 -> [] p4) : - +-> M, |== [] p4 : - +-> M, |== p4 - +-> s0 --> s2 - +-> M, |== p4 - +-> s2 --> s34 - +-> M, |== p4 - +-> s34 --> s42 - +-> M, |== p4 - +-> s42 --> s44 - +-> M, |== p4 - +-> s44 --> s34 + +-> M, |== [] p4 : + +-> M, |== p4 + +-> s0 --> s2 + +-> M, |== p4 + +-> s2 --> s34 + +-> M, |== p4 + +-> s34 --> s42 + +-> M, |== p4 + +-> s42 --> s44 + +-> M, |== p4 + +-> s44 --> s34 @end smallexample @noindent @@ -3435,24 +3430,19 @@ which can be seen from the proof. This chapter gives the details on how to use @command{lbtt} for testing LTL-to-B@"uchi translation algorithm implementations that are not supported by the basic distribution. (See -@ifnottex @ref{The lbtt-translate utility} -@end ifnottex -@iftex -the next chapter -@end iftex for information on how to connect several publicly available LTL-to-B@"uchi translator implementations to @command{lbtt}.) @menu * Translator interface:: @command{lbtt}'s requirements for an - LTL-to-B@"uchi translator. + LTL-to-B@"uchi translator. * Format for LTL formulas:: How @command{lbtt} passes LTL formulas - to the translators. -* Buchi automata:: How @command{lbtt} expects the translators - to present their output. + to the translators. +* Format for automata:: How @command{lbtt} expects the translators + to present their output. * The lbtt-translate utility:: An interface for two LTL-to-B@"uchi - translators. + translators. @end menu @@ -3479,7 +3469,7 @@ The translator executable should read its input (an LTL formula) from @var{input-file} and write its output (a B@"uchi automaton) into @var{output-file} (without removing the input file); see @ifnottex -@ref{Format for LTL formulas} and @ref{Buchi automata} +@ref{Format for LTL formulas} and @ref{Format for automata} @end ifnottex @iftex the following two sections @@ -3507,7 +3497,7 @@ Algorithm -@node Format for LTL formulas, Buchi automata, Translator interface, Interfacing with lbtt +@node Format for LTL formulas, Format for automata, Translator interface, Interfacing with lbtt @section Input file format for LTL formulas @cindex LTL-to-B@"uchi translators, LTL formula input file format @@ -3520,41 +3510,41 @@ notation) is as follows: @smallexample @var{formula} @r{::=} `t' - @r{// ``true''} - @r{|} `f' - @r{// ``false''} - @r{|} `p'@r{[}0@r{---}9@r{]+} - @r{// atomic proposition with} - @r{// a nonnegative integer} - @r{// identifier} - @r{|} `!' @var{sp} @var{formula} - @r{// negation} - @r{|} `X' @var{sp} @var{formula} - @r{// ``next time''} - @r{|} `F' @var{sp} @var{formula} - @r{// ``finally''} - @r{|} `G' @var{sp} @var{formula} - @r{// ``globally''} - @r{|} `&' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// conjunction} - @r{|} `|' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// disjunction} - @r{|} `i' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// implication} - @r{|} `e' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// equivalence} - @r{|} `^' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// exclusive or} - @r{|} `U' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// ``(strong) until''} - @r{|} `V' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// ``(weak) release''} - @r{|} `W' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// ``weak until''} - @r{|} `M' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// ``strong release''} - @r{|} `B' @var{sp} @var{formula} @var{sp} @var{formula} - @r{// ``before''} + @r{// ``true''} + @r{|} `f' + @r{// ``false''} + @r{|} `p'@r{[}0@r{---}9@r{]+} + @r{// atomic proposition with} + @r{// a nonnegative integer} + @r{// identifier} + @r{|} `!' @var{sp} @var{formula} + @r{// negation} + @r{|} `X' @var{sp} @var{formula} + @r{// ``next time''} + @r{|} `F' @var{sp} @var{formula} + @r{// ``finally''} + @r{|} `G' @var{sp} @var{formula} + @r{// ``globally''} + @r{|} `&' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// conjunction} + @r{|} `|' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// disjunction} + @r{|} `i' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// implication} + @r{|} `e' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// equivalence} + @r{|} `^' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// exclusive or} + @r{|} `U' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// ``(strong) until''} + @r{|} `V' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// ``(weak) release''} + @r{|} `W' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// ``weak until''} + @r{|} `M' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// ``strong release''} + @r{|} `B' @var{sp} @var{formula} @var{sp} @var{formula} + @r{// ``before''} @end smallexample @noindent @@ -3591,8 +3581,8 @@ line options (@pxref{Command line options}) to prevent -@node Buchi automata, The lbtt-translate utility, Format for LTL formulas, Interfacing with lbtt -@section Output file format for B@"uchi automata +@node Format for automata, The lbtt-translate utility, Format for LTL formulas, Interfacing with lbtt +@section Output file format for automata @cindex file formats, LTL-to-B@"uchi translator output file @cindex LTL-to-B@"uchi translators, automaton output file format @@ -3609,49 +3599,49 @@ The output file generated by the translator should contain an @var{automaton} described using the following grammar: @smallexample -@var{automaton} @r{::=} @var{number-of-states} @var{sp} @var{number-of-acceptance-conditions} @var{states} +@var{automaton} @r{::=} @var{num-states} @var{sp} @var{num-conds} @var{states} -@var{number-of-states} @r{::=} @r{[}0@r{---}9@r{]+} +@var{num-states} @r{::=} @r{[}0@r{---}9@r{]+} -@var{number-of-acceptance-conditions} @r{::=} @r{[}0@r{---}9@r{]+} +@var{num-conds} @r{::=} @r{[}0@r{---}9@r{]+} @var{states} @r{::=} @var{states} @var{sp} @var{state} - @r{|} @r{// empty} + @r{|} @r{// empty} -@var{state} @r{::=} @var{state-id} @var{sp} @var{initial?} @var{acceptance-conditions} @var{sp} `-1' @var{transitions} @var{sp} `-1' +@var{state} @r{::=} @var{state-id} @var{sp} @var{initial?} @var{conds} @var{sp} `-1' @var{transitions} @var{sp} `-1' @var{state-id} @r{::=} @r{[}0@r{---}9@r{]+} @var{initial?} @r{::=} `0' @r{|} `1' -@var{acceptance-conditions} @r{::=} @var{acceptance-conditions} @var{sp} @var{acceptance-set-id} - @r{|} @r{// empty} +@var{conds} @r{::=} @var{conds} @var{sp} @var{acceptance-set-id} + @r{|} @r{// empty} @var{acceptance-set-id} @r{::=} @r{[}0@r{---}9@r{]+} @var{transitions} @r{::=} @var{transitions} @var{sp} @var{transition} - @r{|} @r{// empty} + @r{|} @r{// empty} @var{transition} @r{::=} @var{state-id} @var{sp} @var{guard-formula} @var{guard-formula} @r{::=} `t' - @r{// ``true''} - @r{|} `f' - @r{// ``false''} - @r{|} `p'@r{[}0@r{---}9@r{]+} - @r{// atomic proposition} - @r{|} `!' @var{sp} @var{guard-formula} - @r{// negation} - @r{|} `&' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} - @r{// conjunction} - @r{|} `|' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} - @r{// disjunction} - @r{|} `i' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} - @r{// implication} - @r{|} `e' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} - @r{// equivalence} - @r{|} `^' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} - @r{// exclusive or} + @r{// ``true''} + @r{|} `f' + @r{// ``false''} + @r{|} `p'@r{[}0@r{---}9@r{]+} + @r{// atomic proposition} + @r{|} `!' @var{sp} @var{guard-formula} + @r{// negation} + @r{|} `&' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} + @r{// conjunction} + @r{|} `|' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} + @r{// disjunction} + @r{|} `i' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} + @r{// implication} + @r{|} `e' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} + @r{// equivalence} + @r{|} `^' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula} + @r{// exclusive or} @end smallexample @noindent (The quoted characters denote the characters themselves; @var{sp} denotes any @@ -3679,7 +3669,7 @@ The state and acceptance condition identifiers need not be successive, and the states or acceptance conditions can be listed in any order. The only restrictions are that the identifiers of different states and acceptance conditions should be unique and that the total number of different identifiers -should equal @var{number-of-states} or @var{number-of-acceptance-conditions}, +should equal @var{num-states} or @var{num-conds}, respectively. (The same identifiers can be shared between states and acceptance conditions, however.) @@ -3743,7 +3733,7 @@ The following example illustrates the file format. -@node The lbtt-translate utility, , Buchi automata, Interfacing with lbtt +@node The lbtt-translate utility, , Format for automata, Interfacing with lbtt @section The @command{lbtt-translate} utility @cindex @command{lbtt-translate} (executable file) @@ -3812,17 +3802,18 @@ installation instructions. Then add the following @samp{Algorithm} section in @smallexample Algorithm @{ - Name = "@var{name for the implementation}" - Path = "@var{path-to-@command{lbtt-translate}} @var{implementation-selector} @var{path-to-executable}" + Name = "@r{[@var{name for the implementation}]}" + Path = "@r{[@var{path-to-@command{lbtt-translate}}]}" + Parameters = "@r{[@var{implementation selector}]} @r{[@var{path to executable}]}" Enabled = Yes @} @end smallexample @noindent -where @var{path-to-@command{lbtt-translate}} contains the complete path and +where [@var{path-to-@command{lbtt-translate}}] contains the complete path and file name of the @command{lbtt-translate} tool executable, -@var{implementation-selector} is either of the options @samp{--lbt} or -@samp{--spin}, and @var{path-to-executable} is the full path +[@var{implementation selector}] is either of the options @samp{--lbt} or +@samp{--spin}, and [@var{path to executable}] is the full path of the tool executable. The names of these executables are usually (assuming a normal installation) @command{lbt} and @command{spin}, respectively. @@ -3849,7 +3840,7 @@ E.@: Clarke Jr., O.@: Grumberg and D.@: Peled. Model checking. The MIT Press, 1999. @item @anchor{[Cou99]} [Cou99] -J-M. Couvreur. On-the-fly verification of linear temporal logic. In +J.-M. Couvreur. On-the-fly verification of linear temporal logic. In @i{Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99), volume I}, volume 1708 of @i{Lecture Notes in Computer Science}, pages 253---271. Springer-Verlag, 1999. @@ -3964,18 +3955,18 @@ manipulates. @menu * LTL formulas:: @command{lbtt} uses traditional semantics - for propositional linear temporal - logic. -* Generalized Buchi automata:: The B@"uchi automata used by @command{lbtt} - have one initial state, labels on - transitions and zero or more - acceptance conditions. + for propositional linear temporal + logic. +* Generalized automata:: The B@"uchi automata used by @command{lbtt} + have one initial state, labels on + transitions and zero or more + acceptance conditions. * State spaces:: State spaces are Kripke structures - with a total transition relation. + with a total transition relation. @end menu -@node LTL formulas, Generalized Buchi automata, Definitions, Definitions +@node LTL formulas, Generalized automata, Definitions, Definitions @appendixsec LTL formulas @command{lbtt} uses the traditional definition for propositional linear @@ -4355,8 +4346,8 @@ $(\varphi\;{\bf B}\;\psi) \equiv_{\rm def} \neg(\neg\varphi\;\bf{U}\;\psi)$ -@node Generalized Buchi automata, State spaces, LTL formulas, Definitions -@appendixsec Generalized B@"uchi automata +@node Generalized automata, State spaces, LTL formulas, Definitions +@appendixsec Generalized automata @cindex B@"uchi automata, formal definition @cindex generalized B@"uchi automata, formal definition @@ -4375,7 +4366,7 @@ $2^{AP}$ with one initial state, labels on transitions and zero or more acceptance conditions. -@appendixsubsec Formal definition of generalized B@"uchi automata +@appendixsubsec Formal definition of generalized automata Formally, a generalized B@"uchi automaton can be represented as a tuple @iftex @@ -4664,7 +4655,7 @@ of some states and then adjusting the transition labels appropriately. -@node State spaces, , Generalized Buchi automata, Definitions +@node State spaces, , Generalized automata, Definitions @appendixsec State spaces @cindex state space, formal definition @@ -4743,7 +4734,7 @@ propositions that hold in the state. @printindex ky -@node Concept index, , User command index, Top +@node Concept index, , User command index, Top @unnumbered Concept index @printindex cp diff --git a/lbtt/src/BuchiAutomaton.h b/lbtt/src/BuchiAutomaton.h index e1bd12ca4..dcd034bd8 100644 --- a/lbtt/src/BuchiAutomaton.h +++ b/lbtt/src/BuchiAutomaton.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,15 +20,11 @@ #ifndef BUCHIAUTOMATON_H #define BUCHIAUTOMATON_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "EdgeContainer.h" #include "Exception.h" diff --git a/lbtt/src/Config-parse.yy b/lbtt/src/Config-parse.yy index 74230c9fc..b51a8c942 100644 --- a/lbtt/src/Config-parse.yy +++ b/lbtt/src/Config-parse.yy @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or diff --git a/lbtt/src/Configuration.cc b/lbtt/src/Configuration.cc index 7ea1f6f08..ff4b8fb67 100644 --- a/lbtt/src/Configuration.cc +++ b/lbtt/src/Configuration.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -17,10 +17,6 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #include #include @@ -97,7 +93,7 @@ const struct Configuration::IntegerRange Configuration::STATESPACE_SIZE_RANGE const struct Configuration::IntegerRange Configuration::STATESPACE_MAX_SIZE_RANGE = {1, LONG_MAX, "minimum state space size exceeds the maximum state space " - "size"}; + "size"}; @@ -312,7 +308,7 @@ void Configuration::read(int argc, char* argv[]) { long int interval_length = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(interval_length, GENERATION_RANGE, false); if (opttype == OPT_FORMULACHANGEINTERVAL) @@ -426,14 +422,14 @@ void Configuration::read(int argc, char* argv[]) { long int number_of_rounds = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(number_of_rounds, ROUND_COUNT_RANGE, false); global_options.number_of_rounds = number_of_rounds; locked_options.insert(make_pair(CFG_GLOBALOPTIONS, CFG_ROUNDS)); } break; - + case OPT_SHOWCONFIG : print_config = true; break; @@ -446,7 +442,7 @@ void Configuration::read(int argc, char* argv[]) { long int rounds_to_skip = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(rounds_to_skip, ROUND_COUNT_RANGE, false); global_options.init_skip = rounds_to_skip; } @@ -465,7 +461,7 @@ void Configuration::read(int argc, char* argv[]) { long int verbosity = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(verbosity, VERBOSITY_RANGE, false); global_options.verbosity = verbosity; locked_options.insert(make_pair(CFG_GLOBALOPTIONS, CFG_VERBOSITY)); @@ -475,17 +471,17 @@ void Configuration::read(int argc, char* argv[]) case OPT_VERSION : cout << "lbtt " PACKAGE_VERSION "\n" - "lbtt is free software; you may change and " - "redistribute it under the terms of\n" - "the GNU General Public License. lbtt comes with " - "NO WARRANTY. See the file\n" - "COPYING for details.\n"; + "lbtt is free software; you may change and " + "redistribute it under the terms of\n" + "the GNU General Public License. lbtt comes with " + "NO WARRANTY. See the file\n" + "COPYING for details.\n"; exit(0); break; case OPT_ABBREVIATEDOPERATORS : case OPT_NOABBREVIATEDOPERATORS : - formula_options.allow_abbreviated_operators + formula_options.allow_abbreviated_operators = (opttype == OPT_ABBREVIATEDOPERATORS); locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_ABBREVIATEDOPERATORS)); @@ -512,7 +508,7 @@ void Configuration::read(int argc, char* argv[]) { long int priority = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(priority, PRIORITY_RANGE, false); @@ -546,7 +542,7 @@ void Configuration::read(int argc, char* argv[]) case OPT_FALSEPRIORITY : symbol = ::Ltl::LTL_FALSE; - locked_options.insert(make_pair(CFG_FORMULAOPTIONS, + locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_FALSEPRIORITY)); break; @@ -594,7 +590,7 @@ void Configuration::read(int argc, char* argv[]) case OPT_RELEASEPRIORITY : symbol = ::Ltl::LTL_V; - locked_options.insert(make_pair(CFG_FORMULAOPTIONS, + locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_RELEASEPRIORITY)); break; @@ -658,13 +654,13 @@ void Configuration::read(int argc, char* argv[]) locked_options.insert(make_pair(CFG_FORMULAOPTIONS, CFG_OUTPUTMODE)); break; - + case OPT_FORMULAPROPOSITIONS : case OPT_STATESPACEPROPOSITIONS : { long int num_propositions = parseCommandLineInteger - (command_line_options[option_index].name, optarg); + (command_line_options[option_index].name, optarg); checkIntegerRange(num_propositions, PROPOSITION_COUNT_RANGE, false); @@ -710,7 +706,7 @@ void Configuration::read(int argc, char* argv[]) { long int size = parseCommandLineInteger - (command_line_options[option_index].name, value); + (command_line_options[option_index].name, value); checkIntegerRange(size, min_size_range, false); @@ -797,7 +793,7 @@ void Configuration::read(int argc, char* argv[]) locked_options.insert(make_pair(CFG_STATESPACEOPTIONS, CFG_GENERATEMODE)); break; - + case OPT_RANDOMCONNECTEDGRAPH : global_options.statespace_generation_mode = RANDOMCONNECTEDGRAPH; locked_options.insert(make_pair(CFG_STATESPACEOPTIONS, @@ -840,15 +836,15 @@ void Configuration::read(int argc, char* argv[]) if (error) throw ConfigurationException ("", string("unrecognized argument (`") + optarg - + "') for option `--" - + command_line_options[option_index].name + "'"); + + "') for option `--" + + command_line_options[option_index].name + "'"); } while (opttype != -1); if (optind != argc) throw ConfigurationException ("", string("unrecognized command line option `") - + argv[optind] + "'"); + + argv[optind] + "'"); /* * Read the configuration file. @@ -857,8 +853,8 @@ void Configuration::read(int argc, char* argv[]) FILE* configuration_file = fopen(global_options.cfg_filename.c_str(), "r"); if (configuration_file == NULL) throw ConfigurationException - ("", "error opening configuration file `" - + global_options.cfg_filename + "'"); + ("", "error opening configuration file `" + + global_options.cfg_filename + "'"); try { @@ -903,7 +899,7 @@ void Configuration::read(int argc, char* argv[]) } for (set, - ALLOC(unsigned long int) >::const_iterator + ALLOC(unsigned long int) >::const_iterator id = algorithm_id_set.begin(); id != algorithm_id_set.end(); ++id) @@ -933,8 +929,8 @@ void Configuration::read(int argc, char* argv[]) if (global_options.number_of_rounds <= global_options.init_skip) throw ConfigurationException - ("", "the argument for `--skip' must be less than the total " - "number of test rounds"); + ("", "the argument for `--skip' must be less than the total " + "number of test rounds"); /* * Check that there is at least one algorithm available for use. @@ -942,7 +938,7 @@ void Configuration::read(int argc, char* argv[]) if (algorithms.empty()) throw ConfigurationException - ("", "no implementations defined in the configuration file"); + ("", "no implementations defined in the configuration file"); /* * The case where the number of available variables for propositional @@ -962,7 +958,7 @@ void Configuration::read(int argc, char* argv[]) && formula_options.symbol_priority[::Ltl::LTL_TRUE] == 0 && formula_options.symbol_priority[::Ltl::LTL_FALSE] == 0) throw ConfigurationException("", "at least one atomic symbol must have " - "nonzero priority"); + "nonzero priority"); /* * If the operators ->, <->, xor, <>, [], W and M are disallowed, set their @@ -997,15 +993,15 @@ void Configuration::read(int argc, char* argv[]) it->second = formula_options.default_operator_priority; if (it->second > 0 && !unary_operator_allowed) - unary_operator_allowed = - (it->first == ::Ltl::LTL_NEGATION || it->first == ::Ltl::LTL_NEXT + unary_operator_allowed = + (it->first == ::Ltl::LTL_NEGATION || it->first == ::Ltl::LTL_NEXT || it->first == ::Ltl::LTL_FINALLY - || it->first == ::Ltl::LTL_GLOBALLY); + || it->first == ::Ltl::LTL_GLOBALLY); } if (!unary_operator_allowed) throw ConfigurationException("", "at least one unary operator must have " - "a nonzero priority"); + "a nonzero priority"); /* * Initialize the random formula generator with priorities for the LTL @@ -1024,49 +1020,49 @@ void Configuration::read(int argc, char* argv[]) { switch (it->first) { - case ::Ltl::LTL_ATOM : - case ::Ltl::LTL_TRUE : - case ::Ltl::LTL_FALSE : - formula_options.formula_generator.useSymbol(it->first, it->second); - break; + case ::Ltl::LTL_ATOM : + case ::Ltl::LTL_TRUE : + case ::Ltl::LTL_FALSE : + formula_options.formula_generator.useSymbol(it->first, it->second); + break; - case ::Ltl::LTL_NEGATION : - formula_options.formula_generator.useShortOperator + case ::Ltl::LTL_NEGATION : + formula_options.formula_generator.useShortOperator (it->first, it->second); total_short_unary_priority += it->second; - if (formula_options.generate_mode != NNF) + if (formula_options.generate_mode != NNF) { - formula_options.formula_generator.useLongOperator + formula_options.formula_generator.useLongOperator (it->first, it->second); total_long_unary_priority += it->second; } - break; + break; - case ::Ltl::LTL_NEXT : - case ::Ltl::LTL_FINALLY : - case ::Ltl::LTL_GLOBALLY : - formula_options.formula_generator.useShortOperator + case ::Ltl::LTL_NEXT : + case ::Ltl::LTL_FINALLY : + case ::Ltl::LTL_GLOBALLY : + formula_options.formula_generator.useShortOperator (it->first, it->second); total_short_unary_priority += it->second; - formula_options.formula_generator.useLongOperator + formula_options.formula_generator.useLongOperator (it->first, it->second); total_long_unary_priority += it->second; - break; + break; - case ::Ltl::LTL_CONJUNCTION : - case ::Ltl::LTL_DISJUNCTION : - case ::Ltl::LTL_IMPLICATION : - case ::Ltl::LTL_EQUIVALENCE : - case ::Ltl::LTL_XOR : - case ::Ltl::LTL_UNTIL : - case ::Ltl::LTL_V : - case ::Ltl::LTL_WEAK_UNTIL : - case ::Ltl::LTL_STRONG_RELEASE : - case ::Ltl::LTL_BEFORE : - formula_options.formula_generator.useLongOperator + case ::Ltl::LTL_CONJUNCTION : + case ::Ltl::LTL_DISJUNCTION : + case ::Ltl::LTL_IMPLICATION : + case ::Ltl::LTL_EQUIVALENCE : + case ::Ltl::LTL_XOR : + case ::Ltl::LTL_UNTIL : + case ::Ltl::LTL_V : + case ::Ltl::LTL_WEAK_UNTIL : + case ::Ltl::LTL_STRONG_RELEASE : + case ::Ltl::LTL_BEFORE : + formula_options.formula_generator.useLongOperator (it->first, it->second); total_binary_priority += it->second; - break; + break; } } } @@ -1091,9 +1087,9 @@ void Configuration::read(int argc, char* argv[]) ++op) { if (op->second > 0) - { + { switch (op->first) - { + { case ::Ltl::LTL_ATOM : case ::Ltl::LTL_TRUE : case ::Ltl::LTL_FALSE : @@ -1106,18 +1102,18 @@ void Configuration::read(int argc, char* argv[]) = formula_options.formula_generator.size; s <= formula_options.formula_generator.max_size; s++) - { + { if (k >= s) continue; probability += operatorProbability - (op->first, k, s, + (op->first, k, s, total_short_unary_priority, total_long_unary_priority, total_binary_priority, result_cache); } probability /= static_cast - (formula_options.formula_generator.max_size + (formula_options.formula_generator.max_size - formula_options.formula_generator.size + 1); @@ -1158,18 +1154,18 @@ void Configuration::print(ostream& stream, int indent) const Exceptional_ostream estream(&stream, ios::badbit | ios::failbit); estream << string(indent, ' ') + "Program configuration:\n" - + string(indent, ' ') + string(22, '-') + "\n\n" - + string(indent + 2, ' ') - + toString(global_options.number_of_rounds) - + " test round" - + (global_options.number_of_rounds > 1 ? "s" : ""); + + string(indent, ' ') + string(22, '-') + "\n\n" + + string(indent + 2, ' ') + + toString(global_options.number_of_rounds) + + " test round" + + (global_options.number_of_rounds > 1 ? "s" : ""); if (global_options.init_skip > 0) estream << " (of which the first " - + (global_options.init_skip > 1 + + (global_options.init_skip > 1 ? toString(global_options.init_skip) + " rounds " : string("")) - + "will be skipped)"; + + "will be skipped)"; estream << ".\n" + string(indent + 2, ' '); @@ -1181,20 +1177,20 @@ void Configuration::print(ostream& stream, int indent) const estream << "Running in batch mode.\n"; estream << string(indent + 2, ' ') - + "Using " - + (global_options.product_mode == GLOBAL + + "Using " + + (global_options.product_mode == GLOBAL ? "global" : "local") - + " model checking for tests.\n"; + + " model checking for tests.\n"; if (!global_options.transcript_filename.empty()) estream << string(indent + 2, ' ') + "Writing error log to `" - + global_options.transcript_filename + "'.\n"; + + global_options.transcript_filename + "'.\n"; estream << '\n' + string(indent + 2, ' ') + "Implementations:\n"; vector::size_type algorithm_number = 0; - + for (vector ::const_iterator a = algorithms.begin(); a != algorithms.end(); @@ -1218,19 +1214,19 @@ void Configuration::print(ostream& stream, int indent) const estream << "Enabled tests:\n"; if (global_options.do_comp_test) estream << string(indent + 4, ' ') + - "Model checking result cross-comparison test\n"; + "Model checking result cross-comparison test\n"; if (global_options.do_cons_test) estream << string(indent + 4, ' ') + - "Model checking result consistency check\n"; + "Model checking result consistency check\n"; if (global_options.do_intr_test) estream << string(indent + 4, ' ') + - "Büchi automata intersection emptiness check\n"; + "Büchi automata intersection emptiness check\n"; } else estream << "All automata correctness tests disabled.\n"; estream << '\n' + string(indent + 2, ' ') + "Random state spaces:\n" - + string(indent + 4, ' '); + + string(indent + 4, ' '); switch (global_options.statespace_generation_mode) { @@ -1257,15 +1253,15 @@ void Configuration::print(ostream& stream, int indent) const estream << "..." + toString(statespace_generator.max_size); estream << string(" state") - + (statespace_generator.max_size == 1 ? "" : "s") + ", " - + toString(statespace_generator.atoms_per_state) - + " atomic proposition" - + (statespace_generator.atoms_per_state == 1 ? "" : "s") - + ")\n" + string(indent + 4, ' '); + + (statespace_generator.max_size == 1 ? "" : "s") + ", " + + toString(statespace_generator.atoms_per_state) + + " atomic proposition" + + (statespace_generator.atoms_per_state == 1 ? "" : "s") + + ")\n" + string(indent + 4, ' '); if (global_options.statespace_change_interval == 0 || global_options.statespace_change_interval - >= global_options.number_of_rounds) + >= global_options.number_of_rounds) estream << "Using a fixed state space.\n" + string(indent + 4, ' '); else { @@ -1297,16 +1293,16 @@ void Configuration::print(ostream& stream, int indent) const if (global_options.statespace_generation_mode != ENUMERATEDPATH) { estream << "Random seed: " - + toString(global_options.statespace_random_seed) - + '\n' + string(indent + 4, ' '); + + toString(global_options.statespace_random_seed) + + '\n' + string(indent + 4, ' '); if (global_options.statespace_generation_mode & GRAPH) estream << "Random edge probability: " - + toString(statespace_generator.edge_probability) - + '\n' + string(indent + 4, ' '); + + toString(statespace_generator.edge_probability) + + '\n' + string(indent + 4, ' '); estream << "Propositional truth probability: " - + toString(statespace_generator.truth_probability) + + toString(statespace_generator.truth_probability) + "\n"; } @@ -1315,32 +1311,32 @@ void Configuration::print(ostream& stream, int indent) const if (global_options.formula_input_filename.empty()) { estream << "Random LTL formulas:\n" + string(indent + 4, ' ') - + toString(formula_options.formula_generator.size); + + toString(formula_options.formula_generator.size); if (formula_options.formula_generator.max_size - != formula_options.formula_generator.size) + != formula_options.formula_generator.size) estream << "..." - + toString(formula_options.formula_generator.max_size); + + toString(formula_options.formula_generator.max_size); estream << string(" parse tree node") - + (formula_options.formula_generator.max_size == 1 ? "" : "s") - + ", " + + (formula_options.formula_generator.max_size == 1 ? "" : "s") + + ", " + toString(formula_options.formula_generator. number_of_available_variables) + " atomic proposition" - + (formula_options.formula_generator. + + (formula_options.formula_generator. number_of_available_variables == 1 ? "" : "s"); } else estream << "Reading LTL formulas from `" - + global_options.formula_input_filename - + "'."; + + global_options.formula_input_filename + + "'."; estream << '\n' + string(indent + 4, ' '); if (global_options.formula_change_interval == 0 || global_options.formula_change_interval - >= global_options.number_of_rounds) + >= global_options.number_of_rounds) estream << "Using a fixed LTL formula."; else { @@ -1357,7 +1353,7 @@ void Configuration::print(ostream& stream, int indent) const || global_options.formula_change_interval % 100 >= 20) { switch (global_options.formula_change_interval % 10) - { + { case 1 : estream << "st"; break; case 2 : estream << "nd"; break; case 3 : estream << "rd"; break; @@ -1378,18 +1374,18 @@ void Configuration::print(ostream& stream, int indent) const if (global_options.formula_input_filename.empty() && formula_options.generate_mode == NNF) estream << string(indent + 4, ' ') - + "Formulas will be generated into negation normal form.\n"; + + "Formulas will be generated into negation normal form.\n"; else if (formula_options.output_mode == NNF) estream << string(indent + 4, ' ') - + "Formulas will be converted into negation normal form.\n"; + + "Formulas will be converted into negation normal form.\n"; if (global_options.formula_input_filename.empty()) { estream << string(indent + 4, ' ') + "Random seed: " - + toString(global_options.formula_random_seed) - + '\n' + string(indent + 4, ' ') - + "Atomic symbols in use (priority):\n" - + string(indent + 6, ' '); + + toString(global_options.formula_random_seed) + + '\n' + string(indent + 4, ' ') + + "Atomic symbols in use (priority):\n" + + string(indent + 6, ' '); bool first_printed = false; @@ -1410,13 +1406,13 @@ void Configuration::print(ostream& stream, int indent) const switch (op->first) { - case ::Ltl::LTL_ATOM : + case ::Ltl::LTL_ATOM : estream << "propositions"; break; - case ::Ltl::LTL_TRUE : case ::Ltl::LTL_FALSE : + case ::Ltl::LTL_TRUE : case ::Ltl::LTL_FALSE : estream << ::Ltl::infixSymbol(op->first); break; - default : + default : break; } @@ -1425,7 +1421,7 @@ void Configuration::print(ostream& stream, int indent) const estream << '\n' << string(indent + 4, ' ') - + "Operators used for random LTL formula generation:"; + + "Operators used for random LTL formula generation:"; string operator_name_string; string operator_priority_string; @@ -1452,7 +1448,7 @@ void Configuration::print(ostream& stream, int indent) const { operator_name_string = string(11, ' ') + operator_name_string; operator_priority_string = string(11, ' ') - + operator_priority_string; + + operator_priority_string; operator_distribution_string = string(indent + 6, ' ') + "occurrences/formula "; } @@ -1478,7 +1474,7 @@ void Configuration::print(ostream& stream, int indent) const == max_operators_per_line - 1) { estream << '\n' + operator_name_string + '\n' - + operator_priority_string + '\n'; + + operator_priority_string + '\n'; if (!formula_options.symbol_distribution.empty()) estream << operator_distribution_string + '\n'; @@ -1498,7 +1494,7 @@ void Configuration::print(ostream& stream, int indent) const if (number_of_operators_printed % max_operators_per_line != 0) { estream << '\n' + operator_name_string + '\n' + operator_priority_string - + '\n'; + + '\n'; if (!formula_options.symbol_distribution.empty()) estream << operator_distribution_string + '\n'; @@ -1512,7 +1508,7 @@ void Configuration::print(ostream& stream, int indent) const /* ========================================================================= */ string Configuration::algorithmString (vector::size_type + ALLOC(Configuration::AlgorithmInformation) >::size_type algorithm_id) const /* ---------------------------------------------------------------------------- * @@ -1528,7 +1524,7 @@ string Configuration::algorithmString using namespace ::StringUtil; return toString(algorithm_id) + ": `" + *(algorithms[algorithm_id].name) - + '\''; + + '\''; } /* ========================================================================= */ @@ -1544,184 +1540,184 @@ void Configuration::showCommandLineHelp(const char* program_name) * ------------------------------------------------------------------------- */ { cout << string("Usage: ") + program_name - + " [OPTION]...\n\nGeneral options:\n" - " --[no]comparisontest Enable or disable the model " - "checking result\n" - " cross-comparison test\n" - " --configfile=FILE Read configuration from FILE\n" - " --[no]consistencytest Enable or disable the model " - "checking result\n" - " consistency test\n" - " --disable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID...]\n" - " Exclude implementation(s) from " - "tests\n" - " --enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID,...]\n" - " Include implementation(s) into " - "tests\n" - " --formulafile=FILE Read LTL formulas from FILE\n" - " --globalmodelcheck Use global model checking in " - "tests\n" - " (equivalent to " - "`--modelcheck=global')\n" - " -h, --help Show this help and exit\n" - " --interactive=MODE Set the interactivity mode " - "(`always', `onerror', \n" - " `never')\n" - " --[no]intersectiontest Enable or disable the Büchi " - "automata\n" - " intersection emptiness test\n" - " --localmodelcheck Use local model checking in tests" - "\n" - " (equivalent to " - "`--modelcheck=local')\n" - " --logfile=FILE Write error log to FILE\n" - " --modelcheck=MODE Set model checking mode " - "(`global' or `local')\n" - " --nopause Do not pause between test rounds " - "(equivalent to\n" - " `--interactive=never')\n" - " --pause Pause unconditionally after every " - "test round\n" - " (equivalent to " - "`--interactive=always')\n" - " --pauseonerror Pause between test rounds only in " - "case of an\n" - " error (equivalent to " - "`--interactive=onerror')\n" - " --profile Disable all automata correctness " - "tests\n" - " --quiet, --silent Run all tests silently without " - "interruption\n" - " --rounds=NUMBER-OF-ROUNDS Set number of test rounds (1-)\n" - " --showconfig Display current configuration and " - "exit\n" - " --showoperatordistribution Display probability distribution " - "for LTL formula\n" - " operators\n" - " --skip=NUMBER-OF-ROUNDS Set number of test rounds to skip " - "before\n" - " starting tests\n" - " --verbosity=INTEGER Set the verbosity of output (0-5)\n" - " --version Display program version and exit" - "\n\n" - "LTL formula generation options:\n" - " --[no]abbreviatedoperators Allow or disallow operators ->, " - "<->, xor, <>,\n" - " [], u, w in the generated " - "formulas\n" - " --andpriority=INTEGER Set priority for the /\\ operator\n" - " --beforepriority=INTEGER Set priority for the Before " - "operator\n" - " --defaultoperatorpriority=INTEGER\n" - " Set default priority for operators" - "\n" - " --equivalencepriority=INTEGER\n" - " Set priority for the <-> operator\n" - " --falsepriority=INTEGER Set priority for the constant " - "`false'\n" - " --finallypriority=INTEGER Set priority for the <> operator\n" - " --formulachangeinterval=NUMBER-OF-ROUNDS\n" - " Set formula generation interval in " - "test rounds\n" - " (0-)\n" - " --formulageneratemode=MODE Set formula generation mode " - "(`normal', `nnf')\n" - " --formulaoutputmode=MODE Set formula output mode (`normal', " - "`nnf')\n" - " --formulapropositions=NUMBER-OF-PROPOSITIONS\n" - " Set maximum number of atomic " - "propositions in\n" - " generated formulas (0-)\n" - " --formularandomseed=INTEGER Set random seed for the formula " - "generation\n" - " algorithm\n" - " --formulasize=SIZE,\n" - " --formulasize=MIN-SIZE...MAX-SIZE\n" - " Set size of random LTL formulas " - "(1-)\n" - " --[no]generatennf Force or prevent generating LTL " - "formulas in\n" - " negation normal form\n" - " --globallypriority=INTEGER Set priority for the [] operator\n" - " --implicationpriority=INTEGER\n" - " Set priority for the -> operator\n" - " --nextpriority=INTEGER Set priority for the Next operator" - "\n" - " --notpriority=INTEGER Set priority for the negation " - "operator\n" - " --orpriority=INTEGER Set priority for the \\/ operator\n" - " --[no]outputnnf Enable or disable formula " - "translation to\n" - " negation normal form before " - "invoking the\n" - " translators\n" - " --propositionpriority=INTEGER\n" - " Set priority for atomic " - "propositions\n" - " --releasepriority=INTEGER Set priority for the (Weak) Release" - " operator\n" - " --strongreleasepriority=INTEGER\n" - " Set priority for the Strong " - "Release operator\n" - " --truepriority=INTEGER Set priority for the constant " - "`true'\n" - " --untilpriority=INTEGER Set priority for the (Strong) Until" - " operator\n" - " --weakuntilpriority=INTEGER\n" - " Set priority for the Weak Until " - "operator\n" - " --xorpriority=INTEGER Set priority for the xor " - "operator\n\n" - "State space generation options:\n" - " --edgeprobability=PROBABILITY\n" - " Set random edge probability for " - "state spaces\n" - " (0.0--1.0)\n" - " --enumeratedpath Enumerate all paths of a given " - "size and a given\n" - " number of propositions per state " - "(equivalent to\n" - " `--statespacegeneratemode=" - "enumeratedpath')\n" - " --randomconnectedgraph Generate connected graphs as state " - "spaces\n" - " (equivalent to\n" - " `--statespacegeneratemode=" - "randomconnectedgraph')\n" - " --randomgraph Generate random graphs as state " - "spaces\n" - " (equivalent to\n" - " `--statespacegeneratemode=" - "randomgraph')\n" - " --randompath Generate random paths as state " - "spaces\n" - " (equivalent to\n" - " `--statespacegeneratemode=" - "randompath')\n" - " --statespacechangeinterval=NUMBER-OF-ROUNDS\n" - " Set state space generation " - "interval in test\n" - " rounds (0-)\n" - " --statespacegeneratemode=MODE\n" - " Set state space generation mode\n" - " (`randomconnectedgraph', " - "`randomgraph',\n" - " `randompath', `enumeratedpath')\n" - " --statespacepropositions=NUMBER-OF-PROPOSITIONS\n" - " Set number of propositions per " - "state (0-)\n" - " --statespacerandomseed=INTEGER\n" - " Set random seed for the state " - "space generation\n" - " algorithm\n" - " --statespacesize=SIZE,\n" - " --statespacesize=MIN-SIZE...MAX-SIZE\n" - " Set size of generated state spaces " - "(1-)\n" - " --truthprobability=PROBABILITY\n" - " Set truth probability of " - "propositions (0.0--1.0)\n\n" - "Report bugs to .\n"; + + " [OPTION]...\n\nGeneral options:\n" + " --[no]comparisontest Enable or disable the model " + "checking result\n" + " cross-comparison test\n" + " --configfile=FILE Read configuration from FILE\n" + " --[no]consistencytest Enable or disable the model " + "checking result\n" + " consistency test\n" + " --disable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID...]\n" + " Exclude implementation(s) from " + "tests\n" + " --enable=IMPLEMENTATION-ID[,IMPLEMENTATION-ID,...]\n" + " Include implementation(s) into " + "tests\n" + " --formulafile=FILE Read LTL formulas from FILE\n" + " --globalmodelcheck Use global model checking in " + "tests\n" + " (equivalent to " + "`--modelcheck=global')\n" + " -h, --help Show this help and exit\n" + " --interactive=MODE Set the interactivity mode " + "(`always', `onerror', \n" + " `never')\n" + " --[no]intersectiontest Enable or disable the Büchi " + "automata\n" + " intersection emptiness test\n" + " --localmodelcheck Use local model checking in tests" + "\n" + " (equivalent to " + "`--modelcheck=local')\n" + " --logfile=FILE Write error log to FILE\n" + " --modelcheck=MODE Set model checking mode " + "(`global' or `local')\n" + " --nopause Do not pause between test rounds " + "(equivalent to\n" + " `--interactive=never')\n" + " --pause Pause unconditionally after every " + "test round\n" + " (equivalent to " + "`--interactive=always')\n" + " --pauseonerror Pause between test rounds only in " + "case of an\n" + " error (equivalent to " + "`--interactive=onerror')\n" + " --profile Disable all automata correctness " + "tests\n" + " --quiet, --silent Run all tests silently without " + "interruption\n" + " --rounds=NUMBER-OF-ROUNDS Set number of test rounds (1-)\n" + " --showconfig Display current configuration and " + "exit\n" + " --showoperatordistribution Display probability distribution " + "for LTL formula\n" + " operators\n" + " --skip=NUMBER-OF-ROUNDS Set number of test rounds to skip " + "before\n" + " starting tests\n" + " --verbosity=INTEGER Set the verbosity of output (0-5)\n" + " --version Display program version and exit" + "\n\n" + "LTL formula generation options:\n" + " --[no]abbreviatedoperators Allow or disallow operators ->, " + "<->, xor, <>,\n" + " [], u, w in the generated " + "formulas\n" + " --andpriority=INTEGER Set priority for the /\\ operator\n" + " --beforepriority=INTEGER Set priority for the Before " + "operator\n" + " --defaultoperatorpriority=INTEGER\n" + " Set default priority for operators" + "\n" + " --equivalencepriority=INTEGER\n" + " Set priority for the <-> operator\n" + " --falsepriority=INTEGER Set priority for the constant " + "`false'\n" + " --finallypriority=INTEGER Set priority for the <> operator\n" + " --formulachangeinterval=NUMBER-OF-ROUNDS\n" + " Set formula generation interval in " + "test rounds\n" + " (0-)\n" + " --formulageneratemode=MODE Set formula generation mode " + "(`normal', `nnf')\n" + " --formulaoutputmode=MODE Set formula output mode (`normal', " + "`nnf')\n" + " --formulapropositions=NUMBER-OF-PROPOSITIONS\n" + " Set maximum number of atomic " + "propositions in\n" + " generated formulas (0-)\n" + " --formularandomseed=INTEGER Set random seed for the formula " + "generation\n" + " algorithm\n" + " --formulasize=SIZE,\n" + " --formulasize=MIN-SIZE...MAX-SIZE\n" + " Set size of random LTL formulas " + "(1-)\n" + " --[no]generatennf Force or prevent generating LTL " + "formulas in\n" + " negation normal form\n" + " --globallypriority=INTEGER Set priority for the [] operator\n" + " --implicationpriority=INTEGER\n" + " Set priority for the -> operator\n" + " --nextpriority=INTEGER Set priority for the Next operator" + "\n" + " --notpriority=INTEGER Set priority for the negation " + "operator\n" + " --orpriority=INTEGER Set priority for the \\/ operator\n" + " --[no]outputnnf Enable or disable formula " + "translation to\n" + " negation normal form before " + "invoking the\n" + " translators\n" + " --propositionpriority=INTEGER\n" + " Set priority for atomic " + "propositions\n" + " --releasepriority=INTEGER Set priority for the (Weak) Release" + " operator\n" + " --strongreleasepriority=INTEGER\n" + " Set priority for the Strong " + "Release operator\n" + " --truepriority=INTEGER Set priority for the constant " + "`true'\n" + " --untilpriority=INTEGER Set priority for the (Strong) Until" + " operator\n" + " --weakuntilpriority=INTEGER\n" + " Set priority for the Weak Until " + "operator\n" + " --xorpriority=INTEGER Set priority for the xor " + "operator\n\n" + "State space generation options:\n" + " --edgeprobability=PROBABILITY\n" + " Set random edge probability for " + "state spaces\n" + " (0.0--1.0)\n" + " --enumeratedpath Enumerate all paths of a given " + "size and a given\n" + " number of propositions per state " + "(equivalent to\n" + " `--statespacegeneratemode=" + "enumeratedpath')\n" + " --randomconnectedgraph Generate connected graphs as state " + "spaces\n" + " (equivalent to\n" + " `--statespacegeneratemode=" + "randomconnectedgraph')\n" + " --randomgraph Generate random graphs as state " + "spaces\n" + " (equivalent to\n" + " `--statespacegeneratemode=" + "randomgraph')\n" + " --randompath Generate random paths as state " + "spaces\n" + " (equivalent to\n" + " `--statespacegeneratemode=" + "randompath')\n" + " --statespacechangeinterval=NUMBER-OF-ROUNDS\n" + " Set state space generation " + "interval in test\n" + " rounds (0-)\n" + " --statespacegeneratemode=MODE\n" + " Set state space generation mode\n" + " (`randomconnectedgraph', " + "`randomgraph',\n" + " `randompath', `enumeratedpath')\n" + " --statespacepropositions=NUMBER-OF-PROPOSITIONS\n" + " Set number of propositions per " + "state (0-)\n" + " --statespacerandomseed=INTEGER\n" + " Set random seed for the state " + "space generation\n" + " algorithm\n" + " --statespacesize=SIZE,\n" + " --statespacesize=MIN-SIZE...MAX-SIZE\n" + " Set size of generated state spaces " + "(1-)\n" + " --truthprobability=PROBABILITY\n" + " Set truth probability of " + "propositions (0.0--1.0)\n\n" + "Report bugs to .\n"; } /* ========================================================================= */ @@ -1809,12 +1805,12 @@ long int Configuration::parseCommandLineInteger if (*endptr != '\0' || value.empty()) throw ConfigurationException - ("", "the argument for `--" + option + "' must be a nonnegative " - "integer"); + ("", "the argument for `--" + option + "' must be a nonnegative " + "integer"); if (val == LONG_MIN || val == LONG_MAX) throw ConfigurationException - ("", "the argument for `--" + option + "' is out of range"); + ("", "the argument for `--" + option + "' is out of range"); return val; } @@ -1899,7 +1895,7 @@ double Configuration::operatorProbability { if (arity == 1 && total_short_unary_priority > 0) result = static_cast(priority) - / static_cast(total_short_unary_priority); + / static_cast(total_short_unary_priority); else result = 0.0; } @@ -1931,7 +1927,7 @@ double Configuration::operatorProbability total_long_unary_priority, total_binary_priority, result_cache) - * operatorProbability(op, k - i, n - m - 1, + * operatorProbability(op, k - i, n - m - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, @@ -1946,7 +1942,7 @@ double Configuration::operatorProbability if (op != ::Ltl::LTL_NEGATION || formula_options.generate_mode != NNF) result += static_cast(priority) - * operatorProbability(op, k - 1, n - 1, + * operatorProbability(op, k - 1, n - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, @@ -1965,7 +1961,7 @@ double Configuration::operatorProbability total_long_unary_priority, total_binary_priority, result_cache) - * operatorProbability(op, k - 1 - i, n - m - 1, + * operatorProbability(op, k - 1 - i, n - m - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, @@ -1976,7 +1972,7 @@ double Configuration::operatorProbability } result += static_cast(p1) - * operatorProbability(op, k, n - 1, + * operatorProbability(op, k, n - 1, total_short_unary_priority, total_long_unary_priority, total_binary_priority, diff --git a/lbtt/src/Configuration.h b/lbtt/src/Configuration.h index 3b053c525..bdfeda739 100644 --- a/lbtt/src/Configuration.h +++ b/lbtt/src/Configuration.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,10 +20,6 @@ #ifndef CONFIGURATION_H #define CONFIGURATION_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include @@ -31,7 +27,7 @@ #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Exception.h" #include "FormulaRandomizer.h" #include "StateSpaceRandomizer.h" @@ -55,22 +51,22 @@ public: ~Configuration(); /* Destructor. */ void read(int argc, char* argv[]); /* Reads the program - * configuration. + * configuration. */ void print /* Writes the current */ (ostream& stream = cout, int indent = 0) const; /* configuration (in a - * textual form) to a - * stream. + * textual form) to a + * stream. */ struct AlgorithmInformation; /* See below. */ string algorithmString /* Formats the the id */ (vector::size_type/* the name of the */ + ALLOC(AlgorithmInformation) >::size_type/* the name of the */ algorithm_id) const; /* algorithm into a - * string. + * string. */ static void showCommandLineHelp /* Prints the list of */ @@ -79,52 +75,52 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ enum InteractionMode {NEVER, ALWAYS, ONERROR}; /* Enumeration constants - * affecting the behaviour - * of the program as - * regards user control. + * affecting the behaviour + * of the program as + * regards user control. */ enum FormulaMode {NORMAL, NNF}; /* Enumeration constants - * affecting the generation - * and output of random - * formulae. + * affecting the generation + * and output of random + * formulae. */ enum StateSpaceMode {RANDOMGRAPH = 1, /* Enumeration constants */ - RANDOMCONNECTEDGRAPH = 2, /* affecting the */ + RANDOMCONNECTEDGRAPH = 2, /* affecting the */ GRAPH = 3, /* generation of random */ - RANDOMPATH = 4, /* state spaces. */ - ENUMERATEDPATH = 8, - PATH = 12}; + RANDOMPATH = 4, /* state spaces. */ + ENUMERATEDPATH = 8, + PATH = 12}; enum ProductMode {LOCAL, GLOBAL}; /* Enumeration constants - * for controlling the - * scope of synchronous - * products. + * for controlling the + * scope of synchronous + * products. */ /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ struct AlgorithmInformation /* A structure for storing - * information about a - * particular algorithm - * (name, path to - * executable, command-line - * parameters). + * information about a + * particular algorithm + * (name, path to + * executable, command-line + * parameters). */ { string* name; /* Name of the algorithm. - */ + */ string* path_to_program; /* Path to the executable - * required for running - * the algorithm. + * required for running + * the algorithm. */ string* extra_parameters; /* Additional command-line - * parameters required for - * running the executable. - */ + * parameters required for + * running the executable. + */ bool enabled; /* Determines whether the * algorithm is enabled @@ -136,42 +132,42 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ struct GlobalConfiguration /* A structure for storing - * all the information - * affecting the general - * behaviour of the - * program. + * all the information + * affecting the general + * behaviour of the + * program. */ { int verbosity; /* Determines the verbosity - * of program output (0-5, - * the bigger the value, - * the more information - * will be shown). + * of program output (0-5, + * the bigger the value, + * the more information + * will be shown). */ InteractionMode interactive; /* Controls the behaviour - * of the program as - * regards the ability of - * the user to enter - * commands between test - * rounds. Possible values - * and their meanings are: - * - * NEVER: - * Run all tests without - * interruption. - * ALWAYS: - * Pause after each test - * round to wait for - * user commands. - * ONERROR: - * Try to run the tests - * without interruption. - * However, in case of - * an error, pause and - * wait for user - * commands. - */ + * of the program as + * regards the ability of + * the user to enter + * commands between test + * rounds. Possible values + * and their meanings are: + * + * NEVER: + * Run all tests without + * interruption. + * ALWAYS: + * Pause after each test + * round to wait for + * user commands. + * ONERROR: + * Try to run the tests + * without interruption. + * However, in case of + * an error, pause and + * wait for user + * commands. + */ unsigned long int number_of_rounds; /* Number of test rounds. */ @@ -181,22 +177,22 @@ public: */ unsigned long int statespace_change_interval; /* Determines the frequency - * (in rounds) of how often - * a new state space is - * generated. + * (in rounds) of how often + * a new state space is + * generated. */ - + StateSpaceMode statespace_generation_mode; /* Random state space * generation mode. * Available options are: - * - * RANDOMGRAPH: - * Generate random - * connected graphs as - * state spaces. - * RANDOMPATH: - * Generate paths as - * state spaces, choose + * + * RANDOMGRAPH: + * Generate random + * connected graphs as + * state spaces. + * RANDOMPATH: + * Generate paths as + * state spaces, choose * the loop and the * truth assignments for * atomic propositions @@ -207,47 +203,47 @@ public: * enumerating all * possible paths of a * given length. - */ + */ unsigned long int formula_change_interval; /* Determines the frequency - * (in rounds) of how often - * a new formula is - * generated. + * (in rounds) of how often + * a new formula is + * generated. */ ProductMode product_mode; /* Determines the scope of - * the synchronous products - * computed by the program. - * Possible values and - * their meanings are: - * - * LOCAL: - * The synchronous - * products are computed - * only with respect to - * the initial state of - * the system. This will - * save memory but makes - * the algorithm cross- - * comparisons less - * powerful, possibly - * at the cost of - * chances for finding - * inconsistencies in the - * results. - * GLOBAL: - * The synchronous - * products are computed - * with respect to each - * system state (i.e. - * the formula is model - * checked in each system - * state separately). - * This will usually + * the synchronous products + * computed by the program. + * Possible values and + * their meanings are: + * + * LOCAL: + * The synchronous + * products are computed + * only with respect to + * the initial state of + * the system. This will + * save memory but makes + * the algorithm cross- + * comparisons less + * powerful, possibly + * at the cost of + * chances for finding + * inconsistencies in the + * results. + * GLOBAL: + * The synchronous + * products are computed + * with respect to each + * system state (i.e. + * the formula is model + * checked in each system + * state separately). + * This will usually * require more memory - * than the other - * alternative. - */ + * than the other + * alternative. + */ string cfg_filename; /* Name for the * configuration file. @@ -269,7 +265,7 @@ public: bool do_cons_test; /* Is the model checking * result consistency check - * enabled? + * enabled? */ bool do_intr_test; /* Is the automata @@ -285,9 +281,9 @@ public: }; struct FormulaConfiguration /* A structure for storing - * specific information - * affecting the generation - * of random formulae. + * specific information + * affecting the generation + * of random formulae. */ { int default_operator_priority; /* Default priority for all @@ -304,79 +300,79 @@ public: */ bool allow_abbreviated_operators; /* Determines whether the - * operators ->, <->, xor, + * operators ->, <->, xor, * <>, [], W and M should * be allowed when - * generating random - * formulae (these are - * `abbreviated' operators - * since they could be - * written in an equivalent - * form by using another - * operators). + * generating random + * formulae (these are + * `abbreviated' operators + * since they could be + * written in an equivalent + * form by using another + * operators). */ Configuration::FormulaMode output_mode; /* Determines whether the - * generated formulae are - * to be converted to - * negation normal form - * before passing them to - * the different - * algorithms. Possible - * values are: - * - * NORMAL: - * No conversion. - * NNF: - * Do the conversion - * (this may affect the - * size of the formulae!) - */ + * generated formulae are + * to be converted to + * negation normal form + * before passing them to + * the different + * algorithms. Possible + * values are: + * + * NORMAL: + * No conversion. + * NNF: + * Do the conversion + * (this may affect the + * size of the formulae!) + */ Configuration::FormulaMode generate_mode; /* Determines whether the - * formulae are to be - * generated in negation - * normal form (strict - * size requirement for - * formulae). Possible - * values are: - * - * NORMAL: - * Allow more flexibility - * in the generation of - * formulae. - * NNF: - * Force generation into - * negation normal form. - */ + * formulae are to be + * generated in negation + * normal form (strict + * size requirement for + * formulae). Possible + * values are: + * + * NORMAL: + * Allow more flexibility + * in the generation of + * formulae. + * NNF: + * Force generation into + * negation normal form. + */ ::Ltl::FormulaRandomizer formula_generator; /* Interface to the random - * LTL formula generation - * algorithm. - */ + * LTL formula generation + * algorithm. + */ }; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ vector algorithms; /* information about the - * algorithms used in - * the tests. + ALLOC(AlgorithmInformation) > algorithms; /* information about the + * algorithms used in + * the tests. */ GlobalConfiguration global_options; /* General configuration - * information. + * information. */ FormulaConfiguration formula_options; /* Configuration - * information for - * generating random - * formulae. + * information for + * generating random + * formulae. */ Graph::StateSpaceRandomizer /* Interface to the */ statespace_generator; /* random state space - * generation + * generation * algorithms. */ @@ -392,10 +388,10 @@ public: /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ class ConfigurationException : public Exception /* A class for reporting - * errors when reading - * the configuration file. - */ - { + * errors when reading + * the configuration file. + */ + { public: ConfigurationException /* Constructors. */ (const string& info = "", @@ -458,7 +454,7 @@ private: OPT_CONSISTENCYTEST, OPT_DISABLE, OPT_ENABLE, OPT_FORMULACHANGEINTERVAL, OPT_FORMULAFILE, OPT_FORMULARANDOMSEED, OPT_HELP = 'h', - OPT_GLOBALPRODUCT = 20000, OPT_INTERACTIVE, + OPT_GLOBALPRODUCT = 20000, OPT_INTERACTIVE, OPT_INTERSECTIONTEST, OPT_LOGFILE, OPT_MODELCHECK, OPT_NOCOMPARISONTEST, OPT_NOCONSISTENCYTEST, OPT_NOINTERSECTIONTEST, @@ -497,12 +493,12 @@ private: OPT_STATESPACESIZE, OPT_TRUTHPROBABILITY}; typedef map, double, /* Type definitions for */ - less >, /* the result cache used */ - ALLOC(double) > /* for computing the */ + less >, /* the result cache used */ + ALLOC(double) > /* for computing the */ ProbabilityMapElement; /* probability */ typedef map, /* formula operators. */ - ALLOC(ProbabilityMapElement) > + less, /* formula operators. */ + ALLOC(ProbabilityMapElement) > ProbabilityMap; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ @@ -514,8 +510,8 @@ private: */ void reset(); /* Initializes the - * configuration data - * to default values. + * configuration data + * to default values. */ long int parseCommandLineInteger /* Converts an integer */ diff --git a/lbtt/src/DispUtil.cc b/lbtt/src/DispUtil.cc index 4876a5726..4bfa825e8 100644 --- a/lbtt/src/DispUtil.cc +++ b/lbtt/src/DispUtil.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -17,14 +17,10 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "DispUtil.h" /****************************************************************************** diff --git a/lbtt/src/Exception.h b/lbtt/src/Exception.h index 3ac9e4dfb..a429704b7 100644 --- a/lbtt/src/Exception.h +++ b/lbtt/src/Exception.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -74,7 +74,7 @@ public: virtual ~UserBreakException() throw(); /* Destructor. */ UserBreakException& /* Assignment operator. */ - operator=(const UserBreakException& e); + operator=(const UserBreakException& e); /* `what' inherited from class Exception */ @@ -289,13 +289,13 @@ public: Exceptional_istream /* Constructor. */ (istream *istr, ios::iostate mask = ios::goodbit); - + /* default copy constructor */ - + ~Exceptional_istream(); /* Destructor. */ /* default assignment operator */ - + template /* Operator for reading */ Exceptional_istream &operator>>(T &t); /* from the stream. */ @@ -337,9 +337,9 @@ public: Exceptional_ostream /* Constructor. */ (ostream* ostr, ios::iostate mask = ios::goodbit); - + /* default copy constructor */ - + ~Exceptional_ostream(); /* Destructor. */ /* default assignment operator */ @@ -353,7 +353,7 @@ public: * aware output stream into * a regular output stream. */ - + private: ostream* stream; /* A pointer to the * `regular' output stream @@ -482,7 +482,7 @@ inline UserBreakException& UserBreakException::operator= (const UserBreakException& e) /* ---------------------------------------------------------------------------- * - * Descrption: Assignment operator for class UserBreakException. Assigns the + * Descrption: Assignment operator for class UserBreakException. Assigns the * value of another UserBreakException to `this' one. * * Argument: e -- A reference to a constant UserBreakException. @@ -808,7 +808,7 @@ inline FileWriteException::FileWriteException() : inline FileWriteException::FileWriteException (const string& filename, const string& details) : IOException("error writing to " + filename - + string(details.empty() ? "" : " " + details)) + + string(details.empty() ? "" : " " + details)) /* ---------------------------------------------------------------------------- * * Description: Constructor for class FileWriteException. This constructor @@ -954,7 +954,7 @@ inline Exceptional_istream::Exceptional_istream * * Arguments: istr -- A pointer to an object of type istream. * mask -- A bit mask determining when the Exceptional_istream - * should throw exceptions. The most useful constants + * should throw exceptions. The most useful constants * for the bit mask are * ios::badbit Throw an exception if the input * stream (after performing an input @@ -1060,7 +1060,7 @@ inline Exceptional_ostream::Exceptional_ostream * * Arguments: ostr -- A pointer to an object of type ostream. * mask -- A bit mask determining when the Exceptional_ostream - * should throw exceptions. The most useful constants + * should throw exceptions. The most useful constants * for the bit mask are * ios::badbit Throw an exception if the output * stream (after performing an output diff --git a/lbtt/src/ExternalTranslator.cc b/lbtt/src/ExternalTranslator.cc index 14ae40686..7da7b87d0 100644 --- a/lbtt/src/ExternalTranslator.cc +++ b/lbtt/src/ExternalTranslator.cc @@ -17,10 +17,6 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #include #include diff --git a/lbtt/src/ExternalTranslator.h b/lbtt/src/ExternalTranslator.h index 5dcd21f37..b0f973a81 100644 --- a/lbtt/src/ExternalTranslator.h +++ b/lbtt/src/ExternalTranslator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,10 +20,6 @@ #ifndef EXTERNALTRANSLATOR_H #define EXTERNALTRANSLATOR_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include @@ -33,7 +29,7 @@ #else #include #endif /* HAVE_SSTREAM */ -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Exception.h" #include "LtlFormula.h" #include "translate.h" @@ -210,8 +206,8 @@ private: */ stack > /* information. */ + deque > /* information. */ temporary_file_objects; friend class KecWrapper; /* Friend declarations. */ diff --git a/lbtt/src/FormulaRandomizer.h b/lbtt/src/FormulaRandomizer.h index d9d227b86..a0391d499 100644 --- a/lbtt/src/FormulaRandomizer.h +++ b/lbtt/src/FormulaRandomizer.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,14 +20,10 @@ #ifndef FORMULARANDOMIZER_H #define FORMULARANDOMIZER_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "LtlFormula.h" namespace Ltl diff --git a/lbtt/src/Graph.h.in b/lbtt/src/Graph.h.in index 8a9b3605b..29c8e52e6 100644 --- a/lbtt/src/Graph.h.in +++ b/lbtt/src/Graph.h.in @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -34,7 +34,7 @@ using SLIST_NAMESPACE::slist; #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "Exception.h" diff --git a/lbtt/src/LtlFormula.h b/lbtt/src/LtlFormula.h index 70c56fad4..c5b2efea7 100644 --- a/lbtt/src/LtlFormula.h +++ b/lbtt/src/LtlFormula.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,17 +20,13 @@ #ifndef LTLFORMULA_H #define LTLFORMULA_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "Exception.h" diff --git a/lbtt/src/Makefile.am b/lbtt/src/Makefile.am index fdd6af547..a2ef8a4f1 100644 --- a/lbtt/src/Makefile.am +++ b/lbtt/src/Makefile.am @@ -16,10 +16,10 @@ lbtt_SOURCES = \ FormulaRandomizer.cc \ FormulaRandomizer.h \ FormulaWriter.h \ + LbttAlloc.h \ LtlFormula.cc \ LtlFormula.h \ main.cc \ - ObstackAlloc.h \ PathEvaluator.cc \ PathEvaluator.h \ PathIterator.cc \ diff --git a/lbtt/src/NeverClaimAutomaton.h b/lbtt/src/NeverClaimAutomaton.h index 6b230cd65..0ab31b905 100644 --- a/lbtt/src/NeverClaimAutomaton.h +++ b/lbtt/src/NeverClaimAutomaton.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,16 +20,12 @@ #ifndef NEVERCLAIMAUTOMATON_H #define NEVERCLAIMAUTOMATON_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Exception.h" using namespace std; diff --git a/lbtt/src/ObstackAlloc.h b/lbtt/src/ObstackAlloc.h deleted file mode 100644 index 9f9b0a579..000000000 --- a/lbtt/src/ObstackAlloc.h +++ /dev/null @@ -1,166 +0,0 @@ -/* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 - * Heikki Tauriainen - * - * This program 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 2 - * of the License, or (at your option) any later version. - * - * This program 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, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - */ - -#ifndef ALLOC_H -#define ALLOC_H - -#include - -#ifdef HAVE_SINGLE_CLIENT_ALLOC -#define ALLOC(typename) single_client_alloc -#else -#define ALLOC(typename) allocator -#endif /* HAVE_SINGLE_CLIENT_ALLOC */ - -#ifdef HAVE_OBSTACK_H - -/* GNU libc 2.3's copy of obstack.h uses a definition of __INT_TO_PTR - which does not compile in C++. Fortunately it will not override - an existing definition. */ -#if __GLIBC__ == 2 && __GLIBC_MINOR__ == 3 -# define __INT_TO_PTR(P) ((P) + (char *) 0) -#endif - -#include -#include -#include - -/****************************************************************************** - * - * A wrapper class for allocating memory through an obstack. - * - *****************************************************************************/ - -class ObstackAllocator -{ -public: - ObstackAllocator(); /* Constructor. */ - - ~ObstackAllocator(); /* Destructor. */ - - void* alloc(int size); /* Allocates memory. */ - - void free(void* obj); /* Deallocates memory. */ - - static void failure(); /* Callback function for - * reporting a memory - * allocation failure. - */ -private: - ObstackAllocator(const ObstackAllocator&); /* Prevent copying and */ - ObstackAllocator& operator= /* assignment of */ - (const ObstackAllocator&); /* ObstackAllocator - * objects. - */ - - struct obstack store; /* The obstack. */ -}; - -#define obstack_chunk_alloc std::malloc -#define obstack_chunk_free std::free - - - -/****************************************************************************** - * - * Inline function definitions for class ObstackAllocator. - * - *****************************************************************************/ - -/* ========================================================================= */ -inline ObstackAllocator::ObstackAllocator() -/* ---------------------------------------------------------------------------- - * - * Description: Constructor for class ObstackAllocator. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - obstack_init(&store); -} - -/* ========================================================================= */ -inline ObstackAllocator::~ObstackAllocator() -/* ---------------------------------------------------------------------------- - * - * Description: Destructor for class ObstackAllocator. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - obstack_free(&store, NULL); -} - -/* ========================================================================= */ -inline void* ObstackAllocator::alloc(int size) -/* ---------------------------------------------------------------------------- - * - * Description: Interface to the memory allocator. - * - * Argument: size -- Number of bytes to allocate. - * - * Returns: A pointer to the beginning of the newly allocated memory. - * - * ------------------------------------------------------------------------- */ -{ - return obstack_alloc(&store, size); -} - -/* ========================================================================= */ -inline void ObstackAllocator::free(void* obj) -/* ---------------------------------------------------------------------------- - * - * Description: Interface to the memory deallocation function. - * - * Argument: obj -- A pointer to the object to deallocate. (Because the - * underlying memory allocator is an obstack, freeing - * an object also releases all objects allocated after - * the given object.) - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - obstack_free(&store, obj); -} - -/* ========================================================================= */ -inline void ObstackAllocator::failure() -/* ---------------------------------------------------------------------------- - * - * Description: Callback function for reporting memory allocation failures. - * - * Arguments: None. - * - * Returns: Nothing. - * - * ------------------------------------------------------------------------- */ -{ - throw std::bad_alloc(); -} - -#endif /* HAVE_OBSTACK_H */ - -#endif /* !ALLOC_H */ diff --git a/lbtt/src/PathEvaluator.h b/lbtt/src/PathEvaluator.h index 74693cc50..7b7a178ef 100644 --- a/lbtt/src/PathEvaluator.h +++ b/lbtt/src/PathEvaluator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,13 +20,9 @@ #ifndef PATHEVALUATOR_H #define PATHEVALUATOR_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "Exception.h" #include "LtlFormula.h" diff --git a/lbtt/src/ProductAutomaton.h b/lbtt/src/ProductAutomaton.h index 962829689..060491c7d 100644 --- a/lbtt/src/ProductAutomaton.h +++ b/lbtt/src/ProductAutomaton.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,15 +20,11 @@ #ifndef PRODUCTAUTOMATON_H #define PRODUCTAUTOMATON_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "BuchiAutomaton.h" #include "EdgeContainer.h" diff --git a/lbtt/src/SccIterator.h b/lbtt/src/SccIterator.h index 87e174e72..fceaceeea 100644 --- a/lbtt/src/SccIterator.h +++ b/lbtt/src/SccIterator.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -25,7 +25,7 @@ #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Graph.h" using namespace std; diff --git a/lbtt/src/SharedTestData.h b/lbtt/src/SharedTestData.h index 77bace624..6403c52d4 100644 --- a/lbtt/src/SharedTestData.h +++ b/lbtt/src/SharedTestData.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -21,7 +21,7 @@ #define SHAREDTESTDATA_H #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Exception.h" #include "TestRoundInfo.h" #include "TestStatistics.h" diff --git a/lbtt/src/StatDisplay.h b/lbtt/src/StatDisplay.h index d44c4d8ae..a4a947ad5 100644 --- a/lbtt/src/StatDisplay.h +++ b/lbtt/src/StatDisplay.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,14 +20,10 @@ #ifndef STATDISPLAY_H #define STATDISPLAY_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Configuration.h" #include "TestStatistics.h" diff --git a/lbtt/src/StateSpace.h b/lbtt/src/StateSpace.h index b25eb51b8..338a5a4d1 100644 --- a/lbtt/src/StateSpace.h +++ b/lbtt/src/StateSpace.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,12 +20,8 @@ #ifndef STATESPACE_H #define STATESPACE_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "EdgeContainer.h" #include "Graph.h" diff --git a/lbtt/src/StateSpaceRandomizer.cc b/lbtt/src/StateSpaceRandomizer.cc index 6a4db5d83..951b4567c 100644 --- a/lbtt/src/StateSpaceRandomizer.cc +++ b/lbtt/src/StateSpaceRandomizer.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -17,14 +17,10 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BitArray.h" #include "Exception.h" #include "StateSpaceRandomizer.h" diff --git a/lbtt/src/StringUtil.h b/lbtt/src/StringUtil.h index 271d07ddb..65a9fa790 100644 --- a/lbtt/src/StringUtil.h +++ b/lbtt/src/StringUtil.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,10 +20,6 @@ #ifndef STRINGUTIL_H #define STRINGUTIL_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include @@ -33,7 +29,7 @@ #include #endif /* HAVE_SSTREAM */ #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Exception.h" using namespace std; diff --git a/lbtt/src/TestOperations.cc b/lbtt/src/TestOperations.cc index b215b3705..4504fd4fb 100644 --- a/lbtt/src/TestOperations.cc +++ b/lbtt/src/TestOperations.cc @@ -17,10 +17,6 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #include #include diff --git a/lbtt/src/TestOperations.h b/lbtt/src/TestOperations.h index 23e84469d..f96ccdac3 100644 --- a/lbtt/src/TestOperations.h +++ b/lbtt/src/TestOperations.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,16 +20,12 @@ #ifndef TESTOPERATIONS_H #define TESTOPERATIONS_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Configuration.h" #include "Exception.h" #include "StateSpace.h" diff --git a/lbtt/src/TestRoundInfo.h b/lbtt/src/TestRoundInfo.h index 83edb0d9c..23351792a 100644 --- a/lbtt/src/TestRoundInfo.h +++ b/lbtt/src/TestRoundInfo.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -25,7 +25,7 @@ #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Exception.h" #include "LtlFormula.h" #include "ProductAutomaton.h" diff --git a/lbtt/src/TestStatistics.h b/lbtt/src/TestStatistics.h index d71176ddd..70cc6110e 100644 --- a/lbtt/src/TestStatistics.h +++ b/lbtt/src/TestStatistics.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,14 +20,10 @@ #ifndef TESTSTATISTICS_H #define TESTSTATISTICS_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BuchiAutomaton.h" #include "Configuration.h" #include "ProductAutomaton.h" diff --git a/lbtt/src/UserCommandReader.h b/lbtt/src/UserCommandReader.h index 218a8a438..dfe489291 100644 --- a/lbtt/src/UserCommandReader.h +++ b/lbtt/src/UserCommandReader.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,15 +20,11 @@ #ifndef USERCOMMANDREADER_H #define USERCOMMANDREADER_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Configuration.h" #include "Exception.h" diff --git a/lbtt/src/UserCommands.h b/lbtt/src/UserCommands.h index 368c00a22..31167eae2 100644 --- a/lbtt/src/UserCommands.h +++ b/lbtt/src/UserCommands.h @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -20,17 +20,13 @@ #ifndef USERCOMMANDS_H #define USERCOMMANDS_H -#ifdef __GNUC__ -#pragma interface -#endif /* __GNUC__ */ - #include #include #include #include #include #include -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "BuchiAutomaton.h" #include "Configuration.h" #include "ProductAutomaton.h" diff --git a/lbtt/src/main.cc b/lbtt/src/main.cc index d1b0693ad..197fbe171 100644 --- a/lbtt/src/main.cc +++ b/lbtt/src/main.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -28,7 +28,7 @@ #include #include #endif /* HAVE_READLINE */ -#include "ObstackAlloc.h" +#include "LbttAlloc.h" #include "Configuration.h" #include "DispUtil.h" #include "Exception.h" diff --git a/lbtt/src/translate.cc b/lbtt/src/translate.cc index 4b2d3577e..e21a08287 100644 --- a/lbtt/src/translate.cc +++ b/lbtt/src/translate.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002, 2003 + * Copyright (C) 1999, 2000, 2001, 2002, 2003, 2004 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -17,10 +17,6 @@ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */ -#ifdef __GNUC__ -#pragma implementation -#endif /* __GNUC__ */ - #include #include #include