← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/PetriEngine/TAR/Solver.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/Solver.h
 
1
/*
 
2
 *  Copyright Peter G. Jensen, all rights reserved.
 
3
 */
 
4
 
 
5
/* 
 
6
 * File:   Solver.h
 
7
 * Author: Peter G. Jensen <root@petergjoel.dk>
 
8
 *
 
9
 * Created on April 3, 2020, 8:08 PM
 
10
 */
 
11
 
 
12
#ifndef SOLVER_H
 
13
#define SOLVER_H
 
14
 
 
15
#include "TARAutomata.h"
 
16
#include "range.h"
 
17
#include "PetriEngine/PQL/PQL.h"
 
18
#include "TraceSet.h"
 
19
 
 
20
#include <utility>
 
21
#include <cinttypes>
 
22
 
 
23
namespace PetriEngine {
 
24
    namespace Reachability {
 
25
        using namespace PQL;
 
26
        class Solver {
 
27
        public:
 
28
            using inter_t = std::pair<prvector_t, size_t>;
 
29
            using interpolant_t = std::vector<inter_t>;
 
30
            Solver(PetriNet& net, MarkVal* initial, Condition* query, std::vector<bool>& inq);
 
31
            bool check(trace_t& trace, TraceSet& interpolants);
 
32
            const std::vector<bool>& in_query() const { return _inq; }
 
33
            Condition* query() const { return _query; }
 
34
        private:
 
35
            int64_t findFailure(trace_t& trace, bool to_end);
 
36
            interpolant_t findFree(trace_t& trace);
 
37
            bool computeHoare(trace_t& trace, interpolant_t& ranges, int64_t fail);
 
38
            bool computeTerminal(state_t& end, inter_t& last);
 
39
            PetriNet& _net;
 
40
            MarkVal* _initial;
 
41
            Condition* _query;
 
42
            std::vector<bool> _inq;
 
43
            std::vector<bool> _dirty;
 
44
            std::unique_ptr<int64_t[]> _m;
 
45
            std::unique_ptr<int64_t[]> _failm;
 
46
            std::unique_ptr<MarkVal[]> _mark;
 
47
            std::unique_ptr<uint64_t[]> _use_count;
 
48
#ifndef NDEBUG
 
49
            SuccessorGenerator _gen;
 
50
#endif
 
51
        };
 
52
    }
 
53
}
 
54
 
 
55
#endif /* SOLVER_H */
 
56