← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriParse/PNMLParser.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/PetriParse/PNMLParser.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
 *                     Peter Gjøl Jensen <root@petergjoel.dk>
 
6
 * 
 
7
 * This program is free software: you can redistribute it and/or modify
 
8
 * it under the terms of the GNU General Public License as published by
 
9
 * the Free Software Foundation, either version 3 of the License, or
 
10
 * (at your option) any later version.
 
11
 * 
 
12
 * This program is distributed in the hope that it will be useful,
 
13
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
15
 * GNU General Public License for more details.
 
16
 * 
 
17
 * You should have received a copy of the GNU General Public License
 
18
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
19
 */
 
20
#ifndef PNMLPARSER_H
 
21
#define PNMLPARSER_H
 
22
 
 
23
#include <map>
 
24
#include <string>
 
25
#include <vector>
 
26
#include <fstream>
 
27
#include <rapidxml.hpp>
 
28
 
 
29
#include "../PetriEngine/AbstractPetriNetBuilder.h"
 
30
#include "../PetriEngine/PQL/PQL.h"
 
31
#include "../PetriEngine/Colored/ColoredNetStructures.h"
 
32
#include "../PetriEngine/Colored/Expressions.h"
 
33
#include "../PetriEngine/Colored/Colors.h"
 
34
 
 
35
class PNMLParser {
 
36
 
 
37
    struct Arc {
 
38
        std::string source,
 
39
        target;
 
40
        int weight;
 
41
        PetriEngine::Colored::ArcExpression_ptr expr;
 
42
    };
 
43
    typedef std::vector<Arc> ArcList;
 
44
    typedef ArcList::iterator ArcIter;
 
45
 
 
46
    struct Transition {
 
47
        std::string id;
 
48
        double x, y;
 
49
        PetriEngine::Colored::GuardExpression_ptr expr;
 
50
    };
 
51
    typedef std::vector<Transition> TransitionList;
 
52
    typedef TransitionList::iterator TransitionIter;
 
53
 
 
54
    struct NodeName {
 
55
        std::string id;
 
56
        bool isPlace;
 
57
    };
 
58
    typedef std::unordered_map<std::string, NodeName> NodeNameMap;
 
59
    
 
60
    typedef std::unordered_map<std::string, PetriEngine::Colored::ColorType*> ColorTypeMap;
 
61
    typedef std::unordered_map<std::string, PetriEngine::Colored::Variable*> VariableMap;
 
62
 
 
63
public:
 
64
 
 
65
    struct Query {
 
66
        std::string name, text;
 
67
    };
 
68
    
 
69
    PNMLParser() {
 
70
        builder = NULL;
 
71
    }
 
72
    void parse(std::ifstream& xml,
 
73
            PetriEngine::AbstractPetriNetBuilder* builder);
 
74
 
 
75
    std::vector<Query> getQueries() {
 
76
        return queries;
 
77
    }
 
78
 
 
79
private:
 
80
    void parseElement(rapidxml::xml_node<>* element);
 
81
    void parsePlace(rapidxml::xml_node<>* element);
 
82
    void parseArc(rapidxml::xml_node<>* element, bool inhibitor = false);
 
83
    void parseTransition(rapidxml::xml_node<>* element);
 
84
    void parseDeclarations(rapidxml::xml_node<>* element);
 
85
    void parseNamedSort(rapidxml::xml_node<>* element);
 
86
    PetriEngine::Colored::ArcExpression_ptr parseArcExpression(rapidxml::xml_node<>* element);
 
87
    PetriEngine::Colored::GuardExpression_ptr parseGuardExpression(rapidxml::xml_node<>* element);
 
88
    PetriEngine::Colored::ColorExpression_ptr parseColorExpression(rapidxml::xml_node<>* element);
 
89
    PetriEngine::Colored::AllExpression_ptr parseAllExpression(rapidxml::xml_node<>* element);
 
90
    PetriEngine::Colored::ColorType* parseUserSort(rapidxml::xml_node<>* element);
 
91
    PetriEngine::Colored::NumberOfExpression_ptr parseNumberOfExpression(rapidxml::xml_node<>* element);
 
92
    void parseTransportArc(rapidxml::xml_node<>* element);
 
93
    void parseValue(rapidxml::xml_node<>* element, std::string& text);
 
94
    uint32_t parseNumberConstant(rapidxml::xml_node<>* element);
 
95
    void parsePosition(rapidxml::xml_node<>* element, double& x, double& y);
 
96
    void parseQueries(rapidxml::xml_node<>* element);
 
97
    const PetriEngine::Colored::Color* findColor(const char* name) const;
 
98
    PetriEngine::AbstractPetriNetBuilder* builder;
 
99
    NodeNameMap id2name;
 
100
    ArcList arcs;
 
101
    ArcList inhibarcs;
 
102
    TransitionList transitions;
 
103
    ColorTypeMap colorTypes;
 
104
    VariableMap variables;
 
105
    bool isColored;
 
106
    std::vector<Query> queries;
 
107
};
 
108
 
 
109
#endif // PNMLPARSER_H