← Back to branch summary

~verifypn-stub/verifypn/encoder-fix

« back to all changes in this revision

Viewing changes to PetriEngine/Reducer.h

  • Committer: Jiri Srba
  • Date: 2018-01-04 10:34:16 UTC
  • mfrom: (190.4.12 ctlse)
  • Revision ID: srba.jiri@gmail.com-20180104103416-fjdk15rww3vrbv4k
merged in branch lp:~verifypn-stub/verifypn/ctl-structural adding structurcal reduction
for CTL model checking and Stubborn sets for EF/AG leafs in the CTL algorithm

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reducer.h
114
114
        size_t RuleE() const {
115
115
            return _ruleE;
116
116
        }
117
 
        
 
117
 
 
118
        size_t RuleF() const {
 
119
            return _ruleF;
 
120
        }
 
121
 
118
122
        void postFire(std::ostream&, const std::string& transition);
119
123
        void extraConsume(std::ostream&, const std::string& transition);
120
124
        void initFire(std::ostream&);
122
126
    private:
123
127
        size_t _removedTransitions;
124
128
        size_t _removedPlaces;
125
 
        size_t _ruleA, _ruleB, _ruleC, _ruleD, _ruleE;
 
129
        size_t _ruleA, _ruleB, _ruleC, _ruleD, _ruleE, _ruleF;
126
130
        PetriNetBuilder* parent;
127
131
        bool reconstructTrace = false;
128
132
        std::chrono::high_resolution_clock::time_point _timer;
134
138
        bool ReducebyRuleC(uint32_t* placeInQuery);
135
139
        bool ReducebyRuleD(uint32_t* placeInQuery);
136
140
        bool ReducebyRuleE(uint32_t* placeInQuery);
 
141
        bool ReducebyRuleF(uint32_t* placeInQuery);
137
142
        
138
143
        std::string getTransitionName(uint32_t transition);
139
144
        std::string getPlaceName(uint32_t place);