Dream.cpp

Go to the documentation of this file.
00001 /** @file Dream.cpp
00002 * @author Gabor Madl
00003 * @date Created 06/2005
00004 * @brief Main executable for DREAM.
00005 * This file manages the text-based menu, the XML parser, the simulation, verification and optimization engines of DREAM.
00006 *
00007 *
00008 * =================================================================
00009 * DREAM License v2.0
00010 * 
00011 * DREAM - Distributed Real-time Embedded Analysis Method
00012 * http://dre.sourceforge.net.
00013 * Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.
00014 * 
00015 * This file is part of DREAM.
00016 * 
00017 * DREAM is free software; you can redistribute it and/or modify it
00018 * under the terms of the GNU General Public License version 2 as
00019 * published by the Free Software Foundation. No future versions of
00020 * the GPL license may be automatically applied to DREAM. It is in
00021 * the sole discretion of the copyright holder to determine whether
00022 * DREAM may be released under a different license or terms. There
00023 * are no restrictions on the use of DREAM for any purpose.
00024 * 
00025 * DREAM is distributed in the hope that it will be useful,
00026 * but WITHOUT ANY WARRANTY; without even the implied warranty of
00027 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
00028 * GNU General Public License for more details.
00029 * 
00030 * You should have received a copy of the GNU General Public License
00031 * along with this program; if not, write to the Free Software
00032 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
00033 * MA 02110-1301, USA.
00034 * 
00035 * By submitting comments, suggestions, code, code snippets,
00036 * techniques (including that of usage), and algorithms, submitters
00037 * acknowledge that they have the right to do so, that any such
00038 * submissions are given freely and unreservedly, and that they
00039 * waive any claims to copyright or ownership. In addition,
00040 * submitters acknowledge that any such submission might become
00041 * part of the copyright maintained on the overall body of code,
00042 * which comprises DREAM. By making a submission, submitter agrees
00043 * to these terms. Furthermore, submitters acknowledge that the
00044 * incorporation or modification of such submissions is entirely
00045 * at the discretion of the moderators of the DREAM project.
00046 * 
00047 * DREAM links to the Libxml2 third party library. Please see 
00048 * COPYING-libxml for the copyright information of Libxml2.
00049 * =================================================================
00050 *
00051 * NOTICE: If you use Visual Studio 2005, make sure to apply
00052 * service pack 1, as DREAM uses std::iostream, that leaks memory
00053 * in the VS 2005 C runtime library.
00054 *
00055 * More information:
00056 * http://connect.microsoft.com/VisualStudio/feedback/ViewFeedback.aspx?FeedbackID=98861
00057 *
00058 * DREAM 0.7 Beta is a major jump from previous releases. The main
00059 * discrete event simulation-based model checking is not only more
00060 * stable, but also faster in this release. DREAM 0.7 Beta was checked
00061 * for memory leaks using Valgrind (http://valgrind.org). Several
00062 * memory leaks were traced down and fixed. There are no known
00063 * memory leaks present in the current release.
00064 *
00065 * DREAM 0.7 Beta Linux release now implements several
00066 * optimizations for improved model checking performance. We
00067 * profiled DREAM using Callgrind (http://valgrind.org/info/tools.html),
00068 * and KCacheGrind (http://kcachegrind.sourceforge.net), and
00069 * managed to achieve impressive performance gains (around 2-3x at
00070 * least) compared to previous DREAM releases.
00071 *
00072 * FYI: the Linux version of DREAM 0.7 Beta is faster than the Win XP
00073 * MSVC 2005 version on my laptop (by around 30-50%). If I'm not
00074 * mistaken this hasn't been the case before. GCC is clearly
00075 * improving...
00076 *
00077 * Balanced AVL trees are now used to store branching points and
00078 * race conditions at run-time, resulting in exponential speedups in
00079 * several steps of the model checking method. Implemented XML
00080 * Schema validation. Upgraded verification time reporting to include
00081 * some meaningful data on the simulation speeds. Random
00082 * simulation-based testing now provides an execution trace when a
00083 * deadline is missed. Added performance estimation capability.
00084 * Updated Uppaal interpreter to use the new Uppaal 4 syntax.
00085 *
00086 * Moved source code from CVS to Subversion on Sourceforge. To
00087 * simplify development efforts, only VC7.1, VC8.0 and GNU make/gcc
00088 * build processes are supported in DREAM from now on. Added Visual
00089 * Studio project files for the libxml2 library under Win32.
00090 */
00091 
00092 #include "../algorithm/ModelCheck.h"
00093 #include "IFInterpreter.h"
00094 #include "UppaalInterpreter.h"
00095 #include "../core/Common.h"
00096 
00097 #include "XMLParser.h"
00098 
00099 static void usage ()
00100 {
00101                 std::cout << "Usage:" << std::endl << std::endl
00102                 << "dream [command] [options] <XML input file> [Output file]" << std::endl << std::endl
00103                 << "Commands:" << std::endl
00104                 << "    -cc - Model checking and performance estimation" << std::endl
00105                 << "             (for non-preemptive fixed priority scheduling)." << std::endl
00106                 << "    -if - Input generation for the Verimag IF toolset" << std::endl
00107                 << "             (specify output file)." << std::endl
00108                 << "    -ot - Thread-level subpriority assignment optimization." << std::endl
00109                 << "    -oc - CPU-level priority and subpriority assignment optimization." << std::endl
00110                 << "    -sr - Non-deterministic random discrete event simulation." << std::endl
00111                 << "    -tr - Random simulation-based testing" << std::endl
00112                 << "    -up - Input generation for the UPPAAL model checker" << std::endl
00113                 << "             (specify output file)." << std::endl
00114                 << "    -? - Show this help." << std::endl
00115                 << "Options:" << std::endl
00116                 << "    -dc - Disables race condition combinations checking." << std::endl
00117                 << "    -db - Disables branching point checking." << std::endl
00118                 << "    -dr - Disables race conditions (and their combinations) checking." << std::endl
00119                 << "    -dx - Disables error condition on non-executing tasks." << std::endl
00120                 << "    -ez - Enables race conditions between zero-time events." << std::endl
00121                 << "    -nr [param] - The number of repetitions in various algorithms" << std::endl
00122                 << "             (used by commands -tr, -ot, and -oc)." << std::endl
00123                 << "    -ss [param] - The size of the optimization space" << std::endl
00124                 << "             (used by commands -ot and -oc)." << std::endl
00125                 << "    -tl [param] - The time limit for global time in simulations" << std::endl
00126                 << "             (used by commands -cc, -cm, -tr, and -sr)." << std::endl
00127                 << "    -v - Enables verbose output"
00128 #ifdef DREAM_VERBOSE2
00129                 << std::endl << "       -ve - Enables extremely verbose output"
00130 #endif
00131                 << std::endl << std::endl;
00132 }
00133 
00134 int main (int argc, char* argv[])
00135 {
00136         try
00137         {
00138                 if (argc < 3)
00139                 {
00140                         usage ();
00141                         exit (1);
00142                 }
00143 
00144                 enum {model_checking, random_testing, simulation,
00145                         thread_priority_optimization, cpu_priority_optimization,
00146                         if_interpreter, uppaal_interpreter} command;
00147 
00148                 static const char* const param = argv[1];
00149 
00150                 // Commands
00151                 if (!strncmp (argv[1], "-cc", 3))
00152                         command = model_checking;
00153                 else if (!strncmp (argv[1], "-if", 3))
00154                         command = if_interpreter;
00155                 else if (!strncmp (argv[1], "-ot", 3))
00156                         command = thread_priority_optimization;
00157                 else if (!strncmp (argv[1], "-oc", 3))
00158                         command = cpu_priority_optimization;
00159                 else if (!strncmp (argv[1], "-sr", 3))
00160                         command = simulation;
00161                 else if (!strncmp (argv[1], "-tr", 3))
00162                         command = random_testing;
00163                 else if (!strncmp (argv[1], "-up", 3))
00164                         command = uppaal_interpreter;
00165                 else
00166                 {
00167                         usage ();
00168                         exit (1);
00169                 }
00170 
00171                 // Options
00172                 DREAM::uint i;
00173                 
00174                 for (i = 2; i <= argc; i++)
00175                 {
00176                         if (!strncmp (argv[i], "-nr", 3))
00177                         {
00178                                 // Convert number
00179                                 Option::number_of_repetitions_ = DREAM::chartouint (argv[++i]);
00180                         }
00181                         else if (!strncmp (argv[i], "-ss", 3))
00182                         {
00183                                 // Convert number
00184                                 Option::optimization_space_ = DREAM::chartouint (argv[++i]);
00185                         }
00186                         else if (!strncmp (argv[i], "-tl", 3))
00187                         {
00188                                 // Convert number
00189                                 Option::simulation_time_ = DREAM::chartouint (argv[++i]);
00190                         }
00191                         else if (!strncmp (argv[i], "-db", 3))
00192                         {
00193                                 std::cout << "Branching is disabled during model checking..." << std::endl;
00194                                 Option::branching_ = false;
00195                         }
00196                         else if (!strncmp (argv[i], "-dr", 3))
00197                         {
00198                                 std::cout << "Race conditions are disabled during model checking..." << std::endl;
00199                                 Option::race_condition_ = false;
00200                         }
00201                         else if (!strncmp (argv[i], "-dc", 3))
00202                         {
00203                                 std::cout << "Race condition combinations are disabled during model checking..." << std::endl;
00204                                 Option::race_condition_combination_ = false;
00205                         }
00206                         else if (!strncmp (argv[i], "-dx", 3))
00207                         {
00208                                 std::cout << "Disabling error condition on non-executing tasks during model checking..." << std::endl;
00209                                 Option::non_executing_tasks_ = true;
00210                         }
00211                         else if (!strncmp (argv[i], "-ez", 3))
00212                         {
00213                                 std::cout << "Race conditions between zero-time events are enabled during model checking..." << std::endl;
00214                                 Option::race_condition_zero_ = true;
00215                         }
00216                         else if (!strncmp (argv[i], "-v", 3))
00217                         {
00218                                 std::cout << "Verbose output enabled..." << std::endl;
00219                                 Option::verbose1_ = true;
00220                         }
00221 #ifdef DREAM_VERBOSE2
00222                         else if (!strncmp (argv[i], "-ve", 3))
00223                         {
00224                                 std::cout << "Extremely verbose output enabled..." << std::endl;
00225                                 Option::verbose2_ = true;
00226                         }
00227 #endif
00228                         else break;
00229                 }
00230 
00231                 while (!strncmp (argv[i], "-", 1))
00232                         ++i;
00233 
00234                 static char* xmlFile = argv[i];
00235                 static char* outputFile;
00236 
00237                 if (argv[3])
00238                 {
00239                         outputFile = argv[3];
00240                 }
00241 
00242                 int ret_value = 0;
00243                 DREAM::System system;
00244                 DREAM::XMLParser parser;
00245                 
00246                 // Generate random seed...
00247                 srand ((unsigned)time (NULL));
00248 
00249                 if (command == model_checking)
00250                 {
00251                         if (Option::simulation_time_ == 0)
00252                         {
00253                                 std::cerr << "Simulation time limit is not set." << std::endl;
00254                                 ret_value = 1;
00255                         }
00256                         if (ret_value == 1)
00257                                 exit (1);
00258 
00259                         DREAM::ModelCheck modelcheck (&system);
00260 
00261                         parser.parse (xmlFile, &system);
00262                         if (!modelcheck.trace_based_model_check (&system, true))
00263                                 ret_value = 2;
00264                 }
00265                 else if (command == random_testing)
00266                 {
00267                         if (Option::simulation_time_ == 0)
00268                         {
00269                                 std::cerr << "Simulation time limit is not set." << std::endl;
00270                                 ret_value = 1;
00271                         }
00272                         if (Option::number_of_repetitions_ == 0)
00273                         {
00274                                 std::cerr << "Number of repetitions is not set." << std::endl;
00275                                 ret_value = 1;
00276                         }
00277                         if (ret_value == 1)
00278                                 exit (1);
00279 
00280                         DREAM::ModelCheck modelcheck (&system);
00281 
00282                         parser.parse (xmlFile, &system);
00283                         if (!modelcheck.random_testing (&system, true))
00284                                 ret_value = 2;
00285                 }
00286                 else if (command == simulation)
00287                 {
00288                         if (Option::simulation_time_ == 0)
00289                         {
00290                                 std::cerr << "Simulation time limit is not set." << std::endl;
00291                                 ret_value = 1;
00292                         }
00293                         if (ret_value == 1)
00294                                 exit (1);
00295 
00296                         parser.parse (xmlFile, &system);
00297                         DREAM::Solution solution (&system);
00298                         Option::verbose1_ = true;
00299                         if (solution.fitness (true, false) != 0.0)
00300                                 ret_value = 2;
00301                 }
00302                 else if (command == thread_priority_optimization)
00303                 {
00304                         if (Option::simulation_time_ == 0)
00305                         {
00306                                 std::cerr << "Simulation time limit is not set." << std::endl;
00307                                 ret_value = 1;
00308                         }
00309                         if (Option::number_of_repetitions_ == 0)
00310                         {
00311                                 std::cerr << "Number of repetitions is not set." << std::endl;
00312                                 ret_value = 1;
00313                         }
00314                         if (Option::optimization_space_ == 0)
00315                         {
00316                                 std::cerr << "Optimization space is not set." << std::endl;
00317                                 ret_value = 1;
00318                         }
00319                         if (ret_value == 1)
00320                                 exit (1);
00321 
00322                         DREAM::GeneticOptimize geneticoptimize;
00323                         parser.parse (xmlFile, &system);
00324                         geneticoptimize.thread_level (&system);
00325                         DREAM::Solution solution (&system);
00326                         if (solution.fitness (Option::verbose1_, false) != 0.0)
00327                                 ret_value = 2;
00328                 }
00329                 else if (command == cpu_priority_optimization)
00330                 {
00331                         if (Option::simulation_time_ == 0)
00332                         {
00333                                 std::cerr << "Simulation time limit is not set." << std::endl;
00334                                 ret_value = 1;
00335                         }
00336                         if (Option::number_of_repetitions_ == 0)
00337                         {
00338                                 std::cerr << "Number of repetitions is not set." << std::endl;
00339                                 ret_value = 1;
00340                         }
00341                         if (Option::optimization_space_ == 0)
00342                         {
00343                                 std::cerr << "Optimization space is not set." << std::endl;
00344                                 ret_value = 1;
00345                         }
00346                         if (ret_value == 1)
00347                                 exit (1);
00348 
00349                         DREAM::GeneticOptimize geneticoptimize;
00350 
00351                         parser.parse (xmlFile, &system);
00352                         geneticoptimize.CPU_level (&system);
00353                         DREAM::Solution solution (&system);
00354                         if (solution.fitness (Option::verbose1_, false) != 0.0)
00355                                 ret_value = 2;
00356                 }
00357                 else if (command == if_interpreter)
00358                 {
00359                         if (outputFile == NULL)
00360                         {
00361                                 usage ();
00362                                 throw DREAM::Exception ("No output file was specified for the IF toolset input generation.");
00363                         }
00364                         parser.parse (xmlFile, &system);
00365                         DREAM::IFInterpreter if_interpreter (&system);
00366                         if_interpreter.visitor_if (outputFile);
00367                 }
00368                 else if (command == uppaal_interpreter)
00369                 {
00370                         if (outputFile == NULL)
00371                         {
00372                                 usage ();
00373                                 throw DREAM::Exception ("No output file was specified for the Uppaal input generation.");
00374                         }
00375                         parser.parse (xmlFile, &system);
00376                         DREAM::UppaalInterpreter uppaal_interpreter (&system);
00377                         uppaal_interpreter.visitor_uppaaltemplate (outputFile);
00378                         uppaal_interpreter.visitor_uppaal (outputFile);
00379                 }
00380                 else
00381                 {
00382                         std::cerr << "This functionality is not implemented yet." << std::endl;
00383                         ret_value = 1;
00384                 }
00385 
00386                 return ret_value;
00387         }
00388         catch (DREAM::Exception* &ex)
00389         {
00390                 ex->handler ();
00391                 std::cerr << "Exiting..." << std::endl;
00392                 exit (1);
00393         }
00394         catch (DREAM::Exception ex)
00395         {
00396                 ex.handler ();
00397                 std::cerr << "Exiting..." << std::endl;
00398                 exit (1);
00399         }
00400         catch (std::bad_alloc& out_of_memory)
00401         {
00402                 std::cerr << "\nException! Out of memory: " << out_of_memory.what () << std::endl;
00403                 std::cerr << "Exiting..." << std::endl;
00404                 exit (1);
00405         }
00406         catch (...)
00407         {
00408                 std::cerr << "\nUndefined exception!" << std::endl;
00409                 std::cerr << "Exiting..." << std::endl;
00410                 exit (1);
00411         }
00412 }
00413 

Generated on Fri Jul 27 18:30:03 2007 for DREAM by  doxygen 1.5.1