← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/AbstractPetriNetBuilder.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:
PetriEngine/AbstractPetriNetBuilder.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 ABSTRACTPETRINETBUILDER_H
21
 
#define ABSTRACTPETRINETBUILDER_H
22
 
 
23
 
#include <string>
24
 
 
25
 
#include "PQL/PQL.h"
26
 
#include "Colored/Multiset.h"
27
 
#include "Colored/Expressions.h"
28
 
 
29
 
namespace PetriEngine {
30
 
 
31
 
    /** Abstract builder for petri nets */
32
 
    class AbstractPetriNetBuilder {
33
 
    protected:
34
 
        bool _isColored = false;
35
 
        
36
 
    public:
37
 
        /** Add a new place with a unique name */
38
 
        virtual void addPlace(const std::string& name,
39
 
                int tokens,
40
 
                double x = 0,
41
 
                double y = 0) = 0;
42
 
        /** Add a new colored place with a unique name */
43
 
        virtual void addPlace(const std::string& name,
44
 
                Colored::ColorType* type,
45
 
                Colored::Multiset&& tokens,
46
 
                double x = 0,
47
 
                double y = 0)
48
 
        {
49
 
            std::cerr << "Colored places are not supported in standard P/T nets" << std::endl;
50
 
            exit(ErrorCode);
51
 
        }
52
 
        /** Add a new transition with a unique name */
53
 
        virtual void addTransition(const std::string& name,
54
 
                double x = 0,
55
 
                double y = 0) = 0;
56
 
        /** Add a new colored transition with a unique name */
57
 
        virtual void addTransition(const std::string& name,
58
 
                const Colored::GuardExpression_ptr& guard,
59
 
                double x = 0,
60
 
                double y = 0)
61
 
        {
62
 
            std::cerr << "Colored transitions are not supported in standard P/T nets" << std::endl;
63
 
            exit(ErrorCode);
64
 
        }
65
 
        /** Add input arc with given weight */
66
 
        virtual void addInputArc(const std::string& place,
67
 
                const std::string& transition,
68
 
                bool inhibitor,
69
 
                int) = 0;
70
 
        /** Add colored input arc with given arc expression */
71
 
        virtual void addInputArc(const std::string& place,
72
 
                const std::string& transition,
73
 
                const Colored::ArcExpression_ptr& expr)
74
 
        {
75
 
            std::cerr << "Colored input arcs are not supported in standard P/T nets" << std::endl;
76
 
            exit(ErrorCode);
77
 
        }
78
 
        /** Add output arc with given weight */
79
 
        virtual void addOutputArc(const std::string& transition,
80
 
                const std::string& place,
81
 
                int weight = 1) = 0;
82
 
        /** Add output arc with given arc expression */
83
 
        virtual void addOutputArc(const std::string& transition,
84
 
                const std::string& place,
85
 
                const Colored::ArcExpression_ptr& expr)
86
 
        {
87
 
            std::cerr << "Colored output arcs are not supported in standard P/T nets" << std::endl;
88
 
            exit(ErrorCode);
89
 
        }
90
 
        /** Add color types with id */
91
 
        virtual void addColorType(const std::string& id,
92
 
                Colored::ColorType* type)
93
 
        {
94
 
            std::cerr << "Color types are not supported in standard P/T nets" << std::endl;
95
 
            exit(ErrorCode);
96
 
        }
97
 
        
98
 
        virtual void enableColors() {
99
 
            _isColored = true;
100
 
        }
101
 
 
102
 
        virtual bool isColored() const {
103
 
            return _isColored;
104
 
        }
105
 
 
106
 
        virtual void sort() = 0;
107
 
        
108
 
        virtual ~AbstractPetriNetBuilder() {
109
 
        }
110
 
    };
111
 
 
112
 
}
113
 
 
114
 
#endif // ABSTRACTPETRINETBUILDER_H