UppaalInterpreter.cpp

Go to the documentation of this file.

/** @file UppaalInterpreter.cpp
* @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.
* =================================================================
*/

#include "UppaalInterpreter.h"

namespace DREAM
{

UppaalInterpreter::UppaalInterpreter (DREAM::System* system_ptr)
: system_ptr_ (system_ptr)
{
}

UppaalInterpreter::~UppaalInterpreter ()
{
}

std::string UppaalInterpreter::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
{
        uint k = 0;
        NODE_MAP::const_iterator node_iter;
        std::string output = "en[";

        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if ((node_iter->first) == node->id ())
                {
                                output << k << "]";
                }
                ++k;
        }

        k = 0;
        for (node_iter = node_map->begin (); node_iter != node_map->end (); node_iter++)
        {
                if (node_iter->second->scheduler ()->id () == scheduler_id)
                {
                        if (node_iter->second->priority () <= node->priority ())
                                if ((node_iter->second->priority () < node->priority ()) ||
                                                 (node_iter->second->subpriority () < node->subpriority ()))
                                {       
                                        output << " &amp;&amp; !en[" << k << "]";
                                }
                }
                ++k;
        }

        return output;
}

bool UppaalInterpreter::highestpriority (DREAM::Node* node_ptr)
{
        return node_ptr->scheduler ()->highestpriority (node_ptr);
}

bool UppaalInterpreter::lowestpriority (DREAM::Node* node_ptr)
{
        return node_ptr->scheduler ()->lowestpriority (node_ptr);
}

void UppaalInterpreter::visitor_uppaal (char* outputFile)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        std::ofstream f_stream (outputFile, std::ios::app);

        f_stream << "<instantiation>\n";

        DREAM::NODE_MAP task_map;
        DREAM::NODE_MAP channel_map;
        DREAM::NODE_MAP timer_map;

        system_ptr_->visitor_map (&task_map, &channel_map, &timer_map);

        system_ptr_->visitor_uppaal (&task_map, &channel_map, &timer_map, f_stream);

        f_stream << "</instantiation>\n\n";

        f_stream << "<system>system \n";
        
        uint needcolon = false;

        NODE_MAP::const_iterator node_iter;
        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
        {
                if (needcolon)
                        f_stream << ",\n" << node_iter->first;
                else
                {
                        f_stream << node_iter->first;
                        needcolon = true;
                }
        }

        for (node_iter = channel_map.begin (); node_iter != channel_map.end (); node_iter++)
        {
                if (needcolon)
                        f_stream << ",\n" << node_iter->first;
                else
                {
                        f_stream << node_iter->first;
                        needcolon = true;
                }
        }

        for (node_iter = timer_map.begin (); node_iter != timer_map.end (); node_iter++)
        {
                if (needcolon)
                        f_stream << ",\n" << node_iter->first;
                else
                {
                        f_stream << node_iter->first;
                        needcolon = true;
                }
        }

        SCHEDULER_MAP::const_iterator scheduler_iter;
        const SCHEDULER_MAP* scheduler_map = system_ptr_->scheduler_map ();

        for (scheduler_iter = scheduler_map->begin (); scheduler_iter != scheduler_map->end (); scheduler_iter++)
        {
                if (scheduler_iter->second->CPUs () > 0)
                {
                        if (needcolon)
                                f_stream << ",\n" << scheduler_iter->first;
                        else
                        {
                                f_stream << scheduler_iter->first;
                                needcolon = true;
                        }
                }
        }

        f_stream << ";</system>\n</nta>\n";

        f_stream.close ();
}

void UppaalInterpreter::visitor_uppaaltemplate (char* outputFile)
#ifdef DREAM_ENHANCED_EXCEPTION_CHECKING
        throw (DREAM::Exception)
