← Back to branch summary

~tapaal-dist-ctl/verifypn/warning_fix

« back to all changes in this revision

Viewing changes to PetriEngine/DTAPN/DTAPNTranslator.h

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/DTAPN/DTAPNTranslator.h
 
1
/* PeTe - Petri Engine exTremE
 
2
 * Copyright (C) 2011  Jonas Finnemann Jensen <jopsen@gmail.com>,
 
3
 *                     Thomas Søndersø Nielsen <primogens@gmail.com>,
 
4
 *                     Lars Kærlund Østergaard <larsko@gmail.com>,
 
5
 * 
 
6
 * This program is free software: you can redistribute it and/or modify
 
7
 * it under the terms of the GNU General Public License as published by
 
8
 * the Free Software Foundation, either version 3 of the License, or
 
9
 * (at your option) any later version.
 
10
 * 
 
11
 * This program is distributed in the hope that it will be useful,
 
12
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
 * GNU General Public License for more details.
 
15
 * 
 
16
 * You should have received a copy of the GNU General Public License
 
17
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
18
 */
 
19
#ifndef DTAPNTRANSLATOR_H
 
20
#define DTAPNTRANSLATOR_H
 
21
 
 
22
#include <string>
 
23
#include <list>
 
24
#include <vector>
 
25
 
 
26
#include "../AbstractPetriNetBuilder.h"
 
27
#include "AbstractDTAPNBuilder.h"
 
28
 
 
29
namespace PetriEngine{
 
30
namespace DTAPN {
 
31
 
 
32
/** Translator from DTAPN to PNDV */
 
33
class DTAPNTranslator : public AbstractDTAPNBuilder
 
34
{
 
35
        /** Encapsulates a place */
 
36
        struct Place{
 
37
                std::string name;
 
38
                int tokens;
 
39
                int maxAge;
 
40
                int maxInvariantAge;
 
41
        };
 
42
        typedef std::list<Place> PlaceList;
 
43
        typedef std::list<Place>::iterator PlaceIter;
 
44
        /** Encapsulates a transition */
 
45
        struct Transition{
 
46
                std::string name;
 
47
        };
 
48
        typedef std::list<Transition> TransitionList;
 
49
        typedef std::list<Transition>::iterator TransitionIter;
 
50
        /** An input arc */
 
51
        struct InArc{
 
52
                std::string start;
 
53
                std::string end;
 
54
                int startInterval;
 
55
                int endInterval;
 
56
        };
 
57
        typedef std::list<InArc> InArcList;
 
58
        typedef std::list<InArc>::iterator InArcIter;
 
59
        /** An output arc */
 
60
        struct OutArc{
 
61
                std::string start;
 
62
                std::string end;
 
63
        };
 
64
        typedef std::list<OutArc> OutArcList;
 
65
        typedef std::list<OutArc>::iterator OutArcIter;
 
66
public:
 
67
        DTAPNTranslator(int bound){ this->bound = bound; }
 
68
        void addPlace(const std::string& name, int tokens, int maxInvariantAge, double x = 0, double y = 0);
 
69
        void addTransition(const std::string& name, double x = 0, double y = 0);
 
70
        void addInputArc(const std::string& place, const std::string& transition, int startInterval, int endInterval);
 
71
        void addOutputArc(const std::string& transition, const std::string& place);
 
72
        void makePNDV(AbstractPetriNetBuilder* builder);
 
73
        static std::string translateQuery(const std::string& query);
 
74
private:
 
75
        /** Maximum number of tokens at a place */
 
76
        int bound;
 
77
        /** List of DTAPN places */
 
78
        PlaceList places;
 
79
        /** List of DTAPN transitions */
 
80
        TransitionList transitions;
 
81
        /** List of DTAPN input arcs */
 
82
        InArcList inArcs;
 
83
        /** List of DTAPN output arcs */
 
84
        OutArcList outArcs;
 
85
        /** Returns a DTAPN place with the provided name */
 
86
        Place& findPlace(const std::string& name);
 
87
        /** Make sure it can't collide with stuff we have */
 
88
        std::string escapeIdentifier(std::string identifier);
 
89
        /** Gets a list of input arcs for a transition */
 
90
        InArcList preset(const std::string& transition);
 
91
        /** Gets a list of output arcs for a transition */
 
92
        OutArcList postset(const std::string& transition);
 
93
        /** True, if place is the target of any output arcs */
 
94
        bool isEndPlace(const std::string& place);
 
95
        /** Lock state, when in idle */
 
96
        int lockStateIdle;
 
97
        /** Lock state, when in ageing */
 
98
        int lockStateAgeing;
 
99
        /** Lock state for a transition */
 
100
        std::string lockState(const std::string& transition);
 
101
        /** Pre place to a transition */
 
102
        std::string prePlace(const std::string& transition, int inArcNr);
 
103
        /** Transition from place to pre-place */
 
104
        std::string prePlaceTransition(const std::string& transition, int inArcNr, int tokenIndex);
 
105
        /** Post-place from a transition, only one per place */
 
106
        std::string postPlace(const std::string& place);
 
107
        /** Transition from post-place to place */
 
108
        std::string postPlaceTransition(const std::string& place, int tokenIndex);
 
109
        /** Variable representing the age of a specific token at a place */
 
110
        std::string tokenAgeVariable(const std::string& place, int tokenIndex);
 
111
        /** Max transition between two intermediate ageing places */
 
112
        std::string maxTransition(const std::string& place, int tokenIndex);
 
113
        /** Age transition between two intermediate ageing places */
 
114
        std::string ageTransition(const std::string& place, int tokenIndex);
 
115
        /** An intermediate ageing place*/
 
116
        std::string intermediateAgeingPlace(const std::string& place, int tokenIndex);
 
117
        /** to ensure unique names */
 
118
        bool hasIdentifier(const std::string& id);
 
119
};
 
120
 
 
121
} // DTAPN
 
122
} // PetriEngine
 
123
 
 
124
#endif // DTAPNTRANSLATOR_H