← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/State.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/Structures/State.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 GENERALSTATE_H
20
 
#define GENERALSTATE_H
21
 
 
22
 
#include "../PetriNet.h"
23
 
 
24
 
#include <stdlib.h>
25
 
#include <stdio.h>
26
 
#include <string.h>
27
 
#include <algorithm>
28
 
#include <vector>
29
 
 
30
 
namespace PetriEngine {
31
 
    namespace Structures {
32
 
 
33
 
        /** GeneralState class for reachability searches.
34
 
         * Used in most reachability search cases */
35
 
        class State {
36
 
        public:
37
 
 
38
 
            MarkVal* marking() {
39
 
                return _marking;
40
 
            }
41
 
 
42
 
            const MarkVal* marking() const {
43
 
                return _marking;
44
 
            }
45
 
 
46
 
            void setMarking(MarkVal* m) {
47
 
                _marking = m;
48
 
            }
49
 
            
50
 
            State()
51
 
            {
52
 
                _marking = NULL;
53
 
            }
54
 
            
55
 
            ~State()
56
 
            {
57
 
                delete[] _marking;
58
 
            }
59
 
            
60
 
            void print(PetriNet& net) {
61
 
                for (uint32_t i = 0; i < net.numberOfPlaces(); i++) {
62
 
                    std::cout << net.placeNames()[i] << ": " << _marking[i] << std::endl;   
63
 
                }
64
 
                std::cout << std::endl;
65
 
            }
66
 
        private:
67
 
            MarkVal* _marking;
68
 
        };
69
 
 
70
 
    }
71
 
}
72
 
 
73
 
#endif //GENERALSTATE_H