← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/TAR/TARReachability.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/TAR/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 "TARAutomata.h"
 
24
#include "TraceSet.h"
 
25
#include "AntiChain.h"
 
26
 
 
27
#include "PetriEngine/Reachability/ReachabilitySearch.h"
 
28
 
 
29
 
 
30
namespace PetriEngine {
 
31
    namespace Reachability {
 
32
        class Solver;
 
33
        class TARReachabilitySearch {
 
34
        private:
 
35
            AbstractHandler& _printer;
 
36
            
 
37
 
 
38
        public:
 
39
 
 
40
            TARReachabilitySearch(AbstractHandler& printer, PetriNet& net, Reducer* reducer, int kbound = 0)
 
41
            : _printer(printer), _net(net), _reducer(reducer), _traceset(net) {
 
42
                _kbound = kbound;
 
43
            }
 
44
            
 
45
            ~TARReachabilitySearch()
 
46
            {
 
47
            }
 
48
            
 
49
            void reachable(
 
50
                std::vector<std::shared_ptr<PQL::Condition > >& queries,
 
51
                std::vector<ResultPrinter::Result>& results,
 
52
                bool printstats, bool printtrace);
 
53
        private:
 
54
 
 
55
            void printTrace(trace_t& stack);
 
56
            void nextEdge(AntiChain<uint32_t, size_t>& checked, state_t& state, trace_t& waiting, std::set<size_t>& nextinter);
 
57
            bool tryReach(  bool printtrace, Solver& solver);
 
58
            std::pair<bool,bool> runTAR(    bool printtrace, Solver& solver, std::vector<bool>& use_trans);
 
59
            bool popDone(trace_t& waiting, size_t& stepno);
 
60
            bool doStep(state_t& state, std::set<size_t>& nextinter);
 
61
            void addNonChanging(state_t& state, std::set<size_t>& maximal, std::set<size_t>& nextinter);
 
62
            bool validate(const std::vector<size_t>& transitions);
 
63
 
 
64
            void handleInvalidTrace(trace_t& waiting, int nvalid);
 
65
            std::pair<int,bool>  isValidTrace(trace_t& trace, Structures::State& initial, const std::vector<bool>&, PQL::Condition* query);
 
66
            void printStats();
 
67
            bool checkQueries(  std::vector<std::shared_ptr<PQL::Condition > >&,
 
68
                                std::vector<ResultPrinter::Result>&,
 
69
                                Structures::State&, bool);
 
70
            
 
71
            int _kbound;
 
72
            size_t _stepno = 0;
 
73
            PetriNet& _net;
 
74
            Reducer* _reducer;
 
75
            TraceSet _traceset;
 
76
 
 
77
#ifdef TAR_TIMING
 
78
            double _check_time = 0;
 
79
            double _next_time = 0;
 
80
            double _do_step = 0;
 
81
            double _do_step_next = 0;
 
82
            double _non_change_time = 0;
 
83
            double _follow_time = 0;
 
84
#endif
 
85
        };
 
86
        
 
87
    }
 
88
}
 
89
#endif /* TARREACHABILITY_H */
 
90