← Back to branch summary

~verifypn-cpn/verifypn/queryUnfold

« back to all changes in this revision

Viewing changes to PetriEngine/SuccessorGenerator.h

  • Committer: Niels Christensen
  • Date: 2019-04-30 12:58:19 UTC
  • Revision ID: nchri13@student.aau.dk-20190430125819-8ag624162pyjnhq8
WIP making queries work

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/SuccessorGenerator.h
1
 
/*
2
 
 * To change this license header, choose License Headers in Project Properties.
3
 
 * To change this template file, choose Tools | Templates
4
 
 * and open the template in the editor.
5
 
 */
6
 
 
7
 
/* 
8
 
 * File:   SuccessorGenerator.h
9
 
 * Author: Peter G. Jensen
10
 
 *
11
 
 * Created on 30 March 2016, 19:50
12
 
 */
13
 
 
14
 
#ifndef SUCCESSORGENERATOR_H
15
 
#define SUCCESSORGENERATOR_H
16
 
 
17
 
#include "PetriNet.h"
18
 
#include "Structures/State.h"
19
 
#include <memory>
20
 
 
21
 
namespace PetriEngine {
22
 
class SuccessorGenerator {
23
 
public:
24
 
    SuccessorGenerator(const PetriNet& net);
25
 
    SuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries);
26
 
    virtual ~SuccessorGenerator();
27
 
    void prepare(const Structures::State* state);
28
 
    bool next(Structures::State& write);
29
 
    uint32_t fired()
30
 
    {
31
 
        return _suc_tcounter -1;
32
 
    }
33
 
        
34
 
    const MarkVal* parent() const {
35
 
        return _parent->marking();
36
 
    }
37
 
 
38
 
    void reset();
39
 
    
40
 
protected:
41
 
    /**
42
 
     * Checks if the conditions are met for fireing t, if write != NULL,
43
 
     * then also consumes tokens from write while checking
44
 
     * @param t, transition to fire
45
 
     * @param write, marking to consume from (possibly NULL)
46
 
     * @return true if t is fireable, false otherwise
47
 
     */
48
 
    bool checkPreset(uint32_t t);
49
 
 
50
 
    /**
51
 
     * Consumes tokens in preset of t without from marking write checking
52
 
     * @param write, a marking to consume from
53
 
     * @param t, a transition to fire
54
 
     */
55
 
    void consumePreset(Structures::State& write, uint32_t t);
56
 
 
57
 
    /**
58
 
     * Produces tokens in write, given by t
59
 
     * @param write, a marking to produce to
60
 
     * @param t, a transition to fire
61
 
     */
62
 
    void producePostset(Structures::State& write, uint32_t t);
63
 
private:
64
 
    const PetriNet& _net;
65
 
    const Structures::State* _parent;
66
 
    uint32_t _suc_pcounter;
67
 
    uint32_t _suc_tcounter;
68
 
 
69
 
    friend class ReducingSuccessorGenerator;
70
 
};
71
 
}
72
 
 
73
 
#endif /* SUCCESSORGENERATOR_H */
74