#endif
{
        // This is a somewhat ugly implementation. Anyone feel like rewriting it?
        // Gabe

        std::cout << "\nGenerating UPPAAL input \"" << outputFile << "\"...\n\n";

        uint i, j, k, l;

        DREAM::NODE_MAP task_map;
        DREAM::NODE_MAP channel_map;
        DREAM::NODE_MAP timer_map;

        std::ofstream f_stream (outputFile, std::ios::trunc);

        system_ptr_->visitor_map (&task_map, &channel_map, &timer_map);

        f_stream << "<?xml version=\"1.0\"?>\n\n"
                << "<!--\n"
                << "=================================================================\n"
                << "DREAM License v2.0\n"
                << "\n"
                << "DREAM - Distributed Real-time Embedded Analysis Method\n"
                << "http://dre.sourceforge.net.\n"
                << "Copyright (c) 2005-2007 Gabor Madl, All Rights Reserved.\n"
                << "\n"
                << "This file is part of DREAM.\n"
                << "\n"
                << "DREAM is free software; you can redistribute it and/or modify it\n"
                << "under the terms of the GNU General Public License version 2 as\n"
                << "published by the Free Software Foundation. No future versions of\n"
                << "the GPL license may be automatically applied to DREAM. It is in\n"
                << "the sole discretion of the copyright holder to determine whether\n"
                << "DREAM may be released under a different license or terms. There\n"
                << "are no restrictions on the use of DREAM for any purpose.\n"
                << "\n"
                << "DREAM is distributed in the hope that it will be useful,\n"
                << "but WITHOUT ANY WARRANTY; without even the implied warranty of\n"
                << "MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the\n"
                << "GNU General Public License for more details.\n"
                << "\n"
                << "You should have received a copy of the GNU General Public License\n"
                << "along with this program; if not, write to the Free Software\n"
                << "Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, \n"
                << "MA 02110-1301, USA.\n"
                << "\n"
                << "By submitting comments, suggestions, code, code snippets,\n"
                << "techniques (including that of usage), and algorithms, submitters\n"
                << "acknowledge that they have the right to do so, that any such\n"
                << "submissions are given freely and unreservedly, and that they\n"
                << "waive any claims to copyright or ownership. In addition,\n"
                << "submitters acknowledge that any such submission might become\n"
                << "part of the copyright maintained on the overall body of code,\n"
                << "which comprises DREAM. By making a submission, submitter agrees\n"
                << "to these terms. Furthermore, submitters acknowledge that the\n"
                << "incorporation or modification of such submissions is entirely\n"
                << "at the discretion of the moderators of the DREAM project.\n"
                << "\n"
                << "DREAM links to the Libxml2 third party library. Please see\n"
                << "COPYING-libxml for the copyright information of Libxml2.\n"
                << "=================================================================\n-->" 
                << "\n" << std::endl

        << "<!DOCTYPE nta PUBLIC \"-//Uppaal Team//DTD Flat System 1.0//EN\" "
        << "\"http://www.docs.uu.se/docs/rtmv/uppaal/xml/flat-1_0.dtd\">\n"
        << "<nta>\n<declaration>\nint isidle[";

        uint numberoftasks = task_map.size ();

        f_stream << numberoftasks << "] := {";

        for (i = 1; i <= numberoftasks; i++)
        {
                if (i != numberoftasks)
                        f_stream << "1, ";
                else
                        f_stream << "1";
        }

        f_stream << "};\nint en[";

        f_stream << numberoftasks << "] := {";

        for (i = 1; i <= numberoftasks; i++)
        {
                if (i != numberoftasks)
                        f_stream << "0, ";
                else
                        f_stream << "0";
        }

        f_stream << "};\nint ";

        uint CPUs = system_ptr_->CPUs ();

        for (i = 1; i <= CPUs; i++)
        {
                if (i != CPUs)
                        f_stream << "w" << i << " := 0, ";
                else
                        f_stream << "w" << i << " := 0;\nclock globalclock;\n\n";
        }

        f_stream << "broadcast chan preempt, nullsink, nullsource";

        // Preempt from global to local
        SCHEDULER_MAP::const_iterator scheduler_iter;
        const SCHEDULER_MAP* scheduler_map = system_ptr_->scheduler_map ();

        i = 1;

        for (scheduler_iter = scheduler_map->begin (); scheduler_iter != scheduler_map->end (); scheduler_iter++)
        {
                if (scheduler_iter->second->CPUs () > 0)
                {
                        f_stream << ", preempt" << scheduler_iter->first;
                        ++i;
                }
        }

        NODE_MAP::const_iterator node_iter;

        for (node_iter = timer_map.begin (); node_iter != timer_map.end (); node_iter++)
        {
                f_stream << ", publish" << node_iter->first << "\n";
        }

        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
        {
                f_stream << ", start" << node_iter->first << ", publish" << node_iter->first << ", run" << node_iter->first << "\n";
        }

        for (node_iter = channel_map.begin (); node_iter != channel_map.end (); node_iter++)
        {
                f_stream << ", publish" << node_iter->first << "\n";
        }


        f_stream.flush ();

        // Generate Timer template

        f_stream << ";\n</declaration>\n<template>\n<name x=\"5\" y=\"5\">Timer</name>\n<parameter x=\"5\" y=\"20\">"
                << "const int&amp; period, const int&amp; bcperiod, broadcast chan&amp; publishi</parameter>\n<declaration>clock ce;</declaration>\n"
                << "<location id=\"id40\" x=\"448\" y=\"352\">\n<name x=\"432\" y=\"368\">timer</name>\n<label kind=\"invariant\""
                << " x=\"408\" y=\"384\">ce &lt;= period</label>\n</location>\n<init ref=\"id40\"/>\n<transition>\n<source "
                << "ref=\"id40\"/>\n<target ref=\"id40\"/>\n<label kind=\"guard\" x=\"408\" y=\"264\">ce &gt;= bcperiod</label>\n"
                << "<label kind=\"synchronisation\" x=\"424\" y=\"280\">publishi!</label>\n<label kind=\"assignment\" x=\"432\" "
                << "y=\"296\">ce := 0</label>\n<nail x=\"416\" y=\"328\"/>\n<nail x=\"448\" y=\"320\"/>\n<nail x=\"480\" y=\"328\"/>\n"
                << "</transition>\n</template>\n";

        // Generate Task template

        f_stream << "<template>\n<name x=\"5\" y=\"5\">Task</name>\n<parameter x=\"5\" y=\"20\">const int&amp; pid, const int&amp; wcet, const int&amp; bcet, const int&amp; dl, const int&amp; pr, "
                << "broadcast chan&amp; release, broadcast chan&amp; start, broadcast chan&amp; finish, broadcast chan&amp; preempt</parameter>\n<declaration>clock ce;\nclock cd;\nint et;\nint pre;\n"
                << "</declaration>\n\n<location id=\"id0\" x=\"-128\" y=\"-256\">\n<name x=\"-136\" y=\"-240\">idle</name>\n</location>"
                << "\n\n<location id=\"id1\" x=\"-32\" y=\"-352\">\n<name x=\"-40\" y=\"-344\">run</name>\n<label kind=\"invariant\" "
                << "x=\"-56\" y=\"-328\">ce &lt;= pr</label>\n</location>\n\n<location id=\"id2\" x=\"64\" y=\"-448\">\n<name x=\"48\" "
                << "y=\"-480\">error</name>\n<committed/>\n</location>\n\n<location id=\"id3\" x=\"64\" y=\"-256\">\n<name x=\"48\" "
                << "y=\"-240\">wait</name>\n</location><location id=\"id18\" x=\"-80\" y=\"-304\">\n<name x=\"-128\" y=\"-320\">send</name>"
                << "\n<committed/>\n</location>\n\n<location id=\"id4\" x=\"-128\" y=\"-448\">\n<name x=\"-138\" y=\"-478\">pass</name>\n"
                << "<committed/>\n</location>\n<init ref=\"id0\"/>\n\n<transition>\n<source ref=\"id1\"/>\n<target ref=\"id3\"/>\n"
                << "<label kind=\"synchronisation\" x=\"-8\" y=\"-352\">preempt?</label>\n<label kind=\"assignment\" x=\"8\" y=\"-336\">pre "
                << "+= pr</label>\n<nail x=\"24\" y=\"-312\"/>\n</transition>\n\n<transition>\n<source ref=\"id3\"/>\n<target ref=\"id1\"/>"
                << "\n<label kind=\"assignment\" x=\"-40\" y=\"-296\">ce := 0</label>\n<label kind=\"synchronisation\" x=\"-40\" "
                << "y=\"-312\">start?</label>\n<nail x=\"16\" y=\"-296\"/>\n</transition>\n\n<transition>\n<source ref=\"id0\"/>\n"
                << "<target ref=\"id3\"/>\n<label kind=\"synchronisation\" x=\"-64\" y=\"-272\">release?</label>\n<label kind=\"assignment\" "
                << "x=\"-88\" y=\"-256\">cd := 0, en[pid] := 1,\net := 0, pre := 0</label>\n</transition>\n\n<transition>\n"
                << "<source ref=\"id3\"/>\n<target ref=\"id2\"/>\n<label kind=\"guard\" x=\"0\" y=\"-392\">cd &gt;= dl - pre</label>\n"
                << "<nail x=\"56\" y=\"-352\"/>\n</transition>\n\n<transition>\n<source ref=\"id3\"/>\n<target ref=\"id2\"/>\n"
                << "<label kind=\"synchronisation\" x=\"-8\" y=\"-376\">release?</label>\n<nail x=\"72\" y=\"-352\"/>\n</transition>\n\n"
                << "<transition>\n<source ref=\"id1\"/>\n<target ref=\"id2\"/>\n<label kind=\"synchronisation\" x=\"-40\" "
                << "y=\"-432\">release?</label>\n<nail x=\"8\" y=\"-408\"/>\n</transition>\n\n<transition>\n<source ref=\"id1\"/>\n"
                << "<target ref=\"id2\"/>\n<label kind=\"guard\" x=\"-40\" y=\"-416\">cd &gt;= dl - pre</label>\n<nail x=\"16\" y=\"-392\"/>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id18\"/>\n<target ref=\"id0\"/>\n<label kind=\"synchronisation\" "
                << "x=\"-160\" y=\"-288\">finish!</label>\n<label kind=\"assignment\" x=\"-160\" y=\"-304\">en[pid] := 0</label>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id1\"/>\n<target ref=\"id4\"/>\n<label kind=\"guard\" x=\"-160\" "
                << "y=\"-416\">ce &gt;= pr&amp;&amp;\net + ce &lt; wcet&amp;&amp;\ncd &lt; dl - pre</label>\n<nail x=\"-80\" y=\"-392\"/>\n</transition>\n\n"
                << "<transition>\n<source ref=\"id4\"/>\n<target ref=\"id1\"/>\n<label kind=\"assignment\" x=\"-88\" y=\"-456\">et += pr,\n"
                << "ce := 0</label>\n<nail x=\"-72\" y=\"-408\"/>\n</transition>\n\n<transition>\n<source ref=\"id1\"/>\n<target ref=\"id18\"/>\n"
                << "<label kind=\"guard\" x=\"-160\" y=\"-360\">et + ce &gt;= bcet - pre</label>\n<label kind=\"synchronisation\" x=\"-128\" "
                << "y=\"-344\">start!</label>\n</transition>\n</template>\n\n";

        // Generate non-preemptive Task template

        f_stream << "<template>\n<name x=\"5\" y=\"5\">NonpTask</name>\n<parameter x=\"5\" y=\"20\">const int&amp; pid, const int&amp; wcet, const int&amp; bcet, const int&amp; dl, broadcast "
                << "chan&amp; release, broadcast chan&amp; start, broadcast chan&amp; finish</parameter>\n<declaration>clock ce;\nclock cd;\n</declaration>\n\n<location id=\"id13\" "
                << "x=\"-128\" y=\"-256\">\n<name x=\"-136\" y=\"-240\">idle</name>\n</location>\n\n<location id=\"id14\" x=\"-128\" "
                << "y=\"-448\">\n<name x=\"-136\" y=\"-480\">run</name>\n<label kind=\"invariant\" x=\"-144\" y=\"-432\">ce &lt;= wcet</label>\n"
                << "</location>\n\n<location id=\"id15\" x=\"64\" y=\"-448\">\n<name x=\"48\" y=\"-480\">error</name>\n<committed/>\n"
                << "</location>\n\n<location id=\"id16\" x=\"64\" y=\"-256\">\n<name x=\"48\" y=\"-240\">wait</name>\n</location>\n\n"
                << "<location id=\"id17\" x=\"-128\" y=\"-352\">\n<name x=\"-168\" y=\"-376\">send</name>\n<committed/>\n</location>\n"
                << "<init ref=\"id13\"/>\n\n<transition>\n<source ref=\"id13\"/>\n<target ref=\"id16\"/>\n<label kind=\"synchronisation\" "
                << "x=\"-64\" y=\"-256\">release?</label>\n<label kind=\"assignment\" x=\"-88\" y=\"-240\">cd := 0, en[pid] := 1</label>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id16\"/>\n<target ref=\"id15\"/>\n<label kind=\"guard\" x=\"0\" "
                << "y=\"-392\">cd &gt;= dl</label>\n<nail x=\"56\" y=\"-352\"/>\n</transition>\n\n<transition>\n<source ref=\"id16\"/>\n"
                << "<target ref=\"id15\"/>\n<label kind=\"synchronisation\" x=\"-8\" y=\"-376\">release?</label>\n<nail x=\"72\" y=\"-352\"/>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id14\"/>\n<target ref=\"id15\"/>\n<label kind=\"synchronisation\" x=\"-64\" "
                << "y=\"-480\">release?</label>\n<nail x=\"-32\" y=\"-456\"/>\n</transition>\n\n<transition>\n<source ref=\"id14\"/>\n"
                << "<target ref=\"id15\"/>\n<label kind=\"guard\" x=\"-56\" y=\"-440\">cd &gt;= dl</label>\n<nail x=\"-32\" y=\"-440\"/>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id16\"/>\n<target ref=\"id14\"/>\n<label kind=\"synchronisation\" x=\"-64\" "
                << "y=\"-352\">start?</label>\n<label kind=\"assignment\" x=\"-64\" y=\"-336\">ce := 0</label>\n</transition>\n\n"
                << "<transition>\n<source ref=\"id14\"/>\n<target ref=\"id17\"/>\n<label kind=\"guard\" x=\"-112\" y=\"-392\">ce &gt;= bcet&amp;&amp;\n"
                << "cd &lt; dl</label>\n<label kind=\"synchronisation\" x=\"-112\" y=\"-408\">start!</label>\n</transition>\n\n"
                << "<transition>\n<source ref=\"id17\"/>\n<target ref=\"id13\"/>\n<label kind=\"synchronisation\" x=\"-120\" "
                << "y=\"-320\">finish!</label>\n<label kind=\"assignment\" x=\"-120\" y=\"-304\">en[pid] := 0</label>\n</transition>\n"
                << "</template>\n\n";

        // Generate Channel template

        f_stream << "<template>\n<name x=\"5\" y=\"5\">Channel</name>\n<parameter x=\"5\" y=\"20\">const int&amp; delay, const int&amp; bcdelay, const int&amp; lambdac, "
                << "const int&amp; pid, broadcast chan&amp; release, broadcast chan&amp; publish, broadcast chan&amp; finish</parameter>\n<declaration>clock ce;\nint bufferc := 0;</declaration>\n\n"
                << "<location id=\"id6\" x=\"320\" y=\"448\">\n<name x=\"304\" y=\"464\">idle</name>\n</location>\n\n"
                << "<location id=\"id8\" x=\"512\" y=\"448\">\n<name x=\"504\" y=\"464\">wait</name>\n<label kind=\"invariant\" x=\"536\" "
                << "y=\"464\">ce &lt;= delay</label>\n</location>\n<init ref=\"id6\"/>\n\n<transition>\n<source ref=\"id8\"/>\n"
                << "<target ref=\"id8\"/>\n<label kind=\"synchronisation\" x=\"504\" y=\"400\">release?</label>\n<label "
                << "kind=\"assignment\" x=\"504\" y=\"416\">bufferc++</label>\n<nail x=\"552\" y=\"432\"/>\n<nail x=\"552\" y=\"464\"/>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id8\"/>\n<target ref=\"id6\"/>\n<label kind=\"guard\" x=\"344\" "
                << "y=\"456\">!en[pid] &amp;&amp; ce &gt;= bcdelay</label>\n<label kind=\"synchronisation\" x=\"408\" y=\"472\">publish!</label>\n"
                << "<label kind=\"assignment\" x=\"352\" y=\"472\">bufferc--</label>\n<nail x=\"416\" y=\"456\"/>\n</transition>\n\n"
                << "<transition>\n<source ref=\"id8\"/>\n<target ref=\"id6\"/>\n<label kind=\"guard\" x=\"376\" y=\"408\">en[pid]&amp;&amp;\n"
                << "ce &gt;= bcdelay</label>\n<nail x=\"416\" y=\"440\"/>\n</transition>\n\n<transition>\n<source ref=\"id6\"/>\n"
                << "<target ref=\"id8\"/>\n<label kind=\"synchronisation\" x=\"352\" y=\"368\">release?</label>\n<label "
                << "kind=\"assignment\" x=\"352\" y=\"384\">bufferc++, ce := 0</label>\n<nail x=\"352\" y=\"400\"/>\n<nail x=\"480\" "
                << "y=\"400\"/>\n</transition>\n\n<transition>\n<source ref=\"id6\"/>\n<target ref=\"id6\"/>\n<label kind=\"guard\" "
                << "x=\"256\" y=\"416\">bufferc == 0</label>\n<label kind=\"synchronisation\" x=\"256\" y=\"400\">finish?</label>\n"
                << "<nail x=\"280\" y=\"432\"/>\n<nail x=\"280\" y=\"464\"/>\n</transition>\n\n<transition>\n<source ref=\"id6\"/>\n"
                << "<target ref=\"id8\"/>\n<label kind=\"guard\" x=\"352\" y=\"512\">bufferc &gt; 0</label>\n<label "
                << "kind=\"synchronisation\" x=\"352\" y=\"496\">finish?</label>\n<label kind=\"assignment\" x=\"432\" y=\"512\">"
                << "ce := 0</label>\n<nail x=\"352\" y=\"496\"/><nail x=\"480\" y=\"496\"/>\n</transition>\n</template>\n\n";
 
        // Generate Buffer template (local channel with 0 delay)

        f_stream << "<template>\n<name x=\"5\" y=\"5\">Buffer</name>\n<parameter x=\"5\" y=\"20\">const int&amp; lambdac, const int&amp; pid, broadcast "
                << "chan&amp; release, broadcast chan&amp; publish, broadcast chan&amp; finish</parameter>\n<declaration>int bufferc := 0;</declaration>\n\n<location id=\"id5\" "
                << "x=\"320\" y=\"448\">\n<name x=\"320\" y=\"464\">idle</name>\n</location>\n\n<location id=\"id7\" x=\"512\" y=\"448\">\n"
                << "<name x=\"496\" y=\"464\">wait</name>\n\n<committed/></location>\n<init ref=\"id5\"/>\n\n<transition>\n"
                << "<source ref=\"id5\"/>\n<target ref=\"id7\"/>\n<label kind=\"synchronisation\" x=\"408\" y=\"360\">release?</label>\n"
                << "<label kind=\"assignment\" x=\"360\" y=\"376\">bufferc++</label>\n<label kind=\"guard\" x=\"360\" y=\"360\">!en[pid]"
                << "</label>\n<nail x=\"352\" y=\"400\"/><nail x=\"480\" y=\"400\"/>\n</transition>\n\n<transition>\n<source ref=\"id5\"/>\n"
                << "<target ref=\"id5\"/>\n<label kind=\"guard\" x=\"280\" y=\"384\">bufferc == 0</label>\n<label kind=\"synchronisation\" "
                << "x=\"280\" y=\"368\">finish?</label>\n<nail x=\"304\" y=\"408\"/><nail x=\"280\" y=\"432\"/>\n</transition>\n\n"
                << "<transition>\n<source ref=\"id5\"/>\n<target ref=\"id7\"/>\n<label kind=\"guard\" x=\"360\" y=\"480\">bufferc &gt; "
                << "0</label>\n<label kind=\"synchronisation\" x=\"360\" y=\"464\">finish?</label>\n<nail x=\"352\" y=\"496\"/>\n"
                << "<nail x=\"480\" y=\"496\"/>\n</transition>\n\n<transition>\n<source ref=\"id7\"/>\n<target ref=\"id5\"/>\n"
                << "<label kind=\"synchronisation\" x=\"408\" y=\"408\">publish!</label>\n<label kind=\"assignment\" x=\"360\" "
                << "y=\"424\">bufferc--</label>\n<label kind=\"guard\" x=\"360\" y=\"408\">!en[pid]</label><nail x=\"416\" "
                << "y=\"440\"/></transition>\n\n<transition>\n<source ref=\"id5\"/><target ref=\"id5\"/>\n<label kind=\"guard\" "
                << "x=\"280\" y=\"496\">en[pid]</label>\n<label kind=\"synchronisation\" x=\"328\" y=\"496\">release?</label>\n"
                << "<label kind=\"assignment\" x=\"280\" y=\"512\">bufferc++</label>\n<nail x=\"280\" y=\"464\"/>\n<nail x=\"304\" y=\"488\"/>\n"
                << "</transition>\n\n<transition>\n<source ref=\"id7\"/>\n<target ref=\"id5\"/>\n<label kind=\"guard\" x=\"392\" "
                << "y=\"448\">en[pid]</label>\n<nail x=\"416\" y=\"456\"/>\n</transition>\n</template>\n\n";

        // Generate the schedulers
        i = 1;

        for (scheduler_iter = scheduler_map->begin (); scheduler_iter != scheduler_map->end (); scheduler_iter++)
        {
                if (scheduler_iter->second->CPUs () > 0)
                {
                        j = 1;
                        // Generate idle and select states
                        f_stream << "<template>\n<name x=\"5\" y=\"5\">" << scheduler_iter->first
                                << "</name>\n<parameter x=\"5\" y=\"20\"/>\n<declaration/>\n<location id=\"id" << i*50 + 100 << "\" x=\"128\" y=\"256\">\n"
                                << "<name x=\"120\" y=\"272\">idle</name>\n</location>\n<location id=\"id" << i*50 + 100 + 1 << "\" x=\"320\" y=\"256\">\n"
                                << "<name x=\"288\" y=\"272\">select</name>\n<urgent/>\n</location>\n";

                        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
                        {
                                if (node_iter->second->scheduler ()->id () == scheduler_iter->first)
                                {
                                        // Generate states
                                        if (!lowestpriority (node_iter->second))
                                        {
                                                f_stream << "<location id=\"id" << i*50 + 100 + j*2 << "\" x=\"512\" y=\"" << j*96 + 160 << "\">\n"
                                                << "<name x=\"460\" y=\"" << j*96 + 180 << "\">schedule" << node_iter->first << "</name>\n"
                                                << "</location>\n<location id=\"id" << i*50 + 100 + j*2 + 1 << "\" x=\"416\" y=\"" << j*96 + 160 << "\">\n"
                                                << "<committed/>\n</location>\n";
                                        }
                                        else
                                        {
                                        // We can apply some reductions here - corresponding transitions will change
                                                f_stream << "<location id=\"id" << i*50 + 100 + j*2 << "\" x=\"512\" y=\"" << j*96 + 160 << "\">\n"
                                                << "<name x=\"460\" y=\"" << j*96 + 180 << "\">schedule" << node_iter->first << "</name>\n"
                                                << "</location>\n";
                                        }

                                        ++j;
                                }
                        }

                        f_stream << "<init ref=\"id" << i*50 + 100 << "\"/>\n";

                        // Generate guard for no enabled task on processor
                        f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 1 << "\"/>\n<target ref=\"id" << i*50 + 100 << "\"/>\n"
                                << "<label kind=\"guard\" x=\"112\" y=\"288\">";

                        k = 0; l = 0;

                        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
                        {
                                if (node_iter->second->scheduler ()->id () == scheduler_iter->first)
                                {
                                        if (l != 0)
                                                f_stream << " &amp;&amp; ";
                                        else
                                                l = 1;
                                        f_stream << "!en[" << k << "]";
                                }
                                ++k;
                        }

                        f_stream << "</label>\n<nail x=\"224\" y=\"272\"/>\n</transition>\n";
                        // Generation complete

                        j = 1;

                        for (node_iter = task_map.begin (); node_iter != task_map.end (); node_iter++)
                        {
                                if (node_iter->second->scheduler ()->id () == scheduler_iter->first)
                                {
                                        // Generate transitions for states
                                        f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 << "\"/>\n<target ref=\"id" << i*50 + 100 + 1 << "\"/>\n"
                                                << "<label kind=\"synchronisation\" x=\"136\" y=\"" << j*96 + 124 << "\">";

                                        if (node_iter->second->get_source (&task_map, &channel_map, &timer_map) != NULL)
                                                // We found an ancestor other than a Channel
                                                f_stream << "publish" << node_iter->second->get_source (&task_map, &channel_map, &timer_map)->id ();
                                        else
                                                // The ancestor is a Channel
                                                f_stream << "start" << node_iter->first;

                                        f_stream << "?</label>\n<nail x=\"224\" y=\"" << j*96 + 160 << "\"/>\n</transition>\n";

                                        if (!lowestpriority (node_iter->second))
                                        {
                                                f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 1 << "\"/>\n<target ref=\"id" << i*50 + 100 + j*2 + 1 << "\"/>\n"
                                                << "<label kind=\"guard\" x=\"320\" y=\"" << j*96 + 112 << "\">"
                                                << create_fixedpriority_guard (&task_map, scheduler_iter->first, node_iter->second)
                                                << "</label>\n<label kind=\"synchronisation\" x=\"320\" y=\"" << j*96 + 128 << "\">preempt" 
                                                << scheduler_iter->first << "!</label>\n</transition>\n";

                                                f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 2*j+1 << "\"/>\n<target ref=\"id" << i*50 + 100 + j*2 << "\"/>\n"
                                                << "<label kind=\"synchronisation\" x=\"464\" y=\"" << j*96 + 112 << "\">run" << node_iter->first 
                                                << "!</label>\n</transition>\n";
                                        }
                                        else
                                        {
                                        // Corresponding transition reductions for state space reduction
                                                f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 1 << "\"/>\n<target ref=\"id" << i*50 + 100 + j*2 << "\"/>\n"
                                                << "<label kind=\"guard\" x=\"320\" y=\"" << j*96 + 112 << "\">"
                                                << create_fixedpriority_guard (&task_map, scheduler_iter->first, node_iter->second)
                                                << "</label>\n<label kind=\"synchronisation\" x=\"320\" y=\"" << j*96 + 128 << "\">run" << node_iter->first 
                                                << "!</label>\n<nail x=\"416\" y=\"" << j*96 + 160 << "\"/>\n</transition>\n";
                                        }

                                        f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 2*j << "\"/>\n<target ref=\"id" << i*50 + 100 + 1 << "\"/>\n"
                                                << "<label kind=\"synchronisation\" x=\"336\" y=\"" << j*96 + 168 << "\">run" << node_iter->first
                                                << "?</label>\n<nail x=\"404\" y=\"" << j*96 + 184 << "\"/>\n</transition>\n";

                                        // Transitions for Timer preemptions
                                        k = 1;
                                        NODE_MAP::const_iterator node_iter2;

                                        // We can reduce some transitions here
                                        if (!highestpriority (node_iter->second))
                                        {
                                                for (node_iter2 = timer_map.begin (); node_iter2 != timer_map.end (); node_iter2++)
                                                {
                                                        // Create transition
                                                        if ((node_iter2->second->priority () < node_iter->second->priority ()) &&       // Smaller value = higher priority
                                                                 (node_iter2->second->scheduler () == node_iter->second->scheduler ())) // They are on the same processor
                                                        f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 2*j << "\"/>\n<target ref=\"id" << i*50 + 100 + 1 << "\"/>\n"
                                                                << "<label kind=\"synchronisation\" x=\"336\" y=\"" << j*96 + 5*k + 164 << "\">publish" << node_iter2->first
                                                                << "?</label>\n<nail x=\"" << 404 - 5*k << "\" y=\"" << j*96 + 5*k + 184 << "\"/>\n</transition>\n";
                                                        ++k;
                                                }

                                                for (node_iter2 = task_map.begin (); node_iter2 != task_map.end (); node_iter2++)
                                                {
                                                        // Create transition for preemptions
                                                        if ((node_iter2->second->priority () < node_iter->second->priority ()) &&       // Smaller value = higher priority
                                                                 (node_iter2->second->scheduler () == node_iter->second->scheduler ())) // They are on the same processor
                                                        {
                                                                if (node_iter2->second->get_source (&task_map, &channel_map, &timer_map))
                                                                // We found a higher priority Task initiated by a (possibly remote) Channel
                                                                // This could cause preemptions...
                                                                {
                                                                        f_stream << "<transition>\n<source ref=\"id" << i*50 + 100 + 2*j << "\"/>\n<target ref=\"id" << i*50 + 100 + 1 << "\"/>\n"
                                                                        << "<label kind=\"synchronisation\" x=\"336\" y=\"" << j*96 + 5*k + 164 << "\">start" << node_iter2->first
                                                                        << "?</label>\n<nail x=\"" << 404 - 5*k << "\" y=\"" << j*96 + 5*k + 184 << "\"/>\n</transition>\n";
                                                
                                                                        ++k;
                                                                }
                                                        }
                                                }
                                        }

                                        ++j;
                                }
                        }

                        f_stream << "</template>\n\n";
                        ++i;
                }
        }
        f_stream.close ();
}

};

---