Dream.cpp

Go to the documentation of this file.

/** @file Dream.cpp
* @author Gabor Madl
* @date Created 06/2005
* @brief Main executable for DREAM.
* This file manages the text-based menu, the XML parser, the simulation, verification and optimization engines of DREAM.
*
*
* =================================================================
* DREAM License v2.0
* 
* DREAM - Distributed Real-time Embedded Analysis Method
* http://dre.sourceforge.net.
* Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.
* 
* This file is part of DREAM.
* 
* DREAM is free software; you can redistribute it and/or modify it
* under the terms of the GNU General Public License version 2 as
* published by the Free Software Foundation. No future versions of
* the GPL license may be automatically applied to DREAM. It is in
* the sole discretion of the copyright holder to determine whether
* DREAM may be released under a different license or terms. There
* are no restrictions on the use of DREAM for any purpose.
* 
* DREAM 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., 51 Franklin Street, Fifth Floor, Boston,
* MA 02110-1301, USA.
* 
* By submitting comments, suggestions, code, code snippets,
* techniques (including that of usage), and algorithms, submitters
* acknowledge that they have the right to do so, that any such
* submissions are given freely and unreservedly, and that they
* waive any claims to copyright or ownership. In addition,
* submitters acknowledge that any such submission might become
* part of the copyright maintained on the overall body of code,
* which comprises DREAM. By making a submission, submitter agrees
* to these terms. Furthermore, submitters acknowledge that the
* incorporation or modification of such submissions is entirely
* at the discretion of the moderators of the DREAM project.
* 
* DREAM links to the Libxml2 third party library. Please see 
* COPYING-libxml for the copyright information of Libxml2.
* =================================================================
*
* NOTICE: If you use Visual Studio 2005, make sure to apply
* service pack 1, as DREAM uses std::iostream, that leaks memory
* in the VS 2005 C runtime library.
*
* More information:
* http://connect.microsoft.com/VisualStudio/feedback/ViewFeedback.aspx?FeedbackID=98861
*
* DREAM 0.7 Beta is a major jump from previous releases. The main
* discrete event simulation-based model checking is not only more
* stable, but also faster in this release. DREAM 0.7 Beta was checked
* for memory leaks using Valgrind (http://valgrind.org). Several
* memory leaks were traced down and fixed. There are no known
* memory leaks present in the current release.
*
* DREAM 0.7 Beta Linux release now implements several
* optimizations for improved model checking performance. We
* profiled DREAM using Callgrind (http://valgrind.org/info/tools.html),
* and KCacheGrind (http://kcachegrind.sourceforge.net), and
* managed to achieve impressive performance gains (around 2-3x at
* least) compared to previous DREAM releases.
*
* FYI: the Linux version of DREAM 0.7 Beta is faster than the Win XP
* MSVC 2005 version on my laptop (by around 30-50%). If I'm not
* mistaken this hasn't been the case before. GCC is clearly
* improving...
*
* Balanced AVL trees are now used to store branching points and
* race conditions at run-time, resulting in exponential speedups in
* several steps of the model checking method. Implemented XML
* Schema validation. Upgraded verification time reporting to include
* some meaningful data on the simulation speeds. Random
* simulation-based testing now provides an execution trace when a
* deadline is missed. Added performance estimation capability.
* Updated Uppaal interpreter to use the new Uppaal 4 syntax.
*
* Moved source code from CVS to Subversion on Sourceforge. To
* simplify development efforts, only VC7.1, VC8.0 and GNU make/gcc
* build processes are supported in DREAM from now on. Added Visual
* Studio project files for the libxml2 library under Win32.
*/

#include "../algorithm/ModelCheck.h"
#include "IFInterpreter.h"
#include "UppaalInterpreter.h"
#include "../core/Common.h"

#include "XMLParser.h"

