← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/PetriNet.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/PetriNet.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 PETRINET_H
21
 
#define PETRINET_H
22
 
 
23
 
#include <string>
24
 
#include <vector>
25
 
#include <climits>
26
 
#include <limits>
27
 
#include <iostream>
28
 
 
29
 
namespace PetriEngine {
30
 
 
31
 
    namespace PQL {
32
 
        class Condition;
33
 
    }
34
 
 
35
 
    namespace Structures {
36
 
        class State;
37
 
    }
38
 
 
39
 
    class PetriNetBuilder;
40
 
    class SuccessorGenerator;
41
 
    
42
 
    struct TransPtr {
43
 
        uint32_t inputs;
44
 
        uint32_t outputs;
45
 
    };
46
 
    
47
 
    struct Invariant {
48
 
        uint32_t place;
49
 
        uint32_t tokens;
50
 
        bool inhibitor;
51
 
        int8_t direction;
52
 
        // we can pack things here, but might give slowdown
53
 
    } /*__attribute__((packed))*/; 
54
 
    
55
 
    /** Type used for holding markings values */
56
 
    typedef uint32_t MarkVal;
57
 
 
58
 
    /** Efficient representation of PetriNet */
59
 
    class PetriNet {
60
 
        PetriNet(uint32_t transitions, uint32_t invariants, uint32_t places);
61
 
    public:
62
 
        ~PetriNet();
63
 
        
64
 
        MarkVal* makeInitialMarking();
65
 
        /** Fire transition if possible and store result in result */
66
 
        bool deadlocked(const MarkVal* marking) const;
67
 
        bool fireable(const MarkVal* marking, int transitionIndex);
68
 
        std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const;
69
 
        std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const;
70
 
        uint32_t numberOfTransitions() const {
71
 
            return _ntransitions;
72
 
        }
73
 
 
74
 
        uint32_t numberOfPlaces() const {
75
 
            return _nplaces;
76
 
        }
77
 
        int inArc(uint32_t place, uint32_t transition) const;
78
 
        int outArc(uint32_t transition, uint32_t place) const;
79
 
        
80
 
 
81
 
        const std::vector<std::string>& transitionNames() const
82
 
        {
83
 
            return _transitionnames;
84
 
        }
85
 
        
86
 
        const std::vector<std::string>& placeNames() const
87
 
        {
88
 
            return _placenames;
89
 
        }
90
 
               
91
 
        void print(MarkVal const * const val) const
92
 
        {
93
 
            for(size_t i = 0; i < _nplaces; ++i)
94
 
            {
95
 
                if(val[i] != 0)
96
 
                {
97
 
                    std::cout << _placenames[i] << "(" << i << ")" << " -> " << val[i] << std::endl;
98
 
                }
99
 
            }
100
 
        }
101
 
        
102
 
        void sort();
103
 
        
104
 
        void toXML(std::ostream& out);
105
 
 
106
 
    private:        
107
 
 
108
 
        /** Number of x variables
109
 
         * @remarks We could also get this from the _places vector, but I don't see any
110
 
         * any complexity garentees for this type.
111
 
         */
112
 
        uint32_t _ninvariants, _ntransitions, _nplaces;
113
 
 
114
 
        std::vector<TransPtr> _transitions;
115
 
        std::vector<Invariant> _invariants;
116
 
        std::vector<uint32_t> _placeToPtrs;
117
 
        MarkVal* _initialMarking;
118
 
 
119
 
        std::vector<std::string> _transitionnames;
120
 
        std::vector<std::string> _placenames;
121
 
 
122
 
        friend class PetriNetBuilder;
123
 
        friend class Reducer;
124
 
        friend class SuccessorGenerator;
125
 
        friend class ReducingSuccessorGenerator;
126
 
        friend class STSolver;
127
 
        friend class Filter;
128
 
    };
129
 
 
130
 
} // PetriEngine
131
 
 
132
 
#endif // PETRINET_H