UppaalInterpreter.h

Go to the documentation of this file.

/** @file UppaalInterpreter.h
* @author Gabor Madl
* @date Created 07/2005
* @brief This interpreter generates Uppaal XML input from the DREAM models.
*
*
* =================================================================
* 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.
* =================================================================
*/

#ifndef DREAM_UPPAALINTERPRETER
#define DREAM_UPPAALINTERPRETER

#include "../core/System.h"

namespace DREAM
{

/** The UppaalInterpreter class generates Uppaal XML input from the DREAM models. */
class UppaalInterpreter
{
public:
        /** Constructor. 
        * @param system_ptr is the pointer to the system to be output.
        */
        UppaalInterpreter (DREAM::System* system_ptr);

        /** Destructor. */
        ~UppaalInterpreter ();

        /** Generates the Uppaal XML system description. 
        * It uses the visitor pattern to get the data from the DREAM models. 
        * @param outputFile specifies the output file to be generated.
        */
        void visitor_uppaal (char* outputFile)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
                throw (DREAM::Exception)
#endif
        ;

        /** Generates the Uppaal XML templates. It uses the visitor pattern to get the data from the DREAM models.
        * @param outputFile specifies the output file to be generated.
        */
        void visitor_uppaaltemplate (char* outputFile)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
                throw (DREAM::Exception)
#endif
        ;

private:

        /** Creates guard condition to model fixed-priority scheduling based on priorities.
        * @param node_map contains the Nodes in the Scheduler.
        * @param scheduler_id specifies the Scheduler id.
        * @param node is used to calculate the priority level used in the guard.
        */
        std::string create_fixedpriority_guard (NODE_MAP* node_map, std::string scheduler_id, const DREAM::Node* const node)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
                throw (DREAM::Exception)
#endif
        ;

        /** Determines whether the Task is the highest priority Task in the Scheduler.
        * Used to reduce state space caused by preemptions.
        * @param task_ptr is a pointer to the Task to be checked.
        * @return true if the Task is the highest priority Task in the Scheduler, false otherwise.
        */
        bool highestpriority (DREAM::Node* task_ptr);

        /** Determines whether the Task is the lowest priority Task in the Scheduler.
        * Used to reduce state space caused by preemptions.
        * @param task_ptr is a pointer to the Task to be checked.
        * @return true if the Task is the lowest priority Task in the Scheduler, false otherwise.
        */
        bool lowestpriority (DREAM::Node* task_ptr);

        /** Pointer to store the DREAM system */
        DREAM::System* system_ptr_;

        /** String storing the name of the generated file. */
        std::string filename_;
};

};

#endif

---