static void usage ()
{
                std::cout << "Usage:" << std::endl << std::endl
                << "dream [command] [options] <XML input file> [Output file]" << std::endl << std::endl
                << "Commands:" << std::endl
                << "    -cc - Model checking and performance estimation" << std::endl
                << "             (for non-preemptive fixed priority scheduling)." << std::endl
                << "    -if - Input generation for the Verimag IF toolset" << std::endl
                << "             (specify output file)." << std::endl
                << "    -ot - Thread-level subpriority assignment optimization." << std::endl
                << "    -oc - CPU-level priority and subpriority assignment optimization." << std::endl
                << "    -sr - Non-deterministic random discrete event simulation." << std::endl
                << "    -tr - Random simulation-based testing" << std::endl
                << "    -up - Input generation for the UPPAAL model checker" << std::endl
                << "             (specify output file)." << std::endl
                << "    -? - Show this help." << std::endl
                << "Options:" << std::endl
                << "    -dc - Disables race condition combinations checking." << std::endl
                << "    -db - Disables branching point checking." << std::endl
                << "    -dr - Disables race conditions (and their combinations) checking." << std::endl
                << "    -dx - Disables error condition on non-executing tasks." << std::endl
                << "    -ez - Enables race conditions between zero-time events." << std::endl
                << "    -nr [param] - The number of repetitions in various algorithms" << std::endl
                << "             (used by commands -tr, -ot, and -oc)." << std::endl
                << "    -ss [param] - The size of the optimization space" << std::endl
                << "             (used by commands -ot and -oc)." << std::endl
                << "    -tl [param] - The time limit for global time in simulations" << std::endl
                << "             (used by commands -cc, -cm, -tr, and -sr)." << std::endl
                << "    -v - Enables verbose output"
#ifdef DREAM_VERBOSE2
                << std::endl << "       -ve - Enables extremely verbose output"
#endif
                << std::endl << std::endl;
}

