← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/SuccessorGenerator.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/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
    /**
 
41
     * Checks if the conditions are met for fireing t, if write != NULL,
 
42
     * then also consumes tokens from write while checking
 
43
     * @param t, transition to fire
 
44
     * @param write, marking to consume from (possibly NULL)
 
45
     * @return true if t is fireable, false otherwise
 
46
     */
 
47
    bool checkPreset(uint32_t t);
 
48
 
 
49
    /**
 
50
     * Consumes tokens in preset of t without from marking write checking
 
51
     * @param write, a marking to consume from
 
52
     * @param t, a transition to fire
 
53
     */
 
54
    void consumePreset(Structures::State& write, uint32_t t);
 
55
 
 
56
    /**
 
57
     * Produces tokens in write, given by t
 
58
     * @param write, a marking to produce to
 
59
     * @param t, a transition to fire
 
60
     */
 
61
    void producePostset(Structures::State& write, uint32_t t);
 
62
 
 
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