← Back to branch summary

~tapaal-ltl/verifypn/answer-for-gui

« back to all changes in this revision

Viewing changes to include/LTL/Structures/ProductState.h

  • Committer: srba.jiri at gmail
  • Date: 2021-04-02 18:13:50 UTC
  • mfrom: (230.1.28 mcc2021)
  • Revision ID: srba.jiri@gmail.com-20210402181350-k71xtjut3r48l1o5
merged in lp:~tapaal-ltl/verifypn/mcc2021 adding LTL, colored fixed-point unfolding for CPN and other performance improvements

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/Structures/ProductState.h
 
1
/* Copyright (C) 2020  Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
 
2
 *                     Simon M. Virenfeldt <simon@simwir.dk>
 
3
 *
 
4
 * This program is free software: you can redistribute it and/or modify
 
5
 * it under the terms of the GNU General Public License as published by
 
6
 * the Free Software Foundation, either version 3 of the License, or
 
7
 * (at your option) any later version.
 
8
 *
 
9
 * This program is distributed in the hope that it will be useful,
 
10
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
12
 * GNU General Public License for more details.
 
13
 *
 
14
 * You should have received a copy of the GNU General Public License
 
15
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
16
 */
 
17
 
 
18
#ifndef VERIFYPN_PRODUCTSTATE_H
 
19
#define VERIFYPN_PRODUCTSTATE_H
 
20
 
 
21
#include "PetriEngine/Structures/State.h"
 
22
 
 
23
namespace LTL {
 
24
    class ProductSuccessorGenerator;
 
25
}
 
26
namespace LTL::Structures {
 
27
    /**
 
28
     * State on the form (M, q) for marking M and NBA state q.
 
29
     * Represented as array of size nplaces + 1, where the last element is the number
 
30
     * of NBA state q, and the first nplaces elements are the actual marking.
 
31
     */
 
32
    class ProductState : public PetriEngine::Structures::State {
 
33
    public:
 
34
        ProductState() : PetriEngine::Structures::State() {}
 
35
 
 
36
        void setMarking(PetriEngine::MarkVal* marking, size_t nplaces)
 
37
        {
 
38
            State::setMarking(marking);
 
39
            // because zero-indexing
 
40
            buchi_state_idx = nplaces;
 
41
        }
 
42
 
 
43
        //TODO override equality operators to handle both marking and NBA state
 
44
        size_t getBuchiState() const {
 
45
            return marking()[buchi_state_idx];
 
46
        }
 
47
 
 
48
        void setBuchiState(size_t state) {
 
49
            marking()[buchi_state_idx] = state;
 
50
        }
 
51
 
 
52
        [[nodiscard]] bool markingEqual(const PetriEngine::MarkVal *rhs) const {
 
53
            for (size_t i = 0; i < buchi_state_idx; ++i) {
 
54
                if (marking()[i] != rhs[i]) {
 
55
                    return false;
 
56
                }
 
57
            }
 
58
            return true;
 
59
        }
 
60
 
 
61
        bool operator==(const ProductState &rhs) const {
 
62
            for (size_t i = 0; i <= buchi_state_idx; ++i) {
 
63
                if (marking()[i] != rhs.marking()[i]) {
 
64
                    return false;
 
65
                }
 
66
            }
 
67
            return true;
 
68
        }
 
69
 
 
70
        size_t size() const { return buchi_state_idx + 1; }
 
71
 
 
72
        bool operator!=(const ProductState &rhs) const {
 
73
            return !(rhs == *this);
 
74
        }
 
75
    private:
 
76
        friend class LTL::ProductSuccessorGenerator;
 
77
        size_t buchi_state_idx;
 
78
    };
 
79
}
 
80
 
 
81
#endif //VERIFYPN_PRODUCTSTATE_H