int main (int argc, char* argv[])
{
        try
        {
                if (argc < 3)
                {
                        usage ();
                        exit (1);
                }

                enum {model_checking, random_testing, simulation,
                        thread_priority_optimization, cpu_priority_optimization,
                        if_interpreter, uppaal_interpreter} command;

                static const char* const param = argv[1];

                // Commands
                if (!strncmp (argv[1], "-cc", 3))
                        command = model_checking;
                else if (!strncmp (argv[1], "-if", 3))
                        command = if_interpreter;
                else if (!strncmp (argv[1], "-ot", 3))
                        command = thread_priority_optimization;
                else if (!strncmp (argv[1], "-oc", 3))
                        command = cpu_priority_optimization;
                else if (!strncmp (argv[1], "-sr", 3))
                        command = simulation;
                else if (!strncmp (argv[1], "-tr", 3))
                        command = random_testing;
                else if (!strncmp (argv[1], "-up", 3))
                        command = uppaal_interpreter;
                else
                {
                        usage ();
                        exit (1);
                }

                // Options
                DREAM::uint i;
                
                for (i = 2; i <= argc; i++)
                {
                        if (!strncmp (argv[i], "-nr", 3))
                        {
                                // Convert number
                                Option::number_of_repetitions_ = DREAM::chartouint (argv[++i]);
                        }
                        else if (!strncmp (argv[i], "-ss", 3))
                        {
                                // Convert number
                                Option::optimization_space_ = DREAM::chartouint (argv[++i]);
                        }
                        else if (!strncmp (argv[i], "-tl", 3))
                        {
                                // Convert number
                                Option::simulation_time_ = DREAM::chartouint (argv[++i]);
                        }
                        else if (!strncmp (argv[i], "-db", 3))
                        {
                                std::cout << "Branching is disabled during model checking..." << std::endl;
                                Option::branching_ = false;
                        }
                        else if (!strncmp (argv[i], "-dr", 3))
                        {
                                std::cout << "Race conditions are disabled during model checking..." << std::endl;
                                Option::race_condition_ = false;
                        }
                        else if (!strncmp (argv[i], "-dc", 3))
                        {
                                std::cout << "Race condition combinations are disabled during model checking..." << std::endl;
                                Option::race_condition_combination_ = false;
                        }
                        else if (!strncmp (argv[i], "-dx", 3))
                        {
                                std::cout << "Disabling error condition on non-executing tasks during model checking..." << std::endl;
                                Option::non_executing_tasks_ = true;
                        }
                        else if (!strncmp (argv[i], "-ez", 3))
                        {
                                std::cout << "Race conditions between zero-time events are enabled during model checking..." << std::endl;
                                Option::race_condition_zero_ = true;
                        }
                        else if (!strncmp (argv[i], "-v", 3))
                        {
                                std::cout << "Verbose output enabled..." << std::endl;
                                Option::verbose1_ = true;
                        }
#ifdef DREAM_VERBOSE2
                        else if (!strncmp (argv[i], "-ve", 3))
                        {
                                std::cout << "Extremely verbose output enabled..." << std::endl;
                                Option::verbose2_ = true;
                        }
#endif
                        else break;
                }

                while (!strncmp (argv[i], "-", 1))
                        ++i;

                static char* xmlFile = argv[i];
                static char* outputFile;

                if (argv[3])
                {
                        outputFile = argv[3];
                }

                int ret_value = 0;
                DREAM::System system;
                DREAM::XMLParser parser;
                
                // Generate random seed...
                srand ((unsigned)time (NULL));

                if (command == model_checking)
                {
                        if (Option::simulation_time_ == 0)
                        {
                                std::cerr << "Simulation time limit is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (ret_value == 1)
                                exit (1);

                        DREAM::ModelCheck modelcheck (&system);

                        parser.parse (xmlFile, &system);
                        if (!modelcheck.trace_based_model_check (&system, true))
                                ret_value = 2;
                }
                else if (command == random_testing)
                {
                        if (Option::simulation_time_ == 0)
                        {
                                std::cerr << "Simulation time limit is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (Option::number_of_repetitions_ == 0)
                        {
                                std::cerr << "Number of repetitions is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (ret_value == 1)
                                exit (1);

                        DREAM::ModelCheck modelcheck (&system);

                        parser.parse (xmlFile, &system);
                        if (!modelcheck.random_testing (&system, true))
                                ret_value = 2;
                }
                else if (command == simulation)
                {
                        if (Option::simulation_time_ == 0)
                        {
                                std::cerr << "Simulation time limit is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (ret_value == 1)
                                exit (1);

                        parser.parse (xmlFile, &system);
                        DREAM::Solution solution (&system);
                        Option::verbose1_ = true;
                        if (solution.fitness (true, false) != 0.0)
                                ret_value = 2;
                }
                else if (command == thread_priority_optimization)
                {
                        if (Option::simulation_time_ == 0)
                        {
                                std::cerr << "Simulation time limit is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (Option::number_of_repetitions_ == 0)
                        {
                                std::cerr << "Number of repetitions is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (Option::optimization_space_ == 0)
                        {
                                std::cerr << "Optimization space is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (ret_value == 1)
                                exit (1);

                        DREAM::GeneticOptimize geneticoptimize;
                        parser.parse (xmlFile, &system);
                        geneticoptimize.thread_level (&system);
                        DREAM::Solution solution (&system);
                        if (solution.fitness (Option::verbose1_, false) != 0.0)
                                ret_value = 2;
                }
                else if (command == cpu_priority_optimization)
                {
                        if (Option::simulation_time_ == 0)
                        {
                                std::cerr << "Simulation time limit is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (Option::number_of_repetitions_ == 0)
                        {
                                std::cerr << "Number of repetitions is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (Option::optimization_space_ == 0)
                        {
                                std::cerr << "Optimization space is not set." << std::endl;
                                ret_value = 1;
                        }
                        if (ret_value == 1)
                                exit (1);

                        DREAM::GeneticOptimize geneticoptimize;

                        parser.parse (xmlFile, &system);
                        geneticoptimize.CPU_level (&system);
                        DREAM::Solution solution (&system);
                        if (solution.fitness (Option::verbose1_, false) != 0.0)
                                ret_value = 2;
                }
                else if (command == if_interpreter)
                {
                        if (outputFile == NULL)
                        {
                                usage ();
                                throw DREAM::Exception ("No output file was specified for the IF toolset input generation.");
                        }
                        parser.parse (xmlFile, &system);
                        DREAM::IFInterpreter if_interpreter (&system);
                        if_interpreter.visitor_if (outputFile);
                }
                else if (command == uppaal_interpreter)
                {
                        if (outputFile == NULL)
                        {
                                usage ();
                                throw DREAM::Exception ("No output file was specified for the Uppaal input generation.");
                        }
                        parser.parse (xmlFile, &system);
                        DREAM::UppaalInterpreter uppaal_interpreter (&system);
                        uppaal_interpreter.visitor_uppaaltemplate (outputFile);
                        uppaal_interpreter.visitor_uppaal (outputFile);
                }
                else
                {
                        std::cerr << "This functionality is not implemented yet." << std::endl;
                        ret_value = 1;
                }

                return ret_value;
        }
        catch (DREAM::Exception* &ex)
        {
                ex->handler ();
                std::cerr << "Exiting..." << std::endl;
                exit (1);
        }
        catch (DREAM::Exception ex)
        {
                ex.handler ();
                std::cerr << "Exiting..." << std::endl;
                exit (1);
        }
        catch (std::bad_alloc& out_of_memory)
        {
                std::cerr << "\nException! Out of memory: " << out_of_memory.what () << std::endl;
                std::cerr << "Exiting..." << std::endl;
                exit (1);
        }
        catch (...)
        {
                std::cerr << "\nUndefined exception!" << std::endl;
                std::cerr << "Exiting..." << std::endl;
                exit (1);
        }
}

---