← Back to branch summary

~tapaal-ltl/verifypn/rule-D-fix

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/StateConstraints.h

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Structures/StateConstraints.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 STATECONSTRAINTS_H
 
20
#define STATECONSTRAINTS_H
 
21
 
 
22
#include "../PetriNet.h"
 
23
#include "BitField.h"
 
24
 
 
25
#include <vector>
 
26
 
 
27
namespace PetriEngine{
 
28
namespace Structures{
 
29
 
 
30
#define CONSTRAINT_INFTY        1<<20
 
31
 
 
32
/** A set of linear constraits that a state can satisfy */
 
33
class StateConstraints
 
34
{
 
35
        /** Constraint on a place or variable */
 
36
        struct Constraint{
 
37
                int min, max;
 
38
        };
 
39
public:
 
40
        StateConstraints(size_t nPlaces, size_t nVars){
 
41
                this->nPlaces = nPlaces;
 
42
                this->nVars = nVars;
 
43
                pcs = new Constraint[nPlaces];
 
44
                vcs = new Constraint[nVars];
 
45
                reset();
 
46
        }
 
47
        StateConstraints(const PetriNet& net){
 
48
                nPlaces = net.numberOfPlaces();
 
49
                nVars = net.numberOfVariables();
 
50
                pcs = new Constraint[nPlaces];
 
51
                vcs = new Constraint[nVars];
 
52
                reset();
 
53
        }
 
54
        ~StateConstraints(){
 
55
                if(pcs){
 
56
                        delete[] pcs;
 
57
                        pcs = NULL;
 
58
                }
 
59
                if(vcs){
 
60
                        delete[] vcs;
 
61
                        vcs = NULL;
 
62
                }
 
63
        }
 
64
        /** Set place maximum, returns false if this causes a conflict */
 
65
        bool setPlaceMax(int place, MarkVal max){
 
66
                if(pcs[place].min > max)
 
67
                        return false;
 
68
                if(max < pcs[place].max)
 
69
                        pcs[place].max = max;
 
70
                return true;
 
71
        }
 
72
        /** Set place maximum, returns false if this causes a conflict */
 
73
        bool setPlaceMin(int place, MarkVal min){
 
74
                if(pcs[place].max < min)
 
75
                        return false;
 
76
                if(min > pcs[place].min)
 
77
                        pcs[place].min = min;
 
78
                return true;
 
79
        }
 
80
        /** Set place maximum, returns false if this causes a conflict */
 
81
        bool setVarMax(int var, MarkVal max){
 
82
                if(vcs[var].min > max)
 
83
                        return false;
 
84
                if(max < vcs[var].max)
 
85
                        vcs[var].max = max;
 
86
                return true;
 
87
        }
 
88
        /** Set place maximum, returns false if this causes a conflict */
 
89
        bool setVarMin(int var, MarkVal min){
 
90
                if(vcs[var].max < min)
 
91
                        return false;
 
92
                if(min > vcs[var].min)
 
93
                        vcs[var].min = min;
 
94
                return true;
 
95
        }
 
96
        /** Attempts to merge two StateConstraints, return NULL if can't be merged */
 
97
        StateConstraints* merge(const StateConstraints* constraint) const;
 
98
        /** True, if every marking satisfied by subset is also satisfied by this */
 
99
        bool isSuperSet(const StateConstraints* subset) const;
 
100
        bool isEqual(const StateConstraints* other) const{
 
101
                return this->isSuperSet(other) && other->isSuperSet(this);
 
102
        }
 
103
        /** Reset all constraints */
 
104
        void reset();
 
105
 
 
106
        /** Attempts to solve using lp_solve, returns True if the net cannot satisfy these constraints! */
 
107
        bool isImpossible(const PetriNet& net, const MarkVal* marking, const VarVal* valuation) const;
 
108
        /** Attempts to solve using lp_solve size of fire vector */
 
109
        int fireVectorSize(const PetriNet& net, const MarkVal* marking, const VarVal* valuation) const;
 
110
        /** True if the state constraint contains exactly one state */
 
111
        bool isSpecific() const;
 
112
 
 
113
        /** Merge the two sets of StateConstraints such that one from A and one from B is always satisfied, when one in the return value is
 
114
         * @remarks This will take ownership of the provided StateConstraints, and delete them or own them
 
115
         */
 
116
        static std::vector<StateConstraints*> mergeAnd(const std::vector<StateConstraints*>& A, const std::vector<StateConstraints*>& B);
 
117
        /** Merge the two sets of StateConstraints such that either on from A or B is always satisfied, when one in the return value is
 
118
         * @remarks This will take ownership of the provided StateConstraints, and delete them or own them
 
119
         */
 
120
        static std::vector<StateConstraints*> mergeOr(const std::vector<StateConstraints*>& A, const std::vector<StateConstraints*>& B);
 
121
 
 
122
        static StateConstraints* requirePlaceMin(const PetriNet& net, int place, MarkVal value);
 
123
        static StateConstraints* requirePlaceMax(const PetriNet& net, int place, MarkVal value);
 
124
        static StateConstraints* requirePlaceEqual(const PetriNet& net, int place, MarkVal value);
 
125
        static StateConstraints* requireVarMin(const PetriNet& net, int var, MarkVal value);
 
126
        static StateConstraints* requireVarMax(const PetriNet& net, int var, MarkVal value);
 
127
        static StateConstraints* requireVarEqual(const PetriNet& net, int var, MarkVal value);
 
128
private:
 
129
        size_t nPlaces, nVars;
 
130
        Constraint* pcs;
 
131
        Constraint* vcs;
 
132
 
 
133
        BitField maxTrap(const PetriNet& net, BitField places, const MarkVal* resultMarking) const;
 
134
        bool isInMaxTrap(const PetriNet& net, size_t place, const BitField& places, const MarkVal* resultMarking) const;
 
135
        BitField minimalTrap(const PetriNet& net, const MarkVal* marking, const MarkVal* resultMarking) const;
 
136
        bool isMarked(const BitField& places, const MarkVal* marking) const;
 
137
};
 
138
 
 
139
} // Structures
 
140
} // PetriEngine
 
141
 
 
142
#endif // STATECONSTRAINTS_H