← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/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:
include/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
        uint32_t initial(size_t id) const;
 
65
        MarkVal* makeInitialMarking() const;
 
66
        /** Fire transition if possible and store result in result */
 
67
        bool deadlocked(const MarkVal* marking) const;
 
68
        bool fireable(const MarkVal* marking, int transitionIndex);
 
69
        std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const;
 
70
        std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const;
 
71
        uint32_t numberOfTransitions() const {
 
72
            return _ntransitions;
 
73
        }
 
74
 
 
75
        uint32_t numberOfPlaces() const {
 
76
            return _nplaces;
 
77
        }
 
78
        int inArc(uint32_t place, uint32_t transition) const;
 
79
        int outArc(uint32_t transition, uint32_t place) const;
 
80
        
 
81
 
 
82
        const std::vector<std::string>& transitionNames() const
 
83
        {
 
84
            return _transitionnames;
 
85
        }
 
86
        
 
87
        const std::vector<std::string>& placeNames() const
 
88
        {
 
89
            return _placenames;
 
90
        }
 
91
               
 
92
        void print(MarkVal const * const val) const
 
93
        {
 
94
            for(size_t i = 0; i < _nplaces; ++i)
 
95
            {
 
96
                if(val[i] != 0)
 
97
                {
 
98
                    std::cout << _placenames[i] << "(" << i << ")" << " -> " << val[i] << std::endl;
 
99
                }
 
100
            }
 
101
        }
 
102
        
 
103
        void sort();
 
104
        
 
105
        void toXML(std::ostream& out);
 
106
        
 
107
        const MarkVal* initial() const {
 
108
            return _initialMarking;
 
109
        }
 
110
 
 
111
    private:        
 
112
 
 
113
        /** Number of x variables
 
114
         * @remarks We could also get this from the _places vector, but I don't see any
 
115
         * any complexity garentees for this type.
 
116
         */
 
117
        uint32_t _ninvariants, _ntransitions, _nplaces;
 
118
 
 
119
        std::vector<TransPtr> _transitions;
 
120
        std::vector<Invariant> _invariants;
 
121
        std::vector<uint32_t> _placeToPtrs;
 
122
        MarkVal* _initialMarking;
 
123
 
 
124
        std::vector<std::string> _transitionnames;
 
125
        std::vector<std::string> _placenames;
 
126
 
 
127
        friend class PetriNetBuilder;
 
128
        friend class Reducer;
 
129
        friend class SuccessorGenerator;
 
130
        friend class ReducingSuccessorGenerator;
 
131
        friend class STSolver;
 
132
    };
 
133
 
 
134
} // PetriEngine
 
135
 
 
136
#endif // PETRINET_H