#include "../algorithm/ModelCheck.h"
#include "IFInterpreter.h"
#include "UppaalInterpreter.h"
#include "../core/Common.h"
#include "XMLParser.h"
Go to the source code of this file.
Functions | |
| static void | usage () |
| int | main (int argc, char *argv[]) |
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.
Definition in file Dream.cpp.
| int main | ( | int | argc, | |
| char * | argv[] | |||
| ) |
Definition at line 134 of file Dream.cpp.
References Option::branching_, DREAM::chartouint(), DREAM::GeneticOptimize::CPU_level(), DREAM::Solution::fitness(), DREAM::Exception::handler(), Option::non_executing_tasks_, Option::number_of_repetitions_, Option::optimization_space_, DREAM::XMLParser::parse(), Option::race_condition_, Option::race_condition_combination_, Option::race_condition_zero_, DREAM::ModelCheck::random_testing(), Option::simulation_time_, DREAM::GeneticOptimize::thread_level(), DREAM::ModelCheck::trace_based_model_check(), usage(), Option::verbose1_, DREAM::IFInterpreter::visitor_if(), DREAM::UppaalInterpreter::visitor_uppaal(), and DREAM::UppaalInterpreter::visitor_uppaaltemplate().
1.5.1