← Back to branch summary

~verifypn-maintainers/verifypn/emptyTracePrint

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/TARReachability.h

  • Committer: Jiri Srba
  • Date: 2018-04-18 10:58:36 UTC
  • mfrom: (197.3.78 cpn_ctlss)
  • Revision ID: srba.jiri@gmail.com-20180418105836-a5rha272u0om4u77
merged in branch lp:~verifypn-cpn/verifypn/cpn_ctlss/

CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reachability/TARReachability.h
 
1
/* 
 
2
 * File:   TARReachability.h
 
3
 * Author: Peter G. Jensen
 
4
 * 
 
5
 * Created on January 2, 2018, 8:36 AM
 
6
 * 
 
7
 * This program is free software: you can redistribute it and/or modify
 
8
 * it under the terms of the GNU General Public License as published by
 
9
 * the Free Software Foundation, either version 3 of the License, or
 
10
 * (at your option) any later version.
 
11
 * 
 
12
 * This program is distributed in the hope that it will be useful,
 
13
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
15
 * GNU General Public License for more details.
 
16
 * 
 
17
 * You should have received a copy of the GNU General Public License
 
18
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
19
 */
 
20
 
 
21
#ifndef TARREACHABILITY_H
 
22
#define TARREACHABILITY_H
 
23
#include <z3++.h>
 
24
#include "ReachabilitySearch.h"
 
25
#include "../TAR/TARAutomata.h"
 
26
namespace PetriEngine {
 
27
    namespace Reachability {
 
28
        class TARReachabilitySearch {
 
29
        private:
 
30
            ResultPrinter& printer;
 
31
            
 
32
 
 
33
        public:
 
34
 
 
35
            TARReachabilitySearch(ResultPrinter& printer, PetriNet& net, Reducer* reducer, int kbound = 0)
 
36
            : printer(printer), _net(net), _reducer(reducer) {
 
37
                _kbound = kbound;
 
38
            }
 
39
            
 
40
            ~TARReachabilitySearch()
 
41
            {
 
42
            }
 
43
            
 
44
            void reachable(
 
45
                std::vector<std::shared_ptr<PQL::Condition > >& queries,
 
46
                std::vector<ResultPrinter::Result>& results,
 
47
                bool printstats, bool printtrace);
 
48
        protected:
 
49
            virtual void addNonChanging(state_t& state, std::vector<size_t>& maximal, std::vector<size_t>& nextinter);
 
50
            virtual std::vector<size_t> expandSimulation(std::vector<size_t>& from);
 
51
            virtual bool followSymbol(std::vector<size_t>& from, std::vector<size_t>& nextinter, size_t symbol);
 
52
            z3::expr computeParameters(
 
53
                z3::context& context, std::vector<z3::expr>& encoded, z3::expr& param_reach, 
 
54
                const std::vector<uint32_t>&, const std::vector<bool>& inq, const std::vector<bool>& read);
 
55
        private:
 
56
            typedef std::vector<state_t> waiting_t;
 
57
            void printTrace(waiting_t& stack);
 
58
            bool tryReach(   const std::shared_ptr<PQL::Condition>& query, 
 
59
                                        std::vector<ResultPrinter::Result>& results,
 
60
                                        bool printstats, bool printtrace, Structures::State& initial);
 
61
            size_t computeSimulation(size_t index, size_t sim_hint = 1, size_t simed_hint = 0);
 
62
            bool popDone(waiting_t& waiting, size_t& stepno);
 
63
            bool checkInclussion(state_t& state, std::vector<size_t>& nextinter, z3::context& ctx);
 
64
 
 
65
            void handleInvalidTrace(waiting_t& waiting, int nvalid);
 
66
            std::pair<int,bool>  isValidTrace(waiting_t& trace, z3::context& context, bool probe, Structures::State& initial, z3::expr& query, const std::vector<bool>& inq, z3::expr& param);
 
67
            bool findValidRange( int& from, 
 
68
                                            const int to, 
 
69
                                            z3::context& context, 
 
70
                                            z3::expr_vector& interpolant, 
 
71
                                            std::vector<z3::expr>& encoded);
 
72
            int constructAutomata(int from, waiting_t& trace, z3::expr_vector& inter, z3::context& context);
 
73
            std::pair<bool, size_t> stateForPredicate(int type, z3::expr pred, z3::context& context, size_t sim_hint = 1, size_t simed_hint = 0);
 
74
            void printStats();
 
75
            bool checkQueries(  std::vector<std::shared_ptr<PQL::Condition > >&,
 
76
                                std::vector<ResultPrinter::Result>&,
 
77
                                Structures::State&, bool);
 
78
            ResultPrinter::Result printQuery(std::shared_ptr<PQL::Condition>& query, size_t i, ResultPrinter::Result);
 
79
            
 
80
            int _kbound;
 
81
            PetriNet& _net;
 
82
            Reducer* _reducer;
 
83
            struct el_t
 
84
            {
 
85
                z3::expr expr;
 
86
                size_t state;
 
87
                el_t(z3::expr e, size_t s) : expr(e), state(s) {};
 
88
            };
 
89
            std::unordered_map<size_t, std::vector<el_t>> intmap;
 
90
            std::vector<AutomataState> states;
 
91
            std::vector<size_t> simorder;
 
92
            std::map<size_t, std::vector<size_t>> edge_interpolants;
 
93
 
 
94
        };
 
95
        
 
96
    }
 
97
}
 
98
#endif /* TARREACHABILITY_H */
 
99